17 #include <unordered_set>
21 std::unordered_set<irep_idt> &property_set)
23 for(goto_programt::instructionst::iterator
31 irep_idt property_id=it->source_location.get_property_id();
33 std::unordered_set<irep_idt>::iterator c_it =
34 property_set.find(property_id);
36 if(c_it==property_set.end())
39 property_set.erase(c_it);
50 std::map<irep_idt, std::size_t> &property_counters)
52 for(goto_programt::instructionst::iterator
60 irep_idt function=it->source_location.get_function();
63 if(!it->source_location.get_property_class().empty())
68 std::string class_infix=
69 id2string(it->source_location.get_property_class());
72 std::replace(class_infix.begin(), class_infix.end(),
' ',
'_');
80 std::size_t &count=property_counters[prefix];
86 it->source_location.set_property_id(property_id);
92 std::map<irep_idt, std::size_t> property_counters;
98 const std::list<std::string> &properties)
105 const std::list<std::string> &properties)
107 std::unordered_set<irep_idt> property_set;
109 property_set.insert(properties.begin(), properties.end());
114 if(!property_set.empty())
116 "property " +
id2string(*property_set.begin()) +
" unknown",
122 std::map<irep_idt, std::size_t> property_counters;
124 for(goto_functionst::function_mapt::iterator
141 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.