Go to the documentation of this file.
29 loop_idst::const_iterator l_it=loop_ids.begin();
32 if(l_it==loop_ids.end())
34 if(!it->is_backwards_goto())
37 const unsigned loop_id=it->loop_number;
54 if(l_it!=loop_ids.end())
56 message.error() <<
"Loop " << *l_it <<
" not found"
65 const std::string &loop_ids,
73 std::string val=loop_ids.substr(idx, next-idx);
76 if(delim==std::string::npos)
79 std::string fn=val.substr(0, delim);
82 loop_map[fn].insert(nr);
84 if(next==std::string::npos)
94 const std::string &loop_ids,
106 loop_mapt::const_iterator it=loop_map.begin();
109 if(it==loop_map.end() || it->first<f_it->first)
111 else if(it->first==f_it->first)
118 if(it!=loop_map.end())
120 message.error() <<
"No function " << it->first <<
" in goto program"
Class that provides messages with a built-in verbosity 'level'.
#define Forall_goto_program_instructions(it, program)
static bool parse_loop_ids(const std::string &loop_ids, loop_mapt &loop_map)
std::map< irep_idt, loop_idst > loop_mapt
Skip over selected loops by adding gotos.
const irept & find(const irep_namet &name) const
static bool skip_loops(goto_programt &goto_program, const loop_idst &loop_ids, messaget &message)
std::set< unsigned > loop_idst
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
unsigned safe_string2unsigned(const std::string &str, int base)
#define Forall_goto_functions(it, functions)
instructionst instructions
The list of instructions in the goto program.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
unsignedbv_typet size_type()
The Boolean constant true.
const source_locationt & source_location() const
instructionst::iterator targett