36 std::optional<unsigned> thread_nr;
39 auto c_pos = val.find(
':');
40 if(c_pos != std::string::npos)
42 std::string nr = val.substr(0, c_pos);
44 val.erase(0, nr.size() + 1);
48 auto last_c_pos = val.rfind(
':');
49 if(last_c_pos != std::string::npos)
51 std::string
id = val.substr(0, last_c_pos);
59 if(maybe_fn && maybe_fn->
type.
id() == ID_code)
65 auto last_dot_pos = val.rfind(
'.');
66 if(last_dot_pos == std::string::npos)
69 "invalid loop identifier " + id,
"unwindset"};
72 std::string function_id =
id.substr(0, last_dot_pos);
73 std::string loop_nr_label =
id.substr(last_dot_pos + 1);
75 if(loop_nr_label.empty())
78 "invalid loop identifier " + id,
"unwindset"};
84 log.warning() <<
"loop identifier " <<
id
85 <<
" for non-existent function provided with unwindset"
98 "invalid loop identifier " + id,
"unwindset"};
101 bool found = std::any_of(
105 return instruction.is_backwards_goto() &&
106 instruction.loop_number == nr;
111 log.warning() <<
"loop identifier " <<
id
112 <<
" provided with unwindset does not match any loop"
119 std::optional<unsigned> nr;
120 std::optional<source_locationt> location;
125 instruction.labels.begin(),
126 instruction.labels.end(),
127 loop_nr_label) != instruction.labels.end())
129 location = instruction.source_location();
132 location->remove(ID_hide);
135 location.has_value() && instruction.is_backwards_goto() &&
136 instruction.source_location() == *location)
142 <<
"loop identifier " <<
id
145 nr = instruction.loop_number;
151 log.warning() <<
"loop identifier " <<
id
152 <<
" provided with unwindset does not match any loop"
161 std::string uw_string = val.substr(last_c_pos + 1);
164 std::optional<unsigned> uw(0);
166 if(uw_string.empty())
171 if(thread_nr.has_value())
183 const std::list<std::string> &unwindset,
186 for(
auto &element : unwindset)
190 std::optional<unsigned>
197 thread_loop_map.find(std::pair<irep_idt, unsigned>(loop_id, thread_nr));
200 return tl_it->second;
213 const std::string &file_name,
219 throw "cannot open file "+file_name;
221 std::stringstream buffer;
222 buffer << file.rdbuf();
224 std::vector<std::string> unwindset_elements =
227 for(
auto &element : unwindset_elements)
Abstract interface to eager or lazy GOTO models.
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 bool can_produce_function(const irep_idt &id) const =0
Determines if this model can produce a body for the given function.
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.
std::optional< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
void parse_unwindset_one_loop(std::string loop_limit, message_handlert &message_handler)
void parse_unwind(const std::string &unwind)
std::optional< 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
void parse_unwindset(const std::list< std::string > &unwindset, message_handlert &message_handler)
std::optional< 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)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
#define widen_if_needed(s)