cprover
goto_diff_base.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: GOTO-DIFF Base Class
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_diff.h"
13 
14 #include <util/json_expr.h>
15 #include <util/options.h>
16 
19 
22 {
24 
25  switch(message_handler.get_ui())
26  {
28  {
29  msg.result() << "total number of functions: " << total_functions_count
30  << '\n' << messaget::eom;
33  "modified functions", modified_functions, goto_model2);
35  "deleted functions", deleted_functions, goto_model1);
36  msg.result() << messaget::eom;
37  break;
38  }
40  {
41  json_objectt json_result;
42  json_result["totalNumberOfFunctions"]=
45  json_result["newFunctions"].make_array(), new_functions, goto_model2);
47  json_result["modifiedFunctions"].make_array(),
49  goto_model2);
51  json_result["deletedFunctions"].make_array(),
53  goto_model1);
54  msg.result() << json_result << messaget::eom;
55  break;
56  }
58  {
59  msg.error() << "XML output not supported yet" << messaget::eom;
60  }
61  }
62 }
63 
69  const std::string &group_name,
70  const std::set<irep_idt> &function_group,
71  const goto_modelt &goto_model) const
72 {
73  messaget(message_handler).result() << group_name << ':' << messaget::eom;
74  for(const auto &function_name : function_group)
75  {
76  output_function(function_name, goto_model);
77  }
78 }
79 
84  const irep_idt &function_name,
85  const goto_modelt &goto_model) const
86 {
88 
89  namespacet ns(goto_model.symbol_table);
90  const symbolt &symbol = ns.lookup(function_name);
91 
92  msg.result() << " " << symbol.location.get_file() << ": " << function_name;
93 
94  if(options.get_bool_option("show-properties"))
95  {
96  const auto goto_function_it =
97  goto_model.goto_functions.function_map.find(function_name);
99  goto_function_it != goto_model.goto_functions.function_map.end());
100  const goto_programt &goto_program = goto_function_it->second.body;
101 
102  for(const auto &ins : goto_program.instructions)
103  {
104  if(!ins.is_assert())
105  continue;
106 
107  const source_locationt &source_location = ins.source_location;
108  irep_idt property_id = source_location.get_property_id();
109  msg.result() << "\n " << property_id;
110  }
111  }
112 
113  msg.result() << messaget::eom;
114 }
115 
121  json_arrayt &result,
122  const std::set<irep_idt> &function_group,
123  const goto_modelt &goto_model) const
124 {
125  for(const auto &function_name : function_group)
126  {
128  result.push_back(jsont()).make_object(), function_name, goto_model);
129  }
130 }
131 
137  json_objectt &result,
138  const irep_idt &function_name,
139  const goto_modelt &goto_model) const
140 {
141  namespacet ns(goto_model.symbol_table);
142  const symbolt &symbol = ns.lookup(function_name);
143 
144  result["name"] = json_stringt(function_name);
145  result["sourceLocation"] = json(symbol.location);
146 
147  if(options.get_bool_option("show-properties"))
148  {
149  const auto goto_function_it =
150  goto_model.goto_functions.function_map.find(function_name);
151  CHECK_RETURN(
152  goto_function_it != goto_model.goto_functions.function_map.end());
153  const goto_programt &goto_program = goto_function_it->second.body;
154 
156  result["properties"].make_array(), ns, function_name, goto_program);
157  }
158 }
const goto_modelt & goto_model1
Definition: goto_diff.h:47
void output_function(const irep_idt &function_name, const goto_modelt &goto_model) const
Output function information in plain text format.
uit get_ui() const
Definition: ui_message.h:30
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: json.h:23
const goto_modelt & goto_model2
Definition: goto_diff.h:48
ui_message_handlert & message_handler
Definition: goto_diff.h:46
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.
Definition: symbol.h:27
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
jsont & push_back(const jsont &json)
Definition: json.h:163
Symbol Table + CFG.
unsigned total_functions_count
Definition: goto_diff.h:51
virtual void output_functions() const
Output diff result.
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
Expressions in JSON.
mstreamt & error() const
Definition: message.h:386
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
static eomt eom
Definition: message.h:284
std::set< irep_idt > modified_functions
Definition: goto_diff.h:52
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
const irep_idt & get_file() const
mstreamt & result() const
Definition: message.h:396
Options.
Show the properties.
json_objectt & make_object()
Definition: json.h:290
void output_function_group(const std::string &group_name, const std::set< irep_idt > &function_group, const goto_modelt &goto_model) const
Output group of functions in plain text format.
const irep_idt & get_property_id() const
void convert_function_json(json_objectt &result, const irep_idt &function_name, const goto_modelt &goto_model) const
Convert function information to 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
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:87
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
void convert_function_group_json(json_arrayt &result, const std::set< irep_idt > &function_group, const goto_modelt &goto_model) const
Convert a function group to JSON.
const optionst & options
Definition: goto_diff.h:49
std::set< irep_idt > deleted_functions
Definition: goto_diff.h:52
std::set< irep_idt > new_functions
Definition: goto_diff.h:52
GOTO-DIFF Base Class.