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->make_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()!="")
64  {
65  if(prefix!="")
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!="")
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  Forall_goto_functions(it, goto_functions)
112  if(!it->second.is_inlined())
113  set_properties(it->second.body, property_set);
114 
115  if(!property_set.empty())
117  "property " + id2string(*property_set.begin()) + " unknown",
118  "--property id");
119 }
120 
121 void label_properties(goto_functionst &goto_functions)
122 {
123  std::map<irep_idt, std::size_t> property_counters;
124 
125  for(goto_functionst::function_mapt::iterator
126  it=goto_functions.function_map.begin();
127  it!=goto_functions.function_map.end();
128  it++)
129  label_properties(it->second.body, property_counters);
130 }
131 
133 {
135 }
136 
138  goto_functionst &goto_functions)
139 {
140  for(goto_functionst::function_mapt::iterator
141  f_it=goto_functions.function_map.begin();
142  f_it!=goto_functions.function_map.end();
143  f_it++)
144  {
145  goto_programt &goto_program=f_it->second.body;
146 
147  for(goto_programt::instructionst::iterator
148  i_it=goto_program.instructions.begin();
149  i_it!=goto_program.instructions.end();
150  i_it++)
151  {
152  if(!i_it->is_assert())
153  continue;
154  i_it->guard=false_exprt();
155  }
156  }
157 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void make_assertions_false(goto_modelt &goto_model)
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
function_mapt function_map
Set the properties to check.
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
A collection of goto functions.
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
The Boolean constant false.
Definition: std_expr.h:4452
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
#define Forall_goto_functions(it, functions)
void label_properties(goto_modelt &goto_model)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32