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