[Checkers] Nullness inference

[Fausto Spoto]

Hi!

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.

I will check the results now. I suspect that they will mostly coincide
with your manual annotations. There will be cases where my analyzer is
less precise and they will be very interesting to me. There might be
cases of the other way round, but I do not expect an automatic tool to
be more precise than a manual annotation. I expect it to build a good
annotation in a few seconds, that's all.

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.

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...

Fausto

On Sat, 2009-01-03 at 15:08 -0800, Michael Ernst wrote:
> Mahmood-
> 
> Your generalization of my suggestion seems correct; you're right that I
> didn't spell out all the details, but that's essentially what I had in
> mind.  Thanks!
> 
> Technically, I like this increased precision.  The question that remains
> for me is how important this is.  Fausto has already shown that it can come
> up in practice, so that isn't the question.  I wonder if a programmer would
> prefer his more precise (and more tricky) type, or if there are places that
> it enables other precision that eases type-checking or understanding.  I
> could go either way -- I just don't have any evidence.
> 
>                     -Mike
-------------- next part --------------
A non-text attachment was scrubbed...
Name: juliaOutput.tgz
Type: application/x-compressed-tar
Size: 5391 bytes
Desc: not available
Url : https://lists.csail.mit.edu/mailman/private/checkers/attachments/20090107/8262043d/attachment-0001.bin 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: TestUtilMDE.java
Type: text/x-java
Size: 109688 bytes
Desc: not available
Url : https://lists.csail.mit.edu/mailman/private/checkers/attachments/20090107/8262043d/attachment-0001.java