Expand description
Auto-generated module
🤖 Generated with SplitRS
Structs§
- AndersenPTA
- A simplified Andersen points-to analysis using a constraint worklist.
- Const
Prop State - A simple constant propagation state: maps variables to known constant values or marks them as non-constant (⊤).
- Eraser
State - Eraser algorithm state for a single memory location.
- Fixpoint
Solver - A generic monotone framework fixpoint solver. Each node in the program has an associated abstract value.
- IFCTracker
- Tracks information flow labels for a set of variables.
- Null
Tracker - Tracks nullability for program variables.
- PDGraph
- A simplified program dependence graph over statement indices.
- Taint
State - A simple variable-level taint tracking state.
- Typestate
Automaton - Represents a finite-state automaton for resource protocol checking.
States are
usizeindices; transitions are labeled by operation names.
Enums§
- Interval
- An abstract interval element: either
[lo, hi]or ⊥ (empty). - Nullability
- Three-valued nullability: definitely null, definitely non-null, or unknown.
- Security
Level - Security label for two-point lattice: Low < High.
- Sign
- Abstract sign: {⊥, Neg, Zero, Pos, ⊤}.