figure out why Infer assumes that the receiver of a call is a distinct object

[rgrig]

The example

class Repro {
  static Repro good;
  void f() {
    good.hashCode();
 //   while (this != Repro.good);
  }
  static void g(Repro x) {
    x.f();
  }
  static void h() {
    Repro x = good = new Repro();
    g(x);
  }
}

does not infer any specs on h. The reason is that the specs on g require the argument (x) and the static field (good) to be both allocated on the heap, and therefore distinct objects. In the symbolic execution of the body of g (during re-execution at least) Infer adds the assumption that x must be a distinct object on the heap. It adds this assumption just before calling f.

[rgrig]

It's a heuristic done on purpose. Infer can be given a hint with an if.