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