Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
94 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
symbol_tablet symex_symbol_table
FIFO save queue: paths are resumed in the order that they were saved.
std::list< instructiont > instructionst
Base class for all expressions.
symbol_tablet & symbol_table
void append(goto_programt::instructionst &instructions)
Storage of symbolic execution paths to resume.
bool constant_propagation
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::unique_ptr< T > util_make_unique(Ts &&... ts)
void append_loop(goto_programt &program, goto_programt::targett loop_header)
goto_functionst functions
exprt eval(const exprt &e)
The main class for the forward symbolic simulator.
scratch_programt(symbol_tablet &_symbol_table, message_handlert &mh)
targett assume(const exprt &guard)
symex_target_equationt equation
std::unique_ptr< propt > satcheck
void append_path(patht &path)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
instructionst instructions
The list of instructions in the goto program.
A collection of goto functions.
std::list< path_nodet > patht
Decision procedure interface for various SMT 2.x solvers.
A generic container class for the GOTO intermediate representation of one function.
static optionst get_default_options()
targett assign(const exprt &lhs, const exprt &rhs)
goto_symex_statet symex_state
instructionst::iterator targett