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.

SymbolicConcreteInput

One concrete symbolic input materialized from a solver model.

SymbolicExecutor

SMT-LIB-backed symbolic executor.

SymbolicInvariantRunInput

Input for bounded symbolic invariant execution.

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 🔒

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.