15 #include <unordered_set> 19 std::unordered_set<irep_idt> &property_set)
21 for(goto_programt::instructionst::iterator
29 irep_idt property_id=it->source_location.get_property_id();
31 std::unordered_set<irep_idt>::iterator c_it =
32 property_set.find(property_id);
34 if(c_it==property_set.end())
37 property_set.erase(c_it);
48 std::map<irep_idt, std::size_t> &property_counters)
50 for(goto_programt::instructionst::iterator
58 irep_idt function=it->source_location.get_function();
61 if(it->source_location.get_property_class()!=
"")
66 std::string class_infix=
67 id2string(it->source_location.get_property_class());
70 std::replace(class_infix.begin(), class_infix.end(),
' ',
'_');
78 std::size_t &count=property_counters[prefix];
84 it->source_location.set_property_id(property_id);
90 std::map<irep_idt, std::size_t> property_counters;
96 const std::list<std::string> &properties)
103 const std::list<std::string> &properties)
105 std::unordered_set<irep_idt> property_set;
107 property_set.insert(properties.begin(), properties.end());
110 if(!it->second.is_inlined())
113 if(!property_set.empty())
114 throw "property "+
id2string(*property_set.begin())+
" not found";
119 std::map<irep_idt, std::size_t> property_counters;
121 for(goto_functionst::function_mapt::iterator
136 for(goto_functionst::function_mapt::iterator
143 for(goto_programt::instructionst::iterator
148 if(!i_it->is_assert())
const std::string & id2string(const irep_idt &d)
void make_assertions_false(goto_modelt &goto_model)
function_mapt function_map
Set the properties to check.
instructionst instructions
The list of instructions in the goto program.
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
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.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define Forall_goto_functions(it, functions)
goto_programt & goto_program
void label_properties(goto_modelt &goto_model)
goto_functionst goto_functions
GOTO functions.