12 #ifndef CPROVER_GOTO_PROGRAMS_INTERPRETER_CLASS_H 13 #define CPROVER_GOTO_PROGRAMS_INTERPRETER_CLASS_H 40 typedef std::unordered_map<irep_idt, unsigned, irep_id_hash>
memory_mapt;
51 typedef std::vector<memory_cellt>
memoryt;
71 const std::vector<mp_integer> &rhs);
75 std::vector<mp_integer> &dest)
const;
92 goto_functionst::function_mapt::const_iterator
function;
98 std::vector<mp_integer> v;
101 throw "invalid boolean value";
107 std::vector<mp_integer> &dest)
const;
114 #endif // CPROVER_GOTO_PROGRAMS_INTERPRETER_CLASS_H The type of an expression.
goto_programt::const_targett PC
goto_programt::const_targett next_PC
Goto Programs with Functions.
void read(mp_integer address, std::vector< mp_integer > &dest) const
void evaluate(const exprt &expr, std::vector< mp_integer > &dest) const
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
std::vector< memory_cellt > memoryt
std::unordered_map< irep_idt, unsigned, irep_id_hash > memory_mapt
std::stack< stack_framet > call_stackt
instructionst::const_iterator const_targett
interpretert(const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
const goto_functionst & goto_functions
std::size_t stack_pointer
bool evaluate_boolean(const exprt &expr) const
mp_integer return_value_address
const symbol_tablet & symbol_table
unsigned get_size(const typet &type) const
void assign(mp_integer address, const std::vector< mp_integer > &rhs)
unsigned old_stack_pointer
goto_functionst::function_mapt::const_iterator return_function
Base class for all expressions.
mp_integer evaluate_address(const exprt &expr) const
goto_programt::const_targett return_PC
void execute_function_call()