The Checker Framework Manual:
Custom pluggable types for Java

enough

import org.checkerframework.checker.nullness.qual.*;

public class GetStarted {
    void sample() {
        @NonNull Object ref = new Object();
    }
}

  @NonNull Object ref = null;

GetStarted.java:5: incompatible types.
found   : @Nullable <nulltype>
required: @NonNull Object
        @NonNull Object ref = null;
                              ^
1 error

  @Interned String intern() { ... }             // return value
  int compareTo(@NonNull String other) { ... }  // parameter
  @NonNull List<@Interned String> messages;     // non-null list of interned Strings

  @Interned String intern() { ... }               // return value
  int compareTo(@NonNull String other) { ... }    // parameter
  String toString(@Tainted MyClass this) { ... }  // receiver ("this" parameter)
  @NonNull List<@Interned String> messages;       // generics:  non-null list of interned Strings
  @Interned String @NonNull [] messages;          // arrays:  non-null array of interned Strings
  myDate = (@Initialized Date) beingConstructed;  // cast

  javac -processor nullness MyFile.java
  javac -processor org.checkerframework.checker.nullness.NullnessChecker MyFile.java

  api group: 'org.apache.bcel', name: 'bcel', version: '6.3.1'
  api group: 'commons-io', name: 'commans-io', version: '2.8'

  api group: 'org.checkerframework.annotatedlib', name: 'bcel', version: '6.3.1'
  api group: 'org.checkerframework.annotatedlib', name: 'commons-io', version: '2.8.0.1'

    -ANullnessChecker_lint=redundantNullComparison
    -Aorg.checkerframework.checker.guieffect.GuiEffectChecker_lint=debugSpew

  org.checkerframework.checker.nullness.NullnessChecker
  org.checkerframework.checker.interning.InterningChecker

  javac -processor org.checkerframework.checker.nullness.NullnessChecker MyFile.java
  javac -processor NullnessChecker MyFile.java
  javac -processor nullness MyFile.java

  javac -processor NullnessChecker,RegexChecker MyFile.java
  javac -processor nullness,regex MyFile.java

  @Nullable Object x = ...;
  x.toString();                 // warning
  x.toString();                 // no warning

// The below code increments variable i by adding 1 to it.
i++;

  /** @throws NullPointerException if arg is null */
  void m1(Object arg) {
    arg.toString();
    ...
  }

  /** @throws NullPointerException if arg is null */
  void m2(Object arg) {
    Objects.requireNonNull(arg);
    ...
  }

  com.google.common.base.Preconditions.checkNotNull(Object)
  java.lang.Double.valueOf(String)
  java.lang.Objects.requireNonNull(Object)
  java.lang.String.contains(CharSequence)
  org.junit.Assert.assertNotNull(Object)
  org.junit.jupiter.api.Assert.assertNotNull(Object)

101  public interface Multiset<E> extends Collection<E> {
...
122    /**
123     * Adds a number of occurrences of an element to this multiset.
...
129     * @param element the element to add occurrences of; may be {@code null} only
130     *     if explicitly allowed by the implementation
...
137     * @throws NullPointerException if {@code element} is null and this
138     *     implementation does not permit null elements. Note that if {@code
139     *     occurrences} is zero, the implementation may opt to return normally.
140     */
141    int add(@Nullable E element, int occurrences);

  class MyNullPermittingMultiset implements Multiset<@Nullable Object> { ... }
  class MyNullProhibitingMultiset implements Multiset<@NonNull Object> { ... }

  class MyNullPermittingMultiset<E extends @Nullable Object> implements Multiset<E> { ... }
  class MyNullProhibitingMultiset<E extends @NonNull Object> implements Multiset<E> { ... }

  @NonNull myvar = unannotated_method();   // WARNING: unannotated_method may return null

  @Nullable Object   obj;  // might be null
  @NonNull  Object nnobj;  // never null
  ...
  obj.toString()         // checker warning:  dereference might cause null pointer exception
  nnobj = obj;           // checker warning:  nnobj may become null
  if (nnobj == null)     // checker warning:  redundant test

@DefaultQualifier(value = Nullable.class, locations = TypeUseLocation.FIELD)
class MyClass {
    Object nullableField = null;
    @NonNull Object nonNullField = new Object();
}

  class Class<T> {
    @EnsuresNonNullIf(expression="getComponentType()", result=true)
    public native boolean isArray();

    public native @Nullable Class<?> getComponentType();
  }

    if (clazz.isArray()) {
      // no possible null dereference on the following line
      TypeMirror componentType = typeFromClass(clazz.getComponentType());
      ...
    }

  Object [] oa = new Object[10];

  @MonotonicNonNull Object [] temp = new @MonotonicNonNull Object[10];
  for (int i = 0; i < temp.length; ++i) {
    temp[i] = new Object();
  }
  @SuppressWarnings("nullness") // temp array is now fully initialized
  @NonNull Object [] oa = temp;

    // might return null
    @Nullable Object getObject(...) { ... }

    void myMethod() {
      @SuppressWarnings("nullness") // with argument x, getObject always returns a non-null value
      @NonNull Object o2 = getObject(x);
    }

  // One way to use castNonNull as a cast:
  @NonNull String s = castNonNull(possiblyNull1);

  // Another way to use castNonNull as a cast:
  castNonNull(possiblyNull2).toString();

  // It is possible, but not recommmended, to use castNonNull as a statement:
  // (It would be better to write an assert statement with @AssumeAssertion
  // in its message, instead.)
  castNonNull(possiblyNull3);
  possiblyNull3.toString();

     ...
     * @param q the queue with which the reference is to be registered,
     *          or {@code null} if registration is not required
     */
    public WeakReference(@Nullable T referent, ReferenceQueue<? super T> q) {
      ...

  javac -processor org.checkerframework.checker.nullness.NullnessChecker docs/examples/NullnessExample.java

  javac -processor org.checkerframework.checker.nullness.NullnessChecker docs/examples/NullnessExampleWithWarnings.java

assert var != null : "@AssumeAssertion(nullness)";

     // declare getObject() to possibly return null
     @Nullable Object getObject() { ... }

     void myMethod() {
       @Nullable Object o = getObject();
       // SpotBugs issues no warning about calling toString on a possibly-null reference!
       o.toString();
     }

  public class MyClass {
    private @NonNull Object f;
    public MyClass(int x) {
      // Error because constructor contains no assignment to this.f.
      // By the time the constructor exits, f must be initialized to a non-null value.
    }
    public MyClass(int x, int y) {
      // Error because this.f is accessed before f is initialized.
      // At the beginning of the constructor's execution, accessing this.f
      // yields null, even though field f has a non-null type.
      this.f.toString();
      f = new Object();
    }
    public MyClass(int x, int y, int z) {
      m();
      f = new Object();
    }
    public void m() {
      // Error because this.f is accessed before f is initialized,
      // even though the access is not in a constructor.
      // When m is called from the constructor, accessing f yields null,
      // even though field f has a non-null type.
      this.f.toString();
    }

class C {
  @NonNull Object f;
  @Nullable Object g;
  ...
}

  class MyClass {
    Object field1;
    Object field2;
    Object field3;

    public MyClass(String arg1) {
      this.field1 = arg1;
      init_other_fields();
    }

    // A helper routine that initializes all the fields other than field1.
    @EnsuresNonNull({"field2", "field3"})
    private void init_other_fields(@UnderInitialization(Object.class) MyClass this) {
      field2 = new Object();
      field3 = new Object();
    }

    public MyClass(String arg1, String arg2, String arg3) {
      this.field1 = arg1;
      this.field2 = arg2;
      this.field3 = arg3;
      checkRep();
    }

    // Verify that the representation invariants are satisfied.
    // Works as long as the MyClass fields are initialized, even if the receiver's
    // class is a subclass of MyClass and not all of the subclass fields are initialized.
    private void checkRep(@UnderInitialization(MyClass.class) MyClass this) {
      ...
    }

  }

class A {
   @NonNull String a;
   public A() {
       a = "";
       // Now, all fields of A are initialized.
       // However, if this constructor is invoked as part of 'new B()', then
       // the fields of B are not yet initialized.
       // If we would type 'this' as @Initialized, then the following call is valid:
       doSomething();
   }
   void doSomething() {}
}

class B extends A {
   @NonNull String b;
   @Override
   void doSomething() {
       // Dereferencing 'b' is ok, because 'this' is @Initialized and 'b' @NonNull.
       // However, when executing 'new B()', this line throws a null-pointer exception.
       b.toString();
   }
}

class A {
  Object aField;
  A() {
    aField = new Object();
  }
}
class B extends A {
  Object bField;
  B() {
    super();
    bField = new Object();
  }
}

class A {
  Object aField;
  A() {
    aField = new Object();
  }
  Object get() {
    return aField;
  }
}
class B extends A {
  Object bField;
  B() {
    super();
    bField = new Object();
  }
  @Override
  Object get() {
    return bField;
  }
}

@Initialized A w;
@Initialized B x;
@UnderInitialization(A.class) A y;
@UnderInitialization(A.class) B z;

class A {
  Object aField;
  A() {
    aField = new Object();
    process(5);  // illegal call
  }
  public void process(int arg) { ... }
}

Client.java:7: error: [method.invocation.invalid] call to process(int) not allowed on the given receiver.
    process(5);  // illegal call
           ^
  found   : @UnderInitialization(A.class) A
  required: @Initialized A

class B extends A {
  List<Integer> processed;
  B() {
    super();
    processed = new ArrayList<Integer>();
  }
  @Override
  public void process(int arg) {
    super();
    processed.add(arg);
  }
}
class Client {
  public static void main(String[] args) {
    new B();
  }
}

  public void process(@UnderInitialization(A.class) A this, int arg) { ... }

  class List<T> {
    @NotOnlyInitialized
    Node<T> sentinel;

    public List() {
      this.sentinel = new Node<>(this);
    }

    void insert(@Nullable T data) {
      this.sentinel.insertAfter(data);
    }

    public static void main() {
      List<Integer> l = new List<>();
      l.insert(1);
      l.insert(2);
    }
  }

  class Node<T> {
    @NotOnlyInitialized
    Node<T> prev;

    @NotOnlyInitialized
    Node<T> next;

    @NotOnlyInitialized
    List parent;

    @Nullable
    T data;

    // for sentinel construction
    Node(@UnderInitialization List parent) {
      this.parent = parent;
      this.prev = this;
      this.next = this;
    }

    // for data node construction
    Node(Node<T> prev, Node<T> next, @Nullable T data) {
      this.parent = prev.parent;
      this.prev = prev;
      this.next = next;
      this.data = data;
    }

    void insertAfter(@Nullable T data) {
      Node<T> n = new Node<>(this, this.next, data);
      this.next.prev = n;
      this.next = n;
    }
  }

MyFile.java:123: error: call to initHelper() not allowed on the given receiver.
    initHelper();
              ^
  found   : @UnderInitialization(com.google.Bar.class) MyClass
  required: @Initialized MyClass

class MyClass {
  void initHelper(@UnknownInitialization MyClass this, String param1) { ... }
}

public class MyClass {
  @NonNull Object field;
  public MyClass() {
    field = new Object();
    helperMethod();
  }
  private void helperMethod() {
  }
}

MyClass.java:7: error: call to helperMethod() not allowed on the given receiver.
    helperMethod();
                ^
  found   : @UnderInitialization(MyClass.class) MyClass
  required: @Initialized MyClass
1 error

public class Graph<N> {
  Map<N, Integer> nodes = new HashMap<>();
}

class Client {
  @Nullable Graph<@KeyFor("g.nodes") String> g;
}

Graph.java:14: error: [type.argument.type.incompatible] incompatible types in type argument.
  @Nullable Graph<@KeyFor("g.nodes") String> g;
                  ^
  found   : @KeyFor("this.g.nodes") String
  required: [extends @UnknownKeyFor Object super @UnknownKeyFor null]

public class Graph<@KeyForBottom N> {
...

Map<String,Date> m, n;
@KeyFor("m") String km;
@KeyFor("n") String kn;
@KeyFor({"m", "n"}) String kmn;
km = kmn;   // OK - a key for maps m and n is also a key for map m
km = kn;    // error: a key for map n is not necessarily a key for map m

Map<String,Object> m;
Collection<@KeyFor("m") String> coll;
coll.add(x);   // error: element type is @KeyFor("m") String, but x does not have that type
m.put(x, ...);

Map<String,Object> m;
Collection<@KeyFor("m") String> coll;
m.put(x, ...);    // after this statement, x has type @KeyFor("m") String
coll.add(x);      // OK

Map<String,Date> m = new Map<>();
String k = "key";
@KeyFor("m") String km;

km = k;   // Error since k is not known to be a key for map m.

m.put(k, ...);
// At this point, the type of k is refined to @KeyFor("m") String.
km = k;   // OK

if (m.containsKey(k)) {
    // At this point, the type of k is refined to @KeyFor("m") String.
    km = k;   // OK
    ...
} else {
    km = k;   // Error since k is not known to be a key for map m.
    ...
}

class MyClass {
    private Map<String,Object> m;
    private String k;   // The type of k defaults to @UnknownKeyFor String
    private @KeyFor("m") String km;

    public void myMethod() {
        if (m.containsKey(k)) {
            km = k;   // OK: the type of k is refined to @KeyFor("m") String

            sideEffectFreeMethod();
            km = k;   // OK: the type of k is not affected by the method call
                      // and remains @KeyFor("m") String

            otherMethod();
            km = k;   // error: At this point, the type of k is once again
                      // @UnknownKeyFor String, because otherMethod might have
                      // side-effected k such that it is no longer a key for map m.
        }
    }

    @SideEffectFree
    private void sideEffectFreeMethod() { ... }

    private void otherMethod() { ... }
}

javac -processor optional MyFile.java ...
javac -processor org.checkerframework.checker.optional.OptionalChecker MyFile.java ...

    // might return a possibly-empty Optional
    Optional<T> wrapWithOptional(...) { ... }

    void myMethod() {
      @SuppressWarnings("optional") // with argument x, wrapWithOptional always returns a non-empty Optional
      @Present Optional<T> optX = wrapWithOptional(x);
    }

  // One way to use castPresent as a cast:
  @Present Optional<String> optString = castPresent(possiblyEmpty1);

  // Another way to use castPresent as a cast:
  castPresent(possiblyEmpty2).toString();

  // It is possible, but not recommmended, to use castPresent as a statement:
  // (It would be better to write an assert statement with @AssumeAssertion
  // in its message, instead.)
  castPresent(possiblyEmpty3);
  possiblyEmpty3.toString();

  Integer x = new Integer(22);
  Integer y = new Integer(22);
  System.out.println(x == y);  // prints false!

            String s1 = ...;  // type is (uninterned) "String"
  @Interned String s2 = ...;  // type is "@Interned String"

@Interned class InternedClass {
  @UnknownInterned InternedClass() {
    // error, "this" is @UnknownInterned.
    @Interned InternedClass that = this;
  }

  @SuppressWarnings("intern") // Only creation of an InternedClass object.
  static final InternedClass ONE = new InternedClass();
}

new InternedClass().intern() // no error

@InternMethod
public InternedClass intern() {
  // Type of "this" inside an @InternMethod is @UnknownInterned
  @Interned InternedClass that = this; // error

  if (!pool.contains(this)) {
    @SuppressWarnings("interning:assignment.type.incompatible")
    @Interned InternedClass internedThis = this;
    pool.add(internedThis);
  }
  return pool.get(this);
}

@Interned class AnotherInternedClass {
  // manually verified that all constructor invocations used such that all
  // new objects are interned
  @SuppressWarnings("super.invocation.invalid")
  @Interned AnotherInternedClass() {}
}

@Interned String i = "22";
          String s = new Integer(22).toString();

class MyType {
  final static @InternedDistinct MyType SPECIAL = new MyType(...);
  ...
}

                    Date  date;
          @Interned Date idate;
  @InternedDistinct Date ddate;
  ...
  if (date == idate) ...  // error: reference equality test is unsafe
  idate = date;           // error: idate's referent might no longer be interned
  ddate = idate;          // error: idate's referent might be equals() to some other value

MyFile.java:716: error: [interning:not.interned] attempting to use a non-@Interned comparison operand
        if (date == idate)
            ^

  javac -processor org.checkerframework.checker.interning.InterningChecker docs/examples/InterningExample.java

  javac -processor org.checkerframework.checker.interning.InterningChecker docs/examples/InterningExampleWithWarnings.java

javac -processor calledmethods MyFile.java ...
javac -processor org.checkerframework.checker.calledmethods.CalledMethodsChecker MyFile.java ...

  class MyObjectBuilder {
    MyObject build(@CalledMethods({"setX", "setY"}) MyObjectBuilder this) { ... }
  }

    class MyObjectSubBuilder extends MyObjectBuilder {
      @Override
      MyObject build(@CalledMethods({"setX", "setY"}) MyObjectSubBuilder this) {
        MyObject o = super.build();
        if ((o.getX() == null) != (o.getY() == null)) {
          throw new IllegalArgumentException("Nullness for x and y should be equal");
        }
        return o;
      }
    }

      class MyObjectBuilder {

        @This
        MyObjectBuilder setXMod42(int x) {
          return setX(x % 42);
        }
      }

    @EnsuresCalledMethods(value = "#1", methods = {"x", "y"})
    void m(Param p) { ... }

  @EnsuresCalledMethods(value="#1", methods="close")
  public void closeSocket(Socket sock) throws IOException {
      sock.close();
      m();
  }

    @EnsuresCalledMethodsIf(expression = "#1", methods = {"x", "y"}, result=true)
    boolean m(Param p) { ... }

    @EnsuresCalledMethods(expression = "#1", methods = {"close"})
    @EnsuresCalledMethodsOnException(expression = "#1", methods = {"close"})
    void closeIfNonNull(Closeable p) {
      if (p != null) {
        p.close();
      }
    }

javac -processor resourceleak MyFile.java ...
javac -processor org.checkerframework.checker.resourceleak.ResourceLeakChecker MyFile.java ...

{
  Socket s = null;
  // 1. @MustCall({}) @CalledMethodsBottom
  try {
    s = new Socket(myHost, myPort);
    // 2. @MustCall("close") @CalledMethods({})
  } catch (Exception e) {
    // do nothing
  } finally {
    if (s != null) {
      s.close();
      // 3. @MustCall("close") @CalledMethods("close")
    } else {
      // do nothing
      // 4. @MustCall("close") @CalledMethodsBottom
    }
    // 5. @MustCall("close") @CalledMethods("close")
  }
  // 6. @MustCall("close") @CalledMethods("close")
}

  void example(String myHost, int myPort) throws IOException {
    Socket s = new Socket(myHost, myPort);
    closeSocket(s);
  }
  void closeSocket(@Owning @MustCall("close") Socket t) {
    try {
      t.close();
    } catch (IOException e) {
      e.printStackTrace();
    }
  }

  void example(String myHost, int myPort) throws Exception {
    // Error: `s` is not closed on all paths
    Socket s = new Socket(myHost, myPort);

    // `closeSocket` does not have to close `s` when it throws IOException.
    // Instead, this method has to catch the exception and close `s`.
    closeSocket(s);
  }

  void closeSocket(@Owning Socket t) throws IOException {
    throw new IOException();
  }

  @EnsuresCalledMethodsOnException(value = "#1", methods = "close")
  public Constructor(@Owning Closeable resource) {
    this.resource = resource;
    try {
      initialize();
    } catch (Exception e) {
      resource.close();
      throw e;
    }
  }

  private final @Owning Socket socket;

  public ConstructorThatCanThrow() throws IOException {
    Socket s = new Socket(myHost, myPort);
    try {
      initialize(s); // may throw IOException
    } catch (Exception e) {
      s.close();
      throw e;
    }
    this.socket = s;
  }

  static @Owning PrintWriter debugLog = new PrintWriter("debug.log");

@MustCallAlias BufferedOutputStream(@MustCallAlias OutputStream out);

  @MustCall("close") // default qualifier for uses of SocketContainer
  class SocketContainer {
    private @Owning Socket sock;

    public SocketContainer() { sock = ...; }

    void close() { sock.close() };

    @CreatesMustCallFor("this")
    void reconnect() {
      if (!sock.isClosed()) {
        sock.close();
      }
      sock = ...;
    }
  }

  void foo() {
    Socket s = ...;
    bar();
    s.close();
  }

  -AresourceLeakIgnoredExceptions=java.lang.Error, =java.lang.NullPointerException

  -AresourceLeakIgnoredExceptions=default,package.MyCustomException

@NavigationMode int NAVIGATION_MODE_STANDARD = 0;
@NavigationMode int NAVIGATION_MODE_LIST = 1;
@NavigationMode int NAVIGATION_MODE_TABS = 2;

@NavigationMode int getNavigationMode();

void setNavigationMode(@NavigationMode int mode);

package myPackage.qual;

import java.lang.annotation.Documented;
import java.lang.annotation.ElementType;
import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
import org.checkerframework.checker.fenum.qual.FenumTop;
import org.checkerframework.framework.qual.SubtypeOf;

@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(FenumTop.class)
public @interface MyFenum {}

  javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \
        -processor org.checkerframework.checker.fenum.FenumChecker \
        -Aquals=myPackage.qual.MyFenum MyFile.java ...

  javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \
        -processor org.checkerframework.checker.fenum.FenumChecker \
        -AqualDirs=/full/path/to/myProject/bin:/full/path/to/myLibrary/bin MyFile.java ...

  .../myProject/bin/myPackage/qual/MyFenum.class

  javac -processor org.checkerframework.checker.fenum.FenumChecker MyFile.java ...

@SuppressWarnings("fenum:assignment.type.incompatible") // initialization of fake enums
class MyConsts {
  public static final @Fenum("A") int ACONST1 = 1;
  public static final @Fenum("A") int ACONST2 = 2;
}

@SuppressWarnings("fenum:assignment.type.incompatible")   // initialization of fake enums
public class TestStatic {
  public static final @Fenum("A") int ACONST1 = 1;
  public static final @Fenum("A") int ACONST2 = 2;

  public static final @Fenum("B") int BCONST1 = 4;
  public static final @Fenum("B") int BCONST2 = 5;
}

class FenumUser {
  @Fenum("A") int state1 = TestStatic.ACONST1;     // ok
  @Fenum("B") int state2 = TestStatic.ACONST1;     // Incompatible fenums forbidden!

  void fenumArg(@Fenum("A") int p) {}

  void fenumTest() {
    state1 = 4;                     // Direct use of value forbidden!
    state1 = TestStatic.BCONST1;    // Incompatible fenums forbidden!
    state1 = TestStatic.ACONST2;    // ok

    fenumArg(5);                    // Direct use of value forbidden!
    fenumArg(TestStatic.BCONST1);   // Incompatible fenums forbidden!
    fenumArg(TestStatic.ACONST1);   // ok
  }
 }

  public boolean execute(@Untainted String sql) throws SQLException;
  public boolean executeUpdate(@Untainted String sql) throws SQLException;

  public StringBuffer append(StringBuffer this, String toAppend);

  @Tainted StringBuffer tsb;
  @Tainted String ts;
  @Untainted StringBuffer usb;
  @Untainted String us;

  tsb.append(ts);
  usb.append(us);

  // UNSOUND annotation -- do not do this!
  public @PolyTainted StringBuffer append(@PolyTainted StringBuffer this, @PolyTainted String toAppend);

  usb.append(ts); // illegal invocation

  @MayReleaseLocks
  @ReleasesNoLocks
  @LockingFree
  @SideEffectFree
  @Pure

class MyClass {
  final ReentrantLock lock; // Initialized in the constructor

  @GuardedBy("lock") Object x = new Object();
  @GuardedBy("lock") Object y = x; // OK, since dereferences of y will require "lock" to be held.
  @GuardedBy({}) Object z = x; // ILLEGAL since dereferences of z don't require "lock" to be held.
  @GuardedBy("lock") Object myMethod() { // myMethod is implicitly annotated with @ReleasesNoLocks.
     return x; // OK because the return type is annotated with @GuardedBy("lock")
  }

  [...]

  void exampleMethod() {
     x.toString(); // ILLEGAL because the lock is not known to be held
     y.toString(); // ILLEGAL because the lock is not known to be held
     myMethod().toString(); // ILLEGAL because the lock is not known to be held
     lock.lock();
     x.toString();  // OK: the lock is known to be held
     y.toString();  // OK: the lock is known to be held, and toString() is annotated with @SideEffectFree.
     myMethod().toString(); // OK: the lock is known to be held, since myMethod
                            // is implicitly annotated with @ReleasesNoLocks.
  }
}

class MyClass {
  private final @GuardedBy("<self>") Object x = new Object();
  void method() {
    x.toString(); // ILLEGAL because x is not known to be held.
    synchronized(x) {
      x.toString(); // OK: x is known to be held.
    }
  }

  public @GuardedBy("<self>") Object get_x() {
    return x; // OK, since the return type is @GuardedBy("<self>").
  }
}

class MyOtherClass {
  void method() {
    MyClass m = new MyClass();
    final @GuardedBy("<self>") Object o = m.get_x();
    o.toString(); // ILLEGAL because o is not known to be held.
    synchronized(o) {
      o.toString(); // OK: o is known to be held.
    }
  }
}

class MyClass {
    final Object lockA = new Object();
    final Object lockB = new Object();
    @GuardedBy("lockA") Object x = new Object();
    @GuardedBy({"lockA", "lockB"}) Object y = new Object();
    void myMethod() {
        y = x;      // ILLEGAL; if legal, later statement x.toString() would cause trouble
        synchronized(lockA) {
          x.toString();  // dereferences y's value without holding lock lockB
        }
    }
}

  void helper1(@GuardedBy("myLock") Object a) {
    a.toString(); // ILLEGAL: the lock is not held
    synchronized(myLock) {
      a.toString();  // OK: the lock is held
    }
  }
  @Holding("myLock")
  void helper2(@GuardedBy("myLock") Object b) {
    b.toString(); // OK: the lock is held
  }
  void helper3(@GuardedBy("myLock") Object d) {
    d.toString(); // ILLEGAL: the lock is not held
  }
  void myMethod2(@GuardedBy("myLock") Object e) {
    helper1(e);  // OK to pass to another routine without holding the lock
                 // (but helper1's body has an error)
    e.toString(); // ILLEGAL: the lock is not held
    synchronized (myLock) {
      helper2(e); // OK: the lock is held
      helper3(e); // OK, but helper3's body has an error
    }
  }

package java.util.concurrent.locks;

class ReentrantLock {

    @EnsuresLockHeld("this")
    public void lock();

    @EnsuresLockHeldIf(expression="this", result=true)
    public boolean tryLock();

    ...
}

public class Monitor {

    private final ReentrantLock lock; // Initialized in the constructor

    ...

    @EnsuresLockHeld("lock")
    public void enter() {
       lock.lock();
    }

    ...
}

private Object myField;
private final ReentrantLock lock; // Initialized in the constructor
private @GuardedBy("lock") Object x; // Initialized in the constructor

[...]

// This method does not use locks or synchronization, but it cannot
// be annotated as @SideEffectFree since it alters myField.
@LockingFree
void myMethod() {
  myField = new Object();
}

@SideEffectFree
int mySideEffectFreeMethod() {
  return 0;
}

@MayReleaseLocks
void myUnlockingMethod() {
  lock.unlock();
}

@ReleasesNoLocks
void myLockingMethod() {
  lock.lock();
}

@MayReleaseLocks
void clientMethod() {
  if (lock.tryLock()) {
    x.toString(); // OK: the lock is held
    myMethod();
    x.toString(); // OK: the lock is still held since myMethod is locking-free
    mySideEffectFreeMethod();
    x.toString(); // OK: the lock is still held since mySideEffectFreeMethod is side-effect-free
    myUnlockingMethod();
    x.toString(); // ILLEGAL: myUnlockingMethod may have released a lock
  }
  if (lock.tryLock()) {
    x.toString(); // OK: the lock is held
    myLockingMethod();
    x.toString(); // OK: the lock is held
  }
  if (lock.isHeldByCurrentThread()) {
    x.toString(); // OK: the lock is known to be held
  }
}

@LockingFree
public @GuardSatisfied(1) StringBuffer append(@GuardSatisfied(1) StringBuffer this,
                                              @GuardSatisfied(2) String str)

final ReentrantLock lock1, lock2; // Initialized in the constructor
@GuardedBy("lock1") StringBuffer filename;
@GuardedBy("lock2") StringBuffer extension;
...
lock1.lock();
lock2.lock();
filename = filename.append(extension);

  @Holding("myLock")
  void myMethod() {
    ...
  }

  void myMethod() {
    synchronized (myLock) {   // no-op:  re-acquire a lock that is already held
      ...
    }
  }

  javac -processor index MyJavaFile.java
  javac -processor org.checkerframework.checker.index.IndexChecker MyJavaFile.java

  @Positive int @ArrayLen(9) []

  String @ArrayLen(2) [] @ArrayLen(4) []

  class String {
    char charAt(@IndexFor("this") index) { ... }
  }

  class Arrays {
    void fill(Object[] a, @IndexFor("#1") int fromIndex, @IndexOrHigh("#1") int toIndex, Object val)
  }

  for (int i = 0; i < array.length - 1; ++i) {
    arr[i] = arr[i+1];
  }

  int start;
  int end;
  int[] shorter;
  @HasSubsequence(value="shorter", from="this.start", to="this.end")
  int[] longer;

  String getThirdElement(String[] arr) {
    return arr[2];
  }

  String getThirdElement(String @MinLen(3) [] arr) {
    return arr[2];
  }

  String getThirdElement(String @ArrayLen(3) [] arr) {
    return arr[2];
  }

  boolean lessThan(double[] arr1, double @SameLen("#1") [] arr2) {
    for (int i = 0; i < arr1.length; i++) {
      if (arr1[i] < arr2[i]) {
        return true;
      } else if (arr1[i] > arr2[i]) {
        return false;
      }
    }
    return false;
  }

 i == -1 || ( i >= 0       && i <= receiver.length() - substring.length()                  )
 i == -1 || ( @NonNegative && @LTLengthOf(value="receiver", offset="substring.length()-1") )
 @SubstringIndexFor(value="receiver", offset="substring.length()-1")

  public static String removeSubstring(String original, String removed) {
    int i = original.indexOf(removed);
    if (i != -1) {
      return original.substring(0, i) + original.substring(i + removed.length());
    }
    return original;
  }

  int i = receiver.indexOf(substring);
  // i is @GTENegativeOne and @LTEqLengthOf("receiver")
  // i is not @LTLengthOf(value = "receiver", offset = "substring.length()-1")
  if (i != -1) {
    // i is @NonNegative and @LTLengthOf(value = "receiver", offset = "substring.length()-1")
    int j = i + substring.length();
    // j is @IndexOrHigh("receiver")
    return receiver.substring(j); // this call is safe
  }

/** ArrayWrapper is a fixed-size generic collection. */
public class ArrayWrapper<T> {
    private final Object @SameLen("this") [] delegate;

    @SuppressWarnings("index") // constructor creates object of size @SameLen(this) by definition
    ArrayWrapper(@NonNegative int size) {
        delegate = new Object[size];
    }

    public @LengthOf("this") int size() {
        return delegate.length;
    }

    public void set(@IndexFor("this") int index, T obj) {
        delegate[index] = obj;
    }

    @SuppressWarnings("unchecked") // required for normal Java compilation due to unchecked cast
    public T get(@IndexFor("this") int index) {
        return (T) delegate[index];
    }
}

    public static void clearIndex1(ArrayWrapper<? extends Object> a, @IndexFor("#1") int i) {
        a.set(i, null);
    }

    public static void clearIndex2(ArrayWrapper<? extends Object> a, int i) {
        if (0 <= i && i < a.size()) {
            a.set(i, null);
        }
    }

public @Regex String parenthesize(@Regex String regex) {
    return "(" + regex + ")"; // Even though the parentheses are not @Regex Strings,
                              // the whole expression is a @Regex String
}

String regex = getRegexFromUser();
if (! RegexUtil.isRegex(regex)) {
   throw new RuntimeException("Error parsing regex " + regex, RegexUtil.regexException(regex));
}
Pattern p = Pattern.compile(regex);

  String.format("%y", 7);           // error: invalid format string

  String.format("%d", "a string");  // error: invalid argument type for %d

  String.format("%d %s", 7);        // error: missing argument for %s
  String.format("%d", 7, 3);        // warning: unused argument 3
  String.format("{0}", 7);          // warning: unused argument 7, because {0} is wrong syntax

    void printFloatAndInt(@Format({FLOAT, INT}) String fs) {
        System.out.printf(fs, 3.1415, 42);
    }

    printFloatAndInt("Float %f, Number %d");  // OK
    printFloatAndInt("Float %f");             // error

    String.format("%d", 5);         // OK
    String.format("%d", "hello");   // error

    format("Char %1$c, Int %1$d", (int)42);            // OK
    format("Char %1$c, Int %1$d", new Character(42));  // error
    format("Char %1$c, Int %1$d", (long)42);           // error

    @Format({FLOAT, INT}) String f;

    f = "%f %d";       // OK
    f = "%s %d";       // OK, %s is weaker than %f
    f = "%f";          // warning: last argument is ignored
    f = "%f %d %s";    // error: too many arguments
    f = "%d %d";       // error: %d is not weaker than %f

    String.format(f, 0.8, 42);

    String.format("%d", 42);                      // OK
    String.format(Locale.GERMAN, "%d", 42);       // OK
    String.format(new Object());                  // error (1a)
    String.format("%y");                          // error (1a)
    String.format("%2$s", "unused", "used");      // warning (1b)
    String.format("%1$d %1$f", 5.5);              // error (1c)
    String.format("%1$d %1$f %d", null, 6);       // error (1c)
    String.format("%s");                          // error (2a)
    String.format("%s", "used", "ignored");       // warning (2b)
    String.format("%c",4.2);                      // error (2c)
    String.format("%c", (String)null);            // error (2c)
    String.format("%1$d %1$f", new Object[]{1});  // warning (3)
    String.format("%s", new Object[]{"hello"});   // warning (3)

    class A {
        public String toString() {
            throw new Error();
        }
    }

    class B implements Formattable {
        public void formatTo(Formatter fmt, int f,
                int width, int precision) {
            throw new Error();
        }
    }

    // The checker issues no errors or warnings for the
    // following illegal invocations of format methods.
    String.format(null);          // NullPointerException (1)
    String.format("%s", new A()); // Error (2)
    String.format("%s", new B()); // Error (3)
    String.format("%c", (int)-1); // IllegalFormatCodePointException (4)

@FormatMethod
void log(String format, Object... args) {
    if (enabled) {
        logfile.print(indent_str);
        logfile.printf(format , args);
    }
}

Scanner s = new Scanner(System.in);
String fs = s.next();
System.out.printf(fs, "hello", 1337);          // error: fs is not known to be a format string

Scanner s = new Scanner(System.in);
@Format({GENERAL, INT}) String fs = s.next();  // error: fs is not known to have the given type
System.out.printf(fs, "hello", 1337);          // OK

Scanner s = new Scanner(System.in);
String format = s.next()
try {
    format = FormatUtil.asFormat(format, GENERAL, INT);
} catch (IllegalFormatException e) {
    // Replace this by your own error handling.
    System.err.println("The user entered the following invalid format string: " + format);
    System.exit(2);
}
// fs is now known to be of type: @Format({GENERAL, INT}) String
System.out.printf(format, "hello", 1337);

  // Warning: the second argument is missing.
  MessageFormat.format("{0} {1}", 3.1415);
  // String argument cannot be formatted as Time type.
  MessageFormat.format("{0, time}", "my string");
  // Invalid format string: unknown format type: thyme.
  MessageFormat.format("{0, thyme}", new Date());
  // Invalid format string: missing the right brace.
  MessageFormat.format("{0", new Date());
  // Invalid format string: the argument index is not an integer.
  MessageFormat.format("{0.2, time}", new Date());
  // Invalid format string: "#.#.#" subformat is invalid.
  MessageFormat.format("{0, number, #.#.#}", 3.1415);

  static void method(@I18nFormatFor("#2") String format, Object... args) {
    // the body may use the parameters like this:
    MessageFormat.format(format, args);
  }

  method("{0, number} {1}", 3.1415, "A string");  // OK
  // error: The string "hello" cannot be formatted as a Number.
  method("{0, number} {1}", "hello", "goodbye");

  @I18nFormat({NUMBER, DATE}) String f;

  f = "{0, number, #.#} {1, date}"; // OK
  f = "{0, number} {1}";            // OK, GENERAL is weaker (less restrictive) than DATE
  f = "{0} {1, date}";              // OK, GENERAL is weaker (less restrictive) than NUMBER
  f = "{0, number}";                // warning: last argument is ignored
  f = "{0}";                        // warning: last argument is ignored
  f = "{0, number} {1, number}";    // error: NUMBER is stronger (more restrictive) than DATE
  f = "{0} {1} {2}";                // error: too many arguments

  @I18nFormat({GENERAL, NUMBER}) String format;
  // OK.
  format = "{0} {1, number}";
  // OK, GENERAL is weaker (less restrictive) than NUMBER.
  format = "{0} {1}";
  // OK, it is legal to have fewer arguments than required (less restrictive).
  // But the warning will be issued instead.
  format = "{0}";

  // Error, the format string is stronger (more restrictive) than the specifiers.
  format = "{0} {1} {2}";
  // Error, the format string is more restrictive. NUMBER is a subtype of GENERAL.
  format = "{0, number} {1, number}";

  key1 = The number is {0, number}.

  String formatPattern = ResourceBundle.getBundle("resource1").getString("key1");
  System.out.println(MessageFormat.format(formatPattern, 2.2361));

      // suppose the bundle "MyResource" contains:  key1={0, number} {1, date}
      String value = ResourceBundle.getBundle("MyResource").getString("key1");
      MessageFormat.format(value, 3.14, new Date());  // OK
      // error: incompatible types in argument; found String, expected number
      MessageFormat.format(value, "Text", new Date());

      void test1(String format) {
        if (I18nFormatUtil.hasFormat(format, I18nConversionCategory.GENERAL,
                                             I18nConversionCategory.NUMBER)) {
          MessageFormat.format(format, "Hello", 3.14);  // OK
          // error: incompatible types in argument; found String, expected number
          MessageFormat.format(format, "Hello", "Bye");
          // error: missing arguments; expected 2 but 1 given
          MessageFormat.format(format, "Bye");
          // error: too many arguments; expected 2 but 3 given
          MessageFormat.format(format, "A String", 3.14, 3.14);
        }
      }

      static void method(@I18nFormatFor("#2") String f, Object... args) {...}

      // OK, MessageFormat.format(...) would return "3.14 Hello greater than one"
      method("{0, number} {1} {2, choice,0#zero|1#one|1<greater than one}",
             3.14, "Hello", 100);

      // error: incompatible types in argument; found String, expected number
      method("{0, number} {1}", "Bye", "Bye");

      @I18nFormat({I18nConversionCategory.DATE}) String;
      s1 = "{0}";
      s1 = "{0, number}";        // error: incompatible types in assignment

  javac -processor org.checkerframework.checker.propkey.PropertyKeyChecker
        -Abundlenames=MyResource MyFile.java ...

  javac -processor org.checkerframework.checker.i18n.I18nChecker -Abundlenames=MyResource MyFile.java ...

  javac -processor org.checkerframework.checker.compilermsgs.CompilerMessagesChecker
        -Apropfiles=messages.properties MyFile.java ...

    Object mymethod(int i, double d, Thread t)

    (IDLjava/lang/Thread;)Ljava/lang/Object;

@SafeEffect
public void calledFromBackgroundThreads(JLabel l) {
    l.setText("Foo");       // Error: calling a @UIEffect method from a @SafeEffect method
    Display.syncExec(new Runnable {
        @UIEffect // inferred by default
        public void run() {
            l.setText("Bar");  // OK: accessing JLabel from code run on the UI thread
        }
    });

}

  javac -processor org.checkerframework.checker.guieffect.GuiEffectChecker MyFile.java ...

@PolyUIType
public interface Runnable {
    @PolyUIEffect
    void run();
}

@AlwaysSafe Runnable s = ...;    s.run();    // s.run() is @SafeEffect
@PolyUI Runnable p = ...;        p.run();    // p.run() is @PolyUIEffect (context-dependent)
@UI Runnable u = ...;            u.run();    // u.run() is @UIEffect

@UI
public class UIRunnable extends Runnable {...}
@AlwaysSafe
public class SafeRunnable extends Runnable {...}

public @PolyUI Runnable id(@PolyUI Runnable r) {
    return r;
}

@PolyUIType
public interface Dispatcher {
    @PolyUIEffect
    void dispatch(@PolyUI Runnable toRun);
}
@SafeType
public class SafeDispatcher implements Dispatcher {
    @Override
    public void dispatch(@AlwaysSafe Runnable toRun) {
        runOnBackgroundThread(toRun);
    }
}

@AlwaysSafe SafeDispatcher s = ...;
@UI Runnable uitask = ...;
s.dispatch(uitask);

@m int meters = 5 * UnitsTools.m;
@s int secs = 2 * UnitsTools.s;
@mPERs int speed = meters / secs;

@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf({Time.class})
@UnitsMultiple(quantity=s.class, prefix=Prefix.nano)
public @interface ns {}

  javac -processor org.checkerframework.checker.units.UnitsChecker MyFile.java ...

  javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \
        -processor org.checkerframework.checker.units.UnitsChecker \
        -Aunits=myPackage.qual.MyUnit,myPackage.qual.MyOtherUnit MyFile.java ...

  javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \
        -processor org.checkerframework.checker.units.UnitsChecker \
        -AunitsDirs=/full/path/to/myProject/bin:/full/path/to/myLibrary/bin MyFile.java ...

  .../myProject/bin/myPackage/qual/MyUnit.class
  .../myProject/bin/myPackage/qual/MyOtherUnit.class

public class SignednessManualExample {

    int s1 = -2;
    int s2 = -1;

    @Unsigned int u1 = 2147483646; // unsigned: 2^32 - 2, signed: -2
    @Unsigned int u2 = 2147483647; // unsigned: 2^32 - 1, signed: -1

    void m() {
        int w = s1 / s2; // OK: result is 2, which is correct for -2 / -1
        int x = u1 / u2; // ERROR: result is 2, which is incorrect for (2^32 - 2) / (2^32 - 1)
    }

    int s3 = -1;
    int s4 = 5;

    @Unsigned int u3 = 2147483647; // unsigned: 2^32 - 1, signed: -1
    @Unsigned int u4 = 5;

    void m2() {
        int y = s3 % s4; // OK: result is -1, which is correct for -1 % 5
        int z = u3 % u4; // ERROR: result is -1, which is incorrect for (2^32 - 1) % 5 = 2
    }
}

    void useLocalVariables() {

        int s1 = -2;
        int s2 = -1;

        @Unsigned int u1 = 2147483646; // unsigned: 2^32 - 2, signed: -2
        @Unsigned int u2 = 2147483647; // unsigned: 2^32 - 1, signed: -1

        int w = s1 / s2; // OK: result is 2, which is correct for -2 / -1
        int x = u1 / u2; // OK; computation over constants, interpreted as signed; result is signed
    }

        @Unsigned int u1 = (@Unsigned int) 2147483646;

MyClass.java:1465: error: int hashCode() in MyClass cannot override int hashCode(Object this) in java.lang.Object;
attempting to use an incompatible purity declaration
    public int hashCode() {
               ^
  found   : []
  required: [SIDE_EFFECT_FREE, DETERMINISTIC]

class Object {
  ...
  @Pure int hashCode() { ... }
}

public void flowSensitivityExample(boolean b) {
    int i = 1;     // i has type:  @IntVal({1}) int
    if (b) {
        i = 2;     // i now has type:  @IntVal({2}) int
    }
                   // i now has type:  @IntVal({1,2}) int
    i = i + 1;     // i now has type:  @IntVal({2,3}) int
}

@StaticallyExecutable @Pure
public static int myAdd(int a, int b) {
    return a + b;
}

public void bar() {
    int a = 5;            // a has type:  @IntVal({5}) int
    int b = 4;            // b has type:  @IntVal({4}) int
    int c = myAdd(a, b);  // c has type:  @IntVal({9}) int
}

  -processor org.checkerframework.common.value.ValueChecker
  -classpath $CLASSPATH:MY_PROJECT/build/

  -processor org.checkerframework.common.value.ValueChecker
  -processorpath ${CHECKERFRAMEWORK}/checker/build/libs/checker-3.6.1-SNAPSHOT.jar:MY_PROJECT/build/

  ...
  if (i > 5) {
    // i now has type:  @IntRange(from=5, to=Integer.MAX_VALUE)
    i = i + 1;
    // If i started out as Integer.MAX_VALUE, then i is now Integer.MIN_VALUE.
    // i's type is now @IntRange(from=Integer.MIN_VALUE, to=Integer.MAX_VALUE).
    // When ignoring overflow, i's type is now @IntRange(from=6, to=Integer.MAX_VALUE).
  }

class MyBuilder {
  @This MyBuilder setName(String name) {
    this.name = name;
    return this;
  }
}

@AutoValue
abstract class Animal {
  abstract String name();
  abstract int numberOfLegs();
  static Builder builder() {
    return new AutoValue_Animal.Builder();
  }
  @AutoValue.Builder
  abstract static class Builder {
    abstract Builder setName(String value);       // @This is automatically added here
    abstract Builder setNumberOfLegs(int value);  // @This is automatically added here
    abstract Animal build();
  }
}

    class AutoValue_Animal {
      static final class Builder extends Animal.Builder {
        private String name;
        private Integer numberOfLegs;
        @This Animal.Builder setName(String name) {
          this.name = name;
          return this;
        }
        @This Animal.Builder setNumberOfLegs(int numberOfLegs) {
          this.numberOfLegs = numberOfLegs;
          return this;
        }
        @Override
        Animal build() {
          return new AutoValue_Animal(this.name, this.numberOfLegs);
        }
      }
    }

public class LocationInfo {
    @NonNull Location getCurrentLocation() {  ...  }
}

public class Example {
    LocationInfo privateLocation = ... ;
    String getCurrentCity() throws Exception {
        Method getCurrentLocationObj = LocationInfo.class.getMethod("getCurrentLocation");
        Location currentLocation = (Location) getCurrentLocationObj.invoke(privateLocation);
        return currentLocation.nameOfCity();
    }
}

error: [dereference.of.nullable] dereference of possibly-null reference currentLocation
        return currentLocation.nameOfCity();
               ^
1 error

@MethodVal(className={"java.util.HashMap", "java.util.HashMap"},
           methodName={"containsKey", "containsValue"},
           params={1, 1})

javac -processor org.checkerframework.common.initializedfields.InitializedFieldsChecker MyFile.java

javac -processor ValueChecker,InitializedFieldsChecker MyFile.java

import org.checkerframework.checker.index.qual.Positive;

class MyClass {
  @Positive int x;
  MyClass() {
    // empty body
  }

  @Positive int getX() {
    return x;
  }
}

import org.checkerframework.checker.index.qual.Positive;

class MyClass {
  @Positive int x;
  MyClass() {
    foo(this);
    x = 1;
  }

  @Positive int foo() {
    // ... use x, expecting it to be positive ...
  }
}

import org.checkerframework.checker.index.qual.Positive;

class MyClass {

  @Positive int x;
  @Positive int y;
  int z;

  // Warning: field y is not initialized
  MyClass() {
    x = 1;
  }
}

  @Unique Object u = ...;
  Object o = u;                    // (not.unique) type-checking error!

  void mightDoAnything(Object o) { ... }

  @Unique Object u = ...;
  mightDoAnything(u);  // type-checking error, because the callee may create an alias of the passed argument

Object id(@Unique Object p) {
    return p;     // (not.unique) type-checking error!
}

@Unique Object u = ...;
Object o = id(u);

Object id(@LeakedToResult Object p) {
    return p;
}

@Unique Object u = ...;
id(u);                   // method call result is not used
Object o1 = ...;
Object o2 = id(o1);      // argument is not @Unique

void aliasInCatchBlock() {
    @Unique Exception uex = new Exception();
    try {
        throw uex;    // (not.unique) type-checking error!
    } catch (Exception ex) {
        // uex and ex refer to the same object here.
    }
}

void aliasInArrayInitializer() {
    @Unique Object o = new Object();
    Object[] ar = new Object[] { o };  // (not.unique) type-checking error!
    // The expressions o and ar[0] are now aliased.
}

class MyClass {
    @Unique Object field;
    void makesAlias() {
        MyClass myClass2 = this;
        // this.field is now an alias of myClass2.field
    }
}

List<@Unique Object> l1 = ...;
List<@Unique Object> l2 = l1;

// Annotations on the StringBuffer class, used in the examples below.
// class StringBuffer {
//  @Unique StringBuffer();
//  StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked String s);
// }

void foo() {
    StringBuffer sb = new StringBuffer();    // sb is refined to @Unique.

    StringBuffer sb2 = sb;                   // sb loses its refinement.
    // Both sb and sb2 have aliases and because of that have type @MaybeAliased.
}

void bar() {
    StringBuffer sb = new StringBuffer();     // sb is refined to @Unique.

    sb.append("someString");
    // sb stays @Unique, as no aliases are created.

    StringBuffer sb2 = sb.append("someString");
    // sb is leaked and becomes @MaybeAliased.

    // Both sb and sb2 have aliases and because of that have type @MaybeAliased.
}

    package java.net;

    import org.checkerframework.checker.mustcall.qual.InheritableMustCall;

    @InheritableMustCall({"close"}) class Socket { }

  @MustCall({"toString"}) String foo(@MustCall({"hashCode"}) String arg) {
    return arg;
  }

  interface Partition<ELEMENT extends @Nullable Object, CLASS extends @Nullable Object> {}

  class MultiRandSelector<T> {
    private Partition<T, T> eq;
  }

error: [type.argument] incompatible type argument for type parameter ELEMENT of Partitioner.
        private Partitioner<T, T> eq;
                            ^
  found   : T extends @MustCallUnknown Object
  required: @MustCall Object
error: [type.argument] incompatible type argument for type parameter CLASS of Partitioner.
        private Partitioner<T, T> eq;
                               ^
  found   : T extends @MustCallUnknown Object
  required: @MustCall Object

  javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \
        -processor org.checkerframework.common.subtyping.SubtypingChecker \
        -Aquals=myPackage.qual.MyQual,myPackage.qual.OtherQual MyFile.java ...

  javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \
        -processor org.checkerframework.common.subtyping.SubtypingChecker \
        -AqualDirs=/full/path/to/myProject/bin:/full/path/to/myLibrary/bin MyFile.java

package myPackage.qual;

import org.checkerframework.framework.qual.DefaultFor;
import org.checkerframework.framework.qual.SubtypeOf;
import java.lang.annotation.ElementType;
import java.lang.annotation.Target;

/**
 * Denotes that the representation of an object is encrypted.
 */
@SubtypeOf(PossiblyUnencrypted.class)
@DefaultFor({TypeUseLocation.LOWER_BOUND})
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface Encrypted {}

package myPackage.qual;

import org.checkerframework.framework.qual.DefaultQualifierInHierarchy;
import org.checkerframework.framework.qual.SubtypeOf;
import java.lang.annotation.ElementType;
import java.lang.annotation.Target;

/**
 * Denotes that the representation of an object might not be encrypted.
 */
@DefaultQualifierInHierarchy
@SubtypeOf({})
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface PossiblyUnencrypted {}

$ javac myPackage/qual/Encrypted.java myPackage/qual/PossiblyUnencrypted.java

import myPackage.qual.Encrypted;

...

public @Encrypted String encrypt(String text) {
    // ...
}

// Only send encrypted data!
public void sendOverInternet(@Encrypted String msg) {
    // ...
}

void sendText() {
    // ...
    @Encrypted String ciphertext = encrypt(plaintext);
    sendOverInternet(ciphertext);
    // ...
}

void sendPassword() {
    String password = getUserPassword();
    sendOverInternet(password);
}

  javac -processorpath myqualpath -processor org.checkerframework.common.subtyping.SubtypingChecker 
        -Aquals=myPackage.qual.Encrypted,myPackage.qual.PossiblyUnencrypted YourProgram.java

YourProgram.java:42: incompatible types.
found   : @myPackage.qual.PossiblyUnencrypted java.lang.String
required: @myPackage.qual.Encrypted java.lang.String
    sendOverInternet(password);
                     ^

  javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \
        -processor org.checkerframework.common.subtyping.SubtypingChecker \
        -AqualDirs=/full/path/to/myProject/bin:/full/path/to/myLibrary/bin YourProgram.java

  .../myProject/bin/myPackage/qual/Encrypted.class
  .../myProject/bin/myPackage/qual/PossiblyUnencrypted.class

void method(Object o) { ... }
<U> void use(List<U> list) {
  method(list.get(0));
}

void method(@NotMyType Object o) { ... }
<@U extends @MyTypeUnknown Object> void use(List<U> list) {
  // type error: list.get(0) has type @MyTypeUnknown, method expects @NotMyType
  method(list.get(0));
}

compile group: 'software.amazon.checkerframework', name: 'aws-kms-compliance-checker', version: '1.0.2'

  class MyList<T extends @NonNull Object> {...}

  MyList<@NonNull String> m1;       // OK
  MyList<@Nullable String> m2;      // error

  class MyList<@LowerBound T extends @UpperBound Object> { ... }

  class MyRegexes<@Regex(5) T extends @Regex(1) String> { ... }

  MyRegexes<@Regex(0) String> mu;   // error - @Regex(0) is not a subtype of @Regex(1)
  MyRegexes<@Regex(1) String> m1;   // OK
  MyRegexes<@Regex(3) String> m3;   // OK
  MyRegexes<@Regex(5) String> m5;   // OK
  MyRegexes<@Regex(6) String> m6;   // error - @Regex(6) is not a supertype of @Regex(5)

  class MyListOfNonNulls<@NonNull T extends @NonNull Object> { ... }
  class MyListOfNullables<@Nullable T extends @Nullable Object> { ... }

  MyListOfNonNulls<@NonNull Number> v1;      // OK
  MyListOfNonNulls<@Nullable Number> v2;     // error
  MyListOfNullables<@NonNull Number> v4;     // error
  MyListOfNullables<@Nullable Number> v3;    // OK

  class MyClass<@Nullable T extends @NonNull Object>  // error: @Nullable is not a subtype of @NonNull

  class MyClass<T>
  class MyClass<T extends Object>

  class MyClass<T>                 ==  class MyClass<T extends @Nullable Object>
  class MyClass<T extends Object>  ==  class MyClass<T extends @NonNull Object>

  class MyClass2<T> {
    ...
    @Nullable T myField = null;
    ...
  }

  List<? extends CharSequence> ls;
  ls = new ArrayList<String>();      // OK
  ls = new ArrayList<Integer>();     // error: Integer is not a subtype of CharSequence

  List<? extends @NonNull CharSequence> ls;
  ls = new ArrayList<@NonNull String>();    // OK
  ls = new ArrayList<@Nullable String>();   // error: @Nullable is not a subtype of @NonNull

  List<@LowerBound ? extends @UpperBound CharSequence> lo;
  List<@UpperBound ? super @NonNull Number> ls;

  List<@NonNull ?> lnn;
  List<@NonNull ? extends @NonNull Object> lnn;
  List<@NonNull ? super @NonNull void> lnn;

  class MyList1<@Nullable T> { ... }
  class MyList1a<@Nullable T extends @Nullable Object> { ... } // same as MyList1
  class MyList2<@NonNull T extends @NonNull Object> { ... }
  class MyList2a<T extends @NonNull Object> { ... } // same as MyList2
  class MyList3<T extends @Nullable Object> { ... }

  T t;
  @Nullable T nble;      // Section "Type annotations on a use of a generic type variable", below,
  @NonNull T nn;         // further explains the meaning of "@Nullable T" and "@NonNull T".
  void add(T arg) {}
  T get(int i) {}

    Collections.<@MyTypeAnnotation Object>sort(l, c);

public static void addNumbers(List<? super @SignednessBottom Integer> list) { ... }

  @PolyNull T cast(@PolyNull Object obj) { ... }

   @NonNull T cast( @NonNull Object obj) { ... }
  @Nullable T cast(@Nullable Object obj) { ... }

  // Returns null if either argument is null.
  @PolyNull T max(@PolyNull T x, @PolyNull T y);

   @NonNull T max( @NonNull T x,  @NonNull T y);
  @Nullable T max(@Nullable T x, @Nullable T y);

void moveBetweenStacks(Stack<@PolyNull Object> s1, Stack<@PolyNull Object> s2) {
  s1.push(s2.pop());
}

<T> void moveBetweenStacks(Stack<T> s1, Stack<T> s2) {
  s1.push(s2.pop());
}

  public static int indexOf(@PolyNull Object[] a, @Nullable Object elt) { ... }

  @Nullable Object[] a1;
  @NonNull Object[] a2;

  indexOf(a1, someObject);
  indexOf(a2, someObject);

 public static <T extends @Nullable Object> int indexOf(T[] a, @Nullable Object elt) { ... }
 public static <T extends @Nullable Object> int indexOf(T[] a, T elt) { ... }

  void write(@PolySigned byte[] b) { ... }

  void m(@PolyNull Object obj)

  void m(@NonNull Object obj)
  void m(@Nullable Object obj)

  void m(@Nullable Object obj)

  void m2a(List<@PolyNull MySubClass> strings)

  void m2b(List<? extends @Nullable MySubClass> strings)

@HasQualifierParameter(Tainted.class)
class StringBuffer { ... }

@HasQualifierParameter(Tainted.class)
class Buffer {
  void append(@PolyTainted Buffer this, @PolyTainted String s) { ... }
}

@Untainted Buffer untaintedBuffer = ...;
@Tainted String taintedString = ...;
untaintedBuffer.append(taintedString); // error: (argument.type.incompatible)

@HasQualifierParameter(Tainted.class)
class Buffer {
  @PolyTainted String field;
}

    void method(@Untainted StringBuffer buffer) {
        StringBuffer local = buffer;
        executeSql(local.toString());
    }

    void executeSql(@Untainted String code) {
        // ...
    }

@HasQualifierParameter(Tainted.class)
package mypackage;

    @HasQualifierParameter(Tainted.class)
    interface Buffer {
        void append(@PolyTainted String s);
    }

    public class ClassQPTypeVarTest {
        <T> @Tainted T cast(T param) {
            return param;
        }

        void bug(@Untainted Buffer b, @Tainted String s) {
            cast(b).append(s);  // error
        }
    }

  String[] strings = new String[] {"hello"};
  Object[] objects = strings;
  objects[0] = new Object();
  String myString = strs[0];

String[] myStrings = {"hello"};

  @C class MyClass {}

  @NonNull class Optional { ... }

  Map<String, Optional> m;
  String key = ...;
  Optional value = m.get(key);
  if (value != null) {
    ...
  }

@DefaultQualifierForUse(B.class)
class MyClass {}

@DefaultQualifierForUse(C.class)
@C class MyClass {}

@NoDefaultQualifierForUse
@C class MyClass {}

import org.checkerframework.framework.qual.DefaultQualifier;
import org.checkerframework.checker.nullness.qual.NonNull;

@DefaultQualifier(NonNull.class)
class MyClass {

  public boolean compile(File myFile) { // myFile has type "@NonNull File"
    if (!myFile.exists())          // no warning: myFile is non-null
      ...
    @Nullable File srcPath = ...;  // must annotate to specify "@Nullable File"
    if (srcPath.exists())          // warning: srcPath might be null
      ...
  }

  @DefaultQualifier(Tainted.class)
  public boolean isJavaFile(File myfile) {  // myFile has type "@Tainted File"
    ...
  }
}

@DefaultQualifierInHierarchy
@DefaultFor({ TypeUseLocation.EXCEPTION_PARAMETER })
public @interface NonNull {}

public @interface Nullable {}

  public boolean equals(@Nullable Object obj) {
      ...
  }

class MyList<@Nullable T extends @Nullable Object> {}

MyList<?> listOfNullables;
MyList<@Nullable ? extends @Nullable Object> listOfNullables;

class MyList<@Regex(5) T extends @Regex(1) Object> {}

MyList<?> listOfRegexes;
MyList<@Regex(5) ? extends @Regex(1) Object> listOfRegexes;

class MyList<@NonNull T extends @Nullable Object> {}

MyList<? extends Object> listOfNonNulls;
MyList<@NonNull ? extends @NonNull Object> listOfNonNulls2;

  String concatenate(String p1, String p2)

  @Top String concatenate(@Bottom String p1, @Bottom String p2)

@B class MyClass {
  @C MyClass() {}
}

  @Untainted class MyClass {
    MyClass() {}
  }

  @Nullable String myVar;
  ...                   // myVar has type @Nullable String here.
  myVar.hashCode();     // warning: possible dereference of null.
  ...
  if (myVar != null) {
    ...                 // myVar has type @NonNull String here.
    myVar.hashCode();   // no warning.
  }

  @Nullable String myVar;
  ...                   // myVar has type @Nullable String
  myVar = "hello";
  ...                   // myVar has type @NonNull String
  myVar.hashCode();     // no warning
  ...
  myVar = myMap.get(someKey);
  ...                   // myVar has type @Nullable String
  myVar.hashCode();     // warning: posible dereference of null

  void m2(@Unannotated String s) {
    s = RegexUtil.asRegex(s, 2);  // asRegex throws an exception if its argument is not
                                  // a regex with the given number of capturing groups
    ...   // s now has type "@Regex(2) String"
  }

    public final String protocol = "https";

    public final @Nullable String protocol = "https";

class DBObject {
  @Nullable Date updatedAt;

  void m() {
    // updatedAt is @Nullable, so warning about .getTime()
    ... updatedAt.getTime() ... // warning about possible NullPointerException

    if (updatedAt == null) {
      updatedAt = new Date();
    }

    // updatedAt is now @NonNull, so .getTime() call is OK
    ... updatedAt.getTime() ...
  }
}

  @Nullable Object myField;

  int computeValue() { ... }

  void m() {
    ...
    if (myField != null) {
                        // The type of myField is now "@NonNull Object".
      int result = computeValue();
                        // The type of myField is now "@Nullable Object",
                        // because computeValue might have set myField to null.
      myField.toString(); // Warning: possible null pointer exception.
    }
  }

  @SideEffectFree
  int computeValue() { ... }

  @MonotonicNonNull Object myField;

  @EnsuresNonNull("myField")
  int computeValue() { ... }

  @RequiresNonNull("myField")
  @EnsuresNonNull("myField")
  int computeValue() { ... }

  @Nullable Object getField(Object arg) { ... }

  void m() {
    ...
    if (x.getField(y) != null) {
      x.getField(y).toString(); // warning: possible null pointer exception
    }
  }

  @Pure
  @Nullable Object getField(Object arg) { ... }

    var list1 = new ArrayList<@Tainted String>(); // type of list1 is ArrayList<@Tainted String>
    var list2 = new ArrayList<@Untainted String>(); // type of list2 is ArrayList<@Untainted String>

    var list1 = new ArrayList<@Tainted String>(); // type of list1 is ArrayList<@Tainted String>
    var list2 = new ArrayList<@Untainted String>(); // type of list2 is ArrayList<@Untainted String>
    var list3 = list1; // type of list3 is ArrayList<@Tainted String>
    list2 = list1; // assignment error

  @EnsuresNonNullIf(expression="readLine()", result=true)
  @Pure public boolean ready() throws IOException { ... }

class Person {
  final @Nullable String nickname;
  public Person(@Nullable String nickname) {
    this.nickname = nickname;
  }
}

// A rapper always has a nickname.
@FieldInvariant(qualifier = NonNull.class, field = "nickname")
class Rapper extends Person {
  public Rapper(String nickname) {
    super(nickname);
  }
  void method() {
    ... nickname.length() ...   // legal, nickname is non-null in this class.
  }
}

class Animal {}
class Mammal extends Animal { ... }
class Marsupial extends Mammal {
  int pouchSize;  // pouch capacity, in cubic centimeters
  ...
}

class Animal {
  @Unused(when=Mammal.class)
  int pouchSize;  // pouch capacity, in cubic centimeters
  ...
}
@interface Mammal {}
@interface Marsupial {}

@Marsupial Animal joey = ...;
... joey.pouchSize ...    // OK
@Mammal Animal mae = ...;
... mae.pouchSize ...    // compile-time error

class @Mammal-Animal { ... }
class @Marsupial-Animal {
  int pouchSize;  // pouch capacity, in cubic centimeters
  ...
}

MyFile.java:107: error: [dereference.of.nullable] dereference of possibly-null reference myList
          myList.add(elt);
          ^

  @SuppressWarnings("tainting:cast.unsafe") // expr is untainted because ... [explanation goes here]
  @Untainted String myvar = expr;

  @Untainted String myvar;
  ...
  @SuppressWarnings("tainting:cast.unsafe") // expr is untainted because ...
  myvar = expr;

  @SuppressWarnings("tainting")              // suppresses all tainting-related warnings
  @SuppressWarnings("cast")                  // suppresses warnings from all checkers about casts
  @SuppressWarnings("unsafe")                // suppresses warnings from all checkers about unsafe code
  @SuppressWarnings("cast.unsafe")           // suppresses warnings from all checkers about unsafe casts
  @SuppressWarnings("tainting:cast")         // suppresses tainting warnings about casts
  @SuppressWarnings("tainting:unsafe")       // suppresses tainting warnings about unsafe code
  @SuppressWarnings("tainting:cast.unsafe")  // suppresses tainting warnings about unsafe casts

@SuppressWarnings("cast") // cast is redundant (except when checking nullness)
@SuppressWarnings("interning") // FbType.FREE is interned but is not annotated
@SuppressWarnings("interning") // equality testing optimization
@SuppressWarnings("nullness") // used portion of array is non-null
@SuppressWarnings("nullness") // oi.factory is a static method, so null first argument is OK
@SuppressWarnings("purity") // side effect to local state of type BitSet

@SuppressWarnings("flowexpr.parse.error") // https://tinyurl.com/cfissue/862
@SuppressWarnings("keyfor") // https://tinyurl.com/cfissue/877

while (c != Object.class) {
  ...
  c = c.getSuperclass();
  assert c != null
    : "@AssumeAssertion(nullness): c was not Object, so its superclass is not null";
 }

  public String myGet(String key, String def) {
    checkNotNull(key, "key"); // NOI18N
    ...
  }

package java.util;
class Objects {
  @EnsuresNonNull("#1")
  public static <T> @NonNull T requireNonNull(@Nullable T obj);
}

  $CHECKERFRAMEWORK/bin/wpi.sh -- --checker nullness

  wpi.sh [-d PROJECTDIR] [-t TIMEOUT] [-c COMPILATION_TARGET] [-b EXTRA_BUILD_ARGS] [-g GRADLECACHEDIR] -- [DLJC-ARGS]

wpi-many.sh -o outdir -i /path/to/repo.list -t 7200 -- --checker optional

wpi-annotation-paths.sh outdir-results

git clone https://github.com/mernst/plume-lib.git
cd plume-lib
make jar
$CHECKERFRAMEWORK/checker/bin/infer-and-annotate.sh \
    "LockChecker,NullnessChecker" java/plume.jar:java/lib/junit-4.12.jar:$JAVA_HOME/lib/tools.jar \
    $(find java/src/plume/ -name "*.java")
# View the results
git diff

  javac -processor org.checkerframework.checker.interning.InterningChecker \
    -Astubs=path/to/String.astub:stubs MyFile.java MyOtherFile.java ...

package java.util;
class Random {
  @Insecure int nextInt();
}

package java.security;
class SecureRandom extends Random {
  @Secure int nextInt();
}

Random r = ...;
SecureRandom sr = ...;

@Secure int i1 = r.nextInt(); // error
@Secure int i2 = sr.nextInt(); // OK

  import org.checkerframework.checker.interning.qual.Interned;
  package java.lang;
  @Interned class Class<T> {}
  class String {
    @Interned String intern();
  }

  mkdir project-stubs
  cp -R project/src project-stubs
  java -cp $CHECKERFRAMEWORK/checker/dist/checker.jar org.checkerframework.framework.stub.JavaStubifier project-stubs
  find project-stubs -type f -name "*.java" -exec rename 's/.java$/.astub/' {} \;

find project-stubs/ -name "*.java" -type f | xargs cat > project.astub

checker/src/main/java/org/checkerframework/checker/regex/apache-xerces.astub
checker/src/main/java/org/checkerframework/checker/signature/javaparser.astub

  sourceSets {
    main {
        resources {
            srcDirs += ['src/main/java']
        }
    }
  }

AnnotationFileParser: Method isLLowerCase(char) not found in type java.lang.Character

AnnotationFileParser: Method enableForegroundNdefPush(Activity,NdefPushCallback)
      not found in type android.nfc.NfcAdapter

  javac -processor org.checkerframework.checker.interning.InterningChecker \
    -Aajava=path/to/String.ajava:ajavadir MyFile.java MyOtherFile.java ...

  java -cp $CHECKERFRAMEWORK/checker/dist/checker.jar \
    org.checkerframework.framework.ajava.InsertAjavaAnnoations \
    <path-to-ajava-files> <path-to-java-files>

import java.lang.annotation.Documented;
import java.lang.annotation.Target;
import java.lang.annotation.ElementType;
import org.checkerframework.common.subtyping.qual.Unqualified;
import org.checkerframework.framework.qual.SubtypeOf;

@Documented
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(Unqualified.class)
public @interface Encrypted {}

myPackage/
  | qual/                               type qualifiers
  | MyPropChecker.java                  interface to the compiler
  | MyPropVisitor.java                  [optional] type rules
  | MyPropAnnotatedTypeFactory.java     [optional] type introduction and dataflow rules

  javac -processor mypackage.MyPropChecker SourceFile.java

  void testHierarchy(@UnknownSign int us, @NonNegative int nn) {
    @UnknownSign int a = us;
    @UnknownSign int b = nn;
    // :: error: (assignment.type.incompatible)
    @NonNegative int c = us;  // expected error on this line
    @NonNegative int d = nn;
  }

  javac -processor mypackage.MyChecker File1.java File2.java ...

  void testArrayIndexing(String[] myArray, @UnknownSign int us, @NonNegative int nn) {
    myArray[us];  // expected error on this line
    myArray[nn];
  }

  void testTypeIntroduction(String[] myArray) {
    @NonNegative nn1 = -1;  // expected error on this line
    @NonNegative nn2 = 0;
    @NonNegative nn3 = 1;
    @NonNegative nn4 = myArray.length;
  }

  void testDataflow(@UnknownSign int us, @NonNegative int nn) {
    @NonNegative nn2;
    nn2 = us;  // expected error on this line
    if (us > j) {
      nn2 = us;
    }
    if (us >= j) {
      nn2 = us;
    }
    if (j < us) {
      nn2 = us;
    }
    if (j <= us) {
      nn2 = us;
    }
    nn = us;  // expected error on this line
  }

package mypackage.qual;
import java.lang.annotation.Documented;
import java.lang.annotation.ElementType;
import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
import org.checkerframework.framework.qual.DefaultQualifierInHierarchy;
import org.checkerframework.framework.qual.SubtypeOf;
/**
 * The run-time value of the integer is unknown.
 *
 * @checker_framework.manual #nonnegative-checker Non-Negative Checker
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf({})
@DefaultQualifierInHierarchy
public @interface UnknownSign {}

package mypackage.qual;
import java.lang.annotation.Documented;
import java.lang.annotation.ElementType;
import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
import java.lang.annotation.Target;
import org.checkerframework.framework.qual.LiteralKind;
import org.checkerframework.framework.qual.SubtypeOf;
/**
 * Indicates that the value is greater than or equal to zero.
 *
 * @checker_framework.manual #nonnegative-checker Non-Negative Checker
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf({UnknownSign.class})
public @interface NonNegative {}

    @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
    @SubtypeOf( { Nullable.class } )
    public @interface NonNull {}

    @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
    @SubtypeOf( {} )
    public @interface Nullable {}

  import java.lang.annotation.ElementType;
  import java.lang.annotation.Target;
  import org.checkerframework.framework.qual.PolymorphicQualifier;

  @PolymorphicQualifier
  @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
  public @interface PolyNull {}

  void foo(@PolySigned Object a, @PolySigned Object b) { ... }

  void foo(@UnknownSignedness Object a, @UnknownSignedness Object b) { ... }

  Objects.equals((@UnknownSignedness) mySigned, (@UnknownSignedness) myUnsigned)

@SomeAnn MyClass x = ...;
Object y = x;
MyClass z = (MyClass) y;

@SomeAnn MyClass x = ...;
Object y = x;
MyClass z = (MyClass) y;

<T> T f() {
    return null;
}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@TargetLocations({TypeUseLocation.LOWER_BOUND, TypeUseLocation.UPPER_BOUND})

class MyClass {
   Object field = ...;
   @Anno("this.field") Object field2 = ...;
}

  package my.package;
  import org.checkerframework.common.basetype.BaseTypeChecker;
  @SupportedLintOptions({"dotequals"})
  public final class InterningChecker extends BaseTypeChecker {}

  package my.package;
  import org.checkerframework.common.basetype.BaseTypeChecker;
  @SupportedLintOptions({"flow", "cast", "cast:redundant"})
  public class NullnessChecker extends BaseTypeChecker {}

  javac -processor DistanceUnitChecker,VelocityUnitChecker,MassUnitChecker MyFile.java

  javac -processor MyUnitCheckers MyFile.java

  public class MyUnitCheckers extends AggregateChecker {
    protected Collection<Class<? extends SourceChecker>> getSupportedCheckers() {
      return Arrays.asList(DistanceUnitChecker.class,
                           VelocityUnitChecker.class,
                           MassUnitChecker.class);
    }
  }

  @SupportedLintOptions({"myflag"})

  checker.getLintOption("myflag", false)

  javac -processor mypackage.MyChecker -Alint=myflag

  @SupportedOptions({"myoption"})

  checker.getOption("myoption")

  javac -processor mypackage.MyChecker -Amyoption=p1,p2

    @Nullable Object myObject;
    @NonNull Object myNonNullObject;
    ...
    myNonNullObject = myObject;  // invalid assignment

  @Override
  protected TreeAnnotator createTreeAnnotator() {
      return new ListTreeAnnotator(super.createTreeAnnotator(), new MyTreeAnnotator(this));
  }

  @Override
  protected TypeAnnotator createTypeAnnotator() {
      return new ListTypeAnnotator(new MyTypeAnnotator(this), super.createTypeAnnotator());
  }

  @Regex(0) String asRegex(String s, int groups) { ... }

  @Nullable String s;
    if (s != null) {
      ...
    } else {
      ...
    }

  public MyCheckerTransfer(CFAnalysis analysis) {
    super(analysis);
  }

  public TransferResult<CFValue, CFStore> visitMethodInvocation(
    MethodInvocationNode n, TransferInput<CFValue, CFStore> in)  { ... }

VariableTree:
  name: "a"
  type:
    IdentifierTree
      name: String
  initializer:
    LiteralTree
      value: ""

  @Override
  public TransferResult<CFValue, CFStore> visitMethodInvocation(...)
    ...
    MethodAccessNode target = n.getTarget();
    ExecutableElement method = target.getMethod();
    Node receiver = target.getReceiver();
    if (receiver instanceof ClassNameNode) {
      String receiverName = ((ClassNameNode) receiver).getElement().toString();

      // Is this a call to static method isRegex(s, groups) in a class named RegexUtil?
      if (receiverName.equals("RegexUtil")
          && ElementUtils.matchesElement(method,
                 "isRegex", String.class, int.class)) {
            ...

  AnnotationMirror regexAnnotation;
  Node count = n.getArgument(1);
  if (count instanceof IntegerLiteralNode) {
    // argument is a literal integer
    IntegerLiteralNode iln = (IntegerLiteralNode) count;
    Integer groupCount = iln.getValue();
    regexAnnotation = factory.createRegexAnnotation(groupCount);
  } else {
    // argument is not a literal integer; fall back to @Regex(), which is the same as @Regex(0)
    regexAnnotation = AnnotationBuilder.fromClass(factory.getElementUtils(), Regex.class);
  }

  CFValue newResultValue = analysis.createSingleAnnotationValue(regexAnnotation,
      result.getResultValue().getType().getUnderlyingType());

  return new RegularTransferResult<>(newResultValue, result.getRegularStore());

        // disable flow inference
        super(checker, /*useFlow=*/ false);

class MyNullnessTest {
  void method() {
    Object nullable = null;
    // :: error: (dereference.of.nullable)
    nullable.toString();
  }
}

javacheck -processor mypackage.MyProcessor -Aflowdotdir=. MyClass.java
for dotfile in *.dot; do dot -Tpdf -o "$dotfile.pdf" "$dotfile"; done

dot -Tsvg <file.dot> -o <file.svg>

java -Xbootclasspath/p:$CHECKERFRAMEWORK/checker/dist/javac.jar \
  -cp $CHECKERFRAMEWORK/checker/dist/checker.jar \
  org.checkerframework.dataflow.cfg.visualize.CFGVisualizeLauncher \
  MyClass.java --class MyClass --method test --pdf

java -cp $CHECKERFRAMEWORK/checker/dist/checker.jar \
  org.checkerframework.dataflow.cfg.visualize.CFGVisualizeLauncher \
  MyClass.java --class MyClass --method test --pdf

java -Xbootclasspath/p:$CHECKERFRAMEWORK/checker/dist/javac.jar \
  -cp $CHECKERFRAMEWORK/checker/dist/checker.jar \
  org.checkerframework.dataflow.cfg.visualize.CFGVisualizeLauncher \
  MyClass.java --class MyClass --method test --string

$ javac -processor org.checkerframework.checker.interning.InterningChecker \
    docs/examples/InternedExampleWithWarnings.java -Ashowchecks -Anomsgtext -Afilenames

[InterningChecker] InterningExampleWithWarnings.java
 success (line  18): STRING_LITERAL "foo"
     actual: DECLARED @org.checkerframework.checker.interning.qual.Interned java.lang.String
   expected: DECLARED @org.checkerframework.checker.interning.qual.Interned java.lang.String
 success (line  19): NEW_CLASS new String("bar")
     actual: DECLARED java.lang.String
   expected: DECLARED java.lang.String
docs/examples/InterningExampleWithWarnings.java:21: (not.interned)
    if (foo == bar) {
            ^
 success (line  22): STRING_LITERAL "foo == bar"
     actual: DECLARED @org.checkerframework.checker.interning.qual.Interned java.lang.String
   expected: DECLARED java.lang.String
1 error

java -jar "$CHECKERFRAMEWORK/checker/dist/checker.jar" \
    -J-Xdebug -J-Xrunjdwp:transport=dt_socket,server=y,suspend=y,address=5005 \
    -processor org.checkerframework.checker.nullness.NullnessChecker \
    src/sandbox/FileToCheck.java

 * @checker_framework.manual #optional-checker Optional Checker
 * @checker_framework.manual #qualifier-polymorphism Qualifier polymorphism

android {
    ...
    compileOptions {
        sourceCompatibility JavaVersion.VERSION_1_8
        targetCompatibility JavaVersion.VERSION_1_8
    }
}

 android {
    ...
      buildTypes {
      ...
        checkTypes {
            javaCompileOptions.annotationProcessorOptions.
                    classNames.add("org.checkerframework.checker.nullness.NullnessChecker")
            // You can pass options like so:
            // javaCompileOptions.annotationProcessorOptions.arguments.put("warns", "")
        }
    }
}

configurations {
    errorproneJavac {
        description = 'Java 9 compiler; required to run the Checker Framework under JDK 8.'
    }
}

dependencies {
    ... existing dependencies...
    ext.checkerFrameworkVersion = '3.42.0-eisop4'
    implementation "io.github.eisop:checker-qual-android:${checkerFrameworkVersion}"
    // or if you use no annotations in source code the above line could be
    // compileOnly "io.github.eisop:checker-qual-android:${checkerFrameworkVersion}"
    annotationProcessor "io.github.eisop:checker:${checkerFrameworkVersion}"
    errorproneJavac 'com.google.errorprone:javac:9+181-r4173-1'
}

gradle.projectsEvaluated {
    tasks.withType(JavaCompile).all { compile ->
        if (compile.name.contains("CheckTypes")) {
            options.fork = true
            options.forkOptions.jvmArgs += ["-Xbootclasspath/p:${configurations.errorproneJavac.asPath}".toString()]
        }
    }
}

gradlew assembleCheckTypes

android {
    ...
    compileOptions {
        sourceCompatibility JavaVersion.VERSION_1_8
        targetCompatibility JavaVersion.VERSION_1_8
    }
}

 android {
    ...
      buildTypes {
      ...
        checkTypes {
            javaCompileOptions.annotationProcessorOptions.
                    classNames.add("org.checkerframework.checker.nullness.NullnessChecker")
            // You can pass options like so:
            // javaCompileOptions.annotationProcessorOptions.arguments.put("warns", "")
        }
    }
}

dependencies {
    ... existing dependencies...
    ext.checkerFrameworkVersion = '3.42.0-eisop4'
    implementation "io.github.eisop:checker-qual-android:${checkerFrameworkVersion}"
    // or if you use no annotations in source code the above line could be
    // compileOnly "io.github.eisop:checker-qual-android:${checkerFrameworkVersion}"
    annotationProcessor "io.github.eisop:checker:${checkerFrameworkVersion}"
}

gradlew assembleCheckTypes

  <property environment="env"/>
  <property name="checkerframework" value="${env.CHECKERFRAMEWORK}" />
  <condition property="cfJavac" value="javac.bat" else="javac">
    <os family="windows" />
  </condition>
  <presetdef name="cf.javac">
    <javac fork="yes" executable="${checkerframework}/checker/bin/${cfJavac}" >
      <compilerarg value="-version"/>
      <compilerarg value="-implicit:class"/>
    </javac>
  </presetdef>

  <target name="check-nullness"
          description="Check for null pointer dereferences"
          depends="clean,...">
    <!-- use cf.javac instead of javac -->
    <cf.javac ... >
      <compilerarg line="-processor org.checkerframework.checker.nullness.NullnessChecker"/>
      <!-- optional, to not check uses of library methods:
        <compilerarg value="-AskipUses=^(java\.awt\.|javax\.swing\.)"/>
      -->
      <compilerarg line="-Xmaxerrs 10000"/>
      ...
    </cf.javac>
  </target>

prebuilt_jar(
    name = 'checker-framework',
    binary_jar = 'checker-3.42.0-eisop4.jar',
    visibility = [ 'PUBLIC' ]
)

prebuilt_jar(
    name = 'checker-qual',
    binary_jar = 'checker-qual-3.42.0-eisop4.jar',
    visibility = [ 'PUBLIC' ]
)

java_library (
    name = 'hello',
    srcs = glob(['src/main/java/**/*.java']),
    java_version = '1.8',
    provided_deps = [ ':checker-framework', ':checker-qual' ],
# To add annotation processing
    annotation_processors = [ 'org.checkerframework.checker.units.UnitsChecker' ],
    annotation_processor_deps = [ ':checker-framework', ':checker-qual' ],
)

./buck clean
./buck fetch //...
./buck build --verbose 8 //app:main

./buck clean && ./buck fetch //... && ./buck build //app:main -c tools.javac=$(which javac)

  export CHECKERFRAMEWORK=${HOME}/checker-framework-3.42.0-eisop4
  export PATH=${CHECKERFRAMEWORK}/checker/bin:${PATH}

  export CHECKERFRAMEWORK=${HOME}/checker-framework-3.42.0-eisop4
  alias javacheck='$CHECKERFRAMEWORK/checker/bin/javac'

  java -jar "$CHECKERFRAMEWORK/checker/dist/checker.jar" -cp "myclasspath" -processor nullness MyFile.java

  # Unix
  export CHECKERFRAMEWORK=${HOME}/checker-framework-3.42.0-eisop4
  alias javacheck='java -jar "$CHECKERFRAMEWORK/checker/dist/checker.jar"'

  # Windows
  set CHECKERFRAMEWORK = C:\Program Files\checker-framework-3.42.0-eisop4\
  doskey javacheck=java -jar "%CHECKERFRAMEWORK%\checker\dist\checker.jar" $*

javac \
-J-Xbootclasspath/p:$CHECKERFRAMEWORK/checker/dist/javac.jar \
-cp $CHECKERFRAMEWORK/checker/dist/checker-qual.jar \
-processorpath $CHECKERFRAMEWORK/checker/dist/checker.jar \
-processor org.checkerframework.checker.nullness.NullnessChecker \
-source 8 -target 8

error: SourceChecker.typeProcessingStart: unexpected Throwable (NoSuchMethodError);
message: com.sun.tools.javac.code.Type.stripMetadata()Lcom/sun/tools/javac/code/Type;

java.lang.NoSuchFieldError: ANNOTATION_PROCESSOR_MODULE_PATH

javac \
-J--add-exports=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED \
-J--add-exports=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED \
-J--add-exports=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED \
-J--add-exports=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED \
-J--add-exports=jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED \
-J--add-exports=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED \
-J--add-exports=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED \
-J--add-exports=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED \
-J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED \
-processorpath $CHECKERFRAMEWORK/checker/dist/checker.jar \
-cp $CHECKERFRAMEWORK/checker/dist/checker-qual.jar \
-processor org.checkerframework.checker.nullness.NullnessChecker

WARNING: An illegal reflective access operation has occurred
WARNING: Illegal reflective access by org.checkerframework.javacutil.Resolver
  (file:$CHECKERFRAMEWORK/checker/dist/checker.jar) to method com.sun.tools.javac.comp.Resolve.findMethod(...)
WARNING: Please consider reporting this to the maintainers of org.checkerframework.javacutil.Resolver
WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
WARNING: All illegal access operations will be denied in a future release

java.lang.IllegalAccessError: class org.checkerframework.javacutil.AbstractTypeProcessor
  (in unnamed module ...) cannot access class com.sun.tools.javac.processing.JavacProcessingEnvironment
  (in module jdk.compiler) because module jdk.compiler does not export com.sun.tools.javac.processing
  to unnamed module ...

javac \
  -J--add-exports=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED \
  -J--add-exports=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED \
  -J--add-exports=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED \
  -J--add-exports=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED \
  -J--add-exports=jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED \
  -J--add-exports=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED \
  -J--add-exports=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED \
  -J--add-exports=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED \
  -J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED \
  -processorpath $CHECKERFRAMEWORK/checker/dist/checker.jar \
  --module-path $CHECKERFRAMEWORK/checker/dist/checker-qual.jar \
  -processor org.checkerframework.checker.nullness.NullnessChecker

  @Getter @Setter
  private @Regex String role;

  public @Regex String getRole() { return role; }
  public void setRole(@Regex String role) { this.role = role; }

  lombok.copyableAnnotations += my.checker.qual.MyTypeAnnotation

  <dependencies>
    ... existing <dependency> items ...

    <!-- Annotations from the Checker Framework: nullness, interning, locking, ... -->
    <dependency>
      <groupId>io.github.eisop</groupId>
      <artifactId>checker-qual</artifactId>
      <version>3.42.0-eisop4</version>
    </dependency>
  </dependencies>

  mvn versions:use-latest-versions -Dincludes="io.github.eisop:*"

  <profiles>
    <profile>
      <id>checkerframework</id>
      <!-- If you omit the activation block, run mvn with "-P checkerframework" to run checkers. -->
      <activation>
        <jdk>[1.8,)</jdk>
      </activation>
      <build>
        <plugins>
          <plugin>
            <artifactId>maven-compiler-plugin</artifactId>
            <version>3.11.0</version>
            <configuration>
              <fork>true</fork> <!-- Must fork or else JVM arguments are ignored. -->
              <annotationProcessorPaths>
                <path>
                  <groupId>io.github.eisop</groupId>
                  <artifactId>checker</artifactId>
                  <version>3.42.0-eisop4</version>
                </path>
              </annotationProcessorPaths>
              <annotationProcessors>
                <!-- Add all the checkers you want to enable here -->
                <annotationProcessor>org.checkerframework.checker.nullness.NullnessChecker</annotationProcessor>
              </annotationProcessors>
              <compilerArgs>
                <arg>-Xmaxerrs</arg>
                <arg>10000</arg>
                <arg>-Xmaxwarns</arg>
                <arg>10000</arg>
                <!-- <arg>-Awarns</arg> --> <!-- -Awarns turns type-checking errors into warnings. -->
              </compilerArgs>
            </configuration>
          </plugin>
        </plugins>
      </build>
    </profile>

    <profile>
      <id>checkerframework-jdk8</id>
      <activation>
        <jdk>1.8</jdk>
      </activation>
      <!-- using github.com/google/error-prone-javac is required when running on JDK 8 -->
      <properties>
        <javac.version>9+181-r4173-1</javac.version>
      </properties>
      <build>
        <plugins>
          <plugin>
            <!-- This plugin execution will copy the com.google.errorprone:javac jar file to
                 your project’s output directory without adding that jar as an explicit
                 dependency. -->
            <groupId>org.apache.maven.plugins</groupId>
            <artifactId>maven-dependency-plugin</artifactId>
            <executions>
              <execution>
                <goals>
                  <goal>copy</goal>
                </goals>
                <phase>process-sources</phase>
                <configuration>
                  <artifact>com.google.errorprone:javac:${javac.version}:jar</artifact>
                  <outputDirectory>${project.build.directory}/javac</outputDirectory>
                </configuration>
              </execution>
            </executions>
          </plugin>
          <plugin>
            <groupId>org.apache.maven.plugins</groupId>
            <artifactId>maven-compiler-plugin</artifactId>
            <configuration>
              <compilerArgs combine.children="append">
                <arg>-J-Xbootclasspath/p:${project.build.directory}/javac/javac-${javac.version}.jar</arg>
              </compilerArgs>
            </configuration>
          </plugin>
        </plugins>
      </build>
    </profile>

    <profile>
      <id>checkerframework-jdk9orlater</id>
      <activation>
        <jdk>[9,)</jdk>
      </activation>
      <build>
        <plugins>
          <plugin>
            <groupId>org.apache.maven.plugins</groupId>
            <artifactId>maven-compiler-plugin</artifactId>
            <configuration>
              <compilerArgs combine.children="append">
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED</arg>
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED</arg>
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED</arg>
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED</arg>
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED</arg>
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED</arg>
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED</arg>
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED</arg>
                <arg>-J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED</arg>
              </compilerArgs>
            </configuration>
          </plugin>
        </plugins>
      </build>
    </profile>
  </profiles>

<executions>
  <execution>
    <id>default-compile</id>
    ...
  </execution>
</executions>

<compilerArgs>
  ...
  <arg>-verbose</arg>

  <properties>
    ... existing <property> items ...

    <!-- Needed for animal-sniffer-maven-plugin version 1.19 which is broken (version 1.20 is fixed). -->
    <animal.sniffer.skip>true</animal.sniffer.skip>
  </properties>

./gradlew publishToMavenLocal

  <property environment="env"/>
  <property name="checkerframework" value="${env.CHECKERFRAMEWORK}" />
  <condition property="cfJavac" value="javac.bat" else="javac">
    <os family="windows" />
  </condition>
  <presetdef name="cf.javac">
    <javac fork="yes" executable="${checkerframework}/checker/bin/${cfJavac}" >
      <compilerarg value="-version"/>
      <compilerarg value="-implicit:class"/>
    </javac>
  </presetdef>

  <target depends="-init-ap-cmdline-properties" if="ap.supported.internal"
        name="-init-macrodef-javac-with-processors">
    <echo message = "${checkerframework}"/>
    <macrodef name="javac" uri="http://www.netbeans.org/ns/j2se-project/3">
        <attribute default="${src.dir}" name="srcdir"/>
        <attribute default="${build.classes.dir}" name="destdir"/>
        <attribute default="${javac.classpath}" name="classpath"/>
        <attribute default="${javac.processorpath}" name="processorpath"/>
        <attribute default="${build.generated.sources.dir}/ap-source-output" name="apgeneratedsrcdir"/>
        <attribute default="${includes}" name="includes"/>
        <attribute default="${excludes}" name="excludes"/>
        <attribute default="${javac.debug}" name="debug"/>
        <attribute default="${empty.dir}" name="sourcepath"/>
        <attribute default="${empty.dir}" name="gensrcdir"/>
        <element name="customize" optional="true"/>
        <sequential>
            <property location="${build.dir}/empty" name="empty.dir"/>
            <mkdir dir="${empty.dir}"/>
            <mkdir dir="@{apgeneratedsrcdir}"/>
            <cf.javac debug="@{debug}" deprecation="${javac.deprecation}"
                    destdir="@{destdir}" encoding="${source.encoding}"
                    excludes="@{excludes}" fork="${javac.fork}"
                    includeantruntime="false" includes="@{includes}"
                    source="${javac.source}" sourcepath="@{sourcepath}"
                    srcdir="@{srcdir}" target="${javac.target}"
                    tempdir="${java.io.tmpdir}">
                <src>
                    <dirset dir="@{gensrcdir}" erroronmissingdir="false">
                        <include name="*"/>
                    </dirset>
                </src>
                <classpath>
                    <path path="@{classpath}"/>
                </classpath>
                <compilerarg line="${endorsed.classpath.cmd.line.arg}"/>
                <compilerarg line="${javac.profile.cmd.line.arg}"/>
                <compilerarg line="${javac.compilerargs}"/>
                <compilerarg value="-processorpath"/>
                <compilerarg path="@{processorpath}:${empty.dir}"/>
                <compilerarg line="${ap.processors.internal}"/>
                <compilerarg line="${annotation.processing.processor.options}"/>
                <compilerarg value="-s"/>
                <compilerarg path="@{apgeneratedsrcdir}"/>
                <compilerarg line="${ap.proc.none.internal}"/>
                <compilerarg line="-processor org.checkerframework.checker.nullness.NullnessChecker"/>
                <compilerarg line="-Xmaxerrs 10000"/>
                <compilerarg line="-Xmaxwarns 10000"/>
                <customize/>
            </cf.javac>
        </sequential>
    </macrodef>
  </target>
  <target name="-post-jar">
  </target>

javacOptions ++= Seq(
    "-J-Xbootclasspath/p:$CHECKERFRAMEWORK/checker/dist/javac.jar",
    "-cp $CHECKERFRAMEWORK/checker/dist/checker-qual.jar",
    "-processorpath $CHECKERFRAMEWORK/checker/dist/checker.jar",
    "-processor org.checkerframework.checker.nullness.NullnessChecker",
    "-source 8", "-target 8"
  )

javacOptions ++= Seq(
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED",
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED",
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED",
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED",
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED",
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED",
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED",
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED",
    "-J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED",
    "-processorpath $CHECKERFRAMEWORK/checker/dist/checker.jar",
    "-cp $CHECKERFRAMEWORK/checker/dist/checker-qual.jar",
    "-processor org.checkerframework.checker.nullness.NullnessChecker"
  )

For compiling modularized code:
javacOptions ++= Seq(
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED",
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED",
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED",
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED",
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED",
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED",
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED",
    "-J--add-exports=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED",
    "-J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED",
    "-processorpath $CHECKERFRAMEWORK/checker/dist/checker.jar",
    "--module-path $CHECKERFRAMEWORK/checker/dist/checker-qual.jar",
    "-processor org.checkerframework.checker.nullness.NullnessChecker"
  )

  /** Return index of the search key, if it is contained it the sorted array a; otherwise ... */
  int binarySearch(Object @Sorted [] a, Object key)

  found   : ? extends T extends @UnknownKeyFor Object
  required: [extends @UnknownKeyFor Object super @UnknownKeyFor null]

  if (myobject.myfield != null) {
    myobject.myfield.toString();
  }

  if (myField != null) {
    myField.hashCode();   // no warning
    someMethod();
    myField.hashCode();   // warning about potential NullPointerException
  }

class MyClass {

  final String field = "%d";

  String method() {
    return "%d";
  }

  void method m() {
    String local = "%d";
    String.format(local, 5);    // Format String Checker verifies the call is safe
    String.format(field, 5);    // Format String Checker warns the call might not be safe
    String.format(method(), 5); // Format String Checker warns the call might not be safe
  }
}

void nullnessExample1(@Nullable Object x) {
    Object y = x;
    if (x != null) {
      System.out.println(y.toString());
    }
  }

  void nullnessExample12(@Nullable Object x) {
    if (x != null) {
      Object y = x;
      System.out.println(y.toString());
    }
  }

  void requiresPositive(@Positive int arg) {}

  void intExample1(int x) {
    int y = x*x;
    if (x > 0) {
      requiresPositive(y);
    }
  }

  void intExample2(int x) {
    int y = x*x;
    if (y > 0) {
      requiresPositive(x);
    }
  }

  void intExample1a(int x) {
    if (x > 0) {
      int y = x*x;
      requiresPositive(y);
    }
  }

  void falsePositive2(int arg) {
    Object o;
    if (arg * arg >= arg) { // always true!
      o = new Object();
    }
    o.toString();  // Nullness Checker issues a false positive warning
  }

  void falsePositive1(boolean b) {
    Object o;
    if (b) {
      o = new Object();
    }
    if (b) {
      o.toString();  // Nullness Checker issues a false positive warning
    }
  }

  class MyClass {
    void requiresA(@A MyClass this) { ... }
    void requiresB(@B MyClass this) { ... }
  }

  @A MyClass myA = ...;
  @B MyClass myB = ...;

  myA.requiresA()    // OK
  myA.requiresB()    // compile-time error
  myB.requiresA()    // OK
  myB.requiresB()    // OK

  void method(String @NonEmpty [] x) {}
  void method(String @NonEmpty ... x) {}

  void method(@English String [] x) {}
  void method(@English String ... x) {}

  @Version("2.0") Widget createWidget(String value) { ... }

  entity.hibernate. @Nullable User x;

  @Nullable entity.hibernate.User x;  // illegal Java syntax

error: scoping construct for static nested type cannot be annotated
error: scoping construct cannot be annotated with type-use annotation

  import android.support.annotation.NonNull;
  ...
  @NonNull Object [] returnsArray();

  import org.checkerframework.checker.nullness.qual.NonNull;
  ...
  Object @NonNull [] returnsArray();

    @Deprecated    // programmers should not use this class
    class MyClass { ... }

    @Override      // this method overrides a method in a supertype
    void myMethod() { ... }

    @SuppressWarnings(...) // compiler should not warn about the initialization expr
    int myField = INITIALIZATION-EXPRESSION;

    @Override
    @Regex String getPattern() { ... }

    @GuardedBy("myLock")
    @NonNull String myField;

  // Wrong formatting
  @Positive
  public int numItems;

  // Right
  public @Positive int numItems;

  // Wrong formatting
  @Nullable
  public Object getThing() {
    ...
  }

  // Right
  public @Nullable Object getThing() {
    ...
  }

  // Wrong formatting
  @Deprecated URL toURL() {
    ...
  }

  // Right
  @Deprecated
  URL toURL() {
    ...
  }

  @Deprecated
  public @Interned class Level {
    ...
  }

class MyClass<T> { ... }
class MyClass<T extends Object> { ... }

class MyClass<T>                 ==  class MyClass<T extends @TOPTYPEANNO Object>
class MyClass<T extends Object>  ==  class MyClass<T extends @DEFAULTANNO Object>

  @SubtypeOf(Unqualified.class)
  @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
  public @interface Encrypted {}

checker-framework/stubparser/dist/stubparser.jar(org/checkerframework/stubparser/ast/CompilationUnit.class):
warning: [classfile] Signature attribute introduced in version 49.0 class files is ignored in version 46.0 class files

com.sun.tools.javac.code.Symbol$CompletionFailure: class file for com.sun.source.tree.Tree not found

...\build.xml:59: Error running ${env.CHECKERFRAMEWORK}\checker\bin\javac.bat compiler

.../bin/javac: Command not found

error: Annotation processor 'org.checkerframework.checker.signedness.SignednessChecker' not found

The hierarchy of the type ClassName is inconsistent

The type com.sun.source.util.AbstractTypeProcessor cannot be resolved.
  It is indirectly referenced from required .class files

  java.lang.ArrayStoreException: sun.reflect.annotation.TypeNotPresentExceptionProxy

Caused by: java.util.zip.ZipException: error in opening zip file
    at java.util.zip.ZipFile.open(Native Method)
    at java.util.zip.ZipFile.<init>(ZipFile.java:131)

error: SourceChecker.typeProcess: unexpected Throwable (OutOfMemoryError) while processing ...
  ; message: GC overhead limit exceeded

error: scoping construct for static nested type cannot be annotated
error: scoping construct cannot be annotated with type-use annotation

if (currentOutgoing != null && !message.isCompleted()) {
    currentOutgoing.continueBuffering(message);
}

warning: [dereference.of.nullable] dereference of possibly-null reference currentOutgoing
    currentOutgoing.continueBuffering(message);
    ^

method sleep in class Thread cannot be applied to given types
cannot find symbol: constructor StringBuffer(StringBuffer)

mypackage/MyClass.java:2044: warning: incompatible types in assignment.
      T retval = null;
                 ^
  found   : null
  required: T extends @MyQualifier Object

MyFile.java:123: error: incompatible types in argument.
                        myModel.addElement("Scanning directories...");
                                           ^
  found   : String
  required: ? extends Object

  DefaultListModel myModel;

  DefaultListModel<String> myModel;

error: annotation type not applicable to this kind of declaration
    ... List<@NonNull String> ...

The annotation @NonNull is disallowed for this location

public String(char value[], @IndexFor("value") int offset, @IndexOrHigh("value") int count) { ... }

[expression.unparsable.type.invalid] Expression in dependent type annotation invalid:
Use "#1" rather than "value"

public String(char value[], @IndexFor("#1") int offset, @IndexOrHigh("#1") int count) { ... }

  void m() {
    String t = "";
    t.toString();
    try {
    } catch (Throwable e) {
        t.toString(); // Nullness Checker issues spurious (dereference.of.nullable)
    }

  error: annotation values must be of the form 'name=value'
        @LTLengthOf("firstName", "lastName") int index;
                    ^

        @LTLengthOf({"firstName", "lastName"}) int index;

sudo apt-get -qqy update
sudo apt-get -qqy install \
 openjdk-17-jdk \
 ant cpp git gradle jq libcurl3-gnutls \
 make maven pipx python3-pip python3-requests unzip wget \
 autoconf devscripts dia hevea imagemagick junit latexmk \
 librsvg2-bin libasound2-dev libcups2-dev libfontconfig1-dev \
 libx11-dev libxext-dev libxrender-dev libxrandr-dev libxtst-dev libxt-dev \
 pdf2svg rsync shellcheck \
 texlive-font-utils texlive-fonts-recommended \
 texlive-latex-base texlive-latex-extra texlive-latex-recommended
pipx install black
pipx install flake8
pipx install html5validator
pipx ensurepath

  export JAVA_HOME=${JAVA_HOME:-$(dirname "$(dirname "$(readlink -f "$(which javac)")")")}

brew update
brew install git ant hevea maven librsvg unzip make
brew tap homebrew/cask-versions
brew install --cask temurin@17
brew install --cask mactex

mkdir -p $HOME/Library/texmf/tex/latex
cp -p /usr/local/Cellar/hevea/2.36/lib/hevea/hevea.sty $HOME/Library/texmf/tex/latex/

export JAVA_HOME=$(/usr/libexec/java_home -v 17)

export JAVA_HOME=/Library/Java/JavaVirtualMachines/adoptopenjdk-17.jdk/Contents/Home/

git clone https://github.com/eisop/checker-framework.git checker-framework
export CHECKERFRAMEWORK=$(pwd)/checker-framework

  cd $CHECKERFRAMEWORK
  ./gradlew assemble

export PATH=$CHECKERFRAMEWORK/checker/bin:${PATH}

  cd $CHECKERFRAMEWORK
  ./gradlew publishToMavenLocal

  cd $CHECKERFRAMEWORK
  ./gradlew allTests

docker pull mdernst/cf-ubuntu-jdk17
docker run -it mdernst/cf-ubuntu-jdk17 /bin/bash

cd $CHECKERFRAMEWORK
git pull
checker/bin-devel/clone-related.sh

x.f	f is @NonNull	f is @Nullable
x is @Initialized	@Initialized @NonNull	@Initialized @Nullable
x is @UnderInitialization	@UnknownInitialization @Nullable	@UnknownInitialization @Nullable
x is @UnknownInitialization	@UnknownInitialization @Nullable	@UnknownInitialization @Nullable

@KeyForBottom default	@UnknownKeyFor default (current choice)

class MyClass1<@UnknownKeyFor T> {	class MyClass1<T> {
‍ ‍T var = null; // OK	‍ ‍T var = null; // OK

class MyClass2<T> {
‍ ‍@UnknownKeyFor T var = null; // OK

class MyClass3<T> {
‍ ‍T var = null; // ERROR

	class MySet1<T> implements Set<T> { }
	MySet1<@KeyFor("m") String> s1; // ERROR

class Set<E> { }	class Set<@KeyForBottom E> { }
class MySet2<T> implements Set<T> { }	class MySet2<@KeyForBottom T> implements Set<T> { }
MySet2<@KeyFor("m") String> s2; // OK ‍ ‍ ‍	MySet2<@KeyFor("m") String> s2; // OK

fully qualified name	Class.getName	field descriptor	binary name	internal form	Class.getSimpleName
int	int	I	n/a for primitive type	n/a for primitive type	int
int[][]	[[I	[[I	n/a for array type	n/a for array type	int[][]
MyClass	MyClass	LMyClass;	MyClass	MyClass	MyClass
MyClass[]	[LMyClass;	[LMyClass;	n/a for array type	n/a for array type	MyClass[]
n/a for anonymous class	MyClass$22	LMyClass$22;	MyClass$22	MyClass$22	(empty string)
n/a for array of anon. ‍class	[LMyClass$22;	[LMyClass$22;	n/a for array type	n/a for array type	[]
java.lang.Integer	java.lang.Integer	Ljava/lang/Integer;	java.lang.Integer	java/lang/Integer	Integer
java.lang.Integer[]	[Ljava.lang.Integer;	[Ljava/lang/Integer;	n/a for array type	n/a for array type	Integer[]
pkg.Outer.Inner	pkg.Outer$Inner	Lpkg/Outer$Inner;	pkg.Outer$Inner	pkg/Outer$Inner	Inner
pkg.Outer.Inner[]	[Lpkg.Outer$Inner;	[Lpkg/Outer$Inner;	n/a for array type	n/a for array type	Inner[]
n/a for anonymous class	pkg.Outer$22	Lpkg/Outer$22;	pkg.Outer$22	pkg/Outer$22	(empty string)
n/a for array of anon. ‍class	[Lpkg.Outer$22;	[Lpkg/Outer$22;	n/a for array type	n/a for array type	[]

	Initialization Checker	Initialized Fields Checker
superclasses	tracks initialization of supertype fields	checks one class at a time
partial initialization	changes the types of fields that are not initialized	unsound treatment of partially-initialized objects (*)
type systems	works only with the Nullness Checker (**)	works for any type system
disabling	always runs with the Nullness Checker	can be enabled/disabled per run

Subtyping Checker	Nullness Checker	Index Checker	Tainting Checker	…	Your Checker
Base Checker (enforces subtyping rules)						Type inference	Other tools
Checker Framework (enables creation of pluggable type-checkers)						Annotation File Utilities (.java ↔ .class files)
Java type annotations syntax and classfile format (no built-in semantics)

Declarations	Expression	Expression’s nullness type, or checker error
class C { @NonNull Object f; @Nullable Object g; ... }
@NonNull @Initialized C a;	a	@NonNull
	a.f	@NonNull
	a.g	@Nullable
@NonNull @UnderInitialization C b;	b	@NonNull
	b.f	@MonotonicNonNull
	b.g	@Nullable
@Nullable @Initialized C c;	c	@Nullable
	c.f	error: deref of nullable
	c.g	error: deref of nullable
@Nullable @UnderInitialization C d;	d	@Nullable
	d.f	error: deref of nullable
	d.g	error: deref of nullable

x.f = y	y is @Initialized	y is @UnderInitialization	y is @UnknownInitialization
x is @Initialized	yes	no	no
x is @UnderInitialization	yes	yes	yes
x is @UnknownInitialization	yes	no	no

	MyList1	MyList2	MyList3
t = null;	OK	error	error
t = nble;	OK	error	error
nble = null;	OK	OK	OK
nn = null;	error	error	error
t = this.get(0);	OK	OK	OK
nble = this.get(0);	OK	OK	OK
nn = this.get(0);	error	OK	error
this.add(t);	OK	OK	OK
this.add(nble);	OK	error	error
this.add(nn);	OK	OK	OK

The Checker Framework Manual: Custom pluggable types for Java

https://eisop.github.io/

Version 3.42.0-eisop4 (12 Jul 2024)

Contents

Chapter ‍1 Introduction

1.1 How to read this manual

1.2 How it works: Pluggable types

1.3 Installation

1.4 Example use: detecting a null pointer bug

Chapter ‍2 Using a checker

2.1 Where to write type annotations

2.2 Running a checker

2.2.1 Using annotated libraries

2.2.2 Summary of command-line options

2.2.3 Checker auto-discovery

2.2.4 Shorthand for built-in checkers

2.3 What the checker guarantees

2.4 Tips about writing annotations

2.4.1 Write annotations before you run a checker

2.4.2 How to get started annotating legacy code

Start small

Annotations are a specification

Write good code

2.4.3 Annotations indicate non-exceptional behavior

Methods that crash when passed certain values

Nullness example

Optional example

Permitting crashes in some called methods

Methods that sometimes crash when passed certain values

2.4.4 Subclasses must respect superclass annotations

2.4.5 What to do if a checker issues a warning about your code

Step 1: Explain correctness: write a proof

Step 2: Translate the proof into annotations.

Step 3: Re-run the checker

2.4.6 Calls to unannotated code (legacy libraries)

Chapter ‍3 Nullness Checker

3.1 What the Nullness Checker guarantees

3.1.1 Nullness Checker optional warnings

3.2 Nullness annotations

3.2.1 Nullness qualifiers

3.2.2 Nullness method annotations

3.2.3 Initialization qualifiers

3.2.4 Map key qualifiers

3.3 Writing nullness annotations

3.3.1 Implicit qualifiers

3.3.2 Default annotation

3.3.3 Conditional nullness

3.3.4 Nullness and array initialization

3.3.5 Nullness and conversions from collections to arrays

3.3.6 Run-time checks for nullness

3.3.7 Inference of @NonNull and @Nullable annotations

3.4 Suppressing nullness warnings

3.4.1 Suppressing warnings with assertions and method calls

3.4.2 Null arguments to collection classes

3.4.3 Conservative nullness annotations on the JDK

3.5 Examples

3.5.1 Tiny examples

3.5.2 Example annotated source code

3.5.3 Publications

3.6 Tips for getting started

3.7 Other tools for nullness checking

3.7.1 Which tool is right for you?

3.7.2 Incompatibility note about FindBugs and SpotBugs @Nullable

3.7.3 Relationship to Optional<T>

3.8 Initialization Checker

3.8.1 Initialization qualifiers

3.8.2 How an object becomes initialized

3.8.3 @UnderInitialization examples

3.8.4 Partial initialization

3.8.5 Method calls from the constructor

3.8.6 Initialization of circular data structures

3.8.7 How to handle warnings

“error: the constructor does not initialize fields: …”

“call to … is not allowed on the given receiver”

3.8.8 Suppressing warnings

3.8.9 More details about initialization checking

Use of method annotations

Source of the type system

Chapter ‍4 Map Key Checker

4.1 Invoking the Map Key Checker

The Checker Framework Manual:
Custom pluggable types for Java