@@ -54,32 +54,34 @@ class PossiblyConcurrentCallable extends Callable {
54
54
}
55
55
}
56
56
57
+ private VarAccess getANonInitializationAccess ( Field f ) {
58
+ result = f .getAnAccess ( ) and
59
+ exists ( Callable c | c = result .getEnclosingCallable ( ) |
60
+ not (
61
+ c = f .getDeclaringType ( ) .getACallable ( ) and
62
+ ( c instanceof Constructor or c instanceof InitializerMethod )
63
+ )
64
+ )
65
+ }
66
+
57
67
/**
58
68
* Holds if all accesses to `v` (outside of initializers) are locked in the same way.
59
69
*/
60
70
predicate alwaysLocked ( Field f ) {
61
71
exists ( Variable lock |
62
- forex ( VarAccess access |
63
- access = f .getAnAccess ( ) and not access .getEnclosingCallable ( ) instanceof InitializerMethod
64
- |
72
+ forex ( VarAccess access | access = getANonInitializationAccess ( f ) |
65
73
locallySynchronizedOn ( access , _, lock )
66
74
)
67
75
)
68
76
or
69
77
exists ( RefType thisType |
70
- forex ( VarAccess access |
71
- access = f .getAnAccess ( ) and
72
- not access .getEnclosingCallable ( ) instanceof Constructor and
73
- not access .getEnclosingCallable ( ) instanceof InitializerMethod
74
- |
78
+ forex ( VarAccess access | access = getANonInitializationAccess ( f ) |
75
79
locallySynchronizedOnThis ( access , thisType )
76
80
)
77
81
)
78
82
or
79
83
exists ( RefType classType |
80
- forex ( VarAccess access |
81
- access = f .getAnAccess ( ) and not access .getEnclosingCallable ( ) instanceof InitializerMethod
82
- |
84
+ forex ( VarAccess access | access = getANonInitializationAccess ( f ) |
83
85
locallySynchronizedOnClass ( access , classType )
84
86
)
85
87
)
0 commit comments