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 builtin_models summary provides more precise hand-crafted invariants. Otherwise it falls back to the summary-based approach.