@@ -21,13 +21,29 @@ predicate initFunc(GlobalVariable v, Function f) {
2121 )
2222}
2323
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+
34+ predicate safeAccess ( VariableAccess access ) {
35+ // it is safe if the variable access is part of a `sizeof` expression
36+ exists ( SizeofExprOperator e | e .getAChild * ( ) = access )
37+ }
38+
2439predicate useFunc ( GlobalVariable v , Function f ) {
2540 exists ( VariableAccess access |
2641 v .getAnAccess ( ) = access and
2742 access .isRValue ( ) and
28- access .getEnclosingFunction ( ) = f
29- ) and
30- not initFunc ( v , f )
43+ access .getEnclosingFunction ( ) = f and
44+ not safeAccess ( access ) and
45+ not dominatingInitInFunc ( v , f , access )
46+ )
3147}
3248
3349predicate uninitialisedBefore ( GlobalVariable v , Function f ) {
@@ -38,12 +54,14 @@ predicate uninitialisedBefore(GlobalVariable v, Function f) {
3854 exists ( Call call , Function g |
3955 uninitialisedBefore ( v , g ) and
4056 call .getEnclosingFunction ( ) = g and
41- ( not functionInitialises ( f , v ) or locallyUninitialisedAt ( v , call ) ) and
57+ ( not functionInitialises ( g , v ) or locallyUninitialisedAt ( v , call ) ) and
4258 resolvedCall ( call , f )
4359 )
4460}
4561
4662predicate functionInitialises ( Function f , GlobalVariable v ) {
63+ initFunc ( v , f )
64+ or
4765 exists ( Call call |
4866 call .getEnclosingFunction ( ) = f and
4967 initialisedBy ( v , call )
@@ -60,7 +78,8 @@ predicate locallyUninitialisedAt(GlobalVariable v, Call call) {
6078 exists ( Call mid |
6179 locallyUninitialisedAt ( v , mid ) and not initialisedBy ( v , mid ) and callPair ( mid , call )
6280 )
63- )
81+ ) and
82+ not dominatingInitInFunc ( v , call .getEnclosingFunction ( ) , call )
6483}
6584
6685predicate initialisedBy ( GlobalVariable v , Call call ) {
0 commit comments