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,
55 {
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,
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,
149  const goto_functionst &goto_functions)
150 {
152  json_arrayt json_properties;
153 
154  for(const auto &fct : goto_functions.function_map)
155  if(!fct.second.is_inlined())
156  convert_properties_json(json_properties, ns, fct.first, fct.second.body);
157 
158  json_objectt json_result;
159  json_result["properties"] = json_properties;
160  msg.result() << json_result;
161 }
162 
164  const namespacet &ns,
167  const goto_functionst &goto_functions)
168 {
170  show_properties_json(ns, message_handler, goto_functions);
171  else
172  for(const auto &fct : goto_functions.function_map)
173  if(!fct.second.is_inlined())
174  show_properties(ns, fct.first, message_handler, ui, fct.second.body);
175 }
176 
178  const goto_modelt &goto_model,
181 {
182  const namespacet ns(goto_model.symbol_table);
185  else
186  show_properties(ns, message_handler, ui, goto_model.goto_functions);
187 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
Goto Programs with Functions.
Definition: json.h:23
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
jsont & push_back(const jsont &json)
Definition: json.h:163
Symbol Table + CFG.
source_locationt source_location
Definition: message.h:214
nonstd::optional< T > optionalt
Definition: optional.h:35
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
Expressions in JSON.
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
const irep_idt & get_basic_block_covered_lines() const
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Definition: xml.h:18
std::string data
Definition: xml.h:30
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
xmlt & new_element(const std::string &name)
Definition: xml.h:86
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
mstreamt & result() const
Definition: message.h:312
#define UNREACHABLE
Definition: invariant.h:271
goto_programt & goto_program
Definition: cover.cpp:63
Show the properties.
json_objectt & make_object()
Definition: json.h:290
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
const irep_idt & get_comment() const
const irep_idt & get_property_id() const
const irep_idt & get_property_class() const
void show_properties_json(const namespacet &ns, message_handlert &message_handler, const goto_functionst &goto_functions)
bool empty() const
Definition: dstring.h:73
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
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
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. ...
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:83
void show_properties(const namespacet &ns, const irep_idt &identifier, message_handlert &message_handler, ui_message_handlert::uit ui, const goto_programt &goto_program)