39 if(
c_pos != std::string::npos)
43 val.erase(0,
nr.size() + 1);
68 "invalid loop identifier " + id,
"unwindset"};
77 "invalid loop identifier " + id,
"unwindset"};
83 log.warning() <<
"loop identifier " <<
id
84 <<
" for non-existent function provided with unwindset"
97 "invalid loop identifier " + id,
"unwindset"};
100 bool found = std::any_of(
104 return instruction.is_backwards_goto() &&
105 instruction.loop_number == nr;
110 log.warning() <<
"loop identifier " <<
id
111 <<
" provided with unwindset does not match any loop"
124 instruction.labels.begin(),
125 instruction.labels.end(),
128 location = instruction.source_location();
131 location.has_value() && instruction.is_backwards_goto() &&
132 instruction.source_location() == *location)
134 nr = instruction.loop_number;
141 log.warning() <<
"loop identifier " <<
id
142 <<
" provided with unwindset does not match any loop"
147 id = function_id +
"." + std::to_string(*
nr);
161 if(thread_nr.has_value())
169 const std::list<std::string> &unwindset,
172 for(
auto &element : unwindset)
189 thread_loop_map.find(std::pair<irep_idt, unsigned>(loop_id, thread_nr));
192 return tl_it->second;
205 const std::string &file_name,
211 std::ifstream
file(file_name);
215 throw "cannot open file "+file_name;
217 std::stringstream buffer;
218 buffer <<
file.rdbuf();
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'.
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)
std::wstring widen(const char *s)