Different default nullness annotations for source and class files?

[GoogleCodeExporter]

If the nullness checker is run on both of the attached source files, no errors 
are reported. However, if the nullness checker is run on Delta.java with the 
class file for ImmutableList on the classpath, an error is reported:

$ javac -version -processor checkers.nullness.NullnessChecker Delta.java 
com/google/common/collect/ImmutableList.java -d bin/
javac 1.8.0-jsr308-1.6.7
$ javac -version -processor checkers.nullness.NullnessChecker -cp bin/ 
Delta.java 
javac 1.8.0-jsr308-1.6.7
Delta.java:7: error: incompatible types in type argument.
    this.field = ImmutableList.copyOf(field);
                                     ^
  found   : E extends @Initialized @Nullable Object
  required: @Initialized @NonNull Object
1 error

I believe the issue is that signature of ImmutableList.copyOf in the source 
file is:

public static <E> List<E> copyOf(Iterable<? extends E> elements);

But after being compiled, the signature in the class file as:

public static <E extends java/lang/Object> java.util.List<E> 
copyOf(java.lang.Iterable<? extends E>);

The manual section '18.1.4  Defaults for bounds' 
(http://types.cs.washington.edu/checker-framework/current/checkers-manual.html#g
enerics) explains the distinction the nullness checker makes between <T> and <T 
extends Object>, but it looks like the distinction breaks down for class files 
when the implicit 'extends Object' is made explicit by the compiler.

Original issue reported on code.google.com by cus...@google.com on 14 Oct 2013 at 9:05

Attachments:

• repro.zip

[GoogleCodeExporter]

This is related to Issue 240: once we only have the Element, either because 
it's a different class or because we go through bytecode, the defaulting logic 
changes.
We need to find a way to store the defaults back into the Element and bytecode, 
to allow for this.

Original comment by wdi...@gmail.com on 15 Oct 2013 at 3:38

[GoogleCodeExporter]

As expected, this issue went away with the fix for Issue 240.
I added a test case at:
checker-framework/checkers/tests/nullness-extra/issue265/
Please do let us know whether this fixes your issue.

Original comment by wdi...@gmail.com on 7 Feb 2014 at 9:01

• Changed state: Pushed

[GoogleCodeExporter]

Original comment by Jonathan...@gmail.com on 20 Feb 2014 at 6:41

• Changed state: Fixed