Skip to main content

Module verify

Module verify 

Source

Modulesยง

alias_hazard
Shared alias hazard analysis for both legacy and VM backends.
call_summary
Interprocedural call summaries for the staged verifier.
contract
def_use
Verify-specific extensions for def-use computation.
display
driver
Driver utilities for the staged verifier pipeline.
engine
Symbolic-VM-based verification engine.
loop_sensitivity
Loop-sensitivity planning for the staged verifier.
path_extractor
Path extraction for verification targets.
property_checker
Unified property checker for the symbolic VM.
report
Diagnostics and summaries for the staged verifier pipeline.
slicer
target
valid_cstr_util
vm
Symbolic MIR Virtual Machine.