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->guard.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!=
"" && line[line.size()-1]==
'\r')
262 line.resize(line.size()-1);
265 sequence.push_back(line);
278 if(!i_it->is_function_call())
285 if(f.
id()!=ID_symbol)
292 std::string name=
from_expr(ns, identifier, f);
294 if(java_type_suffix!=std::string::npos)
295 name.erase(java_type_suffix);
297 std::cout <<
"found call to " << name;
301 std::cout <<
" with arguments ";
302 for(exprt::operandst::const_iterator
exprt simplify_expr(const exprt &src, const namespacet &ns)
const irep_idt & get_identifier() const
const goto_functionst & goto_functions
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
function_mapt function_map
unsignedbv_typet size_type()
Memory-mapped I/O Instrumentation for Goto Programs.
symbol_tablet symbol_table
Symbol table.
const std::vector< irep_idt > & sequence
bool operator==(const statet &other) const
goto_programt::const_targett return_address
const irep_idt & id() const
goto_programt::const_targett pc
#define INITIALIZE_FUNCTION
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
std::list< Target > get_successors(Target target) const
bool operator==(const call_stack_entryt &other) const
std::size_t operator()(const statet &s) const
std::unordered_set< statet, state_hash > statest
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
goto_functionst::function_mapt::const_iterator f
A generic container class for the GOTO intermediate representation of one function.
static void list_calls_and_arguments(const namespacet &ns, const irep_idt &function, const goto_programt &goto_program)
size_t hash_string(const dstringt &s)
goto_functionst::function_mapt::const_iterator f
void show_call_sequences(const irep_idt &caller, const goto_programt &goto_program)
Base class for all expressions.
void check_call_sequence(const goto_modelt &goto_model)
std::vector< call_stack_entryt > call_stack
goto_programt & goto_program
check_call_sequencet(const goto_modelt &_goto_model, const std::vector< irep_idt > &_sequence)
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
const irept & find(const irep_namet &name) const
goto_functionst goto_functions
GOTO functions.
const code_function_callt & to_code_function_call(const codet &code)