Postcondition annotations that reference "this" in conditional blocks aren't lubbed correctly afterward

[kelloggm]

Consider the following program (checked in as checker/tests/calledmethods/EnsuresCalledMethodsThisLub.java on this branch: https://github.com/kelloggm/checker-framework/tree/postcondition-this-bug):

import org.checkerframework.checker.calledmethods.qual.CalledMethods;
import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;

class EnsuresCalledMethodsThisLub {

  @EnsuresCalledMethods(
      value = "#1",
      methods = {"toString", "equals"})
  void call1(Object obj) {
    obj.toString();
    obj.equals(null);
  }

  @EnsuresCalledMethods(
      value = "#1",
      methods = {"toString", "hashCode"})
  void call2(Object obj) {
    obj.toString();
    obj.hashCode();
  }

  void test(boolean b) {
    if (b) {
      call1(this);
    } else {
      call2(this);
    }
    @CalledMethods("toString") Object obj1 = this;
    // :: error: (assignment)
    @CalledMethods({"toString", "equals"}) Object obj2 = this;
  }

  void test_arg(Object arg, boolean b) {
    if (b) {
      call1(arg);
    } else {
      call2(arg);
    }
    @CalledMethods("toString") Object obj1 = arg;
    // :: error: (assignment)
    @CalledMethods({"toString", "equals"}) Object obj2 = arg;
  }
}

I expect that the two errors above will be issued. However, when this test is run, only the second error is issued.

In particular, the type of this in test after the end of the if statement is @CalledMethods({"toString", "equals", "call1"}) - indicating that only the then store was propagated past the end of the if block. Instead, I would expect the two stores to be LUB'd to give @CalledMethods("toString"), as occurs in the second example (test_arg()).

I don't know of any of other type system that has a postcondition annotation that can reference this besides Called Methods, so I haven't reproduced this with any other checker. However, this issue came up when trying to add postcondition inference for "this" to WPI, so I've observed it with the AinferTestChecker and I believe it would apply to any checker where postcondition annotations whose expression resolves to this makes sense.