Module isla_lib::executor [−][src]
This module implements the core of the symbolic execution engine.
Structs
Frame | A |
LocalFrame | A |
Task | A |
TaskState |
Functions
all_unsat_collector | This |
footprint_collector | |
freeze_frame | |
start_multi | Start symbolically executing a Task across |
start_single | Start symbolically executing a Task using just the current thread, collecting the results using the given collector. |
symbolic | Create a Symbolic value of a specified type. Can return a concrete value if the type only
permits a single value, such as for the unit type or the zero-length bitvector type (which is
ideal because SMT solvers don’t allow zero-length bitvectors). Compound types like structs will
be a concrete structure with symbolic values for each field. Returns the |
trace_collector | |
trace_result_collector | |
trace_value_collector | |
unfreeze_frame |
Type Definitions
Backtrace | |
Collector | A collector is run on the result of each path found via symbolic execution through the code. It takes the result of the execution, which is either a combination of the return value and local state at the end of the execution or an error, as well as the shared state and the SMT solver state associated with that execution. It build a final result for all the executions by collecting the results into a type R. |
TraceQueue | |
TraceResultQueue | |
TraceValueQueue |