@@ -21,13 +21,23 @@ predicate initFunc(GlobalVariable v, Function f) {
21
21
)
22
22
}
23
23
24
+ /** Holds if `v` has an initializer in function `f` that dominates `node`. **/
25
+ predicate dominatingInitInFunc ( GlobalVariable v , Function f , ControlFlowNode node ) {
26
+ exists ( VariableAccess initAccess |
27
+ v .getAnAccess ( ) = initAccess and
28
+ initAccess .isUsedAsLValue ( ) and
29
+ initAccess .getEnclosingFunction ( ) = f and
30
+ dominates ( initAccess , node )
31
+ )
32
+ }
33
+
24
34
predicate useFunc ( GlobalVariable v , Function f ) {
25
35
exists ( VariableAccess access |
26
36
v .getAnAccess ( ) = access and
27
37
access .isRValue ( ) and
28
- access .getEnclosingFunction ( ) = f
29
- ) and
30
- not initFunc ( v , f )
38
+ access .getEnclosingFunction ( ) = f and
39
+ not dominatingInitInFunc ( v , f , access )
40
+ )
31
41
}
32
42
33
43
predicate uninitialisedBefore ( GlobalVariable v , Function f ) {
@@ -38,12 +48,14 @@ predicate uninitialisedBefore(GlobalVariable v, Function f) {
38
48
exists ( Call call , Function g |
39
49
uninitialisedBefore ( v , g ) and
40
50
call .getEnclosingFunction ( ) = g and
41
- ( not functionInitialises ( f , v ) or locallyUninitialisedAt ( v , call ) ) and
51
+ ( not functionInitialises ( g , v ) or locallyUninitialisedAt ( v , call ) ) and
42
52
resolvedCall ( call , f )
43
53
)
44
54
}
45
55
46
56
predicate functionInitialises ( Function f , GlobalVariable v ) {
57
+ initFunc ( v , f )
58
+ or
47
59
exists ( Call call |
48
60
call .getEnclosingFunction ( ) = f and
49
61
initialisedBy ( v , call )
@@ -60,7 +72,8 @@ predicate locallyUninitialisedAt(GlobalVariable v, Call call) {
60
72
exists ( Call mid |
61
73
locallyUninitialisedAt ( v , mid ) and not initialisedBy ( v , mid ) and callPair ( mid , call )
62
74
)
63
- )
75
+ ) and
76
+ not dominatingInitInFunc ( v , call .getEnclosingFunction ( ) , call )
64
77
}
65
78
66
79
predicate initialisedBy ( GlobalVariable v , Call call ) {
0 commit comments