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 }
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:74
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
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:92
const irep_idt & get_property_id() const
const irep_idt & get_comment() const
const irep_idt & get_property_class() const
const irep_idt & get_basic_block_covered_lines() const
virtual uit get_ui() const
Definition: ui_message.h:31
Definition: xml.h:21
xmlt & new_element(const std::string &key)
Definition: xml.h:95
Goto Programs with Functions.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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:114
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
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)
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
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 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:504