cprover
java_syntactic_diff.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Syntactic GOTO-DIFF for Java
4 
5 Author: Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #include "java_syntactic_diff.h"
13 
15 
17 {
19  {
20  if(!it->second.body_available())
21  continue;
22 
23  goto_functionst::function_mapt::const_iterator f_it =
24  goto_model2.goto_functions.function_map.find(it->first);
25  if(
26  f_it == goto_model2.goto_functions.function_map.end() ||
27  !f_it->second.body_available())
28  {
29  deleted_functions.insert(it->first);
30  continue;
31  }
32 
33  // check access qualifiers
34  const symbolt *fun1 = goto_model1.symbol_table.lookup(it->first);
35  CHECK_RETURN(fun1 != nullptr);
36  const symbolt *fun2 = goto_model2.symbol_table.lookup(it->first);
37  CHECK_RETURN(fun2 != nullptr);
38  const irep_idt &class_name = fun1->type.get(ID_C_class);
39  bool function_access_changed =
40  fun1->type.get(ID_access) != fun2->type.get(ID_access);
41  bool class_access_changed = false;
42  bool field_access_changed = false;
43  if(!class_name.empty())
44  {
45  const symbolt *class1 = goto_model1.symbol_table.lookup(class_name);
46  CHECK_RETURN(class1 != nullptr);
47  const symbolt *class2 = goto_model2.symbol_table.lookup(class_name);
48  CHECK_RETURN(class2 != nullptr);
49  class_access_changed =
50  class1->type.get(ID_access) != class2->type.get(ID_access);
51  const class_typet &class_type1 = to_class_type(class1->type);
52  const class_typet &class_type2 = to_class_type(class2->type);
53  for(const auto &field1 : class_type1.components())
54  {
55  for(const auto &field2 : class_type2.components())
56  {
57  if(field1.get_name() == field2.get_name())
58  {
59  field_access_changed = field1.get_access() != field2.get_access();
60  break;
61  }
62  }
63  if(field_access_changed)
64  break;
65  }
66  }
67  if(function_access_changed || class_access_changed || field_access_changed)
68  {
69  modified_functions.insert(it->first);
70  continue;
71  }
72 
73  if(!it->second.body.equals(f_it->second.body))
74  {
75  modified_functions.insert(it->first);
76  continue;
77  }
78 
79  goto_programt::instructionst::const_iterator i_it1 =
80  it->second.body.instructions.begin();
81  for(goto_programt::instructionst::const_iterator
82  i_it2 = f_it->second.body.instructions.begin();
83  i_it1 != it->second.body.instructions.end() &&
84  i_it2 != f_it->second.body.instructions.end();
85  ++i_it1, ++i_it2)
86  {
87  if(i_it1->function != i_it2->function)
88  {
89  modified_functions.insert(it->first);
90  break;
91  }
92  }
93  }
95  {
96  if(!it->second.body_available())
97  continue;
98 
100 
101  goto_functionst::function_mapt::const_iterator f_it =
102  goto_model1.goto_functions.function_map.find(it->first);
103  if(
104  f_it == goto_model1.goto_functions.function_map.end() ||
105  !f_it->second.body_available())
106  new_functions.insert(it->first);
107  }
108 
109  return !(
110  new_functions.empty() && modified_functions.empty() &&
111  deleted_functions.empty());
112 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
goto_difft::new_functions
std::set< irep_idt > new_functions
Definition: goto_diff.h:52
class_typet
Class type.
Definition: std_types.h:365
goto_difft::goto_model2
const goto_modelt & goto_model2
Definition: goto_diff.h:48
to_class_type
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition: std_types.h:409
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_difft::goto_model1
const goto_modelt & goto_model1
Definition: goto_diff.h:47
goto_model.h
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
java_syntactic_difft::operator()
virtual bool operator()()
Definition: java_syntactic_diff.cpp:16
java_syntactic_diff.h
goto_difft::total_functions_count
unsigned total_functions_count
Definition: goto_diff.h:51
dstringt::empty
bool empty() const
Definition: dstring.h:75
goto_difft::modified_functions
std::set< irep_idt > modified_functions
Definition: goto_diff.h:52
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
symbolt
Symbol table entry.
Definition: symbol.h:27
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:86
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:149
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
goto_difft::deleted_functions
std::set< irep_idt > deleted_functions
Definition: goto_diff.h:52
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470