checker/tests/lock/TestTreeKinds.java - typetools/checker-framework - Git at Google

 import java.util.Random;
 import java.util.concurrent.locks.ReentrantLock;
 import org.checkerframework.checker.lock.qual.*;
 import org.checkerframework.dataflow.qual.SideEffectFree;

 public class TestTreeKinds {
   class MyClass {
     Object field = new Object();

     @LockingFree
     Object method(@GuardSatisfied MyClass this) {
       return new Object();
     }

     void method2(@GuardSatisfied MyClass this) {}
   }

   @GuardedBy("lock") MyClass m;

   {
     // In constructor/initializer, it's OK not to hold the lock on 'this', but other locks must
     // be respected.
     // :: error: (lock.not.held)
     m.field = new Object();
   }

   final ReentrantLock lock = new ReentrantLock();
   final ReentrantLock lock2 = new ReentrantLock();

   @GuardedBy("lock") MyClass foo = new MyClass();

   MyClass unguardedFoo = new MyClass();

   @EnsuresLockHeld("lock")
   void lockTheLock() {
     lock.lock();
   }

   @EnsuresLockHeld("lock2")
   void lockTheLock2() {
     lock2.lock();
   }

   @EnsuresLockHeldIf(expression = "lock", result = true)
   boolean tryToLockTheLock() {
     return lock.tryLock();
   }

   // This @MayReleaseLocks annotation causes dataflow analysis to assume 'lock' is released after
   // unlockTheLock() is called.
   @MayReleaseLocks
   void unlockTheLock() {}

   @SideEffectFree
   void sideEffectFreeMethod() {}

   @LockingFree
   void lockingFreeMethod() {}

   @MayReleaseLocks
   void nonSideEffectFreeMethod() {}

   @Holding("lock")
   void requiresLockHeldMethod() {}

   MyClass fooArray @GuardedBy("lock") [] = new MyClass[3];

   @GuardedBy("lock") MyClass fooArray2[] = new MyClass[3];

   @GuardedBy("lock") MyClass fooArray3[][] = new MyClass[3][3];

   MyClass fooArray4 @GuardedBy("lock") [][] = new MyClass[3][3];

   MyClass fooArray5[] @GuardedBy("lock") [] = new MyClass[3][3];

   class myClass {
     int i = 0;
   }

   @GuardedBy("lock") myClass myClassInstance = new myClass();

   @GuardedBy("lock") Exception exception = new Exception();

   class MyParametrizedType<T> {
     T foo;
     int l;
   }

   @GuardedBy("lock") MyParametrizedType<MyClass> myParametrizedType = new MyParametrizedType<>();

   MyClass getFooWithWrongReturnType() {
     // :: error: (return)
     return foo; // return of guarded object
   }

   @GuardedBy("lock") MyClass getFoo() {
     return foo;
   }

   MyClass @GuardedBy("lock") [] getFooArray() {
     return fooArray;
   }

   @GuardedBy("lock") MyClass[] getFooArray2() {
     return fooArray2;
   }

   @GuardedBy("lock") MyClass[][] getFooArray3() {
     return fooArray3;
   }

   MyClass @GuardedBy("lock") [][] getFooArray4() {
     return fooArray4;
   }

   MyClass[] @GuardedBy("lock") [] getFooArray5() {
     return fooArray5;
   }

   enum myEnumType {
     ABC,
     DEF
   }

   @GuardedBy("lock") myEnumType myEnum;

   void testEnumType() {
     // TODO: assignment is technically correct, but we could
     // make it friendlier for the user if constant enum values on the RHS
     // automatically cast to the @GuardedBy annotation of the LHS.
     // :: error: (assignment)
     myEnum = myEnumType.ABC;
   }

   final Object intrinsicLock = new Object();

   void testThreadHoldsLock(@GuardedBy("intrinsicLock") MyClass m) {
     if (Thread.holdsLock(intrinsicLock)) {
       m.field.toString();
     } else {
       // :: error: (lock.not.held)
       m.field.toString();
     }
   }

   void testTreeTypes() {
     int i, l;

     MyClass o = new MyClass();
     MyClass f = new MyClass();

     // The following test cases were inspired from annotator.find.ASTPathCriterion.isSatisfiedBy
     // in the Annotation File Utilities

     // TODO: File a bug for the dataflow issue mentioned in the line below.
     // TODO: uncomment: Hits a bug in dataflow:
     // do {
     //     break;
     // } while (foo.field != null); // access to guarded object in condition of do/while loop
     // :: error: (lock.not.held)
     for (foo = new MyClass(); foo.field != null; foo = new MyClass()) {
       break;
     } // access to guarded object in condition of for loop
     // assignment to guarded object (OK) --- foo is still refined to @GuardedBy("lock") after
     // this point, though.
     foo = new MyClass();
     // A simple method call to a guarded object is not considered a dereference (only field
     // accesses are considered dereferences).
     unguardedFoo.method2();
     // Same as above, but the guard must be satisfied if the receiver is @GuardSatisfied.
     // :: error: (lock.not.held)
     foo.method2();
     // attempt to use guarded object in a switch statement
     // :: error: (lock.not.held)
     switch (foo.field.hashCode()) {
     }
     // attempt to use guarded object inside a try with resources
     // try(foo = new MyClass()) { foo.field.toString(); }

     // Retrieving an element from a guarded array is a dereference
     // :: error: (lock.not.held)
     MyClass m = fooArray[0];

     // method call on dereference of unguarded element of *guarded* array
     // :: error: (lock.not.held)
     fooArray[0].field.toString();
     // :: error: (lock.not.held)
     l = fooArray.length; // dereference of guarded array itself

     // method call on dereference of guarded array element
     // :: error: (lock.not.held)
     fooArray2[0].field.toString();
     // method call on dereference of unguarded array - TODO: currently preconditions are not
     // retrieved correctly from array types. This is not unique to the Lock Checker.
     // fooArray2.field.toString();

     // method call on dereference of guarded array element of multidimensional array
     // :: error: (lock.not.held)
     fooArray3[0][0].field.toString();
     // method call on dereference of unguarded single-dimensional array element of unguarded
     // multidimensional array - TODO: currently preconditions are not retrieved correctly from
     // array types. This is not unique to the Lock Checker.
     // fooArray3[0].field.toString();
     // method call on dereference of unguarded multidimensional array - TODO: currently
     // preconditions are not retrieved correctly from array types. This is not unique to the
     // Lock Checker.
     // fooArray3.field.toString();

     // method call on dereference of unguarded array element of *guarded* multidimensional array
     // :: error: (lock.not.held)
     fooArray4[0][0].field.toString();
     // dereference of unguarded single-dimensional array element of *guarded* multidimensional
     // array
     // :: error: (lock.not.held)
     l = fooArray4[0].length;
     // dereference of guarded multidimensional array
     // :: error: (lock.not.held)
     l = fooArray4.length;

     // method call on dereference of unguarded array element of *guarded subarray* of
     // multidimensional array
     // :: error: (lock.not.held)
     fooArray5[0][0].field.toString();
     // dereference of guarded single-dimensional array element of multidimensional array
     // :: error: (lock.not.held)
     l = fooArray5[0].length;
     // dereference of unguarded multidimensional array
     l = fooArray5.length;

     // :: error: (lock.not.held)
     l = getFooArray().length; // dereference of guarded array returned by a method

     // method call on dereference of guarded array element returned by a method
     // :: error: (lock.not.held)
     getFooArray2()[0].field.toString();
     // dereference of unguarded array returned by a method
     l = getFooArray2().length;

     // method call on dereference of guarded array element of multidimensional array returned by
     // a method
     // :: error: (lock.not.held)
     getFooArray3()[0][0].field.toString();
     // dereference of unguarded single-dimensional array element of multidimensional array
     // returned by a method
     l = getFooArray3()[0].length;
     // dereference of unguarded multidimensional array returned by a method
     l = getFooArray3().length;

     // method call on dereference of unguarded array element of *guarded* multidimensional array
     // returned by a method
     // :: error: (lock.not.held)
     getFooArray4()[0][0].field.toString();
     // dereference of unguarded single-dimensional array element of *guarded* multidimensional
     // array returned by a method
     // :: error: (lock.not.held)
     l = getFooArray4()[0].length;
     // dereference of guarded multidimensional array returned by a method
     // :: error: (lock.not.held)
     l = getFooArray4().length;

     // method call on dereference of unguarded array element of *guarded subarray* of
     // multidimensional array returned by a method
     // :: error: (lock.not.held)
     getFooArray5()[0][0].field.toString();
     // dereference of guarded single-dimensional array element of multidimensional array
     // returned by a method
     // :: error: (lock.not.held)
     l = getFooArray5()[0].length;
     // dereference of unguarded multidimensional array returned by a method
     l = getFooArray5().length;

     // Test different @GuardedBy(...) present on the element and array locations.
     @GuardedBy("lock") MyClass @GuardedBy("lock2") [] array = new MyClass[3];
     // :: error: (lock.not.held)
     array[0].field = new Object();
     if (lock.isHeldByCurrentThread()) {
       // :: error: (lock.not.held)
       array[0].field = new Object();
       if (lock2.isHeldByCurrentThread()) {
         array[0].field = new Object();
       }
     }

     // method call on guarded object within parenthesized expression
     // :: error: (lock.not.held)
     String s = (foo.field.toString());
     // :: error: (lock.not.held)
     foo.field.toString(); // method call on guarded object
     // :: error: (lock.not.held)
     getFoo().field.toString(); // method call on guarded object returned by a method
     // :: error: (lock.not.held)
     this.foo.field.toString(); // method call on guarded object using 'this' literal
     // dereference of guarded object in labeled statement
     label:
     // :: error: (lock.not.held)
     foo.field.toString();
     // access to guarded object in instanceof expression (OK)
     if (foo instanceof MyClass) {}
     // access to guarded object in while condition of while loop (OK)
     while (foo != null) {
       break;
     }
     // binary operator on guarded object in else if condition (OK)
     if (false) {
     } else if (foo == o) {
     }
     // access to guarded object in a lambda expression
     Runnable rn =
         () -> {
           // :: error: (lock.not.held)
           foo.field.toString();
         };
     // :: error: (lock.not.held)
     i = myClassInstance.i; // access to member field of guarded object
     // MemberReferenceTrees? how do they work
     fooArray = new MyClass[3]; // second allocation of guarded array (OK)
     // dereference of guarded object in conditional expression tree
     // :: error: (lock.not.held)
     s = i == 5 ? foo.field.toString() : f.field.toString();
     // dereference of guarded object in conditional expression tree
     // :: error: (lock.not.held)
     s = i == 5 ? f.field.toString() : foo.field.toString();
     // Testing of 'return' is done in getFooWithWrongReturnType()
     // throwing a guarded object - when throwing an exception, it must be @GuardedBy({}). Even
     // @GuardedByUnknown is not allowed.
     try {
       // :: error: (throw)
       throw exception;
     } catch (Exception e) {
     }
     // casting of a guarded object to an unguarded object
     // :: error: (assignment)
     @GuardedBy({}) Object e1 = (Object) exception;
     // OK, since the local variable's type gets refined to @GuardedBy("lock")
     Object e2 = (Object) exception;
     // :: error: (lock.not.held)
     l = myParametrizedType.l; // dereference of guarded object having a parameterized type

     // We need to support locking on local variables and protecting local variables because
     // these locals may contain references to fields. Somehow we need to pass along the
     // information of which field it was.

     if (foo == o) { // binary operator on guarded object (OK)
       o.field.toString();
     }

     if (foo == null) {
       // With -AconcurrentSemantics turned off, a cannot.dereference error would be expected,
       // since there is an attempt to dereference an expression whose type has been refined to
       // @GuardedByBottom (due to the comparison to null). However, with -AconcurrentSemantics
       // turned on, foo may no longer be null by now, the refinement to @GuardedByBottom is
       // lost and the refined type of foo is now the declared type ( @GuardedBy("lock") ),
       // resulting in the lock.not.held error.
       // :: error: (lock.not.held)
       foo.field.toString();
     }

     // TODO: Reenable:
     // @PolyGuardedBy should not be written here, but it is not explicitly forbidden by the
     // framework.
     // @PolyGuardedBy MyClass m2 = new MyClass();
     // (cannot.dereference)
     // m2.field.toString();
   }

   @MayReleaseLocks
   public void testLocals() {
     final ReentrantLock localLock = new ReentrantLock();

     @GuardedBy("localLock") MyClass guardedByLocalLock = new MyClass();

     // :: error: (lock.not.held)
     guardedByLocalLock.field.toString();

     @GuardedBy("lock") MyClass local = new MyClass();

     // :: error: (lock.not.held)
     local.field.toString();

     lockTheLock();

     local.field.toString(); // No warning output

     unlockTheLock();
   }

   @MayReleaseLocks
   public void testMethodAnnotations() {
     Random r = new Random();

     if (r.nextBoolean()) {
       lockTheLock();
       requiresLockHeldMethod();
     } else {
       // :: error: (contracts.precondition)
       requiresLockHeldMethod();
     }

     if (r.nextBoolean()) {
       lockTheLock();
       foo.field.toString();

       unlockTheLock();

       // :: error: (lock.not.held)
       foo.field.toString();
     } else {
       // :: error: (lock.not.held)
       foo.field.toString();
     }

     if (tryToLockTheLock()) {
       foo.field.toString();
     } else {
       // :: error: (lock.not.held)
       foo.field.toString();
     }

     if (r.nextBoolean()) {
       lockTheLock();
       sideEffectFreeMethod();
       foo.field.toString();
     } else {
       lockTheLock();
       nonSideEffectFreeMethod();
       // :: error: (lock.not.held)
       foo.field.toString();
     }

     if (r.nextBoolean()) {
       lockTheLock();
       lockingFreeMethod();
       foo.field.toString();
     } else {
       lockTheLock();
       nonSideEffectFreeMethod();
       // :: error: (lock.not.held)
       foo.field.toString();
     }
   }

   void methodThatTakesAnInteger(Integer i) {}

   void testBoxedPrimitiveType() {
     Integer i = null;
     if (i == null) {}

     methodThatTakesAnInteger(i);
   }

   void testReceiverGuardedByItself(@GuardedBy("<self>") TestTreeKinds this) {
     // :: error: (lock.not.held)
     method();
     synchronized (this) {
       method();
     }
   }

   void method(@GuardSatisfied TestTreeKinds this) {}

   void testOtherClassReceiverGuardedByItself(final @GuardedBy("<self>") OtherClass o) {
     // :: error: (lock.not.held)
     o.foo();
     synchronized (o) {
       o.foo();
     }
   }

   class OtherClass {
     void foo(@GuardSatisfied OtherClass this) {}
   }

   void testExplicitLockSynchronized() {
     final ReentrantLock lock = new ReentrantLock();
     // :: error: (explicit.lock.synchronized)
     synchronized (lock) {
     }
   }

   void testPrimitiveTypeGuardedby() {
     // :: error: (immutable.type.guardedby)
     @GuardedBy("lock") int a = 0;
     // :: error: (immutable.type.guardedby)
     @GuardedBy int b = 0;
     // :: error: (immutable.type.guardedby) :: error: (guardsatisfied.location.disallowed)
     @GuardSatisfied int c = 0;
     // :: error: (immutable.type.guardedby) :: error: (guardsatisfied.location.disallowed)
     @GuardSatisfied(1) int d = 0;
     int e = 0;
     // :: error: (immutable.type.guardedby)
     @GuardedByUnknown int f = 0;
     // :: error: (immutable.type.guardedby) :: error: (assignment)
     @GuardedByBottom int g = 0;
   }

   void testBinaryOperatorBooleanResultIsAlwaysGuardedByNothing() {
     @GuardedBy("lock") Object o1 = new Object();
     Object o2 = new Object();
     // boolean variables are implicitly @GuardedBy({}).
     boolean b1 = o1 == o2;
     boolean b2 = o2 == o1;
     boolean b3 = o1 != o2;
     boolean b4 = o2 != o1;
     boolean b5 = o1 instanceof Object;
     boolean b6 = o2 instanceof Object;
     boolean b7 = o1 instanceof @GuardedBy("lock") Object;
     boolean b8 = o2 instanceof @GuardedBy("lock") Object;
   }
 }
	import java.util.Random;
	import java.util.concurrent.locks.ReentrantLock;
	import org.checkerframework.checker.lock.qual.*;
	import org.checkerframework.dataflow.qual.SideEffectFree;

	public class TestTreeKinds {
	class MyClass {
	Object field = new Object();

	@LockingFree
	Object method(@GuardSatisfied MyClass this) {
	return new Object();
	}

	void method2(@GuardSatisfied MyClass this) {}
	}

	@GuardedBy("lock") MyClass m;

	{
	// In constructor/initializer, it's OK not to hold the lock on 'this', but other locks must
	// be respected.
	// :: error: (lock.not.held)
	m.field = new Object();
	}

	final ReentrantLock lock = new ReentrantLock();
	final ReentrantLock lock2 = new ReentrantLock();

	@GuardedBy("lock") MyClass foo = new MyClass();

	MyClass unguardedFoo = new MyClass();

	@EnsuresLockHeld("lock")
	void lockTheLock() {
	lock.lock();
	}

	@EnsuresLockHeld("lock2")
	void lockTheLock2() {
	lock2.lock();
	}

	@EnsuresLockHeldIf(expression = "lock", result = true)
	boolean tryToLockTheLock() {
	return lock.tryLock();
	}

	// This @MayReleaseLocks annotation causes dataflow analysis to assume 'lock' is released after
	// unlockTheLock() is called.
	@MayReleaseLocks
	void unlockTheLock() {}

	@SideEffectFree
	void sideEffectFreeMethod() {}

	@LockingFree
	void lockingFreeMethod() {}

	@MayReleaseLocks
	void nonSideEffectFreeMethod() {}

	@Holding("lock")
	void requiresLockHeldMethod() {}

	MyClass fooArray @GuardedBy("lock") [] = new MyClass[3];

	@GuardedBy("lock") MyClass fooArray2[] = new MyClass[3];

	@GuardedBy("lock") MyClass fooArray3[][] = new MyClass[3][3];

	MyClass fooArray4 @GuardedBy("lock") [][] = new MyClass[3][3];

	MyClass fooArray5[] @GuardedBy("lock") [] = new MyClass[3][3];

	class myClass {
	int i = 0;
	}

	@GuardedBy("lock") myClass myClassInstance = new myClass();

	@GuardedBy("lock") Exception exception = new Exception();

	class MyParametrizedType<T> {
	T foo;
	int l;
	}

	@GuardedBy("lock") MyParametrizedType<MyClass> myParametrizedType = new MyParametrizedType<>();

	MyClass getFooWithWrongReturnType() {
	// :: error: (return)
	return foo; // return of guarded object
	}

	@GuardedBy("lock") MyClass getFoo() {
	return foo;
	}

	MyClass @GuardedBy("lock") [] getFooArray() {
	return fooArray;
	}

	@GuardedBy("lock") MyClass[] getFooArray2() {
	return fooArray2;
	}

	@GuardedBy("lock") MyClass[][] getFooArray3() {
	return fooArray3;
	}

	MyClass @GuardedBy("lock") [][] getFooArray4() {
	return fooArray4;
	}

	MyClass[] @GuardedBy("lock") [] getFooArray5() {
	return fooArray5;
	}

	enum myEnumType {
	ABC,
	DEF
	}

	@GuardedBy("lock") myEnumType myEnum;

	void testEnumType() {
	// TODO: assignment is technically correct, but we could
	// make it friendlier for the user if constant enum values on the RHS
	// automatically cast to the @GuardedBy annotation of the LHS.
	// :: error: (assignment)
	myEnum = myEnumType.ABC;
	}

	final Object intrinsicLock = new Object();

	void testThreadHoldsLock(@GuardedBy("intrinsicLock") MyClass m) {
	if (Thread.holdsLock(intrinsicLock)) {
	m.field.toString();
	} else {
	// :: error: (lock.not.held)
	m.field.toString();
	}
	}

	void testTreeTypes() {
	int i, l;

	MyClass o = new MyClass();
	MyClass f = new MyClass();

	// The following test cases were inspired from annotator.find.ASTPathCriterion.isSatisfiedBy
	// in the Annotation File Utilities

	// TODO: File a bug for the dataflow issue mentioned in the line below.
	// TODO: uncomment: Hits a bug in dataflow:
	// do {
	// break;
	// } while (foo.field != null); // access to guarded object in condition of do/while loop
	// :: error: (lock.not.held)
	for (foo = new MyClass(); foo.field != null; foo = new MyClass()) {
	break;
	} // access to guarded object in condition of for loop
	// assignment to guarded object (OK) --- foo is still refined to @GuardedBy("lock") after
	// this point, though.
	foo = new MyClass();
	// A simple method call to a guarded object is not considered a dereference (only field
	// accesses are considered dereferences).
	unguardedFoo.method2();
	// Same as above, but the guard must be satisfied if the receiver is @GuardSatisfied.
	// :: error: (lock.not.held)
	foo.method2();
	// attempt to use guarded object in a switch statement
	// :: error: (lock.not.held)
	switch (foo.field.hashCode()) {
	}
	// attempt to use guarded object inside a try with resources
	// try(foo = new MyClass()) { foo.field.toString(); }

	// Retrieving an element from a guarded array is a dereference
	// :: error: (lock.not.held)
	MyClass m = fooArray[0];

	// method call on dereference of unguarded element of guarded array
	// :: error: (lock.not.held)
	fooArray[0].field.toString();
	// :: error: (lock.not.held)
	l = fooArray.length; // dereference of guarded array itself

	// method call on dereference of guarded array element
	// :: error: (lock.not.held)
	fooArray2[0].field.toString();
	// method call on dereference of unguarded array - TODO: currently preconditions are not
	// retrieved correctly from array types. This is not unique to the Lock Checker.
	// fooArray2.field.toString();

	// method call on dereference of guarded array element of multidimensional array
	// :: error: (lock.not.held)
	fooArray3[0][0].field.toString();
	// method call on dereference of unguarded single-dimensional array element of unguarded
	// multidimensional array - TODO: currently preconditions are not retrieved correctly from
	// array types. This is not unique to the Lock Checker.
	// fooArray3[0].field.toString();
	// method call on dereference of unguarded multidimensional array - TODO: currently
	// preconditions are not retrieved correctly from array types. This is not unique to the
	// Lock Checker.
	// fooArray3.field.toString();

	// method call on dereference of unguarded array element of guarded multidimensional array
	// :: error: (lock.not.held)
	fooArray4[0][0].field.toString();
	// dereference of unguarded single-dimensional array element of guarded multidimensional
	// array
	// :: error: (lock.not.held)
	l = fooArray4[0].length;
	// dereference of guarded multidimensional array
	// :: error: (lock.not.held)
	l = fooArray4.length;

	// method call on dereference of unguarded array element of guarded subarray of
	// multidimensional array
	// :: error: (lock.not.held)
	fooArray5[0][0].field.toString();
	// dereference of guarded single-dimensional array element of multidimensional array
	// :: error: (lock.not.held)
	l = fooArray5[0].length;
	// dereference of unguarded multidimensional array
	l = fooArray5.length;

	// :: error: (lock.not.held)
	l = getFooArray().length; // dereference of guarded array returned by a method

	// method call on dereference of guarded array element returned by a method
	// :: error: (lock.not.held)
	getFooArray2()[0].field.toString();
	// dereference of unguarded array returned by a method
	l = getFooArray2().length;

	// method call on dereference of guarded array element of multidimensional array returned by
	// a method
	// :: error: (lock.not.held)
	getFooArray3()[0][0].field.toString();
	// dereference of unguarded single-dimensional array element of multidimensional array
	// returned by a method
	l = getFooArray3()[0].length;
	// dereference of unguarded multidimensional array returned by a method
	l = getFooArray3().length;

	// method call on dereference of unguarded array element of guarded multidimensional array
	// returned by a method
	// :: error: (lock.not.held)
	getFooArray4()[0][0].field.toString();
	// dereference of unguarded single-dimensional array element of guarded multidimensional
	// array returned by a method
	// :: error: (lock.not.held)
	l = getFooArray4()[0].length;
	// dereference of guarded multidimensional array returned by a method
	// :: error: (lock.not.held)
	l = getFooArray4().length;

	// method call on dereference of unguarded array element of guarded subarray of
	// multidimensional array returned by a method
	// :: error: (lock.not.held)
	getFooArray5()[0][0].field.toString();
	// dereference of guarded single-dimensional array element of multidimensional array
	// returned by a method
	// :: error: (lock.not.held)
	l = getFooArray5()[0].length;
	// dereference of unguarded multidimensional array returned by a method
	l = getFooArray5().length;

	// Test different @GuardedBy(...) present on the element and array locations.
	@GuardedBy("lock") MyClass @GuardedBy("lock2") [] array = new MyClass[3];
	// :: error: (lock.not.held)
	array[0].field = new Object();
	if (lock.isHeldByCurrentThread()) {
	// :: error: (lock.not.held)
	array[0].field = new Object();
	if (lock2.isHeldByCurrentThread()) {
	array[0].field = new Object();
	}
	}

	// method call on guarded object within parenthesized expression
	// :: error: (lock.not.held)
	String s = (foo.field.toString());
	// :: error: (lock.not.held)
	foo.field.toString(); // method call on guarded object
	// :: error: (lock.not.held)
	getFoo().field.toString(); // method call on guarded object returned by a method
	// :: error: (lock.not.held)
	this.foo.field.toString(); // method call on guarded object using 'this' literal
	// dereference of guarded object in labeled statement
	label:
	// :: error: (lock.not.held)
	foo.field.toString();
	// access to guarded object in instanceof expression (OK)
	if (foo instanceof MyClass) {}
	// access to guarded object in while condition of while loop (OK)
	while (foo != null) {
	break;
	}
	// binary operator on guarded object in else if condition (OK)
	if (false) {
	} else if (foo == o) {
	}
	// access to guarded object in a lambda expression
	Runnable rn =
	() -> {
	// :: error: (lock.not.held)
	foo.field.toString();
	};
	// :: error: (lock.not.held)
	i = myClassInstance.i; // access to member field of guarded object
	// MemberReferenceTrees? how do they work
	fooArray = new MyClass[3]; // second allocation of guarded array (OK)
	// dereference of guarded object in conditional expression tree
	// :: error: (lock.not.held)
	s = i == 5 ? foo.field.toString() : f.field.toString();
	// dereference of guarded object in conditional expression tree
	// :: error: (lock.not.held)
	s = i == 5 ? f.field.toString() : foo.field.toString();
	// Testing of 'return' is done in getFooWithWrongReturnType()
	// throwing a guarded object - when throwing an exception, it must be @GuardedBy({}). Even
	// @GuardedByUnknown is not allowed.
	try {
	// :: error: (throw)
	throw exception;
	} catch (Exception e) {
	}
	// casting of a guarded object to an unguarded object
	// :: error: (assignment)
	@GuardedBy({}) Object e1 = (Object) exception;
	// OK, since the local variable's type gets refined to @GuardedBy("lock")
	Object e2 = (Object) exception;
	// :: error: (lock.not.held)
	l = myParametrizedType.l; // dereference of guarded object having a parameterized type

	// We need to support locking on local variables and protecting local variables because
	// these locals may contain references to fields. Somehow we need to pass along the
	// information of which field it was.

	if (foo == o) { // binary operator on guarded object (OK)
	o.field.toString();
	}

	if (foo == null) {
	// With -AconcurrentSemantics turned off, a cannot.dereference error would be expected,
	// since there is an attempt to dereference an expression whose type has been refined to
	// @GuardedByBottom (due to the comparison to null). However, with -AconcurrentSemantics
	// turned on, foo may no longer be null by now, the refinement to @GuardedByBottom is
	// lost and the refined type of foo is now the declared type ( @GuardedBy("lock") ),
	// resulting in the lock.not.held error.
	// :: error: (lock.not.held)
	foo.field.toString();
	}

	// TODO: Reenable:
	// @PolyGuardedBy should not be written here, but it is not explicitly forbidden by the
	// framework.
	// @PolyGuardedBy MyClass m2 = new MyClass();
	// (cannot.dereference)
	// m2.field.toString();
	}

	@MayReleaseLocks
	public void testLocals() {
	final ReentrantLock localLock = new ReentrantLock();

	@GuardedBy("localLock") MyClass guardedByLocalLock = new MyClass();

	// :: error: (lock.not.held)
	guardedByLocalLock.field.toString();

	@GuardedBy("lock") MyClass local = new MyClass();

	// :: error: (lock.not.held)
	local.field.toString();

	lockTheLock();

	local.field.toString(); // No warning output

	unlockTheLock();
	}

	@MayReleaseLocks
	public void testMethodAnnotations() {
	Random r = new Random();

	if (r.nextBoolean()) {
	lockTheLock();
	requiresLockHeldMethod();
	} else {
	// :: error: (contracts.precondition)
	requiresLockHeldMethod();
	}

	if (r.nextBoolean()) {
	lockTheLock();
	foo.field.toString();

	unlockTheLock();

	// :: error: (lock.not.held)
	foo.field.toString();
	} else {
	// :: error: (lock.not.held)
	foo.field.toString();
	}

	if (tryToLockTheLock()) {
	foo.field.toString();
	} else {
	// :: error: (lock.not.held)
	foo.field.toString();
	}

	if (r.nextBoolean()) {
	lockTheLock();
	sideEffectFreeMethod();
	foo.field.toString();
	} else {
	lockTheLock();
	nonSideEffectFreeMethod();
	// :: error: (lock.not.held)
	foo.field.toString();
	}

	if (r.nextBoolean()) {
	lockTheLock();
	lockingFreeMethod();
	foo.field.toString();
	} else {
	lockTheLock();
	nonSideEffectFreeMethod();
	// :: error: (lock.not.held)
	foo.field.toString();
	}
	}

	void methodThatTakesAnInteger(Integer i) {}

	void testBoxedPrimitiveType() {
	Integer i = null;
	if (i == null) {}

	methodThatTakesAnInteger(i);
	}

	void testReceiverGuardedByItself(@GuardedBy("<self>") TestTreeKinds this) {
	// :: error: (lock.not.held)
	method();
	synchronized (this) {
	method();
	}
	}

	void method(@GuardSatisfied TestTreeKinds this) {}

	void testOtherClassReceiverGuardedByItself(final @GuardedBy("<self>") OtherClass o) {
	// :: error: (lock.not.held)
	o.foo();
	synchronized (o) {
	o.foo();
	}
	}

	class OtherClass {
	void foo(@GuardSatisfied OtherClass this) {}
	}

	void testExplicitLockSynchronized() {
	final ReentrantLock lock = new ReentrantLock();
	// :: error: (explicit.lock.synchronized)
	synchronized (lock) {
	}
	}

	void testPrimitiveTypeGuardedby() {
	// :: error: (immutable.type.guardedby)
	@GuardedBy("lock") int a = 0;
	// :: error: (immutable.type.guardedby)
	@GuardedBy int b = 0;
	// :: error: (immutable.type.guardedby) :: error: (guardsatisfied.location.disallowed)
	@GuardSatisfied int c = 0;
	// :: error: (immutable.type.guardedby) :: error: (guardsatisfied.location.disallowed)
	@GuardSatisfied(1) int d = 0;
	int e = 0;
	// :: error: (immutable.type.guardedby)
	@GuardedByUnknown int f = 0;
	// :: error: (immutable.type.guardedby) :: error: (assignment)
	@GuardedByBottom int g = 0;
	}

	void testBinaryOperatorBooleanResultIsAlwaysGuardedByNothing() {
	@GuardedBy("lock") Object o1 = new Object();
	Object o2 = new Object();
	// boolean variables are implicitly @GuardedBy({}).
	boolean b1 = o1 == o2;
	boolean b2 = o2 == o1;
	boolean b3 = o1 != o2;
	boolean b4 = o2 != o1;
	boolean b5 = o1 instanceof Object;
	boolean b6 = o2 instanceof Object;
	boolean b7 = o1 instanceof @GuardedBy("lock") Object;
	boolean b8 = o2 instanceof @GuardedBy("lock") Object;
	}
	}