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  Forall_goto_functions(it, goto_functions)
112  set_properties(it->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 }
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:67
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:55
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
label_properties
void label_properties(goto_modelt &goto_model)
Definition: set_properties.cpp:43
set_properties.h
Set the properties to check.
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
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:131
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
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:19