[Checkers] Nullness inference

[Michael Ernst]

Fausto-

> I will provide the possibility of using the library mode (and test it
> before!) with the next web interface, but the analyzer will not be
> downloadable.

Thanks for the information.  You might want to note on the webpage that the
download version is out of date.  Is there a reason the new version won't
be downloadable?

> > I should also note that julia inferred the parameter types for  
> > PolyNull.id2() incorrectly.  For a method declared as:
> > 
> >    public Object id2(Object p1, Object p2) {
> >      if (p1 == p2) return p1;
> >      else return p2;
> >    }
> > 
> > The declaration should be
> >    public @PolyNull Object id2(@PolyNull Object l1, @PolyNull Object  
> > l2);
> > not (notice l1 declaration)
> >    public @PolyNull Object id2(@Nullable Object l1, @PolyNull Object  
> > l2);
> 
> I'm not sure that I understand the PolyNull annotation then. For me (and
> for julia) it is enough for l2 (i.e. p2) to be non-null to infer that
> the return value is non-null. This is obvious when p1 != p2. But if p1
> == p2, then from the non-nullness of p2 you infer the non-nullness of p1
> and hence of the return value. So I think that the annotation of julia
> is just more precise (and more semantical). But I might miss something
> in my understanding. Let me know.

This is rather tricky reasoning, but I see that it's correct:

  If p2 is non-null, then null can't be returned by
     if (p1 == p2) return p1;
  because p1 and p2 are the same and p2 is non-null.

Mahmood could augment our type-checker with a similar rule:  within the
scope of a succeeding
     (nonnull == nullable)
test, the nullable value is known to be nonnull.

I'm not sure how often this will come up in practice, though.

                    -Mike