cprover
Loading...
Searching...
No Matches
java_syntactic_diff.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Syntactic GOTO-DIFF for Java
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
11
12#include "java_syntactic_diff.h"
13
16
18{
20 {
21 if(!gf_entry.second.body_available())
22 continue;
23
24 goto_functionst::function_mapt::const_iterator f_it =
26 if(
28 !f_it->second.body_available())
29 {
30 deleted_functions.insert(gf_entry.first);
31 continue;
32 }
33
34 // check access qualifiers
36 CHECK_RETURN(fun1 != nullptr);
38 CHECK_RETURN(fun2 != nullptr);
39 const optionalt<irep_idt> class_name = declaring_class(*fun1);
41 fun1->type.get(ID_access) != fun2->type.get(ID_access);
42 bool class_access_changed = false;
43 bool field_access_changed = false;
44 if(class_name)
45 {
46 const symbolt *class1 = goto_model1.symbol_table.lookup(*class_name);
47 CHECK_RETURN(class1 != nullptr);
48 const symbolt *class2 = goto_model2.symbol_table.lookup(*class_name);
49 CHECK_RETURN(class2 != nullptr);
51 class1->type.get(ID_access) != class2->type.get(ID_access);
54 for(const auto &field1 : class_type1.components())
55 {
56 for(const auto &field2 : class_type2.components())
57 {
58 if(field1.get_name() == field2.get_name())
59 {
60 field_access_changed = field1.get_access() != field2.get_access();
61 break;
62 }
63 }
65 break;
66 }
67 }
69 {
70 modified_functions.insert(gf_entry.first);
71 continue;
72 }
73
74 if(!gf_entry.second.body.equals(f_it->second.body))
75 {
76 modified_functions.insert(gf_entry.first);
77 continue;
78 }
79 }
81 {
82 if(!gf_entry.second.body_available())
83 continue;
84
86
87 goto_functionst::function_mapt::const_iterator f_it =
89 if(
91 !f_it->second.body_available())
92 new_functions.insert(gf_entry.first);
93 }
94
95 return !(
96 new_functions.empty() && modified_functions.empty() &&
97 deleted_functions.empty());
98}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Class type.
Definition std_types.h:325
std::set< irep_idt > modified_functions
Definition goto_diff.h:54
const goto_modelt & goto_model1
Definition goto_diff.h:49
std::set< irep_idt > new_functions
Definition goto_diff.h:54
unsigned total_functions_count
Definition goto_diff.h:53
std::set< irep_idt > deleted_functions
Definition goto_diff.h:54
const goto_modelt & goto_model2
Definition goto_diff.h:50
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition symbol.h:28
Symbol Table + CFG.
Syntactic GOTO-DIFF for Java.
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition std_types.h:381