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()!=
"")
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());
112 if(!it->second.is_inlined())
115 if(!property_set.empty())
117 "property " +
id2string(*property_set.begin()) +
" unknown",
123 std::map<irep_idt, std::size_t> property_counters;
125 for(goto_functionst::function_mapt::iterator
140 for(goto_functionst::function_mapt::iterator
147 for(goto_programt::instructionst::iterator
152 if(!i_it->is_assert())
const std::string & id2string(const irep_idt &d)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void make_assertions_false(goto_modelt &goto_model)
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
function_mapt function_map
Set the properties to check.
instructionst instructions
The list of instructions in the goto program.
A collection of goto functions.
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
The Boolean constant false.
A generic container class for the GOTO intermediate representation of one function.
#define Forall_goto_functions(it, functions)
void label_properties(goto_modelt &goto_model)
goto_functionst goto_functions
GOTO functions.