cprover
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
23 const irep_idt &property,
24 const goto_functionst & goto_functions)
25{
26 for(const auto &fct : goto_functions.function_map)
27 {
28 const goto_programt &goto_program = fct.second.body;
29
30 for(const auto &ins : goto_program.instructions)
31 {
32 if(ins.is_assert())
33 {
34 if(ins.source_location().get_property_id() == property)
35 {
36 return ins.source_location();
37 }
38 }
39 }
40 }
41 return { };
42}
43
45 const namespacet &ns,
46 const irep_idt &identifier,
47 message_handlert &message_handler,
49 const goto_programt &goto_program)
50{
51 messaget msg(message_handler);
52 for(const auto &ins : goto_program.instructions)
53 {
54 if(!ins.is_assert())
55 continue;
56
57 const source_locationt &source_location = ins.source_location();
58
59 const irep_idt &comment=source_location.get_comment();
60 const irep_idt &property_class=source_location.get_property_class();
61 const irep_idt description = (comment.empty() ? "assertion" : comment);
62
63 irep_idt property_id=source_location.get_property_id();
64
65 switch(ui)
66 {
68 {
69 // use me instead
71 "property",
72 {{"name", id2string(property_id)},
73 {"class", id2string(property_class)}},
74 {});
75
76 xmlt &property_l=xml_property.new_element();
77 property_l=xml(source_location);
78
79 xml_property.new_element("description").data=id2string(description);
80 xml_property.new_element("expression").data =
81 from_expr(ns, identifier, ins.condition());
82
84 source_location.get_basic_block_source_lines();
85 if(basic_block_lines.is_not_nil())
86 {
87 xmlt basic_block_lines_xml{"basic_block_lines"};
88 for(const auto &file_entry : basic_block_lines.get_named_sub())
89 {
90 for(const auto &lines_entry : file_entry.second.get_named_sub())
91 {
92 xmlt line{"line"};
93 line.set_attribute("file", id2string(file_entry.first));
94 line.set_attribute("function", id2string(lines_entry.first));
95 line.data = id2string(lines_entry.second.id());
96 basic_block_lines_xml.new_element(line);
97 }
98 }
100 }
101
102 msg.result() << xml_property;
103 }
104 break;
105
108 break;
109
111 msg.result() << "Property " << property_id << ":\n";
112
113 msg.result() << " " << ins.source_location() << '\n'
114 << " " << description << '\n'
115 << " " << from_expr(ns, identifier, ins.condition())
116 << '\n';
117
118 msg.result() << messaget::eom;
119 break;
120
121 default:
123 }
124 }
125}
126
129 const namespacet &ns,
130 const irep_idt &identifier,
131 const goto_programt &goto_program)
132{
133 for(const auto &ins : goto_program.instructions)
134 {
135 if(!ins.is_assert())
136 continue;
137
138 const source_locationt &source_location = ins.source_location();
139
140 const irep_idt &comment=source_location.get_comment();
141 // const irep_idt &function=location.get_function();
142 const irep_idt &property_class=source_location.get_property_class();
143 const irep_idt description = (comment.empty() ? "assertion" : comment);
144
145 irep_idt property_id=source_location.get_property_id();
146
148 {"name", json_stringt(property_id)},
149 {"class", json_stringt(property_class)},
150 {"sourceLocation", json(source_location)},
151 {"description", json_stringt(description)},
152 {"expression", json_stringt(from_expr(ns, identifier, ins.condition()))}};
153
154 const irept &basic_block_lines =
155 source_location.get_basic_block_source_lines();
156 if(basic_block_lines.is_not_nil())
157 {
159 for(const auto &file_entry : basic_block_lines.get_named_sub())
160 {
162 for(const auto &lines_entry : file_entry.second.get_named_sub())
163 {
165 json_stringt{lines_entry.second.id()};
166 }
168 }
169 json_property["basicBlockLines"] = basic_block_lines_json;
170 }
171
172 json_properties.push_back(std::move(json_property));
173 }
174}
175
177 const namespacet &ns,
178 message_handlert &message_handler,
179 const goto_functionst &goto_functions)
180{
181 messaget msg(message_handler);
183
184 for(const auto &fct : goto_functions.function_map)
185 convert_properties_json(json_properties, ns, fct.first, fct.second.body);
186
188 msg.result() << json_result;
189}
190
192 const namespacet &ns,
193 ui_message_handlert &ui_message_handler,
194 const goto_functionst &goto_functions)
195{
196 ui_message_handlert::uit ui = ui_message_handler.get_ui();
198 show_properties_json(ns, ui_message_handler, goto_functions);
199 else
200 for(const auto &fct : goto_functions.function_map)
201 show_properties(ns, fct.first, ui_message_handler, ui, fct.second.body);
202}
203
205 const goto_modelt &goto_model,
206 ui_message_handlert &ui_message_handler)
207{
208 ui_message_handlert::uit ui = ui_message_handler.get_ui();
209 const namespacet ns(goto_model.symbol_table);
211 show_properties_json(ns, ui_message_handler, goto_model.goto_functions);
212 else
213 show_properties(ns, ui_message_handler, goto_model.goto_functions);
214}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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:372
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & result() const
Definition message.h:409
static eomt eom
Definition message.h:297
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:47
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)
optionalt< 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 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
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