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 <algorithm>
17 #include <unordered_set>
18 
20  goto_programt &goto_program,
21  std::unordered_set<irep_idt> &property_set)
22 {
23  for(goto_programt::instructionst::iterator
24  it=goto_program.instructions.begin();
25  it!=goto_program.instructions.end();
26  it++)
27  {
28  if(!it->is_assert())
29  continue;
30 
31  irep_idt property_id=it->source_location.get_property_id();
32 
33  std::unordered_set<irep_idt>::iterator c_it =
34  property_set.find(property_id);
35 
36  if(c_it==property_set.end())
37  it->turn_into_skip();
38  else
39  property_set.erase(c_it);
40  }
41 }
42 
43 void label_properties(goto_modelt &goto_model)
44 {
45  label_properties(goto_model.goto_functions);
46 }
47 
49  goto_programt &goto_program,
50  std::map<irep_idt, std::size_t> &property_counters)
51 {
52  for(goto_programt::instructionst::iterator
53  it=goto_program.instructions.begin();
54  it!=goto_program.instructions.end();
55  it++)
56  {
57  if(!it->is_assert())
58  continue;
59 
60  irep_idt function=it->source_location.get_function();
61 
62  std::string prefix=id2string(function);
63  if(!it->source_location.get_property_class().empty())
64  {
65  if(!prefix.empty())
66  prefix+=".";
67 
68  std::string class_infix=
69  id2string(it->source_location.get_property_class());
70 
71  // replace the spaces by underscores
72  std::replace(class_infix.begin(), class_infix.end(), ' ', '_');
73 
74  prefix+=class_infix;
75  }
76 
77  if(!prefix.empty())
78  prefix+=".";
79 
80  std::size_t &count=property_counters[prefix];
81 
82  count++;
83 
84  std::string property_id=prefix+std::to_string(count);
85 
86  it->source_location.set_property_id(property_id);
87  }
88 }
89 
90 void label_properties(goto_programt &goto_program)
91 {
92  std::map<irep_idt, std::size_t> property_counters;
93  label_properties(goto_program, property_counters);
94 }
95 
97  goto_modelt &goto_model,
98  const std::list<std::string> &properties)
99 {
100  set_properties(goto_model.goto_functions, properties);
101 }
102 
104  goto_functionst &goto_functions,
105  const std::list<std::string> &properties)
106 {
107  std::unordered_set<irep_idt> property_set;
108 
109  property_set.insert(properties.begin(), properties.end());
110 
111  for(auto &gf_entry : goto_functions.function_map)
112  set_properties(gf_entry.second.body, property_set);
113 
114  if(!property_set.empty())
116  "property " + id2string(*property_set.begin()) + " unknown",
117  "--property id");
118 }
119 
120 void label_properties(goto_functionst &goto_functions)
121 {
122  std::map<irep_idt, std::size_t> property_counters;
123 
124  for(goto_functionst::function_mapt::iterator
125  it=goto_functions.function_map.begin();
126  it!=goto_functions.function_map.end();
127  it++)
128  label_properties(it->second.body, property_counters);
129 }
130 
132 {
134 }
135 
137  goto_functionst &goto_functions)
138 {
139  for(auto &f : goto_functions.function_map)
140  {
141  for(auto &i : f.second.body.instructions)
142  {
143  if(i.is_assert())
144  i.set_condition(false_exprt());
145  }
146  }
147 }
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:2726
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:74
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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.