33 std::cout <<
"# " << caller <<
'\n';
34 std::stack<goto_programt::const_targett> stack;
35 std::set<goto_programt::const_targett, goto_programt::target_less_than> 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())
static void list_calls_and_arguments(const namespacet &ns, const goto_programt &goto_program)
void check_call_sequence(const goto_modelt &goto_model)
void show_call_sequences(const irep_idt &caller, const goto_programt &goto_program)
Memory-mapped I/O Instrumentation for Goto Programs.
check_call_sequencet(const goto_modelt &_goto_model, const std::vector< irep_idt > &_sequence)
std::unordered_set< statet, state_hash > statest
const std::vector< irep_idt > & sequence
const goto_functionst & goto_functions
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const irep_idt & get_identifier() const
size_t hash_string(const dstringt &s)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
exprt simplify_expr(exprt src, const namespacet &ns)
#define INITIALIZE_FUNCTION
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
goto_functionst::function_mapt::const_iterator f
goto_programt::const_targett return_address
bool operator==(const call_stack_entryt &other) const
std::size_t operator()(const statet &s) const
goto_functionst::function_mapt::const_iterator f
goto_programt::const_targett pc
bool operator==(const statet &other) const
std::vector< call_stack_entryt > call_stack