Module symbolic_analysis

rapx::analysis::senryx

Module symbolic_analysis 

Source

Structs§

ValueDomain

Enums§

AnaOperand
SymbolicDef

Functions§

binop_to_str 🔒
debug_z3_solver_state 🔒
get_operand_bv 🔒
operand_to_str 🔒
verify_with_z3
Verifies a target property using Z3 SMT solver given variable domains and path constraints. Returns true if the property holds (UNSAT for negation), false otherwise.