Expand description
MIR body visitor that builds state and invokes contract checks. MIR path visitor for Senryx state construction.
BodyVisitor walks selected MIR paths, builds dominated graph state,
records symbolic value definitions, applies call summaries, and invokes
contract checking whenever it reaches an unsafe API callsite.
Structs§
- Body
Visitor - Visitor that traverses one MIR body and builds symbolic and pointer state.
- Check
Result - Per-callsite contract checking result collected during body analysis.
Enums§
- PlaceTy
- Layout abstraction for concrete and generic MIR places.