37#pragma GCC diagnostic push
39# pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
42#pragma GCC diagnostic pop
45 auto c_pos = val.find(
':');
46 if(c_pos != std::string::npos)
48 std::string nr = val.substr(0, c_pos);
50 val.erase(0, nr.size() + 1);
54 auto last_c_pos = val.rfind(
':');
55 if(last_c_pos != std::string::npos)
57 std::string
id = val.substr(0, last_c_pos);
65 if(maybe_fn && maybe_fn->
type.
id() == ID_code)
71 auto last_dot_pos = val.rfind(
'.');
72 if(last_dot_pos == std::string::npos)
75 "invalid loop identifier " + id,
"unwindset"};
78 std::string function_id =
id.substr(0, last_dot_pos);
79 std::string loop_nr_label =
id.substr(last_dot_pos + 1);
81 if(loop_nr_label.empty())
84 "invalid loop identifier " + id,
"unwindset"};
90 log.warning() <<
"loop identifier " <<
id
91 <<
" for non-existent function provided with unwindset"
98 if(isdigit(loop_nr_label[0]))
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(),
133 loop_nr_label) != instruction.labels.end())
135 location = instruction.source_location();
138 location->remove(ID_hide);
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
173 std::string uw_string = val.substr(last_c_pos + 1);
178 if(uw_string.empty())
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();
242 std::vector<std::string> unwindset_elements =
245 for(
auto &element : unwindset_elements)
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.
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 ...
const irep_idt & id() const
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.
typet type
Type of symbol.
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)
nonstd::optional< T > optionalt
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)