Impossible to use version 2.0.0 of @org.eclipse.jdt.annotation.NonNull and @org.eclipse.jdt.annotation.Nullable

[GoogleCodeExporter]

What steps will reproduce the problem?
1.Create in Eclipse a project with compliance JavaSE-1.8.
2.Create the following java file
abstract class Foo<E> {
    E e;

    void bar() {
        e = null;
    }

    abstract <F> Foo<@NonNull F> foo(F newValue);
}
3. The compiler complains that @NonNull cannot be resolved to a type. With 
Ctrl+1, choose the Quick Fix "Copy library with default null annotation to 
build path".
(import org.eclipse.jdt.annotation.NonNull; should be also automatically 
inserted)
4. Ctrl+Click on @NonNull. You should see that the target of @NonNull is 
@Target({ TYPE_USE }), which means that you are really using the version 2.0.0 
of the JDT annotations (and not the version 1.1)
5. Run the Nullness checker adding the version *2.0.0* of the JDT annotations 
to the classpath

What is the expected output? What do you see instead?
Expected: A warning is issued for line 
e = null;
Actual: A compiler error for line
abstract <F> Foo<@NonNull F> foo(F newValue)

What version of the product are you using? On what operating system?
checker-framework: 1.8.5
Eclipse: 4.4.0 (Luna)
Java: 1.8
org.eclipse.jdt.annotations: 2.0.0

Please provide any additional information below.

Original issue reported on code.google.com by ClovisSe...@gmail.com on 25 Sep 2014 at 7:54

[GoogleCodeExporter]

Note also that, after the quick fix, both Eclipse and (the original) javac can 
compile the code without problems.

Original comment by ClovisSe...@gmail.com on 25 Sep 2014 at 7:58

[GoogleCodeExporter]

Hello, 

Thank you for the report.  When encountering bugs in Eclipse please do the 
following.
Go to Eclipse->preferences->Checker Framework
Check the box "Show verbose output"
Then when you run the Checker Framework plugin, you will see command line 
output appear in Eclipse's console window.  Please copy and paste that to the 
original issue.

I believe the issue is that we have a clean room implementation of this 
annotation that differs from the version shown.  This annotation appears on the 
class path in front of Eclipse's when the Checker Framework is run.  
I still get the error message:
/Users/jburke/Documents/workspace/Test/src/Test.java:16: error: annotation type 
not applicable to this kind of declaration
    abstract <F> Foo<@NonNull F> foo(F newValue);

Original comment by Jonathan...@gmail.com on 25 Sep 2014 at 8:07

[GoogleCodeExporter]

> "%JAVA_HOME%/bin/javac" -cp 
C:\eclipse\plugins\org.eclipse.jdt.annotation_2.0.0.v20140415-1436.jar Foo.
java

(no error)

>c:\checker-framework-1.8.6\checker\bin\javac -cp 
C:\eclipse\plugins\org.eclipse.jdt.annotation_2.0.0.v2
0140415-1436.jar Foo.java
Foo.java:10: error: annotation type not applicable to this kind of declaration
    abstract <F> Foo<@NonNull F> foo(F newValue);
                     ^
1 error

Original comment by ClovisSe...@gmail.com on 25 Sep 2014 at 9:20

[GoogleCodeExporter]

It appears that Eclipse has made a breaking, non-backward-compatible change to 
their definition of the @NonNull annotation.  It's a good change!  But it's a 
breaking one nonetheless.

The Checker Framework ships with a cleanroom reimplementation of Eclipse's old 
@NonNull annotation, and it puts that on the classpath.

Here are some options:
 * the Checker Framework continues to include its current reimplementation; this does not work for people expecting the new version of the Eclipse annotations.
 * the Checker Framework updates its reimplementation; this does not work for people expecting the old version of the Eclipse annotations.
 * the Checker Framework drops its reimplementation from its jar file; this leads to compilation errors for people who try to run the Checker Framework on code that includes the Eclipse annotations.  They must manually include the appropriate cleanroom or real annotation implementations on the classpath.
 * the Checker Framework has some way of detecting what version of the Eclipse annotations a developer was expecting to use and automatically chooses that one.  I don't know how to implement this, and it sounds tricky.

I lean toward option #2, on the theory that very few people are currently using 
the Eclipse annotations and those people are in the process of switching to the 
newer ones.

An alternative that could give the best of all worlds (but is extra work, and 
I'm not sure it's worth it!) is to add a flag to the Checker Framework javac to 
enable putting user-specified items before checker.jar on the classpath.

A user can work around the problem by following the instructions in section 
25.1, "Javac compiler" and ensuring that the appropriate items are on the 
classpath before checker.jar, but that is not trivial to do.

Thoughts?

Original comment by michael.ernst@gmail.com on 29 Sep 2014 at 9:53

[GoogleCodeExporter]

Original comment by michael.ernst@gmail.com on 10 Nov 2014 at 7:27

• Changed state: Pushed

[GoogleCodeExporter]

Original comment by jtha...@cs.washington.edu on 20 Dec 2014 at 2:16

• Changed state: Fixed