CBMC
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{
19 for(const auto &gf_entry : goto_model1.goto_functions.function_map)
20 {
21 if(!gf_entry.second.body_available())
22 continue;
23
24 goto_functionst::function_mapt::const_iterator f_it =
25 goto_model2.goto_functions.function_map.find(gf_entry.first);
26 if(
27 f_it == goto_model2.goto_functions.function_map.end() ||
28 !f_it->second.body_available())
29 {
30 deleted_functions.insert(gf_entry.first);
31 continue;
32 }
33
34 // check access qualifiers
35 const symbolt *fun1 = goto_model1.symbol_table.lookup(gf_entry.first);
36 CHECK_RETURN(fun1 != nullptr);
37 const symbolt *fun2 = goto_model2.symbol_table.lookup(gf_entry.first);
38 CHECK_RETURN(fun2 != nullptr);
39 const std::optional<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 }
80 for(const auto &gf_entry : goto_model2.goto_functions.function_map)
81 {
82 if(!gf_entry.second.body_available())
83 continue;
84
86
87 goto_functionst::function_mapt::const_iterator f_it =
88 goto_model1.goto_functions.function_map.find(gf_entry.first);
89 if(
90 f_it == goto_model1.goto_functions.function_map.end() ||
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:562
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
Symbol table entry.
Definition symbol.h:28
Symbol Table + CFG.
Syntactic GOTO-DIFF for Java.
std::optional< 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