Expand description
Foundry’s symbolic EVM executor.
Modules§
Structs§
- Symbolic
Branch Target - One comparison site from a fuzz branch frontier to target during symbolic execution.
- Symbolic
Branch Target Search Result - Result of best-effort symbolic exploration toward one branch target.
- Symbolic
Concrete Input - One concrete symbolic input materialized from a solver model.
- Symbolic
Executor - SMT-LIB-backed symbolic executor.
- Symbolic
Invariant Candidate - One unconfirmed symbolic input produced by invariant candidate search.
- Symbolic
Invariant Candidate Input - Input for best-effort invariant candidate search after one symbolic handler call.
- Symbolic
Invariant Candidate Search Result - Result of best-effort invariant candidate search after one symbolic handler call.
- Symbolic
Invariant RunInput - Input for bounded symbolic invariant execution.
- Symbolic
Invariant Search Limitation - An execution or solver limitation encountered during best-effort candidate search.
- Symbolic
Invariant Step - One concrete step in a symbolic invariant counterexample sequence.
- Symbolic
Invariant Target - A concrete invariant target selected from Foundry’s invariant discovery.
- Symbolic
RunInput - Symbolic
Stats - Symbolic execution counters.
- Symbolic
Storage Assignment - One concrete storage value required to replay a symbolic invariant candidate.
Enums§
- Deferred
Incomplete 🔒 - Deferred
Path 🔒Mode - Symbolic
Error - Error returned by the internal symbolic executor.
- Symbolic
Invariant Counterexample Kind - Part of a symbolic invariant run that produced a replayable counterexample.
- Symbolic
Invariant RunResult - Outcome of bounded symbolic invariant execution.
- Symbolic
RunResult - Outcome of a symbolic test execution.
- Symbolic
Stop Reason - High-level reason a symbolic run stopped without a proof or replayed counterexample.
- Symbolic
VmCheatcode 🔒