cprover
|
#include <interpreter_class.h>
Classes | |
struct | function_assignments_contextt |
struct | function_assignmentt |
class | memory_cellt |
class | stack_framet |
Public Types | |
typedef std::vector< function_assignmentt > | function_assignmentst |
typedef std::vector< mp_integer > | mp_vectort |
typedef std::pair< irep_idt, irep_idt > | assignment_idt |
typedef std::pair< exprt, exprt > | diff_pairt |
typedef std::map< assignment_idt, diff_pairt > | side_effects_differencet |
typedef std::pair< irep_idt, exprt > | input_entryt |
typedef std::map< irep_idt, exprt > | input_valuest |
typedef std::map< irep_idt, typet > | dynamic_typest |
typedef std::map< irep_idt, function_assignmentst > | output_valuest |
typedef std::list< function_assignments_contextt > | function_assignments_contextst |
typedef std::map< irep_idt, std::list< function_assignments_contextt > > | list_input_varst |
Public Member Functions | |
interpretert (const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, message_handlert &_message_handler) | |
void | operator() () |
void | print_memory (bool input_flags) |
Prints the current state of the memory map Since messaget mdofifies class members, print functions are nonconst. More... | |
const dynamic_typest & | get_dynamic_types () |
Public Attributes | |
output_valuest | output_values |
Protected Types | |
typedef std::unordered_map< irep_idt, mp_integer > | memory_mapt |
typedef std::map< mp_integer, irep_idt > | inverse_memory_mapt |
typedef sparse_vectort< memory_cellt > | memoryt |
typedef std::map< std::string, const irep_idt & > | parameter_sett |
typedef std::pair< const irep_idt, const irep_idt > | struct_member_idt |
typedef std::map< struct_member_idt, const exprt > | struct_valuest |
typedef std::stack< stack_framet > | call_stackt |
Protected Member Functions | |
const inverse_memory_mapt::value_type & | address_to_object_record (const mp_integer &address) const |
irep_idt | address_to_identifier (const mp_integer &address) const |
mp_integer | address_to_offset (const mp_integer &address) const |
mp_integer | base_address_to_alloc_size (const mp_integer &address) const |
mp_integer | base_address_to_actual_size (const mp_integer &address) const |
void | build_memory_map () |
Creates a memory map of all static symbols in the program. More... | |
void | build_memory_map (const symbolt &symbol) |
mp_integer | build_memory_map (const irep_idt &id, const typet &type) |
Populates dynamic entries of the memory map. More... | |
typet | concretize_type (const typet &type) |
turns a variable length array type into a fixed array type More... | |
bool | unbounded_size (const typet &) |
mp_integer | get_size (const typet &type) |
Retrieves the actual size of the provided structured type. More... | |
struct_typet::componentt | get_component (const irep_idt &object, const mp_integer &offset) |
retrieves the member at offset More... | |
typet | get_type (const irep_idt &id) const |
returns the type object corresponding to id More... | |
exprt | get_value (const typet &type, const mp_integer &offset=0, bool use_non_det=false) |
retrives the constant value at memory location offset as an object of type type More... | |
exprt | get_value (const typet &type, mp_vectort &rhs, const mp_integer &offset=0) |
returns the value at offset in the form of type given a memory buffer rhs which is typically a structured type More... | |
exprt | get_value (const irep_idt &id) |
void | step () |
executes a single step and updates the program counter More... | |
void | execute_assert () |
void | execute_assume () |
void | execute_assign () |
executes the assign statement at the current pc value More... | |
void | execute_goto () |
executes a goto instruction More... | |
void | execute_function_call () |
void | execute_other () |
executes side effects of 'other' instructions More... | |
void | execute_decl () |
void | clear_input_flags () |
Clears memoy r/w flag initialization. More... | |
void | allocate (const mp_integer &address, const mp_integer &size) |
reserves memory block of size at address More... | |
void | assign (const mp_integer &address, const mp_vectort &rhs) |
sets the memory at address with the given rhs value (up to sizeof(rhs)) More... | |
void | read (const mp_integer &address, mp_vectort &dest) const |
Reads a memory address and loads it into the dest variable. More... | |
void | read_unbounded (const mp_integer &address, mp_vectort &dest) const |
virtual void | command () |
reads a user command and executes it. More... | |
bool | evaluate_boolean (const exprt &expr) |
bool | count_type_leaves (const typet &source_type, mp_integer &result) |
Count the number of leaf subtypes of ty , a leaf type is a type that is not an array or a struct. More... | |
bool | byte_offset_to_memory_offset (const typet &source_type, const mp_integer &byte_offset, mp_integer &result) |
Supposing the caller has an mp_vector representing a value with type 'source_type', this yields the offset into that vector at which to find a value at byte address 'offset'. More... | |
bool | memory_offset_to_byte_offset (const typet &source_type, const mp_integer &cell_offset, mp_integer &result) |
Similarly to the above, the interpreter's memory objects contain mp_integers that represent variable-sized struct members. More... | |
void | evaluate (const exprt &expr, mp_vectort &dest) |
Evaluate an expression. More... | |
mp_integer | evaluate_address (const exprt &expr, bool fail_quietly=false) |
void | initialize (bool init) |
Initializes the memory map of the interpreter and [optionally] runs up to the entry point (thus doing the cprover initialization) More... | |
void | show_state () |
displays the current position of the pc and corresponding code More... | |
Protected Attributes | |
const symbol_tablet & | symbol_table |
const namespacet | ns |
const goto_functionst & | goto_functions |
memory_mapt | memory_map |
inverse_memory_mapt | inverse_memory_map |
memoryt | memory |
mp_integer | stack_pointer |
call_stackt | call_stack |
input_valuest | input_vars |
list_input_varst | function_input_vars |
goto_functionst::function_mapt::const_iterator | function |
goto_programt::const_targett | pc |
goto_programt::const_targett | next_pc |
goto_programt::const_targett | target_assert |
goto_tracet | steps |
bool | done |
bool | show |
bool | stop_on_assertion |
size_t | num_steps |
size_t | total_steps |
dynamic_typest | dynamic_types |
int | num_dynamic_objects |
mp_integer | stack_depth |
int | thread_id |
Static Protected Attributes | |
static const size_t | npos =std::numeric_limits<size_t>::max() |
Additional Inherited Members |
Definition at line 27 of file interpreter_class.h.
typedef std::pair<irep_idt, irep_idt> interpretert::assignment_idt |
Definition at line 62 of file interpreter_class.h.
|
protected |
Definition at line 257 of file interpreter_class.h.
typedef std::pair<exprt, exprt> interpretert::diff_pairt |
Definition at line 65 of file interpreter_class.h.
typedef std::map<irep_idt, typet> interpretert::dynamic_typest |
Definition at line 77 of file interpreter_class.h.
typedef std::list<function_assignments_contextt> interpretert::function_assignments_contextst |
Definition at line 94 of file interpreter_class.h.
typedef std::vector<function_assignmentt> interpretert::function_assignmentst |
Definition at line 57 of file interpreter_class.h.
typedef std::pair<irep_idt, exprt> interpretert::input_entryt |
Definition at line 71 of file interpreter_class.h.
typedef std::map<irep_idt, exprt> interpretert::input_valuest |
Definition at line 74 of file interpreter_class.h.
|
protected |
Definition at line 109 of file interpreter_class.h.
typedef std::map<irep_idt, std::list<function_assignments_contextt> > interpretert::list_input_varst |
Definition at line 96 of file interpreter_class.h.
|
protected |
Definition at line 108 of file interpreter_class.h.
|
protected |
Definition at line 180 of file interpreter_class.h.
typedef std::vector<mp_integer> interpretert::mp_vectort |
Definition at line 59 of file interpreter_class.h.
typedef std::map<irep_idt, function_assignmentst> interpretert::output_valuest |
Definition at line 79 of file interpreter_class.h.
|
protected |
Definition at line 181 of file interpreter_class.h.
typedef std::map<assignment_idt, diff_pairt> interpretert::side_effects_differencet |
Definition at line 68 of file interpreter_class.h.
|
protected |
Definition at line 183 of file interpreter_class.h.
|
protected |
Definition at line 184 of file interpreter_class.h.
|
inline |
Definition at line 30 of file interpreter_class.h.
References show.
|
inlineprotected |
Definition at line 125 of file interpreter_class.h.
References address_to_object_record().
Referenced by assign(), evaluate(), execute_function_call(), get_value(), and print_memory().
|
inlineprotected |
Definition at line 113 of file interpreter_class.h.
References CHECK_RETURN, and inverse_memory_map.
Referenced by address_to_identifier(), and address_to_offset().
|
inlineprotected |
Definition at line 130 of file interpreter_class.h.
References address_to_object_record().
Referenced by assign(), base_address_to_alloc_size(), evaluate(), get_value(), print_memory(), and read_unbounded().
|
protected |
reserves memory block of size at address
Definition at line 75 of file interpreter_evaluate.cpp.
References interpretert::memory_cellt::initialized, integer2ulong(), memory, sparse_vectort< T >::size(), interpretert::memory_cellt::UNKNOWN, and interpretert::memory_cellt::value.
|
protected |
sets the memory at address with the given rhs value (up to sizeof(rhs))
Definition at line 710 of file interpreter.cpp.
References address_to_identifier(), address_to_offset(), messaget::eom(), interpretert::memory_cellt::initialized, integer2size_t(), integer2ulong(), memory, show, sparse_vectort< T >::size(), messaget::status(), total_steps, interpretert::memory_cellt::UNKNOWN, interpretert::memory_cellt::value, and interpretert::memory_cellt::WRITTEN_BEFORE_READ.
Referenced by execute_assign(), execute_function_call(), execute_other(), and step().
|
inlineprotected |
Definition at line 146 of file interpreter_class.h.
References base_address_to_alloc_size(), sparse_vectort< T >::end(), sparse_vectort< T >::find(), integer2ulong(), and memory.
Referenced by get_value(), and read_unbounded().
|
inlineprotected |
Definition at line 135 of file interpreter_class.h.
References address_to_offset(), inverse_memory_map, memory, PRECONDITION, and sparse_vectort< T >::size().
Referenced by base_address_to_actual_size(), and build_memory_map().
|
protected |
Creates a memory map of all static symbols in the program.
Definition at line 863 of file interpreter.cpp.
References dynamic_types, inverse_memory_map, memory, num_dynamic_objects, sparse_vectort< T >::resize(), sparse_vectort< T >::size(), stack_pointer, symbol_table, and symbol_table_baset::symbols.
Referenced by evaluate(), evaluate_address(), execute_function_call(), and initialize().
|
protected |
Definition at line 880 of file interpreter.cpp.
References get_size(), irept::id(), integer2ulong(), inverse_memory_map, symbolt::is_static_lifetime, memory, memory_map, symbolt::name, sparse_vectort< T >::resize(), sparse_vectort< T >::size(), and symbolt::type.
|
protected |
Populates dynamic entries of the memory map.
Definition at line 930 of file interpreter.cpp.
References base_address_to_alloc_size(), concretize_type(), dynamic_types, get_size(), integer2ulong(), inverse_memory_map, memory, memory_map, sparse_vectort< T >::resize(), and sparse_vectort< T >::size().
|
protected |
Supposing the caller has an mp_vector representing a value with type 'source_type', this yields the offset into that vector at which to find a value at byte address 'offset'.
We need this because the interpreter's memory map uses unlabelled variable-width values – for example, a C value { { 1, 2 }, 3, 4 } of type struct { int x[2]; char y; unsigned long z; } would be represented [1,2,3,4], with the source type needed alongside to figure out which member is targeted by a byte-extract operation.
Definition at line 151 of file interpreter_evaluate.cpp.
References count_type_leaves(), evaluate(), irept::id(), member_offset(), ns, pointer_offset_size(), messaget::result(), to_array_type(), and to_struct_type().
Referenced by evaluate(), and evaluate_address().
|
protected |
Clears memoy r/w flag initialization.
Definition at line 92 of file interpreter_evaluate.cpp.
References memory, interpretert::memory_cellt::UNKNOWN, and interpretert::memory_cellt::WRITTEN_BEFORE_READ.
Referenced by initialize().
|
protectedvirtual |
reads a user command and executes it.
Definition at line 125 of file interpreter.cpp.
References BUFSIZE, call_stack, done, messaget::eom(), initialize(), npos, ns, num_steps, jsont::output(), goto_tracet::output(), print_memory(), messaget::result(), show_state(), stack_depth, messaget::status(), step(), and steps.
Referenced by operator()().
turns a variable length array type into a fixed array type
Definition at line 903 of file interpreter.cpp.
References messaget::eom(), evaluate(), irept::find(), from_integer(), irept::id(), messaget::result(), typet::subtype(), and messaget::warning().
Referenced by build_memory_map().
|
protected |
Count the number of leaf subtypes of ty
, a leaf type is a type that is not an array or a struct.
For instance the count for a type such as struct { (int[3])[5]; int }
would be 16 = (3 * 5 + 1).
ty | a type | |
[out] | result | Number of leaf primitive types in ty |
Definition at line 108 of file interpreter_evaluate.cpp.
References struct_union_typet::components(), evaluate(), irept::id(), messaget::result(), to_array_type(), and to_struct_type().
Referenced by byte_offset_to_memory_offset(), evaluate(), and memory_offset_to_byte_offset().
|
protected |
Evaluate an expression.
expr | expression to evaluate | |
[out] | dest | vector in which the result of the evaluation is stored |
Definition at line 295 of file interpreter_evaluate.cpp.
References address_to_identifier(), address_to_offset(), arith_left_shift(), arith_right_shift(), binary2integer(), bitwise_and(), bitwise_neg(), bitwise_or(), bitwise_xor(), build_memory_map(), byte_offset_to_memory_offset(), CHECK_RETURN, count_type_leaves(), DATA_INVARIANT, messaget::eom(), messaget::error(), evaluate_address(), forall_operands, from_expr(), fixedbvt::from_expr(), ieee_floatt::from_expr(), fixedbvt::from_integer(), ieee_floatt::from_integer(), function, get_size(), side_effect_exprt::get_statement(), get_string_container(), get_type(), fixedbvt::get_value(), get_value(), constant_exprt::get_value(), exprt::has_operands(), irept::id(), id2string(), integer2binary(), integer2size_t(), exprt::is_true(), logic_right_shift(), memory, memory_offset_to_byte_offset(), ns, num_dynamic_objects, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), ieee_floatt::pack(), irept::pretty(), read(), read_unbounded(), messaget::result(), rotate_left(), rotate_right(), fixedbvt::set_value(), show, sparse_vectort< T >::size(), fixedbvt::spec, typet::subtype(), to_array_type(), to_bitvector_type(), to_constant_expr(), to_fixedbv_type(), to_floatbv_type(), to_integer(), to_side_effect_expr(), to_signedbv_type(), to_unsignedbv_type(), to_with_expr(), exprt::type(), unbounded_size(), ieee_floatt::unpack(), and messaget::warning().
Referenced by byte_offset_to_memory_offset(), concretize_type(), count_type_leaves(), evaluate_address(), evaluate_boolean(), execute_assign(), execute_function_call(), execute_other(), get_size(), memory_offset_to_byte_offset(), and step().
|
protected |
Definition at line 1068 of file interpreter_evaluate.cpp.
References build_memory_map(), byte_offset_to_memory_offset(), call_stack, struct_union_typet::components(), messaget::eom(), messaget::error(), evaluate(), namespace_baset::follow(), from_expr(), function, member_exprt::get_component_name(), symbol_exprt::get_identifier(), ssa_exprt::get_original_name(), get_size(), irept::id(), is_ssa_expr(), memory, memory_map, ns, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), messaget::result(), sparse_vectort< T >::size(), to_member_expr(), to_ssa_expr(), to_struct_type(), to_symbol_expr(), and exprt::type().
Referenced by evaluate(), execute_assign(), execute_function_call(), execute_other(), and get_value().
|
inlineprotected |
Definition at line 278 of file interpreter_class.h.
References evaluate().
Referenced by execute_assert(), execute_assume(), and execute_goto().
|
protected |
Definition at line 741 of file interpreter.cpp.
References messaget::eom(), messaget::error(), evaluate_boolean(), pc, show, stop_on_assertion, and target_assert.
Referenced by step().
|
protected |
executes the assign statement at the current pc value
Definition at line 655 of file interpreter.cpp.
References assign(), ssa_exprt::can_build_identifier(), messaget::eom(), messaget::error(), evaluate(), evaluate_address(), goto_trace_stept::full_lhs, goto_trace_stept::full_lhs_value, goto_tracet::get_last_step(), get_size(), side_effect_exprt::get_statement(), get_value(), irept::id(), integer2size_t(), integer2ulong(), code_assignt::lhs(), goto_trace_stept::lhs_object, goto_trace_stept::lhs_object_value, memory, pc, interpretert::memory_cellt::READ_BEFORE_WRITTEN, code_assignt::rhs(), steps, to_code_assign(), to_side_effect_expr(), and exprt::type().
Referenced by step().
|
protected |
Definition at line 735 of file interpreter.cpp.
References evaluate_boolean(), and pc.
Referenced by step().
|
protected |
Definition at line 415 of file interpreter.cpp.
References pc, and PRECONDITION.
Referenced by step().
|
protected |
Definition at line 753 of file interpreter.cpp.
References address_to_identifier(), code_function_callt::arguments(), assign(), build_memory_map(), call_stack, messaget::eom(), messaget::error(), evaluate(), evaluate_address(), code_function_callt::function(), function_input_vars, goto_functionst::function_map, code_typet::parametert::get_identifier(), goto_tracet::get_last_step(), get_local_identifiers(), goto_functions, id2string(), goto_trace_stept::identifier, irept::is_not_nil(), code_function_callt::lhs(), interpretert::stack_framet::local_map, namespacet::lookup(), memory, next_pc, ns, interpretert::stack_framet::old_stack_pointer, code_typet::parameters(), pc, PRECONDITION, interpretert::stack_framet::return_function, interpretert::stack_framet::return_pc, interpretert::stack_framet::return_value_address, show, sparse_vectort< T >::size(), stack_pointer, steps, to_code_function_call(), to_code_type(), to_symbol_expr(), symbolt::type, and exprt::type().
Referenced by step().
|
protected |
executes a goto instruction
Definition at line 366 of file interpreter.cpp.
References evaluate_boolean(), next_pc, and pc.
Referenced by step().
|
protected |
executes side effects of 'other' instructions
Definition at line 381 of file interpreter.cpp.
References assign(), DATA_INVARIANT, messaget::eom(), messaget::error(), evaluate(), evaluate_address(), get_size(), id2string(), and pc.
Referenced by step().
|
protected |
retrieves the member at offset
Definition at line 422 of file interpreter.cpp.
References struct_union_typet::components(), namespace_baset::follow(), get_size(), irept::id(), namespacet::lookup(), ns, to_struct_type(), and symbolt::type.
Referenced by get_value().
|
inline |
Definition at line 98 of file interpreter_class.h.
References dynamic_types.
|
protected |
Retrieves the actual size of the provided structured type.
Unbounded objects get allocated 2^32 address space each (of a 2^64 sized space).
type | a structured type |
Definition at line 985 of file interpreter.cpp.
References CHECK_RETURN, struct_union_typet::components(), evaluate(), irept::find(), namespace_baset::follow(), from_integer(), irept::id(), ns, typet::subtype(), to_integer(), to_struct_type(), to_union_type(), exprt::type(), and unbounded_size().
Referenced by build_memory_map(), evaluate(), evaluate_address(), execute_assign(), execute_other(), get_component(), and get_value().
returns the type object corresponding to id
Definition at line 448 of file interpreter.cpp.
References dynamic_types, symbol_table_baset::lookup_ref(), symbol_table, and symbolt::type.
Referenced by evaluate(), and get_value().
|
protected |
retrives the constant value at memory location offset as an object of type type
Definition at line 458 of file interpreter.cpp.
References base_address_to_actual_size(), struct_union_typet::components(), irept::find(), namespace_baset::follow(), get_size(), irept::id(), integer2size_t(), integer2ulong(), memory, ns, messaget::result(), typet::subtype(), to_array_type(), to_integer(), to_struct_type(), and interpretert::memory_cellt::WRITTEN_BEFORE_READ.
Referenced by evaluate(), execute_assign(), and get_value().
|
protected |
returns the value at offset in the form of type given a memory buffer rhs which is typically a structured type
Definition at line 523 of file interpreter.cpp.
References address_to_identifier(), address_to_offset(), base_address_to_actual_size(), struct_union_typet::components(), messaget::eom(), messaget::error(), irept::find(), namespace_baset::follow(), fixedbvt::from_integer(), from_integer(), get_component(), get_size(), get_string_container(), get_type(), get_value(), irept::id(), integer2size_t(), integer2ulong(), memory, ns, PRECONDITION, messaget::result(), sparse_vectort< T >::size(), typet::subtype(), fixedbvt::to_expr(), ieee_floatt::to_expr(), to_floatbv_type(), to_integer(), to_struct_type(), unbounded_size(), and ieee_floatt::unpack().
Definition at line 1051 of file interpreter.cpp.
References dynamic_types, evaluate_address(), get_type(), get_value(), symbol_table_baset::lookup_ref(), symbol_table, and symbolt::type.
|
protected |
Initializes the memory map of the interpreter and [optionally] runs up to the entry point (thus doing the cprover initialization)
Definition at line 61 of file interpreter.cpp.
References build_memory_map(), call_stack, clear_input_flags(), done, goto_functionst::entry_point(), goto_functionst::function_map, goto_functions, input_vars, npos, pc, show_state(), stack_depth, step(), and total_steps.
Referenced by command(), and operator()().
|
protected |
Similarly to the above, the interpreter's memory objects contain mp_integers that represent variable-sized struct members.
This counts the size of type leaves to determine the byte offset corresponding to a memory offset.
Definition at line 228 of file interpreter_evaluate.cpp.
References count_type_leaves(), evaluate(), irept::id(), member_offset(), ns, pointer_offset_size(), messaget::result(), to_array_type(), and to_struct_type().
Referenced by evaluate().
void interpretert::operator() | ( | void | ) |
Definition at line 37 of file interpreter.cpp.
References command(), done, messaget::eom(), messaget::error(), initialize(), messaget::status(), and total_steps.
void interpretert::print_memory | ( | bool | input_flags | ) |
Prints the current state of the memory map Since messaget mdofifies class members, print functions are nonconst.
Definition at line 1071 of file interpreter.cpp.
References address_to_identifier(), address_to_offset(), messaget::debug(), messaget::eom(), interpretert::memory_cellt::initialized, memory, and interpretert::memory_cellt::value.
Referenced by command().
|
protected |
Reads a memory address and loads it into the dest
variable.
Marks cell as READ_BEFORE_WRITTEN
if cell has never been written.
Definition at line 23 of file interpreter_evaluate.cpp.
References interpretert::memory_cellt::initialized, integer2ulong(), memory, interpretert::memory_cellt::READ_BEFORE_WRITTEN, sparse_vectort< T >::size(), interpretert::memory_cellt::UNKNOWN, and interpretert::memory_cellt::value.
Referenced by evaluate().
|
protected |
Definition at line 46 of file interpreter_evaluate.cpp.
References address_to_offset(), base_address_to_actual_size(), interpretert::memory_cellt::initialized, integer2size_t(), memory, interpretert::memory_cellt::READ_BEFORE_WRITTEN, sparse_vectort< T >::size(), interpretert::memory_cellt::UNKNOWN, and interpretert::memory_cellt::value.
Referenced by evaluate().
|
protected |
displays the current position of the pc and corresponding code
Definition at line 102 of file interpreter.cpp.
References messaget::eom(), function, ns, pc, show, messaget::status(), and total_steps.
Referenced by command(), and initialize().
|
protected |
executes a single step and updates the program counter
Definition at line 230 of file interpreter.cpp.
References goto_tracet::add_step(), ASSERT, goto_trace_stept::ASSERT, ASSIGN, assign(), goto_trace_stept::ASSIGNMENT, ASSUME, goto_trace_stept::ASSUME, ATOMIC_BEGIN, goto_trace_stept::ATOMIC_BEGIN, ATOMIC_END, goto_trace_stept::ATOMIC_END, call_stack, CATCH, DEAD, goto_trace_stept::DEAD, DECL, goto_trace_stept::DECL, done, END_FUNCTION, END_THREAD, evaluate(), execute_assert(), execute_assign(), execute_assume(), execute_decl(), execute_function_call(), execute_goto(), execute_other(), function, FUNCTION_CALL, goto_trace_stept::FUNCTION_CALL, goto_trace_stept::FUNCTION_RETURN, goto_tracet::get_last_step(), GOTO, goto_trace_stept::GOTO, LOCATION, goto_trace_stept::LOCATION, next_pc, OTHER, goto_trace_stept::pc, pc, RETURN, SKIP, goto_trace_stept::SPAWN, START_THREAD, steps, thread_id, goto_trace_stept::thread_nr, THROW, total_steps, and goto_trace_stept::type.
Referenced by command(), and initialize().
|
protected |
Definition at line 962 of file interpreter.cpp.
References irept::id(), array_typet::size(), typet::subtype(), to_array_type(), and to_struct_type().
Referenced by evaluate(), get_size(), and get_value().
|
protected |
Definition at line 259 of file interpreter_class.h.
Referenced by command(), evaluate_address(), execute_function_call(), initialize(), and step().
|
protected |
Definition at line 266 of file interpreter_class.h.
Referenced by command(), initialize(), operator()(), and step().
|
protected |
Definition at line 273 of file interpreter_class.h.
Referenced by build_memory_map(), get_dynamic_types(), get_type(), and get_value().
|
protected |
Definition at line 263 of file interpreter_class.h.
Referenced by evaluate(), evaluate_address(), show_state(), and step().
|
protected |
Definition at line 261 of file interpreter_class.h.
Referenced by execute_function_call().
|
protected |
Definition at line 106 of file interpreter_class.h.
Referenced by execute_function_call(), and initialize().
|
protected |
Definition at line 260 of file interpreter_class.h.
Referenced by initialize().
|
protected |
Definition at line 111 of file interpreter_class.h.
Referenced by address_to_object_record(), base_address_to_alloc_size(), and build_memory_map().
|
mutableprotected |
Definition at line 189 of file interpreter_class.h.
Referenced by allocate(), assign(), base_address_to_actual_size(), base_address_to_alloc_size(), build_memory_map(), clear_input_flags(), evaluate(), evaluate_address(), execute_assign(), execute_function_call(), get_value(), print_memory(), read(), and read_unbounded().
|
protected |
Definition at line 110 of file interpreter_class.h.
Referenced by build_memory_map(), and evaluate_address().
|
protected |
Definition at line 264 of file interpreter_class.h.
Referenced by execute_function_call(), execute_goto(), and step().
|
staticprotected |
Definition at line 269 of file interpreter_class.h.
Referenced by command(), and initialize().
|
protected |
Definition at line 104 of file interpreter_class.h.
Referenced by byte_offset_to_memory_offset(), command(), evaluate(), evaluate_address(), execute_function_call(), get_component(), get_size(), get_value(), memory_offset_to_byte_offset(), and show_state().
|
protected |
Definition at line 274 of file interpreter_class.h.
Referenced by build_memory_map(), and evaluate().
|
protected |
Definition at line 270 of file interpreter_class.h.
Referenced by command().
output_valuest interpretert::output_values |
Definition at line 80 of file interpreter_class.h.
|
protected |
Definition at line 264 of file interpreter_class.h.
Referenced by execute_assert(), execute_assign(), execute_assume(), execute_decl(), execute_function_call(), execute_goto(), execute_other(), initialize(), show_state(), and step().
|
protected |
Definition at line 267 of file interpreter_class.h.
Referenced by assign(), evaluate(), execute_assert(), execute_function_call(), interpretert(), and show_state().
|
protected |
Definition at line 275 of file interpreter_class.h.
Referenced by command(), and initialize().
|
protected |
Definition at line 191 of file interpreter_class.h.
Referenced by build_memory_map(), and execute_function_call().
|
protected |
Definition at line 265 of file interpreter_class.h.
Referenced by command(), execute_assign(), execute_function_call(), and step().
|
protected |
Definition at line 268 of file interpreter_class.h.
Referenced by execute_assert().
|
protected |
Definition at line 101 of file interpreter_class.h.
Referenced by build_memory_map(), get_type(), and get_value().
|
protected |
Definition at line 264 of file interpreter_class.h.
Referenced by execute_assert().
|
protected |
Definition at line 276 of file interpreter_class.h.
Referenced by step().
|
protected |
Definition at line 271 of file interpreter_class.h.
Referenced by assign(), initialize(), operator()(), show_state(), and step().