28 const goto_functionst::function_mapt::const_iterator
32 throw "main not found";
37 throw "main has no body";
39 PC=goto_function.
body.instructions.begin();
55 std::cout <<
"\n----------------------------------------------------\n";
57 if(
PC==
function->second.body.instructions.end())
59 std::cout <<
"End of function `" 60 <<
function->first <<
"'\n";
63 function->second.body.output_instruction(
87 if(
PC==
function->second.body.instructions.end())
134 throw "RETURN without call";
136 if(
PC->code.operands().size()==1 &&
139 std::vector<mp_integer> rhs;
144 next_PC=
function->second.body.instructions.end();
156 throw "START_THREAD not yet implemented";
159 throw "END_THREAD not yet implemented";
163 throw "ATOMIC_BEGIN not yet implemented";
166 throw "ATOMIC_END not yet implemented";
169 throw "DEAD not yet implemented";
172 throw "encountered instruction with undefined instruction type";
182 if(
PC->targets.empty())
183 throw "taken goto without target";
185 if(
PC->targets.size()>=2)
186 throw "non-deterministic goto encountered";
194 const irep_idt &statement=
PC->code.get_statement();
196 if(statement==ID_expression)
198 assert(
PC->code.operands().size()==1);
199 std::vector<mp_integer> rhs;
203 throw "unexpected OTHER statement: "+
id2string(statement);
208 assert(
PC->code.get_statement()==ID_decl);
216 std::vector<mp_integer> rhs;
225 std::cout <<
"!! failed to obtain rhs (" 226 << rhs.size() <<
" vs. " 235 const std::vector<mp_integer> &rhs)
237 for(
unsigned i=0; i<rhs.size(); i++, ++address)
242 std::cout <<
"** assigning " << cell.
identifier 243 <<
"[" << cell.
offset <<
"]:=" << rhs[i] <<
'\n';
252 throw "assumption failed";
258 throw "assertion failed";
270 throw "function call to NULL";
272 throw "out-of-range function call";
277 const goto_functionst::function_mapt::const_iterator f_it=
281 throw "failed to find function "+
id2string(identifier);
287 return_value_address=
290 return_value_address=0;
293 std::vector<std::vector<mp_integer> > argument_values;
295 argument_values.resize(function_call.
arguments().size());
297 for(std::size_t i=0; i<function_call.
arguments().size(); i++)
302 if(f_it->second.body_available())
313 std::set<irep_idt> locals;
316 for(
const auto &
id : locals)
328 if(address>=
memory.size())
331 memory[address].identifier=id;
343 if(argument_values.size()<parameters.size())
344 throw "not enough arguments";
346 for(
unsigned i=0; i<parameters.size(); i++)
351 assert(i<argument_values.size());
357 next_PC=f_it->second.body.instructions.begin();
360 throw "no body for "+
id2string(identifier);
368 memory[0].identifier=
"NULL-OBJECT";
382 if(symbol.
type.
id()==ID_code)
393 unsigned address=
memory.size();
394 memory.resize(address+size);
397 for(
unsigned i=0; i<size; i++)
409 if(type.
id()==ID_struct)
416 for(
const auto &comp : components)
418 const typet &sub_type=comp.type();
420 if(sub_type.
id()!=ID_code)
426 else if(type.
id()==ID_union)
433 for(
const auto &comp : components)
435 const typet &sub_type=comp.type();
437 if(sub_type.
id()!=ID_code)
438 max_size=std::max(max_size,
get_size(sub_type));
443 else if(type.
id()==ID_array)
445 const exprt &size_expr=
static_cast<const exprt &
>(type.
find(ID_size));
455 else if(type.
id()==ID_symbol)
bool body_available() const
The type of an expression.
irep_idt name
The unique identifier.
const typet & follow(const typet &src) const
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
const std::string & id2string(const irep_idt &d)
goto_programt::const_targett PC
goto_programt::const_targett next_PC
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
void get_local_identifiers(const goto_function_templatet< goto_programt > &goto_function, std::set< irep_idt > &dest)
std::vector< componentt > componentst
std::vector< parametert > parameterst
const componentst & components() const
void evaluate(const exprt &expr, std::vector< mp_integer > &dest) const
Interpreter for GOTO Programs.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
Interpreter for GOTO Programs.
goto_functionst::function_mapt::const_iterator function
const goto_functionst & goto_functions
std::size_t stack_pointer
static irep_idt entry_point()
bool evaluate_boolean(const exprt &expr) const
function_mapt function_map
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
mp_integer return_value_address
const symbol_tablet & symbol_table
unsigned get_size(const typet &type) const
unsigned integer2unsigned(const mp_integer &n)
void assign(mp_integer address, const std::vector< mp_integer > &rhs)
typet type
Type of symbol.
unsigned old_stack_pointer
goto_functionst::function_mapt::const_iterator return_function
Base class for all expressions.
const parameterst & parameters() const
mp_integer evaluate_address(const exprt &expr) const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
void interpreter(const symbol_tablet &symbol_table, const goto_functionst &goto_functions)
goto_programt::const_targett return_PC
std::size_t integer2size_t(const mp_integer &n)
const typet & subtype() const
const irep_idt & get_identifier() const
const irept & find(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
void execute_function_call()
const code_function_callt & to_code_function_call(const codet &code)