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 <util/json_irep.h>
15 #include <util/ui_message.h>
16 #include <util/xml_irep.h>
17 
18 #include <langapi/language_util.h>
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:
103  UNREACHABLE;
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"] =
138  json_stringt(source_location.get_basic_block_covered_lines());
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:71
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
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_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: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: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:116
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:107
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:503