15 #include <unordered_set> 19 std::unordered_set<irep_idt, irep_id_hash> &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, irep_id_hash>::iterator
32 c_it=property_set.find(property_id);
34 if(c_it==property_set.end())
37 property_set.erase(c_it);
48 std::map<irep_idt, unsigned> &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 unsigned &count=property_counters[prefix];
82 std::string property_id=prefix+std::to_string(count);
84 it->source_location.set_property_id(property_id);
90 std::map<irep_idt, unsigned> property_counters;
96 const std::list<std::string> &properties)
103 const std::list<std::string> &properties)
105 std::unordered_set<irep_idt, irep_id_hash> 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, unsigned> property_counters;
121 for(goto_functionst::function_mapt::iterator
125 if(!it->second.is_inlined())
137 for(goto_functionst::function_mapt::iterator
144 for(goto_programt::instructionst::iterator
149 if(!i_it->is_assert())
const std::string & id2string(const irep_idt &d)
instructionst instructions
The list of instructions in the goto program.
void make_assertions_false(goto_modelt &goto_model)
Set the properties to check.
function_mapt function_map
The boolean constant false.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
#define Forall_goto_functions(it, functions)
void label_properties(goto_modelt &goto_model)
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt, irep_id_hash > &property_set)
goto_functionst goto_functions