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 <algorithm>
15 #include <unordered_set>
16 
19  std::unordered_set<irep_idt> &property_set)
20 {
21  for(goto_programt::instructionst::iterator
22  it=goto_program.instructions.begin();
23  it!=goto_program.instructions.end();
24  it++)
25  {
26  if(!it->is_assert())
27  continue;
28 
29  irep_idt property_id=it->source_location.get_property_id();
30 
31  std::unordered_set<irep_idt>::iterator c_it =
32  property_set.find(property_id);
33 
34  if(c_it==property_set.end())
35  it->make_skip();
36  else
37  property_set.erase(c_it);
38  }
39 }
40 
41 void label_properties(goto_modelt &goto_model)
42 {
43  label_properties(goto_model.goto_functions);
44 }
45 
48  std::map<irep_idt, std::size_t> &property_counters)
49 {
50  for(goto_programt::instructionst::iterator
51  it=goto_program.instructions.begin();
52  it!=goto_program.instructions.end();
53  it++)
54  {
55  if(!it->is_assert())
56  continue;
57 
58  irep_idt function=it->source_location.get_function();
59 
60  std::string prefix=id2string(function);
61  if(it->source_location.get_property_class()!="")
62  {
63  if(prefix!="")
64  prefix+=".";
65 
66  std::string class_infix=
67  id2string(it->source_location.get_property_class());
68 
69  // replace the spaces by underscores
70  std::replace(class_infix.begin(), class_infix.end(), ' ', '_');
71 
72  prefix+=class_infix;
73  }
74 
75  if(prefix!="")
76  prefix+=".";
77 
78  std::size_t &count=property_counters[prefix];
79 
80  count++;
81 
82  std::string property_id=prefix+std::to_string(count);
83 
84  it->source_location.set_property_id(property_id);
85  }
86 }
87 
89 {
90  std::map<irep_idt, std::size_t> property_counters;
91  label_properties(goto_program, property_counters);
92 }
93 
95  goto_modelt &goto_model,
96  const std::list<std::string> &properties)
97 {
98  set_properties(goto_model.goto_functions, properties);
99 }
100 
102  goto_functionst &goto_functions,
103  const std::list<std::string> &properties)
104 {
105  std::unordered_set<irep_idt> property_set;
106 
107  property_set.insert(properties.begin(), properties.end());
108 
109  Forall_goto_functions(it, goto_functions)
110  if(!it->second.is_inlined())
111  set_properties(it->second.body, property_set);
112 
113  if(!property_set.empty())
114  throw "property "+id2string(*property_set.begin())+" not found";
115 }
116 
117 void label_properties(goto_functionst &goto_functions)
118 {
119  std::map<irep_idt, std::size_t> property_counters;
120 
121  for(goto_functionst::function_mapt::iterator
122  it=goto_functions.function_map.begin();
123  it!=goto_functions.function_map.end();
124  it++)
125  label_properties(it->second.body, property_counters);
126 }
127 
129 {
131 }
132 
134  goto_functionst &goto_functions)
135 {
136  for(goto_functionst::function_mapt::iterator
137  f_it=goto_functions.function_map.begin();
138  f_it!=goto_functions.function_map.end();
139  f_it++)
140  {
141  goto_programt &goto_program=f_it->second.body;
142 
143  for(goto_programt::instructionst::iterator
144  i_it=goto_program.instructions.begin();
145  i_it!=goto_program.instructions.end();
146  i_it++)
147  {
148  if(!i_it->is_assert())
149  continue;
150  i_it->guard=false_exprt();
151  }
152  }
153 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
void make_assertions_false(goto_modelt &goto_model)
function_mapt function_map
Set the properties to check.
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
The boolean constant false.
Definition: std_expr.h:4499
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define Forall_goto_functions(it, functions)
goto_programt & goto_program
Definition: cover.cpp:63
void label_properties(goto_modelt &goto_model)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32