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 {
23  switch(ui)
24  {
26  {
27  result() << "total number of functions: " << total_functions_count
28  << '\n';
31  "modified functions", modified_functions, goto_model2);
33  "deleted functions", deleted_functions, goto_model1);
34  result() << eom;
35  break;
36  }
38  {
39  json_objectt json_result;
40  json_result["totalNumberOfFunctions"]=
43  json_result["newFunctions"].make_array(), new_functions, goto_model2);
45  json_result["modifiedFunctions"].make_array(),
47  goto_model2);
49  json_result["deletedFunctions"].make_array(),
51  goto_model1);
52  result() << json_result;
53  break;
54  }
56  {
57  error() << "XML output not supported yet" << eom;
58  }
59  }
60 }
61 
67  const std::string &group_name,
68  const std::set<irep_idt> &function_group,
69  const goto_modelt &goto_model) const
70 {
71  result() << group_name << ":\n";
72  for(const auto &function_name : function_group)
73  {
74  output_function(function_name, goto_model);
75  }
76 }
77 
82  const irep_idt &function_name,
83  const goto_modelt &goto_model) const
84 {
85  namespacet ns(goto_model.symbol_table);
86  const symbolt &symbol = ns.lookup(function_name);
87 
88  result() << " " << symbol.location.get_file() << ": " << function_name
89  << '\n';
90 
91  if(options.get_bool_option("show-properties"))
92  {
93  const auto goto_function_it =
94  goto_model.goto_functions.function_map.find(function_name);
96  goto_function_it != goto_model.goto_functions.function_map.end());
97  const goto_programt &goto_program = goto_function_it->second.body;
98 
99  for(const auto &ins : goto_program.instructions)
100  {
101  if(!ins.is_assert())
102  continue;
103 
104  const source_locationt &source_location = ins.source_location;
105  irep_idt property_id = source_location.get_property_id();
106  result() << " " << property_id << '\n';
107  }
108  }
109 }
110 
116  json_arrayt &result,
117  const std::set<irep_idt> &function_group,
118  const goto_modelt &goto_model) const
119 {
120  for(const auto &function_name : function_group)
121  {
123  result.push_back(jsont()).make_object(), function_name, goto_model);
124  }
125 }
126 
132  json_objectt &result,
133  const irep_idt &function_name,
134  const goto_modelt &goto_model) const
135 {
136  namespacet ns(goto_model.symbol_table);
137  const symbolt &symbol = ns.lookup(function_name);
138 
139  result["name"] = json_stringt(function_name);
140  result["sourceLocation"] = json(symbol.location);
141 
142  if(options.get_bool_option("show-properties"))
143  {
144  const auto goto_function_it =
145  goto_model.goto_functions.function_map.find(function_name);
146  CHECK_RETURN(
147  goto_function_it != goto_model.goto_functions.function_map.end());
148  const goto_programt &goto_program = goto_function_it->second.body;
149 
151  result["properties"].make_array(), ns, function_name, goto_program);
152  }
153 }
ui_message_handlert::uit ui
Definition: goto_diff.h:52
const goto_modelt & goto_model1
Definition: goto_diff.h:49
void output_function(const irep_idt &function_name, const goto_modelt &goto_model) const
Output function information in plain text format.
Definition: json.h:23
const goto_modelt & goto_model2
Definition: goto_diff.h:50
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Symbol Table + CFG.
unsigned total_functions_count
Definition: goto_diff.h:54
virtual void output_functions() const
Output diff result.
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
Expressions in JSON.
mstreamt & error() const
Definition: message.h:302
TO_BE_DOCUMENTED.
Definition: namespace.h:74
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
std::set< irep_idt > modified_functions
Definition: goto_diff.h:55
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
const irep_idt & get_file() const
mstreamt & result() const
Definition: message.h:312
std::string to_string(const string_constraintt &expr)
Used for debug printing.
goto_programt & goto_program
Definition: cover.cpp:63
Options.
Show the properties.
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:83
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
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:51
std::set< irep_idt > deleted_functions
Definition: goto_diff.h:55
std::set< irep_idt > new_functions
Definition: goto_diff.h:55
GOTO-DIFF Base Class.