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/xml.h>
17 #include <util/xml_expr.h>
18 #include <util/json.h>
19 #include <util/json_expr.h>
20 
21 #include <langapi/language_util.h>
22 
23 #include "goto_functions.h"
24 #include "goto_model.h"
25 
26 
28  const irep_idt &property,
29  const goto_functionst & goto_functions)
30 {
31  for(const auto &fct : goto_functions.function_map)
32  {
33  const goto_programt &goto_program = fct.second.body;
34 
35  for(const auto &ins : goto_program.instructions)
36  {
37  if(ins.is_assert())
38  {
39  if(ins.source_location.get_property_id() == property)
40  {
41  return ins.source_location;
42  }
43  }
44  }
45  }
46  return { };
47 }
48 
50  const namespacet &ns,
51  const irep_idt &identifier,
52  message_handlert &message_handler,
54  const goto_programt &goto_program)
55 {
56  messaget msg(message_handler);
57  for(const auto &ins : goto_program.instructions)
58  {
59  if(!ins.is_assert())
60  continue;
61 
62  const source_locationt &source_location=ins.source_location;
63 
64  const irep_idt &comment=source_location.get_comment();
65  const irep_idt &property_class=source_location.get_property_class();
66  const irep_idt description=
67  (comment==""?"assertion":comment);
68 
69  irep_idt property_id=source_location.get_property_id();
70 
71  switch(ui)
72  {
74  {
75  // use me instead
76  xmlt xml_property("property");
77  xml_property.set_attribute("name", id2string(property_id));
78  xml_property.set_attribute("class", id2string(property_class));
79 
80  xmlt &property_l=xml_property.new_element();
81  property_l=xml(source_location);
82 
83  xml_property.new_element("description").data=id2string(description);
84  xml_property.new_element("expression").data=
85  from_expr(ns, identifier, ins.guard);
86 
87  msg.result() << xml_property;
88  }
89  break;
90 
93  break;
94 
96  msg.result() << "Property " << property_id << ":\n";
97 
98  msg.result() << " " << ins.source_location << '\n'
99  << " " << description << '\n'
100  << " " << from_expr(ns, identifier, ins.guard) << '\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=
128  (comment==""?"assertion":comment);
129 
130  irep_idt property_id=source_location.get_property_id();
131 
132  json_objectt &json_property=
133  json_properties.push_back(jsont()).make_object();
134  json_property["name"] = json_stringt(property_id);
135  json_property["class"] = json_stringt(property_class);
136  if(!source_location.get_basic_block_covered_lines().empty())
137  json_property["coveredLines"] =
138  json_stringt(source_location.get_basic_block_covered_lines());
139  json_property["sourceLocation"]=json(source_location);
140  json_property["description"] = json_stringt(description);
141  json_property["expression"]=
142  json_stringt(from_expr(ns, identifier, ins.guard));
143  }
144 }
145 
147  const namespacet &ns,
148  message_handlert &message_handler,
149  const goto_functionst &goto_functions)
150 {
151  messaget msg(message_handler);
152  json_arrayt json_properties;
153 
154  for(const auto &fct : goto_functions.function_map)
155  convert_properties_json(json_properties, ns, fct.first, fct.second.body);
156 
157  json_objectt json_result;
158  json_result["properties"] = json_properties;
159  msg.result() << json_result;
160 }
161 
163  const namespacet &ns,
164  message_handlert &message_handler,
166  const goto_functionst &goto_functions)
167 {
169  show_properties_json(ns, message_handler, goto_functions);
170  else
171  for(const auto &fct : goto_functions.function_map)
172  show_properties(ns, fct.first, message_handler, ui, fct.second.body);
173 }
174 
176  const goto_modelt &goto_model,
177  message_handlert &message_handler,
179 {
180  const namespacet ns(goto_model.symbol_table);
182  show_properties_json(ns, message_handler, goto_model.goto_functions);
183  else
184  show_properties(ns, message_handler, ui, 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:144
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
source_locationt::get_comment
const irep_idt & get_comment() const
Definition: source_location.h:72
source_locationt::get_property_id
const irep_idt & get_property_id() const
Definition: source_location.h:62
source_locationt::get_property_class
const irep_idt & get_property_class() const
Definition: source_location.h:67
json
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:87
show_properties_json
void show_properties_json(const namespacet &ns, message_handlert &message_handler, const goto_functionst &goto_functions)
Definition: show_properties.cpp:146
comment
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
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:49
xml
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:26
goto_model.h
goto_modelt
Definition: goto_model.h:24
messaget::eom
static eomt eom
Definition: message.h:284
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
jsont
Definition: json.h:23
xml.h
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
json_arrayt
Definition: json.h:146
json_objectt
Definition: json.h:244
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:93
messaget::result
mstreamt & result() const
Definition: message.h:396
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
ui_message_handlert::uit::JSON_UI
@ JSON_UI
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:236
language_util.h
show_properties.h
json_expr.h
message_handlert
Definition: message.h:24
source_locationt::get_basic_block_covered_lines
const irep_idt & get_basic_block_covered_lines() const
Definition: source_location.h:87
dstringt::empty
bool empty() const
Definition: dstring.h:75
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
xmlt
Definition: xml.h:18
source_locationt
Definition: source_location.h:20
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
ui_message_handlert::uit::PLAIN
@ PLAIN
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
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:27
json.h
goto_functions.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
xmlt::data
std::string data
Definition: xml.h:30
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
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:163
xml_expr.h
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:86
json_stringt
Definition: json.h:214