cprover
set_properties.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Set Properties
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "set_properties.h"
13 
14 #include <util/exception_utils.h>
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 
45 void label_properties(goto_modelt &goto_model)
46 {
47  label_properties(goto_model.goto_functions);
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 
92 void label_properties(goto_programt &goto_program)
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 
122 void label_properties(goto_functionst &goto_functions)
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.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.