[Checkers] Bug report: compiler and checker framework crash

Mahmood Ali mahmood at MIT.EDU
Wed Jul 2 12:41:31 EDT 2008


Hi Andrzej,

Thank you for your bug report.

I was able to identify and fix both problems.  The fix should be in  
the next release (planned this Thursday or Friday).

As for the odd warning messages, we would appreciate suggestions on  
how to improve the message readability.

You get two types of error messages:
1. five errors of the type 'incompatible types,' like:
     [javac] /DS/home-0/mernst/tmp/JUtil/org/softevo/jutil/graphs/ 
Graph.java:75: incompatible types.
     [javac] found   : @Nullable <nulltype>
     [javac] required: @Raw Map<@NonNull V extends @NonNull  
Serializable, @NonNull Map>
     [javac] 		this.predecessors = null;
     [javac] 		                    ^

The current default for the Nullness checker is that it assumes that  
all types, except for local variable raw types, are non-null types.   
Hence you getting an error regarding assigning a 'null' to the fields.

You may fix this by annotating marking the type of the fields Nullable  
(i.e. @Nullable Map<...> predecessors ).  The reason for having '@Raw'  
is explained in the following item.

2. three errors of the type 'call ... not allowed on the given  
receiver', like:
     [javac] /DS/home-0/mernst/tmp/JUtil/org/softevo/jutil/graphs/ 
Graph.java:79: call to addVertex(V) not allowed on the given receiver.
     [javac] found   : @Raw Graph
     [javac] required: @NonNull Graph
     [javac] 			addVertex (from);
     [javac] 			          ^


The Nullness type system introduce the qualifier Raw to the  
constructors.  It signifies that the object being constructed is in  
the construction phase and that some of its fields (even if marked  
NonNull) may be not be set yet.  Calls to addVertex() from the  
constructor are not guaranteed to be valid as addVertex() may  
dereference fields not yet set.

Unfortunately, such calls would be application invariant false- 
positives.  You cannot simply eliminate these errors by marking  
addVertex() receiver as Raw.

A possible solution, in future releases, might be is that the flow- 
sensitive analysis could determine that if the all the fields have  
been set before a method invocation, then the type of the constructed  
object is 'NonNull Foo' rather than 'Raw Foo'.  In this proposal,  
these errors would be eliminated.  Is it a sound proposal?

Regards,
Mahmood






More information about the checkers mailing list