checker/tests/nullness/AssertAfter2.java

import java.util.HashMap;
import java.util.List;
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;

public class AssertAfter2 {

  public class Graph<T> {

    HashMap<T, List<@KeyFor("childMap") T>> childMap;

    public Graph(HashMap<T, List<@KeyFor("childMap") T>> childMap) {
      this.childMap = childMap;
    }

    @SuppressWarnings("contracts.postcondition")
    @EnsuresNonNull("childMap.get(#1)")
    public void addNode(final T n) {
      // body omitted, not relevant to test case
    }

    public void addEdge(T parent, T child) {
      addNode(parent);
      @NonNull List<@KeyFor("childMap") T> l = childMap.get(parent);
    }

    public void addEdgeBad1(T parent, T child) {
      // :: error: (assignment)
      @NonNull List<@KeyFor("childMap") T> l = childMap.get(parent);
    }

    public void addEdgeBad2(T parent, T child) {
      addNode(parent);
      // :: error: (assignment)
      @NonNull List<@KeyFor("childMap") T> l = childMap.get(child);
    }

    public void addEdgeBad3(T parent, T child) {
      addNode(parent);
      parent = child;
      // :: error: (assignment)
      @NonNull List<@KeyFor("childMap") T> l = childMap.get(parent);
    }

    public void addEdgeOK(T parent, T child) {
      List<@KeyFor("childMap") T> l = childMap.get(parent);
    }
  }

  class MultiParam {

    MultiParam(MultiParam thing, Object f1, Object f2, Object f3) {
      this.thing = thing;
      this.f1 = f1;
      this.f2 = f2;
      this.f3 = f3;
    }

    MultiParam thing;

    @SuppressWarnings("contracts.postcondition")
    @EnsuresNonNull("get(#1, #2, #3)")
    void add(final Object o1, final Object o2, final Object o3) {
      // body omitted, not relevant to test case
    }

    @org.checkerframework.dataflow.qual.Pure
    @Nullable Object get(Object o1, Object o2, Object o3) {
      return null;
    }

    Object f1, f2, f3;

    void addGood1() {
      thing.add(f1, f2, f3);
      @NonNull Object nn = thing.get(f1, f2, f3);
    }

    void addBad1() {
      // :: error: (assignment)
      @NonNull Object nn = get(f1, f2, f3);
    }

    void addBad2() {
      thing.add(f1, f2, f3);
      f1 = new Object();
      // :: error: (assignment)
      @NonNull Object nn = thing.get(f1, f2, f3);
    }

    void addBad3() {
      thing.add(f1, f2, f3);
      f2 = new Object();
      // :: error: (assignment)
      @NonNull Object nn = thing.get(f1, f2, f3);
    }

    void addBad4() {
      thing.add(f1, f2, f3);
      f3 = new Object();
      // :: error: (assignment)
      @NonNull Object nn = thing.get(f1, f2, f3);
    }
  }
}