Expand description
Call handling for the symbolic VM.
Bridges the existing call summary infrastructure (call_summary)
with the new symbolic VM state. The exec_call method is called
from exec.rs when a Call terminator is encountered.
When the callee has MIR available, the VM recursively inlines the callee’s body to achieve context-sensitive precision, unless a fn_simulator summary provides more precise hand-crafted invariants. Otherwise it falls back to the summary-based approach.
Constants§
- MAX_
INLINE_ 🔒DEPTH - Classification of a call site for dispatch prioritization.