Represents symbolic memory backed by binary file sections.

Represents values that can be requested from a solver model.

Represents an SMT solver for symbolic path conditions.

Represents a symbolic memory used in the evaluation.

Represents one or more solver-model query expressions.

Serializes symbolic expressions and path conditions into SMT-LIB.

Represents an error encountered while communicating with an SMT solver.

Represents a parsed solver response.

Parses the small subset of solver output used by SymbEval.

Represents the result of a solver satisfiability query.

Represents a single value returned by a solver's value query.

Represents an avoid condition used by SymbExecutor.Run.

Represents a symbolic byte buffer laid out at a concrete address.

Represents the calling-convention information passed to a call hook.

Represents a symbolic external-call hook.

Represents a target-address-based call hook registry.

Built-in symbolic call hook models.

Represents how the symbolic executor should handle call instructions.

Represents an error encountered during symbolic evaluation.

Represents a symbolic evaluation module for LowUIR.

Represents a symbolic executor over SymbEval's evaluation state.

Symbolic expression helpers.

Represents a symbolic bit-vector value. SymbEval keeps LowUIR condition values as 1-bit bit-vectors. Path conditions contain expressions that are interpreted as the 1-bit true value.

Translates LowUIR expressions into symbolic expressions.

Represents symbolic memory indexed by concrete addresses.

Provides typed accessors over solver-returned symbolic values.

Represents a symbolic query evaluated by SymbExecutor.Run.

Represents a symbolic query and the values to extract for model queries.

Represents one positive answer to a reachability query.

Represents why a symbolic query could not be fully answered.

Represents options for bounded symbolic execution.

Represents a state that was discarded before further exploration.

Represents the answer to a bounded symbolic execution query.

Represents a non-target state where exploration stopped.

Represents one concrete-input answer to a satisfiability query.

Represents a solver backend used by SymbExecutor.

Represents the main symbolic evaluation state.

Provides convenience helpers for a symbolic state.

Represents a symbolic execution point inspected by SymbExecutor queries.

Represents a collection of symbolic variables used in the evaluation state.