37 std::optional<unsigned> thread_nr;
41 if(
c_pos != std::string::npos)
45 val.erase(0,
nr.size() + 1);
70 "invalid loop identifier " + id,
"unwindset"};
79 "invalid loop identifier " + id,
"unwindset"};
85 log.warning() <<
"loop identifier " <<
id
86 <<
" for non-existent function provided with unwindset"
99 "invalid loop identifier " + id,
"unwindset"};
102 bool found = std::any_of(
106 return instruction.is_backwards_goto() &&
107 instruction.loop_number == nr;
112 log.warning() <<
"loop identifier " <<
id
113 <<
" provided with unwindset does not match any loop"
120 std::optional<unsigned>
nr;
121 std::optional<source_locationt> location;
126 instruction.labels.begin(),
127 instruction.labels.end(),
130 location = instruction.source_location();
136 location.has_value() && instruction.is_backwards_goto() &&
137 instruction.source_location() == *location)
143 <<
"loop identifier " <<
id
146 nr = instruction.loop_number;
152 log.warning() <<
"loop identifier " <<
id
153 <<
" provided with unwindset does not match any loop"
158 id = function_id +
"." + std::to_string(*
nr);
165 std::optional<unsigned>
uw(0);
172 if(thread_nr.has_value())
184 const std::list<std::string> &unwindset,
188 for(
auto &element : unwindset)
192std::optional<unsigned>
199 thread_loop_map.find(std::pair<irep_idt, unsigned>(loop_id, thread_nr));
202 return tl_it->second;
215 const std::string &file_name,
222 throw "cannot open file " + file_name;
224 std::stringstream buffer;
225 buffer << file.rdbuf();
Abstract interface to eager or lazy GOTO models.
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.
std::optional< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
void parse_unwindset_one_loop(std::string loop_limit, abstract_goto_modelt &goto_model, message_handlert &message_handler)
void parse_unwind(const std::string &unwind)
void parse_unwindset(const std::list< std::string > &unwindset, abstract_goto_modelt &goto_model, message_handlert &message_handler)
void parse_unwindset_file(const std::string &file_name, abstract_goto_modelt &goto_model, message_handlert &message_handler)
std::optional< unsigned > global_limit
thread_loop_mapt thread_loop_map
unsigned unsafe_string2unsigned(const std::string &str, int base)
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...
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
#define widen_if_needed(s)