[Checkers] Nullness inference

Mahmood Ali mahmood at MIT.EDU
Sat Jan 3 11:36:37 EST 2009


Greetings Mike,

> 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.
>
This rule doesn't address the Fausto's case, as the equality tests  
against polynull not nonnull.

Let me formulate the proposal in a different way:
1. within the scope of a succeeding (p1 == p2) and a subtyping  
relationship exists between them (i.e. not mutable == immutable), then  
both of their types are inferred to be the most restrictive type of  
them.

In this case of of id2 where we had
   if (p == polynull) return p;
p in the return statement would be of polynull type.

A side-effect would be
   if (readOnlyDate == mutableDate)
     readOnlyDate.setTime(0);

2. as a special case of the nullness checker, in the scope of success of
   (polynull == null)
then all null types (even those of null literals) would be refined to  
polynull.  This solves the case of
   @PolyNull Object idNullness(@PolyNull Object p) {
     if (p == null) return null;
     else return "m";
   }

This latter part seems like a hack to me more than anything though.

Regards,
Mahmood




More information about the checkers mailing list