CBMC: /home/runner/work/cbmc/cbmc/src/goto-programs/set_properties.cpp Source File

CBMC
Loading...
Searching...
No Matches
set_properties.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Set Properties
4
5Author: 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{
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)
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 auto sorted = goto_functions.sorted();
135 for(auto &it : sorted)
136 label_properties(it->first, it->second.body, property_counters);
137}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
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
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
Definition goto_model.h:27
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:72
instructionst instructions
The list of instructions in the goto program.
Definition goto_program.h:621
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.

AltStyle によって変換されたページ (->オリジナル) /