CBMC
Loading...
Searching...
No Matches
show_properties.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Show Claims
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "show_properties.h"
13
14#include <util/json_irep.h>
15#include <util/ui_message.h>
16#include <util/xml_irep.h>
17
19
20#include "goto_model.h"
21
22std::optional<source_locationt>
23find_property(const irep_idt &property, const goto_functionst &goto_functions)
24{
25 for(const auto &fct : goto_functions.function_map)
26 {
27 const goto_programt &goto_program = fct.second.body;
28
29 for(const auto &ins : goto_program.instructions)
30 {
31 if(ins.is_assert())
32 {
33 if(ins.source_location().get_property_id() == property)
34 {
35 return ins.source_location();
36 }
37 }
38 }
39 }
40 return { };
41}
42
44 const namespacet &ns,
45 const irep_idt &identifier,
46 message_handlert &message_handler,
48 const goto_programt &goto_program)
49{
50 messaget msg(message_handler);
51 for(const auto &ins : goto_program.instructions)
52 {
53 if(!ins.is_assert())
54 continue;
55
56 const source_locationt &source_location = ins.source_location();
57
58 const irep_idt &comment=source_location.get_comment();
59 const irep_idt &property_class=source_location.get_property_class();
60 const irep_idt description = (comment.empty() ? "assertion" : comment);
61
62 irep_idt property_id=source_location.get_property_id();
63
64 switch(ui)
65 {
67 {
68 // use me instead
70 "property",
71 {{"name", id2string(property_id)},
72 {"class", id2string(property_class)}},
73 {});
74
75 xmlt &property_l=xml_property.new_element();
76 property_l=xml(source_location);
77
78 xml_property.new_element("description").data=id2string(description);
79 xml_property.new_element("expression").data =
80 from_expr(ns, identifier, ins.condition());
81
83 source_location.get_basic_block_source_lines();
84 if(basic_block_lines.is_not_nil())
85 {
86 xmlt basic_block_lines_xml{"basic_block_lines"};
87 for(const auto &file_entry : basic_block_lines.get_named_sub())
88 {
89 for(const auto &lines_entry : file_entry.second.get_named_sub())
90 {
91 xmlt line{"line"};
92 line.set_attribute("file", id2string(file_entry.first));
93 line.set_attribute("function", id2string(lines_entry.first));
94 line.data = id2string(lines_entry.second.id());
95 basic_block_lines_xml.new_element(line);
96 }
97 }
99 }
100
101 msg.result() << xml_property;
102 }
103 break;
104
107 break;
108
110 msg.result() << "Property " << property_id << ":\n";
111
112 msg.result() << " " << ins.source_location() << '\n'
113 << " " << description << '\n'
114 << " " << from_expr(ns, identifier, ins.condition())
115 << '\n';
116
117 msg.result() << messaget::eom;
118 break;
119
120 default:
122 }
123 }
124}
125
128 const namespacet &ns,
129 const irep_idt &identifier,
130 const goto_programt &goto_program)
131{
132 for(const auto &ins : goto_program.instructions)
133 {
134 if(!ins.is_assert())
135 continue;
136
137 const source_locationt &source_location = ins.source_location();
138
139 const irep_idt &comment=source_location.get_comment();
140 // const irep_idt &function=location.get_function();
141 const irep_idt &property_class=source_location.get_property_class();
142 const irep_idt description = (comment.empty() ? "assertion" : comment);
143
144 irep_idt property_id=source_location.get_property_id();
145
147 {"name", json_stringt(property_id)},
148 {"class", json_stringt(property_class)},
149 {"sourceLocation", json(source_location)},
150 {"description", json_stringt(description)},
151 {"expression", json_stringt(from_expr(ns, identifier, ins.condition()))}};
152
153 const irept &basic_block_lines =
154 source_location.get_basic_block_source_lines();
155 if(basic_block_lines.is_not_nil())
156 {
158 for(const auto &file_entry : basic_block_lines.get_named_sub())
159 {
161 for(const auto &lines_entry : file_entry.second.get_named_sub())
162 {
164 json_stringt{lines_entry.second.id()};
165 }
167 }
168 json_property["basicBlockLines"] = basic_block_lines_json;
169 }
170
171 json_properties.push_back(std::move(json_property));
172 }
173}
174
176 const namespacet &ns,
177 message_handlert &message_handler,
178 const goto_functionst &goto_functions)
179{
180 messaget msg(message_handler);
182
183 for(const auto &fct : goto_functions.function_map)
184 convert_properties_json(json_properties, ns, fct.first, fct.second.body);
185
187 msg.result() << json_result;
188}
189
191 const namespacet &ns,
192 ui_message_handlert &ui_message_handler,
193 const goto_functionst &goto_functions)
194{
195 ui_message_handlert::uit ui = ui_message_handler.get_ui();
197 show_properties_json(ns, ui_message_handler, goto_functions);
198 else
199 for(const auto &fct : goto_functions.function_map)
200 show_properties(ns, fct.first, ui_message_handler, ui, fct.second.body);
201}
202
204 const goto_modelt &goto_model,
205 ui_message_handlert &ui_message_handler)
206{
207 ui_message_handlert::uit ui = ui_message_handler.get_ui();
208 const namespacet ns(goto_model.symbol_table);
210 show_properties_json(ns, ui_message_handler, goto_model.goto_functions);
211 else
212 show_properties(ns, ui_message_handler, goto_model.goto_functions);
213}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
const irep_idt & get_property_id() const
const irept & get_basic_block_source_lines() const
const irep_idt & get_property_class() const
const irep_idt & get_comment() const
virtual uit get_ui() const
Definition ui_message.h:33
Definition xml.h:21
void set_attribute(const std::string &attribute, unsigned value)
Definition xml.cpp:198
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
static std::string comment(const rw_set_baset::entryt &entry, bool write)
void show_properties_json(const namespacet &ns, message_handlert &message_handler, const goto_functionst &goto_functions)
void convert_properties_json(json_arrayt &json_properties, const namespacet &ns, const irep_idt &identifier, const goto_programt &goto_program)
Collects the properties in the goto program into a json_arrayt
std::optional< source_locationt > find_property(const irep_idt &property, const goto_functionst &goto_functions)
Returns a source_locationt that corresponds to the property given by an irep_idt.
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Show the properties.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525