cprover
show_properties.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Show Claims
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "show_properties.h"
13 
14 #include <iostream>
15 
16 #include <util/json_irep.h>
17 #include <util/xml_irep.h>
18 
19 #include <langapi/language_util.h>
20 
21 #include "goto_functions.h"
22 #include "goto_model.h"
23 
24 
26  const irep_idt &property,
27  const goto_functionst & goto_functions)
28 {
29  for(const auto &fct : goto_functions.function_map)
30  {
31  const goto_programt &goto_program = fct.second.body;
32 
33  for(const auto &ins : goto_program.instructions)
34  {
35  if(ins.is_assert())
36  {
37  if(ins.source_location.get_property_id() == property)
38  {
39  return ins.source_location;
40  }
41  }
42  }
43  }
44  return { };
45 }
46 
48  const namespacet &ns,
49  const irep_idt &identifier,
50  message_handlert &message_handler,
52  const goto_programt &goto_program)
53 {
54  messaget msg(message_handler);
55  for(const auto &ins : goto_program.instructions)
56  {
57  if(!ins.is_assert())
58  continue;
59 
60  const source_locationt &source_location=ins.source_location;
61 
62  const irep_idt &comment=source_location.get_comment();
63  const irep_idt &property_class=source_location.get_property_class();
64  const irep_idt description = (comment.empty() ? "assertion" : comment);
65 
66  irep_idt property_id=source_location.get_property_id();
67 
68  switch(ui)
69  {
71  {
72  // use me instead
73  xmlt xml_property(
74  "property",
75  {{"name", id2string(property_id)},
76  {"class", id2string(property_class)}},
77  {});
78 
79  xmlt &property_l=xml_property.new_element();
80  property_l=xml(source_location);
81 
82  xml_property.new_element("description").data=id2string(description);
83  xml_property.new_element("expression").data =
84  from_expr(ns, identifier, ins.get_condition());
85 
86  msg.result() << xml_property;
87  }
88  break;
89 
92  break;
93 
95  msg.result() << "Property " << property_id << ":\n";
96 
97  msg.result() << " " << ins.source_location << '\n'
98  << " " << description << '\n'
99  << " " << from_expr(ns, identifier, ins.get_condition())
100  << '\n';
101 
102  msg.result() << messaget::eom;
103  break;
104 
105  default:
106  UNREACHABLE;
107  }
108  }
109 }
110 
112  json_arrayt &json_properties,
113  const namespacet &ns,
114  const irep_idt &identifier,
115  const goto_programt &goto_program)
116 {
117  for(const auto &ins : goto_program.instructions)
118  {
119  if(!ins.is_assert())
120  continue;
121 
122  const source_locationt &source_location=ins.source_location;
123 
124  const irep_idt &comment=source_location.get_comment();
125  // const irep_idt &function=location.get_function();
126  const irep_idt &property_class=source_location.get_property_class();
127  const irep_idt description = (comment.empty() ? "assertion" : comment);
128 
129  irep_idt property_id=source_location.get_property_id();
130 
131  json_objectt json_property{
132  {"name", json_stringt(property_id)},
133  {"class", json_stringt(property_class)},
134  {"sourceLocation", json(source_location)},
135  {"description", json_stringt(description)},
136  {"expression",
137  json_stringt(from_expr(ns, identifier, ins.get_condition()))}};
138 
139  if(!source_location.get_basic_block_covered_lines().empty())
140  json_property["coveredLines"] =
141  json_stringt(source_location.get_basic_block_covered_lines());
142 
143  json_properties.push_back(std::move(json_property));
144  }
145 }
146 
148  const namespacet &ns,
149  message_handlert &message_handler,
150  const goto_functionst &goto_functions)
151 {
152  messaget msg(message_handler);
153  json_arrayt json_properties;
154 
155  for(const auto &fct : goto_functions.function_map)
156  convert_properties_json(json_properties, ns, fct.first, fct.second.body);
157 
158  json_objectt json_result{{"properties", json_properties}};
159  msg.result() << json_result;
160 }
161 
163  const namespacet &ns,
164  ui_message_handlert &ui_message_handler,
165  const goto_functionst &goto_functions)
166 {
167  ui_message_handlert::uit ui = ui_message_handler.get_ui();
169  show_properties_json(ns, ui_message_handler, goto_functions);
170  else
171  for(const auto &fct : goto_functions.function_map)
172  show_properties(ns, fct.first, ui_message_handler, ui, fct.second.body);
173 }
174 
176  const goto_modelt &goto_model,
177  ui_message_handlert &ui_message_handler)
178 {
179  ui_message_handlert::uit ui = ui_message_handler.get_ui();
180  const namespacet ns(goto_model.symbol_table);
182  show_properties_json(ns, ui_message_handler, goto_model.goto_functions);
183  else
184  show_properties(ns, ui_message_handler, goto_model.goto_functions);
185 }
convert_properties_json
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
Definition: show_properties.cpp:111
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
source_locationt::get_comment
const irep_idt & get_comment() const
Definition: source_location.h:71
source_locationt::get_property_id
const irep_idt & get_property_id() const
Definition: source_location.h:61
source_locationt::get_property_class
const irep_idt & get_property_class() const
Definition: source_location.h:66
ui_message_handlert
Definition: ui_message.h:20
show_properties_json
void show_properties_json(const namespacet &ns, message_handlert &message_handler, const goto_functionst &goto_functions)
Definition: show_properties.cpp:147
ui_message_handlert::uit::XML_UI
@ XML_UI
show_properties
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)
Definition: show_properties.cpp:47
goto_model.h
Symbol Table + CFG.
xml_irep.h
goto_modelt
Definition: goto_model.h:26
messaget::eom
static eomt eom
Definition: message.h:297
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
json_irep.h
Util.
json_arrayt
Definition: json.h:165
json_objectt
Definition: json.h:300
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:31
ui_message_handlert::uit
uit
Definition: ui_message.h:22
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
messaget::result
mstreamt & result() const
Definition: message.h:409
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
ui_message_handlert::uit::JSON_UI
@ JSON_UI
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
language_util.h
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
show_properties.h
Show the properties.
message_handlert
Definition: message.h:28
source_locationt::get_basic_block_covered_lines
const irep_idt & get_basic_block_covered_lines() const
Definition: source_location.h:86
dstringt::empty
bool empty() const
Definition: dstring.h:88
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
xmlt
Definition: xml.h:21
source_locationt
Definition: source_location.h:20
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
ui_message_handlert::uit::PLAIN
@ PLAIN
find_property
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.
Definition: show_properties.cpp:25
goto_functions.h
Goto Programs with Functions.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95
json_stringt
Definition: json.h:270