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.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
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.