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.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 }
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:69
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
label_properties
void label_properties(goto_modelt &goto_model)
Definition: set_properties.cpp:45
set_properties.h
Set the properties to check.
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
false_exprt
The Boolean constant false.
Definition: std_expr.h:2811
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
make_assertions_false
void make_assertions_false(goto_modelt &goto_model)
Definition: set_properties.cpp:133
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
set_properties
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
Definition: set_properties.cpp:21