cprover
interpretert Class Reference

#include <interpreter_class.h>

Collaboration diagram for interpretert:
[legend]

Classes

class  memory_cellt
 
class  stack_framet
 

Public Member Functions

 interpretert (const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
 
void operator() ()
 

Protected Types

typedef std::unordered_map< irep_idt, unsigned, irep_id_hashmemory_mapt
 
typedef std::vector< memory_celltmemoryt
 
typedef std::stack< stack_frametcall_stackt
 

Protected Member Functions

void build_memory_map ()
 
void build_memory_map (const symbolt &symbol)
 
unsigned get_size (const typet &type) const
 
void step ()
 
void execute_assert ()
 
void execute_assume ()
 
void execute_assign ()
 
void execute_goto ()
 
void execute_function_call ()
 
void execute_other ()
 
void execute_decl ()
 
void assign (mp_integer address, const std::vector< mp_integer > &rhs)
 
void read (mp_integer address, std::vector< mp_integer > &dest) const
 
void command ()
 
bool evaluate_boolean (const exprt &expr) const
 
void evaluate (const exprt &expr, std::vector< mp_integer > &dest) const
 
mp_integer evaluate_address (const exprt &expr) const
 
void show_state ()
 

Protected Attributes

const symbol_tabletsymbol_table
 
const namespacet ns
 
const goto_functionstgoto_functions
 
memory_mapt memory_map
 
memoryt memory
 
std::size_t stack_pointer
 
call_stackt call_stack
 
goto_functionst::function_mapt::const_iterator function
 
goto_programt::const_targett PC
 
goto_programt::const_targett next_PC
 
bool done
 

Detailed Description

Definition at line 21 of file interpreter_class.h.

Member Typedef Documentation

§ call_stackt

Definition at line 89 of file interpreter_class.h.

§ memory_mapt

typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> interpretert::memory_mapt
protected

Definition at line 40 of file interpreter_class.h.

§ memoryt

typedef std::vector<memory_cellt> interpretert::memoryt
protected

Definition at line 51 of file interpreter_class.h.

Constructor & Destructor Documentation

§ interpretert()

interpretert::interpretert ( const symbol_tablet _symbol_table,
const goto_functionst _goto_functions 
)
inline

Definition at line 24 of file interpreter_class.h.

References operator()().

Member Function Documentation

§ assign()

void interpretert::assign ( mp_integer  address,
const std::vector< mp_integer > &  rhs 
)
protected

§ build_memory_map() [1/2]

void interpretert::build_memory_map ( )
protected

Definition at line 363 of file interpreter.cpp.

References memory, stack_pointer, symbol_table, and symbol_tablet::symbols.

Referenced by operator()().

§ build_memory_map() [2/2]

§ command()

void interpretert::command ( )
protected

Definition at line 69 of file interpreter.cpp.

References BUFSIZE, and done.

Referenced by operator()().

§ evaluate()

§ evaluate_address()

§ evaluate_boolean()

bool interpretert::evaluate_boolean ( const exprt expr) const
inlineprotected

Definition at line 96 of file interpreter_class.h.

References evaluate(), evaluate_address(), and show_state().

Referenced by execute_assert(), execute_assume(), and execute_goto().

§ execute_assert()

void interpretert::execute_assert ( )
protected

Definition at line 255 of file interpreter.cpp.

References evaluate_boolean(), and PC.

Referenced by step().

§ execute_assign()

void interpretert::execute_assign ( )
protected

§ execute_assume()

void interpretert::execute_assume ( )
protected

Definition at line 249 of file interpreter.cpp.

References evaluate_boolean(), and PC.

Referenced by step().

§ execute_decl()

void interpretert::execute_decl ( )
protected

Definition at line 206 of file interpreter.cpp.

References PC.

Referenced by step().

§ execute_function_call()

§ execute_goto()

void interpretert::execute_goto ( )
protected

Definition at line 178 of file interpreter.cpp.

References evaluate_boolean(), next_PC, and PC.

Referenced by step().

§ execute_other()

void interpretert::execute_other ( )
protected

Definition at line 192 of file interpreter.cpp.

References evaluate(), id2string(), and PC.

Referenced by step().

§ get_size()

§ operator()()

§ read()

void interpretert::read ( mp_integer  address,
std::vector< mp_integer > &  dest 
) const
protected

Definition at line 21 of file interpreter_evaluate.cpp.

References integer2size_t(), and memory.

Referenced by evaluate().

§ show_state()

void interpretert::show_state ( )
protected

Definition at line 53 of file interpreter.cpp.

References function, ns, and PC.

Referenced by evaluate_boolean(), and operator()().

§ step()

Member Data Documentation

§ call_stack

call_stackt interpretert::call_stack
protected

Definition at line 90 of file interpreter_class.h.

Referenced by evaluate_address(), execute_function_call(), and step().

§ done

bool interpretert::done
protected

Definition at line 94 of file interpreter_class.h.

Referenced by command(), operator()(), and step().

§ function

goto_functionst::function_mapt::const_iterator interpretert::function
protected

Definition at line 92 of file interpreter_class.h.

Referenced by evaluate(), evaluate_address(), show_state(), and step().

§ goto_functions

const goto_functionst& interpretert::goto_functions
protected

Definition at line 38 of file interpreter_class.h.

Referenced by execute_function_call(), and operator()().

§ memory

memoryt interpretert::memory
protected

Definition at line 52 of file interpreter_class.h.

Referenced by assign(), build_memory_map(), execute_function_call(), and read().

§ memory_map

memory_mapt interpretert::memory_map
protected

Definition at line 41 of file interpreter_class.h.

Referenced by build_memory_map(), and evaluate_address().

§ next_PC

goto_programt::const_targett interpretert::next_PC
protected

Definition at line 93 of file interpreter_class.h.

Referenced by execute_function_call(), execute_goto(), and step().

§ ns

const namespacet interpretert::ns
protected

§ PC

§ stack_pointer

std::size_t interpretert::stack_pointer
protected

Definition at line 54 of file interpreter_class.h.

Referenced by build_memory_map(), execute_function_call(), and step().

§ symbol_table

const symbol_tablet& interpretert::symbol_table
protected

Definition at line 36 of file interpreter_class.h.

Referenced by build_memory_map().


The documentation for this class was generated from the following files: