cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
14
#include <
goto-programs/goto_model.h
>
15
16
bool
syntactic_difft::operator()
()
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);
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(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
83
total_functions_count
++;
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
}
class_typet
Class type.
Definition
std_types.h:325
dstringt::empty
bool empty() const
Definition
dstring.h:89
goto_difft::modified_functions
std::set< irep_idt > modified_functions
Definition
goto_diff.h:54
goto_difft::goto_model1
const goto_modelt & goto_model1
Definition
goto_diff.h:49
goto_difft::new_functions
std::set< irep_idt > new_functions
Definition
goto_diff.h:54
goto_difft::total_functions_count
unsigned total_functions_count
Definition
goto_diff.h:53
goto_difft::deleted_functions
std::set< irep_idt > deleted_functions
Definition
goto_diff.h:54
goto_difft::goto_model2
const goto_modelt & goto_model2
Definition
goto_diff.h:50
irept::get
const irep_idt & get(const irep_idt &name) const
Definition
irep.cpp:44
struct_union_typet::components
const componentst & components() const
Definition
std_types.h:147
symbolt
Symbol table entry.
Definition
symbol.h:28
symbolt::type
typet type
Type of symbol.
Definition
symbol.h:31
syntactic_difft::operator()
virtual bool operator()()
Definition
syntactic_diff.cpp:16
goto_model.h
Symbol Table + CFG.
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition
invariant.h:495
to_class_type
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition
std_types.h:381
syntactic_diff.h
Syntactic GOTO-DIFF.
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
goto-diff
syntactic_diff.cpp
Generated by
1.17.0