37#pragma GCC diagnostic push
39# pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
42#pragma GCC diagnostic pop
46 if(
c_pos != std::string::npos)
50 val.erase(0,
nr.size() + 1);
75 "invalid loop identifier " + id,
"unwindset"};
84 "invalid loop identifier " + id,
"unwindset"};
90 log.warning() <<
"loop identifier " <<
id
91 <<
" for non-existent function provided with unwindset"
104 "invalid loop identifier " + id,
"unwindset"};
107 bool found = std::any_of(
111 return instruction.is_backwards_goto() &&
112 instruction.loop_number == nr;
117 log.warning() <<
"loop identifier " <<
id
118 <<
" provided with unwindset does not match any loop"
131 instruction.labels.begin(),
132 instruction.labels.end(),
135 location = instruction.source_location();
141 location.has_value() && instruction.is_backwards_goto() &&
142 instruction.source_location() == *location)
148 <<
"loop identifier " <<
id
151 nr = instruction.loop_number;
157 log.warning() <<
"loop identifier " <<
id
158 <<
" provided with unwindset does not match any loop"
164#pragma GCC diagnostic push
166# pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
168 id = function_id +
"." + std::to_string(*
nr);
169#pragma GCC diagnostic pop
183 if(thread_nr.has_value())
186#pragma GCC diagnostic push
188# pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
191#pragma GCC diagnostic pop
201 const std::list<std::string> &unwindset,
204 for(
auto &element : unwindset)
215 thread_loop_map.find(std::pair<irep_idt, unsigned>(loop_id, thread_nr));
218 return tl_it->second;
231 const std::string &file_name,
237 throw "cannot open file "+file_name;
239 std::stringstream buffer;
240 buffer <<
file.rdbuf();
Abstract interface to eager or lazy GOTO models.
virtual bool can_produce_function(const irep_idt &id) const =0
Determines if this model can produce a body for the given function.
virtual const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id)=0
Get a GOTO function by name, or throw if no such function exists.
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
This class represents an instruction in the GOTO intermediate representation.
instructionst instructions
The list of instructions in the goto program.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Class that provides messages with a built-in verbosity 'level'.
The symbol table base class interface.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
void parse_unwindset_one_loop(std::string loop_limit, message_handlert &message_handler)
void parse_unwind(const std::string &unwind)
optionalt< unsigned > global_limit
thread_loop_mapt thread_loop_map
void parse_unwindset_file(const std::string &file_name, message_handlert &message_handler)
abstract_goto_modelt & goto_model
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
void parse_unwindset(const std::list< std::string > &unwindset, message_handlert &message_handler)
optionalt< unsigned > string2optional_unsigned(const std::string &str, int base)
Convert string to unsigned similar to the stoul or stoull functions, return nullopt when the conversi...
unsigned unsafe_string2unsigned(const std::string &str, int base)
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
#define widen_if_needed(s)