@@ -21,13 +21,23 @@ 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+
2434predicate useFunc ( GlobalVariable v , Function f ) {
2535 exists ( VariableAccess access |
2636 v .getAnAccess ( ) = access and
2737 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+ )
3141}
3242
3343predicate uninitialisedBefore ( GlobalVariable v , Function f ) {
@@ -38,12 +48,14 @@ predicate uninitialisedBefore(GlobalVariable v, Function f) {
3848 exists ( Call call , Function g |
3949 uninitialisedBefore ( v , g ) and
4050 call .getEnclosingFunction ( ) = g and
41- ( not functionInitialises ( f , v ) or locallyUninitialisedAt ( v , call ) ) and
51+ ( not functionInitialises ( g , v ) or locallyUninitialisedAt ( v , call ) ) and
4252 resolvedCall ( call , f )
4353 )
4454}
4555
4656predicate functionInitialises ( Function f , GlobalVariable v ) {
57+ initFunc ( v , f )
58+ or
4759 exists ( Call call |
4860 call .getEnclosingFunction ( ) = f and
4961 initialisedBy ( v , call )
@@ -60,7 +72,8 @@ predicate locallyUninitialisedAt(GlobalVariable v, Call call) {
6072 exists ( Call mid |
6173 locallyUninitialisedAt ( v , mid ) and not initialisedBy ( v , mid ) and callPair ( mid , call )
6274 )
63- )
75+ ) and
76+ not dominatingInitInFunc ( v , call .getEnclosingFunction ( ) , call )
6477}
6578
6679predicate initialisedBy ( GlobalVariable v , Call call ) {
0 commit comments