CBMC
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  const irep_idt function_identifier,
52  goto_programt &goto_program,
53  std::map<irep_idt, std::size_t> &property_counters)
54 {
55  for(goto_programt::instructionst::iterator
56  it=goto_program.instructions.begin();
57  it!=goto_program.instructions.end();
58  it++)
59  {
60  if(!it->is_assert())
61  continue;
62 
63  // No source location? Create one.
64  if(it->source_location().is_nil())
65  {
66  it->source_location_nonconst() = source_locationt{};
67  it->source_location_nonconst().set_function(function_identifier);
68  }
69 
70  irep_idt function = it->source_location().get_function();
71 
72  std::string prefix=id2string(function);
73  if(!it->source_location().get_property_class().empty())
74  {
75  if(!prefix.empty())
76  prefix+=".";
77 
78  std::string class_infix =
79  id2string(it->source_location().get_property_class());
80 
81  // replace the spaces by underscores
82  std::replace(class_infix.begin(), class_infix.end(), ' ', '_');
83 
84  prefix+=class_infix;
85  }
86 
87  if(!prefix.empty())
88  prefix+=".";
89 
90  std::size_t &count=property_counters[prefix];
91 
92  count++;
93 
94  std::string property_id=prefix+std::to_string(count);
95 
96  it->source_location_nonconst().set_property_id(property_id);
97  }
98 }
99 
100 void label_properties(irep_idt function_identifier, goto_programt &goto_program)
101 {
102  std::map<irep_idt, std::size_t> property_counters;
103  label_properties(function_identifier, goto_program, property_counters);
104 }
105 
107  goto_modelt &goto_model,
108  const std::list<std::string> &properties)
109 {
110  set_properties(goto_model.goto_functions, properties);
111 }
112 
114  goto_functionst &goto_functions,
115  const std::list<std::string> &properties)
116 {
117  std::unordered_set<irep_idt> property_set;
118 
119  property_set.insert(properties.begin(), properties.end());
120 
121  for(auto &gf_entry : goto_functions.function_map)
122  set_properties(gf_entry.second.body, property_set);
123 
124  if(!property_set.empty())
126  "property " + id2string(*property_set.begin()) + " unknown",
127  "--property id");
128 }
129 
130 void label_properties(goto_functionst &goto_functions)
131 {
132  std::map<irep_idt, std::size_t> property_counters;
133 
134  for(goto_functionst::function_mapt::iterator
135  it=goto_functions.function_map.begin();
136  it!=goto_functions.function_map.end();
137  it++)
138  label_properties(it->first, it->second.body, property_counters);
139 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
A collection of goto functions.
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
void set_function(const irep_idt &function)
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void set_properties(goto_programt &goto_program, std::unordered_set< irep_idt > &property_set)
void label_properties(goto_modelt &goto_model)
Set the properties to check.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.