cprover
Loading...
Searching...
No Matches
set_properties.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Set Properties
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "set_properties.h"
13
15
16#include "goto_model.h"
17
18#include <algorithm>
19#include <unordered_set>
20
22 goto_programt &goto_program,
23 std::unordered_set<irep_idt> &property_set)
24{
25 for(goto_programt::instructionst::iterator
26 it=goto_program.instructions.begin();
27 it!=goto_program.instructions.end();
28 it++)
29 {
30 if(!it->is_assert())
31 continue;
32
33 irep_idt property_id = it->source_location().get_property_id();
34
35 std::unordered_set<irep_idt>::iterator c_it =
36 property_set.find(property_id);
37
38 if(c_it==property_set.end())
39 it->turn_into_skip();
40 else
41 property_set.erase(c_it);
42 }
43}
44
46{
48}
49
51 goto_programt &goto_program,
52 std::map<irep_idt, std::size_t> &property_counters)
53{
54 for(goto_programt::instructionst::iterator
55 it=goto_program.instructions.begin();
56 it!=goto_program.instructions.end();
57 it++)
58 {
59 if(!it->is_assert())
60 continue;
61
62 irep_idt function = it->source_location().get_function();
63
64 std::string prefix=id2string(function);
65 if(!it->source_location().get_property_class().empty())
66 {
67 if(!prefix.empty())
68 prefix+=".";
69
70 std::string class_infix =
71 id2string(it->source_location().get_property_class());
72
73 // replace the spaces by underscores
74 std::replace(class_infix.begin(), class_infix.end(), ' ', '_');
75
76 prefix+=class_infix;
77 }
78
79 if(!prefix.empty())
80 prefix+=".";
81
82 std::size_t &count=property_counters[prefix];
83
84 count++;
85
86 std::string property_id=prefix+std::to_string(count);
87
88 it->source_location_nonconst().set_property_id(property_id);
89 }
90}
91
93{
94 std::map<irep_idt, std::size_t> property_counters;
95 label_properties(goto_program, property_counters);
96}
97
99 goto_modelt &goto_model,
100 const std::list<std::string> &properties)
101{
102 set_properties(goto_model.goto_functions, properties);
103}
104
106 goto_functionst &goto_functions,
107 const std::list<std::string> &properties)
108{
109 std::unordered_set<irep_idt> property_set;
110
111 property_set.insert(properties.begin(), properties.end());
112
113 for(auto &gf_entry : goto_functions.function_map)
114 set_properties(gf_entry.second.body, property_set);
115
116 if(!property_set.empty())
118 "property " + id2string(*property_set.begin()) + " unknown",
119 "--property id");
120}
121
123{
124 std::map<irep_idt, std::size_t> property_counters;
125
126 for(goto_functionst::function_mapt::iterator
127 it=goto_functions.function_map.begin();
128 it!=goto_functions.function_map.end();
129 it++)
130 label_properties(it->second.body, property_counters);
131}
132
134{
136}
137
139 goto_functionst &goto_functions)
140{
141 for(auto &f : goto_functions.function_map)
142 {
143 for(auto &i : f.second.body.instructions)
144 {
145 if(i.is_assert())
146 i.set_condition(false_exprt());
147 }
148 }
149}
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
The Boolean constant false.
Definition std_expr.h:2865
A collection of goto functions.
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
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 ...
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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.