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 
18  goto_programt &goto_program,
19  std::unordered_set<irep_idt, irep_id_hash> &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, irep_id_hash>::iterator
32  c_it=property_set.find(property_id);
33 
34  if(c_it==property_set.end())
35  it->type=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 
47  goto_programt &goto_program,
48  std::map<irep_idt, unsigned> &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  unsigned &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 
88 void label_properties(goto_programt &goto_program)
89 {
90  std::map<irep_idt, unsigned> 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, irep_id_hash> 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, unsigned> 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  if(!it->second.is_inlined())
126  label_properties(it->second.body, property_counters);
127 }
128 
130 {
132 }
133 
135  goto_functionst &goto_functions)
136 {
137  for(goto_functionst::function_mapt::iterator
138  f_it=goto_functions.function_map.begin();
139  f_it!=goto_functions.function_map.end();
140  f_it++)
141  {
142  goto_programt &goto_program=f_it->second.body;
143 
144  for(goto_programt::instructionst::iterator
145  i_it=goto_program.instructions.begin();
146  i_it!=goto_program.instructions.end();
147  i_it++)
148  {
149  if(!i_it->is_assert())
150  continue;
151  i_it->guard=false_exprt();
152  }
153  }
154 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
instructionst instructions
The list of instructions in the goto program.
void make_assertions_false(goto_modelt &goto_model)
Set the properties to check.
The boolean constant false.
Definition: std_expr.h:3753
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
#define Forall_goto_functions(it, functions)
void label_properties(goto_modelt &goto_model)
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt, irep_id_hash > &property_set)
goto_functionst goto_functions
Definition: goto_model.h:26