Module concolic

Concolic Tracing

Modules

serialization_format

Concolic Tracing Serialization Format

Structs

ConcolicMetadata

A metadata holding a buffer of a concolic trace.

ConcolicObserver

A standard ConcolicObserver observer, observing constraints written into a memory buffer.

Location

Locations are code locations encountered during concolic tracing

Enums

SymExpr

SymExpr represents a message in the serialization format. The messages in the format are a perfect mirror of the methods that are called on the runtime during execution.

Constants

EXPRESSION_PRUNING

The name of the environment variable that signals the runtime to perform expression pruning.

HITMAP_ENV_NAME

The environment name used to identify the hitmap for the concolic runtime.

NO_FLOAT_ENV_NAME

The name of the environment variable that signals the runtime to concretize floating point operations.

SELECTIVE_SYMBOLICATION_ENV_NAME

The name of the environment variable that contains the byte offsets to be symbolized.

Type Aliases

SymExprRef

A SymExprRef identifies a SymExpr in a trace.