19 #include <unordered_set>
23 std::unordered_set<irep_idt> &property_set)
25 for(goto_programt::instructionst::iterator
33 irep_idt property_id=it->source_location.get_property_id();
35 std::unordered_set<irep_idt>::iterator c_it =
36 property_set.find(property_id);
38 if(c_it==property_set.end())
41 property_set.erase(c_it);
52 std::map<irep_idt, std::size_t> &property_counters)
54 for(goto_programt::instructionst::iterator
62 irep_idt function=it->source_location.get_function();
65 if(!it->source_location.get_property_class().empty())
70 std::string class_infix=
71 id2string(it->source_location.get_property_class());
74 std::replace(class_infix.begin(), class_infix.end(),
' ',
'_');
82 std::size_t &count=property_counters[prefix];
88 it->source_location.set_property_id(property_id);
94 std::map<irep_idt, std::size_t> property_counters;
100 const std::list<std::string> &properties)
107 const std::list<std::string> &properties)
109 std::unordered_set<irep_idt> property_set;
111 property_set.insert(properties.begin(), properties.end());
116 if(!property_set.empty())
118 "property " +
id2string(*property_set.begin()) +
" unknown",
124 std::map<irep_idt, std::size_t> property_counters;
126 for(goto_functionst::function_mapt::iterator
143 for(
auto &i : f.second.body.instructions)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
The Boolean constant false.
A collection of goto functions.
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
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 std::string & id2string(const irep_idt &d)
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
void make_assertions_false(goto_modelt &goto_model)
void label_properties(goto_modelt &goto_model)
Set the properties to check.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.