Go to the documentation of this file.
33 std::cout <<
"# " << caller <<
'\n';
34 std::stack<goto_programt::const_targett> stack;
35 std::set<goto_programt::const_targett> seen;
46 if(!seen.insert(t).second)
48 if(t->is_function_call())
51 if(callee.
id()==ID_symbol)
53 std::cout << caller <<
" -> "
81 const std::vector<irep_idt> &_sequence):
95 goto_functionst::function_mapt::const_iterator
f;
101 f->first==other.
f->first &&
108 goto_functionst::function_mapt::const_iterator
f;
116 f->first==other.
f->first &&
129 s.
pc==s.
f->second.body.instructions.end()?0:
138 typedef std::unordered_set<statet, state_hash>
statest;
144 std::stack<statet> queue;
148 std::cout <<
"empty sequence given\n";
154 goto_functionst::function_mapt::const_iterator f_it=
161 queue.top().pc=f_it->second.body.instructions.begin();
165 while(!queue.empty())
183 std::cout <<
"sequence feasible\n";
188 if(e.
pc==e.
f->second.body.instructions.end())
200 else if(e.
pc->is_function_call())
203 if(
function.
id()==ID_symbol)
211 goto_functionst::function_mapt::const_iterator f_call_it=
222 e.
pc=f_call_it->second.body.instructions.begin();
230 else if(e.
pc->is_goto())
234 if(e.
pc->get_condition().is_true())
249 std::cout <<
"sequence not feasible\n";
256 std::vector<irep_idt> sequence;
259 while(std::getline(std::cin, line))
261 if(!line.empty() && line[line.size() - 1] ==
'\r')
262 line.resize(line.size()-1);
265 sequence.push_back(line);
277 if(!i_it->is_function_call())
284 if(f.
id()!=ID_symbol)
291 std::string name=
from_expr(ns, identifier, f);
293 if(java_type_suffix!=std::string::npos)
294 name.erase(java_type_suffix);
296 std::cout <<
"found call to " << name;
300 std::cout <<
" with arguments ";
301 for(exprt::operandst::const_iterator
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
check_call_sequencet(const goto_modelt &_goto_model, const std::vector< irep_idt > &_sequence)
goto_functionst::function_mapt::const_iterator f
std::size_t operator()(const statet &s) const
const irept & find(const irep_namet &name) const
bool operator==(const statet &other) const
goto_functionst::function_mapt::const_iterator f
Base class for all expressions.
goto_programt::const_targett return_address
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
function_mapt function_map
bool operator==(const call_stack_entryt &other) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
codet representation of a function call statement.
void show_call_sequences(const irep_idt &caller, const goto_programt &goto_program)
void check_call_sequence(const goto_modelt &goto_model)
const irep_idt & get_identifier() const
#define INITIALIZE_FUNCTION
exprt simplify_expr(exprt src, const namespacet &ns)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
size_t hash_string(const dstringt &s)
instructionst instructions
The list of instructions in the goto program.
A collection of goto functions.
goto_functionst goto_functions
GOTO functions.
std::vector< call_stack_entryt > call_stack
Memory-mapped I/O Instrumentation for Goto Programs.
goto_programt::const_targett pc
std::unordered_set< statet, state_hash > statest
A generic container class for the GOTO intermediate representation of one function.
const goto_functionst & goto_functions
const std::vector< irep_idt > & sequence
#define forall_goto_functions(it, functions)
instructionst::const_iterator const_targett
unsignedbv_typet size_type()
symbol_tablet symbol_table
Symbol table.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
#define forall_goto_program_instructions(it, program)
static void list_calls_and_arguments(const namespacet &ns, const goto_programt &goto_program)