@@ -43,7 +43,7 @@ predicate isThreadSafeType(Type t) {
4343}
4444
4545/** Holds if the expression `e` is a thread-safe initializer. */
46- predicate isThreadSafeInitializer ( Expr e ) {
46+ private predicate isThreadSafeInitializer ( Expr e ) {
4747 exists ( string name |
4848 e .( Call ) .getCallee ( ) .getSourceDeclaration ( ) .hasQualifiedName ( "java.util" , "Collections" , name )
4949 |
@@ -132,7 +132,9 @@ class ClassAnnotatedAsThreadSafe extends Class {
132132 * Holds if the field access `a` to the field `f` is not protected by any monitor, and it can be reached via the expression `e` in the method `m`.
133133 * We maintain the invariant that `m = e.getEnclosingCallable()`.
134134 */
135- predicate unlockedAccess ( ExposedField f , Expr e , Method m , ExposedFieldAccess a , boolean write ) {
135+ private predicate unlockedAccess (
136+ ExposedField f , Expr e , Method m , ExposedFieldAccess a , boolean write
137+ ) {
136138 m .getDeclaringType ( ) = this and
137139 (
138140 // base case
@@ -154,7 +156,7 @@ class ClassAnnotatedAsThreadSafe extends Class {
154156 }
155157
156158 /** Holds if the class has an unlocked access to the field `f` via the expression `e` in the method `m`. */
157- predicate hasUnlockedAccess ( ExposedField f , Expr e , Method m , boolean write ) {
159+ private predicate hasUnlockedAccess ( ExposedField f , Expr e , Method m , boolean write ) {
158160 this .unlockedAccess ( f , e , m , _, write )
159161 }
160162
@@ -168,7 +170,7 @@ class ClassAnnotatedAsThreadSafe extends Class {
168170 }
169171
170172 /** Holds if the class has an unlocked access to the field `f` via the expression `e` in the public method `m`. */
171- predicate hasUnlockedPublicAccess ( ExposedField f , Expr e , Method m , boolean write ) {
173+ private predicate hasUnlockedPublicAccess ( ExposedField f , Expr e , Method m , boolean write ) {
172174 this .unlockedPublicAccess ( f , e , m , _, write )
173175 }
174176
@@ -177,7 +179,7 @@ class ClassAnnotatedAsThreadSafe extends Class {
177179 /**
178180 * Holds if the class has an access, locked by exactly one monitor, to the field `f` via the expression `e` in the method `m`.
179181 */
180- predicate hasOnelockedAccess (
182+ private predicate hasOnelockedAccess (
181183 ExposedField f , Expr e , Method m , boolean write , Monitors:: Monitor monitor
182184 ) {
183185 //base
@@ -197,7 +199,7 @@ class ClassAnnotatedAsThreadSafe extends Class {
197199 }
198200
199201 /** Holds if the class has an access, locked by exactly one monitor, to the field `f` via the expression `e` in the public method `m`. */
200- predicate hasOnelockedPublicAccess (
202+ private predicate hasOnelockedPublicAccess (
201203 ExposedField f , Expr e , Method m , boolean write , Monitors:: Monitor monitor
202204 ) {
203205 this .hasOnelockedAccess ( f , e , m , write , monitor ) and
@@ -213,7 +215,7 @@ class ClassAnnotatedAsThreadSafe extends Class {
213215 // Cases where all accesses to a field are protected by at least one monitor
214216 //
215217 /** Holds if the class has an access, locked by at least one monitor, to the field `f` via the expression `e` in the method `m`. */
216- predicate hasOnepluslockedAccess (
218+ private predicate hasOnepluslockedAccess (
217219 ExposedField f , Expr e , Method m , boolean write , Monitors:: Monitor monitor
218220 ) {
219221 //base
@@ -248,7 +250,7 @@ class ClassAnnotatedAsThreadSafe extends Class {
248250 }
249251
250252 /** Holds if the class has an access, not protected by the monitor `m`, to the field `f` via the expression `e` in the method `m`. */
251- predicate escapesMonitor (
253+ private predicate escapesMonitor (
252254 ExposedField f , Expr e , Method m , boolean write , Monitors:: Monitor monitor
253255 ) {
254256 //base
@@ -268,7 +270,7 @@ class ClassAnnotatedAsThreadSafe extends Class {
268270 }
269271
270272 /** Holds if the class has an access, not protected by the monitor `m`, to the field `f` via the expression `e` in the public method `m`. */
271- predicate escapesMonitorPublic (
273+ private predicate escapesMonitorPublic (
272274 ExposedField f , Expr e , Method m , boolean write , Monitors:: Monitor monitor
273275 ) {
274276 this .escapesMonitor ( f , e , m , write , monitor ) and
0 commit comments