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
97 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
symbol_tablet symex_symbol_table
Generate Equation using Symbolic Execution.
FIFO save queue: paths are resumed in the order that they were saved.
std::list< instructiont > instructionst
decision_proceduret * checker
Base class for all expressions.
symbol_tablet & symbol_table
scratch_programt(symbol_tablet &_symbol_table, message_handlert &mh, guard_managert &guard_manager)
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...
This is unused by this implementation of guards, but can be used by other implementations of the same...
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.
bool check_sat(guard_managert &guard_manager)
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::unique_ptr< goto_symex_statet > symex_state
std::list< path_nodet > patht
Decision procedure interface for various SMT 2.x solvers.
Goto Programs with Functions.
A generic container class for the GOTO intermediate representation of one function.
static optionst get_default_options()
bool check_sat(bool do_slice, guard_managert &guard_manager)
targett assign(const exprt &lhs, const exprt &rhs)
instructionst::iterator targett