69 const goto_functionst::function_mapt::const_iterator
73 throw "main not found";
77 if(!goto_function.body_available())
78 throw "main has no body";
80 pc=goto_function.body.instructions.begin();
116 <<
" ----------------------------------------------------\n";
118 if(
pc==
function->second.body.instructions.end())
145 <<
"h: display this menu\n"
146 <<
"j: output json trace\n"
147 <<
"m: output memory dump\n"
148 <<
"o: output goto trace\n"
150 <<
"r: run up to entry point\n"
151 <<
"s#: step a number of instructions\n"
152 <<
"sa: step across a function\n"
153 <<
"so: step out of a function\n"
154 <<
"se: step until end of program\n"
201 else if((
ch==
's') || (
ch==0))
237 if(
pc==
function->second.body.instructions.end())
297 throw "SET_RETURN_VALUE without call";
299 if(
call_stack.top().return_value_address != 0)
320 throw "START_THREAD not yet implemented";
323 throw "END_THREAD not yet implemented";
328 throw "ATOMIC_BEGIN not yet implemented";
332 throw "ATOMIC_END not yet implemented";
341 if(
pc==
function->second.body.instructions.end())
363 throw "encountered instruction with undefined instruction type";
373 if(
pc->targets.empty())
374 throw "taken goto without target";
376 if(
pc->targets.size()>=2)
377 throw "non-deterministic goto encountered";
386 const irep_idt &statement =
pc->get_other().get_statement();
390 pc->code().operands().size() == 1,
391 "expression statement expected to have one operand");
400 while(rhs.size()<size) rhs.insert(rhs.end(),
tmp.begin(),
tmp.end());
402 output.
error() <<
"!! failed to obtain rhs (" << rhs.size() <<
" vs. "
415 throw "unexpected OTHER statement: "+
id2string(statement);
428 throw "request for member of non-struct";
436 for(
const auto &
c : components)
444 throw "access out of struct bounds";
470 result.reserve_operands(components.size());
474 for(
const auto &
c : components)
479 result.copy_to_operands(
operand);
482 return std::move(result);
506 result.copy_to_operands(
operand);
508 return std::move(result);
537 result.reserve_operands(components.size());
545 result.copy_to_operands(
operand);
547 return std::move(result);
573 result.copy_to_operands(
operand);
575 return std::move(result);
633 throw "interpreter: reading from invalid pointer";
651 const exprt &assign_lhs =
pc->assign_lhs();
652 const exprt &assign_rhs =
pc->assign_rhs();
662 output.
error() <<
"!! failed to obtain rhs (" << rhs.size() <<
" vs. "
721 throw "assumption failed";
729 output.
error() <<
"assertion failed at " <<
pc->location_number <<
"\n"
736 const auto &call_lhs =
pc->call_lhs();
737 const auto &call_function =
pc->call_function();
738 const auto &call_arguments =
pc->call_arguments();
744 throw "function call to NULL";
746 throw "out-of-range function call";
757 const goto_functionst::function_mapt::const_iterator
f_it=
761 throw "failed to find function "+
id2string(identifier);
766 if(call_lhs.is_not_nil())
769 return_value_address=0;
776 for(std::size_t i = 0; i < call_arguments.size(); i++)
781 if(
f_it->second.body_available())
792 std::set<irep_idt> locals;
795 for(
const auto &
id : locals)
802 const auto ¶meter_identifiers =
f_it->second.parameter_identifiers;
804 throw "not enough arguments";
806 for(std::size_t i = 0; i < parameter_identifiers.size(); i++)
809 ns.lookup(parameter_identifiers[i]).symbol_expr();
819 list_input_varst::iterator it =
825 PRECONDITION(!it->second.front().return_assignments.empty());
827 evaluate(it->second.front().return_assignments.back().value);
828 if(return_value_address>0)
830 assign(return_value_address, value);
832 it->second.pop_front();
952 if(st.components().empty())
975 for(
const auto &
comp : components)
978 comp.type().id() !=
ID_code,
"struct member must not be of code type");
991 for(
const auto &
comp : components)
994 comp.type().id() !=
ID_code,
"union member must not be of code type");
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Operator to return the address of an object.
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Array constructor from list of elements.
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
The Boolean constant false.
void from_integer(const mp_integer &i)
constant_exprt to_expr() const
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
Step of the trace of a GOTO program.
void add_step(const goto_trace_stept &step)
Add a step at the end of the trace.
void output(const class namespacet &ns, std::ostream &out) const
Outputs the trace in ASCII to a given stream.
goto_trace_stept & get_last_step()
Retrieves the final step in the trace for manipulation (used to fill a trace from code,...
An IEEE 754 floating-point value, including specificiation.
constant_exprt to_expr() const
void unpack(const mp_integer &)
Unbounded, signed integers (mathematical integers, not bitvectors)
mp_integer old_stack_pointer
mp_integer return_value_address
goto_programt::const_targett return_pc
goto_functionst::function_mapt::const_iterator return_function
void clear_input_flags()
Clears memoy r/w flag initialization.
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
void execute_function_call()
mp_integer base_address_to_actual_size(const mp_integer &address) const
void print_memory(bool input_flags)
Prints the current state of the memory map Since messaget mdofifies class members,...
mp_integer evaluate_address(const exprt &expr, bool fail_quietly=false)
virtual void command()
reads a user command and executes it.
goto_functionst::function_mapt::const_iterator function
inverse_memory_mapt inverse_memory_map
symbol_exprt address_to_symbol(const mp_integer &address) const
void execute_goto()
executes a goto instruction
void build_memory_map()
Creates a memory map of all static symbols in the program.
std::vector< mp_integer > mp_vectort
mp_vectort evaluate(const exprt &)
Evaluate an expression.
void execute_assign()
executes the assign statement at the current pc value
list_input_varst function_input_vars
void assign(const mp_integer &address, const mp_vectort &rhs)
sets the memory at address with the given rhs value (up to sizeof(rhs))
std::stack< stack_framet > call_stackt
typet concretize_type(const typet &type)
turns a variable length array type into a fixed array type
mp_integer address_to_offset(const mp_integer &address) const
const symbol_table_baset & symbol_table
void step()
executes a single step and updates the program counter
struct_typet::componentt get_component(const typet &object_type, const mp_integer &offset)
Retrieves the member at offset of an object of type object_type.
mp_integer base_address_to_alloc_size(const mp_integer &address) const
goto_programt::const_targett next_pc
bool evaluate_boolean(const exprt &expr)
mp_integer get_size(const typet &type)
Retrieves the actual size of the provided structured type.
void show_state()
displays the current position of the pc and corresponding code
void initialize(bool init)
Initializes the memory map of the interpreter and [optionally] runs up to the entry point (thus doing...
bool unbounded_size(const typet &)
void execute_other()
executes side effects of 'other' instructions
goto_programt::const_targett pc
dynamic_typest dynamic_types
typet get_type(const irep_idt &id) const
returns the type object corresponding to id
const goto_functionst & goto_functions
const irept & find(const irep_idt &name) const
const irep_idt & id() const
Extract member of struct or union.
mstreamt & warning() const
mstreamt & result() const
mstreamt & status() const
The null pointer constant.
A side_effect_exprt that returns a non-deterministically chosen value.
An expression containing a side effect.
void resize(uint64_t new_size)
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
std::vector< componentt > componentst
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
The Boolean constant true.
The type of an expression, extends irept.
void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
Return in dest the identifiers of the local variables declared in the goto_function and the identifie...
void interpreter(const goto_modelt &goto_model, message_handlert &message_handler)
Interpreter for GOTO Programs.
Interpreter for GOTO Programs.
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
static void stack_depth(goto_programt &goto_program, const symbol_exprt &symbol, const std::size_t i_depth, const exprt &max_depth)
side_effect_exprt & to_side_effect_expr(exprt &expr)
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
char * fgets(char *str, int size, FILE *stream)
std::size_t unsafe_string2size_t(const std::string &str, int base)
string_containert & get_string_container()
Get a reference to the global string container.