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