cprover
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
70 xmlt xml_property(
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.get_condition());
82
83 msg.result() << xml_property;
84 }
85 break;
86
89 break;
90
92 msg.result() << "Property " << property_id << ":\n";
93
94 msg.result() << " " << ins.source_location() << '\n'
95 << " " << description << '\n'
96 << " " << from_expr(ns, identifier, ins.get_condition())
97 << '\n';
98
99 msg.result() << messaget::eom;
100 break;
101
102 default:
104 }
105 }
106}
107
109 json_arrayt &json_properties,
110 const namespacet &ns,
111 const irep_idt &identifier,
112 const goto_programt &goto_program)
113{
114 for(const auto &ins : goto_program.instructions)
115 {
116 if(!ins.is_assert())
117 continue;
118
119 const source_locationt &source_location = ins.source_location();
120
121 const irep_idt &comment=source_location.get_comment();
122 // const irep_idt &function=location.get_function();
123 const irep_idt &property_class=source_location.get_property_class();
124 const irep_idt description = (comment.empty() ? "assertion" : comment);
125
126 irep_idt property_id=source_location.get_property_id();
127
128 json_objectt json_property{
129 {"name", json_stringt(property_id)},
130 {"class", json_stringt(property_class)},
131 {"sourceLocation", json(source_location)},
132 {"description", json_stringt(description)},
133 {"expression",
134 json_stringt(from_expr(ns, identifier, ins.get_condition()))}};
135
136 if(!source_location.get_basic_block_covered_lines().empty())
137 json_property["coveredLines"] =
139
140 json_properties.push_back(std::move(json_property));
141 }
142}
143
145 const namespacet &ns,
146 message_handlert &message_handler,
147 const goto_functionst &goto_functions)
148{
149 messaget msg(message_handler);
150 json_arrayt json_properties;
151
152 for(const auto &fct : goto_functions.function_map)
153 convert_properties_json(json_properties, ns, fct.first, fct.second.body);
154
155 json_objectt json_result{{"properties", json_properties}};
156 msg.result() << json_result;
157}
158
160 const namespacet &ns,
161 ui_message_handlert &ui_message_handler,
162 const goto_functionst &goto_functions)
163{
164 ui_message_handlert::uit ui = ui_message_handler.get_ui();
166 show_properties_json(ns, ui_message_handler, goto_functions);
167 else
168 for(const auto &fct : goto_functions.function_map)
169 show_properties(ns, fct.first, ui_message_handler, ui, fct.second.body);
170}
171
173 const goto_modelt &goto_model,
174 ui_message_handlert &ui_message_handler)
175{
176 ui_message_handlert::uit ui = ui_message_handler.get_ui();
177 const namespacet ns(goto_model.symbol_table);
179 show_properties_json(ns, ui_message_handler, goto_model.goto_functions);
180 else
181 show_properties(ns, ui_message_handler, goto_model.goto_functions);
182}
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
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:598
jsont & push_back(const jsont &json)
Definition: json.h:212
source_locationt source_location
Definition: message.h:247
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_basic_block_covered_lines() const
const irep_idt & get_property_id() 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
xmlt & new_element(const std::string &key)
Definition: xml.h:95
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)
nonstd::optional< T > optionalt
Definition: optional.h:35
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:117
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:108
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
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:503