CBMC
Loading...
Searching...
No Matches
syntactic_diff.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Syntactic GOTO-DIFF
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
11
12#include "syntactic_diff.h"
13
15
17{
18 for(const auto &gf_entry : goto_model1.goto_functions.function_map)
19 {
20 if(!gf_entry.second.body_available())
21 continue;
22
23 goto_functionst::function_mapt::const_iterator f_it =
24 goto_model2.goto_functions.function_map.find(gf_entry.first);
25 if(f_it==goto_model2.goto_functions.function_map.end() ||
26 !f_it->second.body_available())
27 {
28 deleted_functions.insert(gf_entry.first);
29 continue;
30 }
31
32 // check access qualifiers
33 const symbolt *fun1 = goto_model1.symbol_table.lookup(gf_entry.first);
34 CHECK_RETURN(fun1 != nullptr);
35 const symbolt *fun2 = goto_model2.symbol_table.lookup(gf_entry.first);
36 CHECK_RETURN(fun2 != nullptr);
37 const irep_idt &class_name = fun1->type.get(ID_C_class);
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);
49 class1->type.get(ID_access) != class2->type.get(ID_access);
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 }
63 break;
64 }
65 }
67 {
68 modified_functions.insert(gf_entry.first);
69 continue;
70 }
71
72 if(!gf_entry.second.body.equals(f_it->second.body))
73 {
74 modified_functions.insert(gf_entry.first);
75 continue;
76 }
77 }
78 for(const auto &gf_entry : goto_model2.goto_functions.function_map)
79 {
80 if(!gf_entry.second.body_available())
81 continue;
82
84
85 goto_functionst::function_mapt::const_iterator f_it =
86 goto_model1.goto_functions.function_map.find(gf_entry.first);
87 if(f_it==goto_model1.goto_functions.function_map.end() ||
88 !f_it->second.body_available())
89 {
90 new_functions.insert(gf_entry.first);
91 }
92 }
93
94 return !(new_functions.empty() &&
95 modified_functions.empty() &&
96 deleted_functions.empty());
97}
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool empty() const
Definition dstring.h:89
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
virtual bool operator()()
Symbol Table + CFG.
#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
Syntactic GOTO-DIFF.