Crate foundry_evm_symbolic 

Foundry’s symbolic EVM executor.

Modules

abi 🔒

consts 🔒

executor 🔒

runtime 🔒

Structs

PortfolioDiagnostics

SymbolicBranchTarget

One comparison site from a fuzz branch frontier to target during symbolic execution.

SymbolicBranchTargetSearchResult

Result of best-effort symbolic exploration toward one branch target.

SymbolicConcreteInput

One concrete symbolic input materialized from a solver model.

SymbolicExecutor

SMT-LIB-backed symbolic executor.

SymbolicInvariantCandidate

One unconfirmed symbolic input produced by invariant candidate search.

SymbolicInvariantCandidateInput

Input for best-effort invariant candidate search after one symbolic handler call.

SymbolicInvariantCandidateSearchResult

Result of best-effort invariant candidate search after one symbolic handler call.

SymbolicInvariantRunInput

Input for bounded symbolic invariant execution.

SymbolicInvariantSearchLimitation

An execution or solver limitation encountered during best-effort candidate search.

SymbolicInvariantStep

One concrete step in a symbolic invariant counterexample sequence.

SymbolicInvariantTarget

A concrete invariant target selected from Foundry’s invariant discovery.

SymbolicRunInput

SymbolicStats

Symbolic execution counters.

SymbolicStorageAssignment

One concrete storage value required to replay a symbolic invariant candidate.

Enums

DeferredIncomplete 🔒

DeferredPathMode 🔒

SymbolicError

Error returned by the internal symbolic executor.

SymbolicInvariantCounterexampleKind

Part of a symbolic invariant run that produced a replayable counterexample.

SymbolicInvariantRunResult

Outcome of bounded symbolic invariant execution.

SymbolicRunResult

Outcome of a symbolic test execution.

SymbolicStopReason

High-level reason a symbolic run stopped without a proof or replayed counterexample.

SymbolicVmCheatcode 🔒

Constants

BUILTIN_SYMBOLIC_SOLVERS

Symbolic solver names with built-in command-line mappings.

Functions

symbolic_create_bytes_selectors 🔒

symbolic_create_int_selectors 🔒

symbolic_create_uint_selectors 🔒

symbolic_solver_is_builtin

Returns whether solver is one of Foundry’s semantic symbolic solver names.

symbolic_solver_portfolio_availability_warning

Returns a warning when a configured symbolic solver portfolio has unavailable entries.