12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H 13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H 96 #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
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
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)
Base class for all expressions.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
goto_symex_statet symex_state
void set_option(const std::string &option, const bool value)
Storage of symbolic execution paths to resume.