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 
27  const namespacet &ns,
28  const irep_idt &identifier,
30  const goto_programt &goto_program)
31 {
32  for(const auto &ins : goto_program.instructions)
33  {
34  if(!ins.is_assert())
35  continue;
36 
37  const source_locationt &source_location=ins.source_location;
38 
39  const irep_idt &comment=source_location.get_comment();
40  const irep_idt &property_class=source_location.get_property_class();
41  const irep_idt description=
42  (comment==""?"assertion":comment);
43 
44  irep_idt property_id=source_location.get_property_id();
45 
46  switch(ui)
47  {
49  {
50  // use me instead
51  xmlt xml_property("property");
52  xml_property.set_attribute("name", id2string(property_id));
53  xml_property.set_attribute("class", id2string(property_class));
54 
55  xmlt &property_l=xml_property.new_element();
56  property_l=xml(source_location);
57 
58  xml_property.new_element("description").data=id2string(description);
59  xml_property.new_element("expression").data=
60  from_expr(ns, identifier, ins.guard);
61 
62  std::cout << xml_property << '\n';
63  }
64  break;
65 
67  assert(false);
68  break;
69 
71  std::cout << "Property " << property_id << ":\n";
72 
73  std::cout << " " << ins.source_location << '\n'
74  << " " << description << '\n'
75  << " " << from_expr(ns, identifier, ins.guard)
76  << '\n';
77 
78  std::cout << '\n';
79  break;
80 
81  default:
82  assert(false);
83  }
84  }
85 }
86 
87 
89  json_arrayt &json_properties,
90  const namespacet &ns,
91  const irep_idt &identifier,
92  const goto_programt &goto_program)
93 {
94  for(const auto &ins : goto_program.instructions)
95  {
96  if(!ins.is_assert())
97  continue;
98 
99  const source_locationt &source_location=ins.source_location;
100 
101  const irep_idt &comment=source_location.get_comment();
102  // const irep_idt &function=location.get_function();
103  const irep_idt &property_class=source_location.get_property_class();
104  const irep_idt description=
105  (comment==""?"assertion":comment);
106 
107  irep_idt property_id=source_location.get_property_id();
108 
109  json_objectt &json_property=
110  json_properties.push_back(jsont()).make_object();
111  json_property["name"]=json_stringt(id2string(property_id));
112  json_property["class"]=json_stringt(id2string(property_class));
113  json_property["sourceLocation"]=json(source_location);
114  json_property["description"]=json_stringt(id2string(description));
115  json_property["expression"]=
116  json_stringt(from_expr(ns, identifier, ins.guard));
117  }
118 }
119 
121  const namespacet &ns,
122  const goto_functionst &goto_functions)
123 {
124  json_arrayt json_properties;
125 
126  for(const auto &fct : goto_functions.function_map)
127  if(!fct.second.is_inlined())
129  json_properties,
130  ns,
131  fct.first,
132  fct.second.body);
133 
134  json_objectt json_result;
135  json_result["properties"] = json_properties;
136  std::cout << ",\n" << json_result;
137 }
138 
140  const namespacet &ns,
142  const goto_functionst &goto_functions)
143 {
145  show_properties_json(ns, goto_functions);
146  else
147  for(const auto &fct : goto_functions.function_map)
148  if(!fct.second.is_inlined())
149  show_properties(ns, fct.first, ui, fct.second.body);
150 }
151 
153  const goto_modelt &goto_model,
155 {
156  const namespacet ns(goto_model.symbol_table);
158  show_properties_json(ns, goto_model.goto_functions);
159  else
160  show_properties(ns, ui, goto_model.goto_functions);
161 }
void show_properties_json(json_arrayt &json_properties, const namespacet &ns, const irep_idt &identifier, const goto_programt &goto_program)
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:115
instructionst instructions
The list of instructions in the goto program.
Goto Programs with Functions.
Definition: json.h:21
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void show_properties(const namespacet &ns, const irep_idt &identifier, ui_message_handlert::uit ui, const goto_programt &goto_program)
symbol_tablet symbol_table
Definition: goto_model.h:25
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
jsont & push_back(const jsont &json)
Definition: json.h:157
Symbol Table + CFG.
Expressions in JSON.
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Definition: xml.h:18
std::string data
Definition: xml.h:30
xmlt & new_element(const std::string &name)
Definition: xml.h:86
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Show the properties.
json_objectt & make_object()
Definition: json.h:234
const irep_idt & get_comment() const
const irep_idt & get_property_id() const
const irep_idt & get_property_class() const
goto_functionst goto_functions
Definition: goto_model.h:26
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:23