[Checkers] Nullness inference

[Michael Ernst]

Fausto-

> Here is the result of analyzing the utilMDE package. I started the
> analysis from the attached TestUtilMDE.java file, where I uncommented a
> main() method. The original main() method led my analyzer into just a
> few methods. This is typically a consequence of the use of reflection,
> which is a problem for static analysis in general.

Right.  You could always hard-code knowledge about how JUnit happens to
work (which is pretty simple), but it's not clear that is worth doing at
this point.

> I will check the results now. I suspect that they will mostly coincide
> with your manual annotations.
> ...
> I do not expect an automatic tool to
> be more precise than a manual annotation.

The manual annotations are written so as to type-check, so they may be less
precise than the inference results in some cases.  Even if they are the
same, that will be a big benefit since the manual annotations required
human effort.

> For the situations like the id2() method where my analyzer yields a
> result which is too "semantical" for your type checking engines, I
> suspect that they are not frequent situations in practice. But that
> extra information is useful for reducing the number of false warnings
> about possible NullPointerException's, which is the main goal of my
> analyzer.

I agree.  In that particular case, we know how to enhance the checker
to not issue a warning, and if there are enough such examples we will do
so.

> For the reason why the analyzer is not publicly available, it is just
> because we are making it into a commercial tool, for nullness,
> termination, side effects analysis and so on. But the web interface will
> be free of charge, at least for the first months. And we might well
> change our mind...

I see.  Good luck with that.  I imagine that comparing with our tool will
help to improve yours as well.  (And vice versa, of course.)

                    -Mike