Crate foundry_evm_symbolic 

Foundry’s symbolic EVM executor.

Modules

abi 🔒

consts 🔒

executor 🔒

runtime 🔒

Macros

selector 🔒

Structs

PortfolioDiagnostics

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.

Enums

SymbolicError

Error returned by the internal symbolic executor.

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.

Constants

BUILTIN_SYMBOLIC_SOLVERS

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

Functions

selector_for 🔒

Returns the selector_for symbolic public API helper result.

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.