12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H 13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H 88 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SCRATCH_PROGRAM_H
Generate Equation using Symbolic Execution.
targett assign(const exprt &lhs, const exprt &rhs)
std::list< instructiont > instructionst
instructionst instructions
The list of instructions in the goto program.
Goto Programs with Functions.
symbol_tablet & symbol_table
scratch_programt(symbol_tablet &_symbol_table)
Decision procedure interface for various SMT 2.x solvers.
goto_functionst functions
targett assume(const exprt &guard)
exprt eval(const exprt &e)
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 specialization of goto_program_templatet over goto programs in which instructions have codet type...
The main class for the forward symbolic simulator.
symex_target_equationt equation
void append_path(patht &path)
Base class for all expressions.
goto_symex_statet symex_state
instructionst::iterator targett