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())
50 const exprt &callee = t->call_function();
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())
202 const exprt &
function = e.
pc->call_function();
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->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);
275 for(
const auto &instruction : goto_program.
instructions)
277 if(!instruction.is_function_call())
280 const exprt &f = instruction.call_function();
282 if(f.
id()!=ID_symbol)
289 std::string name=
from_expr(ns, identifier, f);
291 if(java_type_suffix!=std::string::npos)
292 name.erase(java_type_suffix);
294 std::cout <<
"found call to " << name;
296 if(!instruction.call_arguments().empty())
298 std::cout <<
" with arguments ";
299 for(exprt::operandst::const_iterator it =
300 instruction.call_arguments().begin();
301 it != instruction.call_arguments().end();
304 if(it != instruction.call_arguments().begin())