import org.checkerframework.checker.lock.qual.GuardSatisfied;
import org.checkerframework.checker.lock.qual.GuardedBy;
import org.checkerframework.checker.lock.qual.GuardedByBottom;
import org.checkerframework.checker.lock.qual.GuardedByUnknown;

public class Strings {
  final Object lock = new Object();

  // These casts are safe because if the casted Object is a String, it must be @GuardedBy({})
  void StringIsGBnothing(
      @GuardedByUnknown Object o1,
      @GuardedBy("lock") Object o2,
      @GuardSatisfied Object o3,
      @GuardedByBottom Object o4) {
    String s1 = (String) o1;
    String s2 = (String) o2;
    String s3 = (String) o3;
    String s4 = (String) o4; // OK
  }

  // Tests that the resulting type of string concatenation is always @GuardedBy({})
  // (and not @GuardedByUnknown, which is the LUB of @GuardedBy({}) (the type of the
  // string literal "a") and @GuardedBy("lock") (the type of param))
  void StringConcat(@GuardedBy("lock") MyClass param) {
    {
      String s1a = "a" + "a";
      // :: error: (lock.not.held)
      String s1b = "a" + param;
      // :: error: (lock.not.held)
      String s1c = param + "a";
      // :: error: (lock.not.held)
      String s1d = param.toString();

      String s2 = "a";
      // :: error: (lock.not.held)
      s2 += param;

      String s3 = "a";
      // In addition to testing whether "lock" is held, tests that the result of a string
      // concatenation has type @GuardedBy({}).
      // :: error: (lock.not.held)
      String s4 = s3 += param;
    }
    synchronized (lock) {
      String s1a = "a" + "a";
      String s1b = "a" + param;
      String s1c = param + "a";
      String s1d = param.toString();

      String s2 = "a";
      s2 += param;

      String s3 = "a";
      // In addition to testing whether "lock" is held, tests that the result of a string
      // concatenation has type @GuardedBy({}).
      String s4 = s3 += param;
    }
  }

  class MyClass {
    Object field = new Object();
  }
}