[Checkers] Nullness inference

[Fausto Spoto]

Hi Michael.

I attach the stub files generated for JFlex. Those for Daikon will be
sent next week, since I am on a slow internet connection and cannot
download the Daikon package at the moment.

For @PolyNull, I understand that it stands for both @Nullable and
@NonNull, like a template in C++. However, I wonder whether you can use
it in every place where a type is allowed. For instance, what is the
meaning of

void m(@PolyNull Object obj)

or

void m(@PolyNull Object obj1, @PolyNull Object obj2)

?

I cannot see any difference wrt

void m(@Nullable Object obj)
void m(@Nullable Object obj1, @Nullable Object obj2)

respectively. Also, what is the meaning of a @PolyNull field:

@PolyNull Object f;

?

Are two @PolyNull methods completely independent wrt the choice made for
their @PolyNull variables?

For the moment, I generate @PolyNull annotations only for methods
returning a reference type whose non-nullness has not been proved, but
which are provably non-null whenever a parameter of the method is
non-null. Attached, you see an example PolyNull.java and the stub file
that my tool generates for it. Non such example is found in JFlex. Do
you have an example of @PolyNull which should be found for JFlex?

There is no special support for generics in my tool. The problem is that
the types have been erased in the bytecode. I can problably instruct the
analyzer to use some types or to consult some source code (this might
take some work, but it is feasable). However, I find many problems. For
instance, in a map class:

class Map<T,D> {
   void put(T from, D to) {}
   void D get(T from) {}
}

it is impossible to prove that get() returns a @NonNull D even through
the program always puts a @NonNull D inside the map. This is because you
have to prove that all calls to get() receive a parameter which has been
already put in the map, a difficult thing to prove.

Can I use your type-checkers on my stub files or should I wait for some
translator?

Have nice new year.
  Fausto
-------------- next part --------------
A non-text attachment was scrubbed...
Name: juliaOutput_for_JFlex.tar
Type: application/x-tar
Size: 102400 bytes
Desc: 
Url : https://lists.csail.mit.edu/mailman/private/checkers/attachments/20081231/c9dcb3bb/attachment-0001.tar 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: PolyNull.java
Type: text/x-java
Size: 507 bytes
Desc: not available
Url : https://lists.csail.mit.edu/mailman/private/checkers/attachments/20081231/c9dcb3bb/attachment-0001.java 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: PolyNull.nullness.stub
Type: text/x-csrc
Size: 618 bytes
Desc: not available
Url : https://lists.csail.mit.edu/mailman/private/checkers/attachments/20081231/c9dcb3bb/attachment-0001.c