18 #include <unordered_set> 28 std::cout <<
"# From " <<
function <<
'\n';
30 std::stack<goto_programt::const_targett>
stack;
31 std::set<goto_programt::const_targett> seen;
41 if(!seen.insert(t).second)
44 if(t->is_function_call())
47 if(function2.
id()==ID_symbol)
50 std::cout <<
function <<
" -> " 70 std::cout <<
"# " <<
function <<
'\n';
79 if(!i_it->is_function_call())
84 if(f1.
id()!=ID_symbol)
113 const std::vector<irep_idt> &_sequence):
127 goto_functionst::function_mapt::const_iterator
f;
133 f->first==other.
f->first &&
140 goto_functionst::function_mapt::const_iterator
f;
148 f->first==other.
f->first &&
161 s.
pc==s.
f->second.body.instructions.end()?0:
170 typedef std::unordered_set<statet, state_hash>
statest;
176 std::stack<statet> queue;
180 std::cout <<
"empty sequence given\n";
186 goto_functionst::function_mapt::const_iterator f_it=
193 queue.top().pc=f_it->second.body.instructions.begin();
197 while(!queue.empty())
215 std::cout <<
"sequence feasible\n";
220 if(e.
pc==e.
f->second.body.instructions.end())
232 else if(e.
pc->is_function_call())
235 if(
function.
id()==ID_symbol)
243 goto_functionst::function_mapt::const_iterator f_call_it=
254 e.
pc=f_call_it->second.body.instructions.begin();
262 else if(e.pc->is_goto())
266 if(e.pc->guard.is_true())
281 std::cout <<
"sequence not feasible\n";
288 std::vector<irep_idt> sequence;
291 while(std::getline(std::cin, line))
293 if(line!=
"" && line[line.size()-1]==
'\r')
294 line.resize(line.size()-1);
297 sequence.push_back(line);
310 if(!i_it->is_function_call())
317 if(f.
id()!=ID_symbol)
321 if(identifier==
"__CPROVER_initialize")
324 std::string name=
from_expr(ns, identifier, f);
326 if(java_type_suffix!=std::string::npos)
327 name.erase(java_type_suffix);
329 std::cout <<
"found call to " << name;
333 std::cout <<
" with arguments ";
334 for(exprt::operandst::const_iterator
exprt simplify_expr(const exprt &src, const namespacet &ns)
check_call_sequencet(const goto_functionst &_goto_functions, const std::vector< irep_idt > &_sequence)
instructionst instructions
The list of instructions in the goto program.
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)
void check_call_sequence(const goto_functionst &goto_functions)
unsignedbv_typet size_type()
Memory-mapped I/O Instrumentation for Goto Programs.
const std::vector< irep_idt > & sequence
std::list< Target > get_successors(Target target) const
bool operator==(const statet &other) const
goto_programt::const_targett return_address
const irep_idt & id() const
instructionst::const_iterator const_targett
goto_programt::const_targett pc
API to expression classes.
bool operator==(const call_stack_entryt &other) const
std::size_t operator()(const statet &s) const
std::unordered_set< statet, state_hash > statest
goto_functionst::function_mapt::const_iterator f
function_mapt function_map
void show_call_sequences(const irep_idt &function, const goto_programt &goto_program, const goto_programt::const_targett start)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
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
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
std::vector< call_stack_entryt > call_stack
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
const irept & find(const irep_namet &name) const
const code_function_callt & to_code_function_call(const codet &code)