Using checker framework with Java 7
Angelika Langer
This is probably a silly question, but ...
I was trying to use the checkers in conjunction with the latest OpenJDK
7 release (b105), that is, I do not want to use the Java compiler that
comes with the checker framework, but want to use the regular JDK 7
compiler.
How does it work? I am looking for instructions on how to specify
-classpath and -processorpath, but could not find any instructions.
Is there a description someplace?
Details of my futile attempts to use the checkers are attached.
Thanks
Angelika
Paulo Henrique Ferreira Costa
You need use the compiler of checker framework, because if you use the java compiler standard, it doesn't call the class that extend the java process API that implement the roles of checker and don't recognize the class of te checker during the compilation.
What you could use ant in the place of checker compiler. I'm send a example in attachment.
I wait that this example help you.
Regards,
Paulo
These are the JVM options I specified (under the assumption that jsr308-all.jar would contain all the checker classes).
%JAVA7_HOME%\bin\javac
-classpath .;%CHECKERS_HOME%\binary\jsr308-all.jar
-processorpath %CHECKERS_HOME%\binary\jsr308-all.jar
-processor checkers.nullness.NullnessChecker
TypeCheckersTest.java
This is the result I receive:
java.lang.Error: NullnessSubchecker processor threw unexpected exception when processing TypeCheckersTest.java
at checkers.source.SourceChecker.typeProcess(SourceChecker.java:223)
at checkers.util.AggregateChecker.typeProcess(AggregateChecker.java:59)
at com.sun.source.util.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:206)
at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished(AbstractTypeProcessor.java:236)
at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished(AbstractTypeProcessor.java:236)
at com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1192)
at com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1151)
at com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:842)
at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:801)
at com.sun.tools.javac.main.Main.compile(Main.java:409)
at com.sun.tools.javac.main.Main.compile(Main.java:327)
at com.sun.tools.javac.main.Main.compile(Main.java:318)
at com.sun.tools.javac.Main.compile(Main.java:82)
at com.sun.tools.javac.Main.main(Main.java:67)
Caused by: java.lang.NoClassDefFoundError: checkers/types/visitors/AnnotatedTypeScanner
at checkers.basetype.BaseTypeChecker.createSourceVisitor(BaseTypeChecker.java:262)
at checkers.basetype.BaseTypeChecker.createSourceVisitor(BaseTypeChecker.java:83)
at checkers.source.SourceChecker.typeProcess(SourceChecker.java:216)
... 13 more
Caused by: java.lang.ClassNotFoundException: checkers.types.visitors.AnnotatedTypeScanner
at java.net.URLClassLoader$1.run(URLClassLoader.java:299)
at java.net.URLClassLoader$1.run(URLClassLoader.java:288)
at java.security.AccessController.doPrivileged(Native Method)
at java.net.URLClassLoader.findClass(URLClassLoader.java:287)
at java.lang.ClassLoader.loadClass(ClassLoader.java:422)
at java.lang.ClassLoader.loadClass(ClassLoader.java:355)
... 16 more
An exception has occurred in the compiler (1.7.0-ea). Please file a bug at the Java Developer Connection (http://java.sun.com/webapps/bugreport) after checking the Bug Parade for duplicates. Include your program and the following diagnostic in your report. Thank you.
java.lang.Error: NullnessSubchecker processor threw unexpected exception when processing TypeCheckersTest.java
at checkers.source.SourceChecker.typeProcess(SourceChecker.java:223)
at checkers.util.AggregateChecker.typeProcess(AggregateChecker.java:59)
at com.sun.source.util.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:206)
at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished(AbstractTypeProcessor.java:236)
at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished(AbstractTypeProcessor.java:236)
at com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1192)
at com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1151)
at com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:842)
at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:801)
at com.sun.tools.javac.main.Main.compile(Main.java:409)
at com.sun.tools.javac.main.Main.compile(Main.java:327)
at com.sun.tools.javac.main.Main.compile(Main.java:318)
at com.sun.tools.javac.Main.compile(Main.java:82)
at com.sun.tools.javac.Main.main(Main.java:67)
Caused by: java.lang.NoClassDefFoundError: checkers/types/visitors/AnnotatedTypeScanner
at checkers.basetype.BaseTypeChecker.createSourceVisitor(BaseTypeChecker.java:262)
at checkers.basetype.BaseTypeChecker.createSourceVisitor(BaseTypeChecker.java:83)
at checkers.source.SourceChecker.typeProcess(SourceChecker.java:216)
... 13 more
Caused by: java.lang.ClassNotFoundException: checkers.types.visitors.AnnotatedTypeScanner
at java.net.URLClassLoader$1.run(URLClassLoader.java:299)
at java.net.URLClassLoader$1.run(URLClassLoader.java:288)
at java.security.AccessController.doPrivileged(Native Method)
at java.net.URLClassLoader.findClass(URLClassLoader.java:287)
at java.lang.ClassLoader.loadClass(ClassLoader.java:422)
at java.lang.ClassLoader.loadClass(ClassLoader.java:355)
... 16 more
Stephan Heiss
But the checker manual.pdf 1.2 page 9 says:
The download includes an updated version of the javac compiler, called
the “Type Annotations compiler” or “JSR 308 compiler”, that will be
shipped with Java 7.
Is it still an actual statement ?
will the definitive java7 support *on the fly* the checker framework?
Regards,
Stephan
( autor of tIDE, http://steph.verwalten.ch/ , supporting the checker framwork )
2010/8/26 Paulo Henrique Ferreira Costa <pauloh...@gmail.com>:
Michael Ernst
Stephan asked:
> The checker manual.pdf 1.2 page 9 says:
> The download includes an updated version of the javac compiler, called
> the "Type Annotations compiler" or "JSR 308 compiler", that will be
> shipped with Java 7.
> Is it still an actual statement ?
Oracle's announced plan is to incorporate all of the changes in the Type
Annotations compiler into the OpenJDK compiler, with the exception of the
annotations-in-comments feature. The Oracle process for incorporating
changes into OpenJDK is a lengthy one, so sometimes it takes a while before
improvements to the Type Annotations compiler appear in OpenJDK.
So far, Oracle has incorporated some of our patches into the OpenJDK. But,
other patches we sent them have been languishing for some time (with no
explanation of why).
Periodically, all public changes to the OpenJDK compiler are merged into
the Type Annotations compiler. This can be done relatively easily, and
without corporate approval required.
As a result, at any moment each compiler may have features the other one
lacks. In general, you are better off using the Type Annotations compiler,
particularly if you are interested in writing and checking type annotations.
For a more detailed description of the differences between the two
compilers, see the Type Annotations compiler README file:
http://types.cs.washington.edu/checker-framework/current/README-jsr308.html#annotations-in-comment
The rest of the quoted text is from Angelika.
> I was trying to use the checkers in conjunction with the latest OpenJDK
> 7 release (b105),
As a minor point, the current release at the time you wrote your mail was
b106. (Now, it is b107; a build is released weekly.)
> that is, I do not want to use the Java compiler that
> comes with the checker framework, but want to use the regular JDK 7
> compiler.
You didn't say in your email why you want to do this. If we understood
why, then we could give a more informative answer.
You are best off following the instructions at
http://types.cs.washington.edu/checker-framework/current/checkers-manual.html
which will let you use the Checker Framework, regardless of what JDK you
are using.
Also, you didn't say whether you are using the entire JDK 7 (I assume so),
or just the JDK 7 compiler. Recall that the JDK consists of components
including:
* compiler
* class libraries
* VM
If you want to use all of JDK 7, you will need to have a relatively high
pain threshold. I've been using it for a couple years, but it requires
extra effort on my part. For example, just this week I had to deal with
recent bugs, such as that the build-in javac creates apparently-illegal
.class files, and that at run time, the system-created OutOfMemoryError
objects are improperly initialized. If you exercise Java less extensively
than, or differently than, I do, then your experience might be different.
> How does it work? I am looking for instructions on how to specify
> -classpath and -processorpath, but could not find any instructions.
> Is there a description someplace?
-classpath and -processorpath are standard javac arguments; you can find
their documentation in the documentation of your compiler.
I hope this helps. Ask again if something is not clear.
-Mike
c...@frontiernet.net
I'm very pleased about the annotations/checker framework making it into Java7 -
and about Eclipse plugin.
But,
- On receiving a generic email I immediately tried the plugin, and just as
immediately had several usability problems that I reported (it seemed more alpha than beta quality).
So I was surprised to see the actual release so quickly - but I'll give it a try and hope the issues were
more surface and perhaps Windows-centric.
- More importantly, I am disappointed to see this about the annotations-in-comments:
> Oracle's announced plan is to incorporate all of the changes in the
> Type
> Annotations compiler into the OpenJDK compiler, with the exception of
> the
> annotations-in-comments feature.
Annotations in comments have been the only way I have found them to be usable so far.
Otherwise there is conflict with other annotations with the same names in other packages;
also, there did not seem to be available a lightweight .jar that simply defined the annotations without any extra stuff.
I hope the usability issues receive some careful attention as releases roll out.
Cheers (and continuing congratulations on this)
- David
Michael Ernst
[Your mail brought up multiple distinct points, so I will address them in
separate responses.]
> I'm very pleased about the annotations/checker framework making it into Java7 -
> and about Eclipse plugin.
Thanks!
I should clarify that only the type annotations syntax is planned as part
of Java 7.
The Checker Framework is a useful tool that happens to use type
annotations, but it is not part of the Java specification nor an official
part of Java. (There is the opportunity for others to build a different
framework and no need to standardize this one.)
People at Oracle have said they would like to include the Checker Framework
as a third-party tool that you get when you download the JDK (the new
modularity mechanisms of Java should make this easier), but there is not
yet a concrete plan regarding that.
-Mike
Michael Ernst
> - On receiving a generic email I immediately tried the plugin, and just as
> immediately had several usability problems that I reported (it seemed more alpha than beta quality).
> So I was surprised to see the actual release so quickly - but I'll give it a try and hope the issues were
> more surface and perhaps Windows-centric.
I'm very sorry to hear this, and I apologize for your experience. Please
let us know of any problems, and we (primarily Asumu, the author) will do
our best to fix them. Asumu starts grad school on September 1, but he
cares about the quality of his code and plans to continue fixing new issues
as they arise, to the greatest extent possible.
I see that both of the 2 outstanding issues at
http://code.google.com/a/eclipselabs.org/p/checker-plugin/issues/list
were reported by you. (Thanks a lot for reporting these! We appreciate
it.)
Issue #5 is awaiting a response from you after Asumu made a change. For
issue #6, the plugin needs to not import every annotation, but only the
ones relevant to the checker that is being used. This is on Asumu's to-do
list, but only affects people using the two checkers (Javari and OIGJ) that
happen to define an annotation of the same name.
Again, I'm sorry you had problems, and thanks again for reporting the bugs,
which helps us to make the tools better.
-Mike
Michael Ernst
> - More importantly, I am disappointed to see this about the annotations-in-comments:
>
> > Oracle's announced plan is to incorporate all of the changes in the
> > Type Annotations compiler into the OpenJDK compiler, with the exception
> > of the annotations-in-comments feature.
This is mentioned in appendix E ("Logistical matters") of the specification:
http://types.cs.washington.edu/jsr308/specification/java-annotation-design.html#logistics
and also in section 16.3 ("Writing annotations in comments for backward
compatibility") of the Checker Framework manual:
http://types.cs.washington.edu/checker-framework/#annotations-in-comments
> Annotations in comments have been the only way I have found them to be usable so far.
> Otherwise there is conflict with other annotations with the same names in other packages;
This is an issue with implicit imports (a bug in the Eclipse plugin that is
manifested with the Javari and OIGJ checkers). The solution had to do
with using fully-qualified names until a fix is available. I don't believe
it is related to annotations in comments, based on my current
understanding.
You are right, however, that if you are not using the Eclipse project's
experimental support for type annotations, then the Eclipse compiler will
complain about annotations outside of comments, which is extremely
irritating and will quickly drive you from Eclipse to some other IDE (until
the Eclipse type annotation support is finished and is public).
> also, there did not seem to be available a lightweight .jar that simply defined the annotations without any extra stuff.
This isn't related to annotations in comments, but file
checkers/checkers-quals.jar is intended to serve this purpose. Does it not
work for you? Or, did you not know about it? It is mentioned in sections
2.1.1 ("Distributing your annotated project") and 16.3.2 ("Implicit import
statements") of the manual, but let me know where else it could be
mentioned.
Thanks,
-Mike
c...@frontiernet.net
----- "Michael Ernst" <mer...@cs.washington.edu> wrote:
>
> This isn't related to annotations in comments, but file
> checkers/checkers-quals.jar is intended to serve this purpose. Does
> it not
> work for you? Or, did you not know about it? It is mentioned in
> sections
> 2.1.1 ("Distributing your annotated project") and 16.3.2 ("Implicit
> import
> statements") of the manual, but let me know where else it could be
> mentioned.
>
I was following the instructions for install and use of the plug-in, which
did not mention that jar file.
Ideally, an Eclipse (or simple Java) project need only include the checkers-quals.jar
on its project classpath, and that .jar is available directly as part of the plug-in
installation, without needing a separate download.
Everything that is needed for running the checkers tool is just part of the
plug-in.
> Thanks,
>
> -Mike
Angelika
Thanks for the clarifications.
You asked why I would want use the regular JDK 7 compiler for type
checking purposes. Well, I thought, that's the way it is supposed to
work ...
Since Sun/Oracle's JDK 7 is supposedly feature-complete and its
release is due in a week (at least according to the published
milestone plan http://openjdk.java.net/projects/jdk7/milestones/) I
was trying to use it as my clients and readers would do: just download
the JDK 7 plus an additional annotation processor for type checking
(if the compiler plugin does not already come as part of the JDK).
And that's it.
My (perhaps incorrect) understanding of the language changes regarding
annotations and the type checker project was that the language changes
will become part of Java 7 (which means that every Java 7 compliant
compiler will support them) and that the type checker would be a
compiler plugin for the Sun/Oracle compiler that processes a
predefined set of annotations such as @NonNull. The corresponding
annotation processor would either come as part of the Sun/Oracle JDK
or can be downloaded separately. My expectation was that the type
checker would just be a regular annotation processor; that's why I
tried to use the standard javac argument -processorpath. It comes as
a surprise to me that a special purpose compiler is needed for
processing the type checker annotations.
Now I am wondering: what will we be seeing in Java 7? A standard
javac compiler that understands type annotations (as specified in
http://types.cs.washington.edu/jsr308/specification/java-annotation-design.html,
i.e. without annotations in comments)? And what about the type
checker itself? How will we ultimately be using it? Is the special
purpose compiler for type checking an interim solution until the final
release of Java 7 or is it the way it is supposed to be?
Angelika
Michael Ernst
> Since Sun/Oracle's JDK 7 is supposedly feature-complete and its
> release is due in a week (at least according to the published
> milestone plan http://openjdk.java.net/projects/jdk7/milestones/)
You'll notice at the same webpage that JSR 308 already appeared in M4. So,
it's not inconsistent for Oracle to say that javac is both
feature-complete, even though some patches remain to be incorporated.
Oracle's publicly-announced plan is to incorporate all the remaining
patches (except annotations in comments), so that things will work in the
way that you had expected. I agree that the fact that they haven't yet
followed through on their promises is an irritation and inconvenience to
everyone.
-Mike
Michael Ernst
> > This isn't related to annotations in comments, but file
> > checkers/checkers-quals.jar is intended to serve this purpose. Does it
> > not work for you? Or, did you not know about it? It is mentioned in
> > sections 2.1.1 ("Distributing your annotated project") and 16.3.2
> > ("Implicit import statements") of the manual, but let me know where
> > else it could be mentioned.
>
> I was following the instructions for install and use of the plug-in, which
> did not mention that jar file.
That's true. The Eclipse plugin is a wrapper around a powerful
type-checking framework. The plugin manual tells you how to use the
plugin, but does not give all details about the underling functionality.
This is similar to the way the Eclipse manual doesn't contain a full
reference manual for the Java language (and every other language that
Eclipse supports).
I'm sorry this wasn't clear. I'll reword the plugin manual, to avoid such
confusion in the future.
> Ideally, an Eclipse (or simple Java) project need only include the
> checkers-quals.jar on its project classpath, and that .jar is available
> directly as part of the plug-in installation, without needing a separate
> download.
A reason for the separate download is to prevent the need for synchronized
releases between the two projects. If a new version of the Checker
Framework is released, you can use it without waiting for a new release of
the Eclipse plugin. And, if you reuse the checkers.jar from your regular
installation of the Checker Framework, then there is no danger of your
regular and Eclipse installations getting out of sync.
> Everything that is needed for running the checkers tool is just part of the
> plug-in.
This is already the case. As explained on the plugin webpage, adding
checkers.jar to your project's classpath is optional.
Also, this is rather different than your original request. If you *only*
want to define the annotations, then you cannot run the checkers. You had
asked, in previous email:
> also, there did not seem to be available a lightweight .jar that simply
> defined the annotations without any extra stuff.
and that is what checkers-quals.jar does.
If you want to *run* the checkers, then I don't believe that the available
.jar files do not contain any "extra stuff". Maybe you can clarify what
the "extra stuff" is, and that will help in answering your real question.
-Mike
c...@frontiernet.net
----- "Michael Ernst" <mer...@cs.washington.edu> wrote:
> David-
> ....
>
>
> > Ideally, an Eclipse (or simple Java) project need only include the
> > checkers-quals.jar on its project classpath, and that .jar is
> available
> > directly as part of the plug-in installation, without needing a
> separate
> > download.
>
> A reason for the separate download is to prevent the need for
> synchronized
> releases between the two projects. If a new version of the Checker
> Framework is released, you can use it without waiting for a new
> release of
> the Eclipse plugin. And, if you reuse the checkers.jar from your
> regular
> installation of the Checker Framework, then there is no danger of
> your
> regular and Eclipse installations getting out of sync.
>
Aah. This is a reasonable rationale. I presume each plugin release will
include the latest checkers framework release, even if additional framework
releases come out between plugin releases. You could also package the checkers.jar
and javac.jar in a separate plug-in feature that could be updated separately,
thereby avoiding the manual download of the jars and setup of the classpath.
> > Everything that is needed for running the checkers tool is just part
> of the
> > plug-in.
>
> This is already the case. As explained on the plugin webpage, adding
> checkers.jar to your project's classpath is optional.
>
I think it was not when I first tried the plugin, but I'm told it is now.
I'll confirm that when I have a chance to revisit my trials.
> Also, this is rather different than your original request. If you
> *only*
> want to define the annotations, then you cannot run the checkers.
Correct. If I'm not running the checkers, but have annotated code, I
want to include the minimum possible additional classes in the code.
For example, if I'm shipping a product in which I have added type annotations,
I will check that before I ship (using the full checkers jars),
but my shipped version should only need
to include checkers-quals.jar to compile and run.
You
> had
> asked, in previous email:
>
> > also, there did not seem to be available a lightweight .jar that
> simply
> > defined the annotations without any extra stuff.
>
> and that is what checkers-quals.jar does.
Right. The plug-in instructions page did not mention this originally.
>
> If you want to *run* the checkers, then I don't believe that the
> available
> .jar files do not contain any "extra stuff". Maybe you can clarify
> what
> the "extra stuff" is, and that will help in answering your real
> question.
You are correct there. It is only extra when you are not running the checkers.
But I'd like clarification on this point:
I would expect architecturally that the checkers-quals.jar should be included in the Eclipse project classpath
and the checkers.jar and javac.jar should be included in the path that runs Eclipse or in a separate classpath that
runs the checkers, but not in the project classpath. Is the tool using the same classpath (the project classpath) both to compile and run the subject program and as the classpath to run the checkers tool itself?
- David
> -Mike
Michael Ernst
Thanks for the suggestions about packaging, which I will defer to those
who know more about those details.
I've attached below the current section 2.1.1 "Distributing your annotated
project" of the Checker Framework manual, which I hope is an improvement
over the previous text.
-Mike
Asumu Takikawa
> You could also package the checkers.jar
> and javac.jar in a separate plug-in feature that could be updated separately,
> thereby avoiding the manual download of the jars and setup of the classpath.
We have considered this and plan to set the feature up this way eventually
in a future release.
> But I'd like clarification on this point:
>
> I would expect architecturally that the checkers-quals.jar should be included in the Eclipse project classpath
> and the checkers.jar and javac.jar should be included in the path that runs Eclipse or in a separate classpath that
> runs the checkers, but not in the project classpath. Is the tool using the same classpath (the project classpath) both to compile and run the subject program and as the classpath to run the checkers tool itself?
The checker plugin does not use the classpath of the target project (in a
user's workspace) to run itself. However, it does utilize the target
project's classpath to run the types compiler, which is necessary if, for
example, your project uses a different Java SDK than the plugin.
If I understood your question correctly, and correct me if I'm wrong,
the answer is no. If by "checkers tool" you meant the types compiler, then
yes, it does use the subject program's classpath.
The types compiler will usually take a copy of checkers.jar from the
plugin's classpath, however, unless the user supplies one.
Cheers,
Asumu