\htmlhr
\chapterAndLabel{Troubleshooting, getting help, and contributing}{troubleshooting}

\begin{sloppypar}
The manual might already answer your question, so first please look for
your answer in the manual,
including this chapter and the FAQ (Chapter~\ref{faq}).
If not, you can use the mailing list,
\code{checker-framework-discuss@googlegroups.com}, to ask other users for
help.  For archives and to subscribe, see \url{https://groups.google.com/forum/#!forum/checker-framework-discuss}.
To report bugs, please see Section~\ref{reporting-bugs}.
If you want to help out, you can give feedback (including on the
documentation), choose a bug and fix it, or select a
project from the ideas list at
% \url{https://github.com/typetools/checker-framework/wiki/Ideas}.
\url{https://rawgit.com/typetools/checker-framework/master/docs/developer/gsoc-ideas.html}.
\end{sloppypar}


\sectionAndLabel{Common problems and solutions}{common-problems}

\begin{itemize}
\item
To verify that you are using the compiler you think you are, you can add
\code{-version} to the command line.  For instance, instead of running
\code{javac -g MyFile.java}, you can run \code{javac \underline{-version} -g
  MyFile.java}.  Then, javac will print out its version number in addition
to doing its normal processing.

\end{itemize}


\subsectionAndLabel{Unable to compile the Checker Framework}{common-problems-compiling}

If you get the following error while compiling the Checker Framework itself:

%BEGIN LATEX
\begin{smaller}
%END LATEX
\begin{Verbatim}
checker-framework/stubparser/dist/stubparser.jar(org/checkerframework/stubparser/ast/CompilationUnit.class):
warning: [classfile] Signature attribute introduced in version 49.0 class files is ignored in version 46.0 class files
\end{Verbatim}
%BEGIN LATEX
\end{smaller}
%END LATEX

\noindent
and you have used Eclipse to compile the Checker Framework, then probably
you are using a very old version of Eclipse.  (If you
install Eclipse from the Ubuntu 16.04 repository, you get Eclipse version
3.8.  Ubuntu 16.04 was released in April 2016, and Eclipse 3.8 was released
in June 2012, with subsequent major releases in June 2013, June 2014, and
June 2015.)
Install the latest version of Eclipse and use it instead.


\subsectionAndLabel{Unable to run the checker, or checker crashes}{common-problems-running}

If you are unable to run the checker, or if the checker or the compiler
terminates with an error, then the problem may be a problem with your environment.
(If the checker or the compiler crashes, that is a bug in the Checker
Framework; please report it.  See Section~\ref{reporting-bugs}.)
This section describes some possible problems and solutions.

\begin{itemize}
\item
  \label{no-such-field-error-release}
  An error that includes \<java.lang.NoSuchFieldError: RELEASE"> means that
  you are not using the correct compiler (you are not using a Java 9+ compiler).

\item
If you get the error

%BEGIN LATEX
\begin{smaller}
%END LATEX
\begin{Verbatim}
com.sun.tools.javac.code.Symbol$CompletionFailure: class file for com.sun.source.tree.Tree not found
\end{Verbatim}
%BEGIN LATEX
\end{smaller}
%END LATEX

\noindent
then you are using the source installation and file \code{tools.jar} is not
on your classpath.  See the installation instructions
(Section~\ref{installation}).

\item
If you get an error like one of the following,

%BEGIN LATEX
\begin{smaller}
%END LATEX
\begin{Verbatim}
...\build.xml:59: Error running ${env.CHECKERFRAMEWORK}\checker\bin\javac.bat compiler
\end{Verbatim}

\begin{Verbatim}
.../bin/javac: Command not found
\end{Verbatim}
%BEGIN LATEX
\end{smaller}
%END LATEX

\noindent
then the problem may be that you have not set the \code{CHECKERFRAMEWORK} environment
variable, as described in Section~\ref{javac-wrapper}.  Or, maybe
you made it a user variable instead of a system variable.

\item
If you get one of these errors:

\begin{alltt}
The hierarchy of the type \emph{ClassName} is inconsistent

The type com.sun.source.util.AbstractTypeProcessor cannot be resolved.
  It is indirectly referenced from required .class files
\end{alltt}

\begin{sloppypar}
\noindent
then you are likely \textbf{not} using the Checker Framework compiler.  Use
either \code{\$CHECKERFRAMEWORK/checker/bin/javac} or one of the alternatives
described in Section~\ref{javac-wrapper}.
\end{sloppypar}


\item
If you get the error

\begin{Verbatim}
  java.lang.ArrayStoreException: sun.reflect.annotation.TypeNotPresentExceptionProxy
\end{Verbatim}

\noindent
If you get an error such as

\begin{Verbatim}
  java.lang.NoClassDefFoundError: java/util/Objects
\end{Verbatim}

\noindent
then you are trying to run the compiler using a JDK 6 or earlier JVM\@.
Install and use a Java 8
% or later
JDK, at least for running the Checker
Framework.

\noindent
% I'm not 100% sure of the following explanation and solution.
then an annotation is not present at run time that was present at compile
time.  For example, maybe when you compiled the code, the \<@Nullable>
annotation was available, but it was not available at run time.
You can use JDK 8 at run time.

\item
\label{troubleshooting-class-file-not-found}
A ``class file for \ldots\ not found'' error, especially for an inner class
in the JDK, is probably due to a JDK version mismatch.  To solve the
problem, you need to perform compilation with a different Java version or
different version of the JDK\@.

In general, Java issues a ``class file for \ldots\ not found'' error when
your classpath contains code that was compiled
with some library, but your classpath does not contain that library itself.

For example, suppose that when you run the compiler, you are using JDK 8,
but some library on your classpath was compiled against JDK 6 or 7, and the
compiled library refers to a class that only appears in JDK 6 or 7.  (If only
one version of Java existed, or the Checker Framework didn't try to support
multiple different versions of Java, this would not be a problem.)

Examples of classes that were removed from the JDK include:

\begin{Verbatim}
  class file for java.io.File$LazyInitialization not found  -- removed in JDK 7
  class file for java.util.Hashtable$EmptyIterator not found  -- removed in JDK 7
  java.lang.NoClassDefFoundError: java/util/Hashtable$EmptyEnumerator  -- removed in JDK 7
  class file for java.util.TimeZone$DisplayNames not found  -- removed in JDK 8
\end{Verbatim}

Examples of classes that were added to the JDK include:

\begin{Verbatim}
  class file for java.util.Vector$Itr not found  -- introduced in JDK 7
  class file for java.lang.Class$ReflectionData not found  -- introduced in JDK 7 release 45
  The type java.lang.Class$ReflectionData cannot be resolved  -- introduced in JDK 8
  class file for java.util.regex.Pattern$HorizWS not found  -- introduced in JDK 9
\end{Verbatim}

You may be able to solve the problem by running

\begin{Verbatim}
  ./gradlew buildJdk assemble
\end{Verbatim}

\noindent
to re-generate files \code{checker/jdk/jdk\{8,9\}.jar} and \code{checker/bin/jdk\{8,9\}.jar}.

That usually works, but if not, then you should recompile the Checker
Framework from source (Section~\ref{build-source}) rather than using
the pre-compiled distribution.


\item
\label{no-such-field-error}
A \<NoSuchFieldError> such as this:

\begin{Verbatim}
java.lang.NoSuchFieldError: NATIVE_HEADER_OUTPUT
\end{Verbatim}

\noindent
Field \<NATIVE\_HEADER\_OUTPUT> was added in JDK 8.
The error message suggests that
you're not executing with the right bootclasspath: some classes were
compiled with the JDK 8 version and expect the field, but you're
executing the compiler on a JDK without the field.

One possibility is that you are not running the Checker Framework compiler
--- use \<javac -version> to check this, then use the right one.  (Maybe
the Checker Framework javac is at the end rather than the beginning of your
path.)

If you are using Ant, then one possibility
is that the javac compiler is using the same JDK as Ant is using.  You can
correct this by being sure to use \<fork="yes"> (see
Section~\ref{ant-task}) and/or setting the \<build.compiler> property to
\<extJavac>.

If you are building from source (Section~\ref{build-source}),
you might need to rebuild the Annotation
File Utilities before recompiling or using the Checker Framework.


\item
If you get an error that contains lines like these:

\begin{Verbatim}
Caused by: java.util.zip.ZipException: error in opening zip file
    at java.util.zip.ZipFile.open(Native Method)
    at java.util.zip.ZipFile.<init>(ZipFile.java:131)
\end{Verbatim}

\noindent
then one possibility is that you have installed the Checker Framework in a
directory that contains special characters that Java's ZipFile
implementation cannot handle.  For instance, if the directory name contains
``\<+>'', then Java 1.6 throws a ZipException, and Java 1.7 throws a
FileNotFoundException and prints out the directory name with ``\<+>''
replaced by blanks.

\item
The Checker Framework sometimes runs out of memory when processing very
large Java files, or files with very large methods.

If you get an error such as
\begin{Verbatim}
error: SourceChecker.typeProcess: unexpected Throwable (OutOfMemoryError) while processing ...; message: GC overhead limit exceeded
\end{Verbatim}

\noindent
then either give the JVM more memory when running the Checker Framework, or
split your files and methods into smaller ones, or both.

\item
\ahref{https://errorprone.info/}{Error Prone} uses the Checker Framework's
dataflow analysis library.
Unfortunately, Error Prone uses an old version of the library, so you
cannot use both Error Prone and the current Checker Framework (because each
one depends on a different version of the dataflow library).

Until the Error Prone tool is \ahref{https://github.com/google/error-prone/issues/1404}{fixed},
you can use an older version of the Checker Framework (the one that Error
Prone is built on), or you can use a switch that causes your build to use either
Error Prone or the Checker Framework, but not both.
The
\ahreforurl{https://github.com/kelloggm/checkerframework-gradle-plugin\#incompatibility-with-error-prone}{Gradle
  plugin documentation} shows how to do the latter for Gradle.

\end{itemize}


\subsectionAndLabel{Unexpected warnings not related to type-checking}{common-problems-non-typechecking}

This section gives solutions for some warning messages that are not related
to type errors in your code.

\begin{itemize}

\item
If you get an error like the following

\begin{Verbatim}
error: scoping construct for static nested type cannot be annotated
error: scoping construct cannot be annotated with type-use annotation
\end{Verbatim}

\noindent
  then you have probably written something like one of the following:
\begin{description}
\item[\<@Nullable java.util.List>]
The correct Java syntax to write an annotation on a fully-qualified type
name is to put the annotation on the simple name part, as in
\<java.util.@Nullable List>.  But, it's usually
better to add \<import java.util.List> to your source file, so that you can
just write \<@Nullable List>.
\item[\<@Nullable Map.Entry>]  You must write \<Outer.@Nullable
StaticNestedClass> rather than \<@Nullable Outer.StaticNestedClass>.
Since a static nested class does not depend on its outer class, the
annotation on the outer class would have no effect and is forbidden.
\end{description}

Java 8 requires that a type qualifier be written directly on the type that
it qualifies, rather than on a scoping mechanism that assists in resolving
the name.  Examples of scoping mechanisms are package names and outer
classes of static nested classes.

The reason for the Java 8 syntax is to avoid syntactic irregularity.  When
writing a member nested class (also known as an inner class), it is
possible to write annotations on both the outer and the inner class:  \<@A1
Outer. @A2 Inner>.  Therefore, when writing a static nested class, the
annotations should go on the same place:  \<Outer. @A3 StaticNested> (rather
than \<@ConfusingAnnotation Outer.\ Nested> where
\<@ConfusingAnnotation> applies to \<Outer> if \<Nested> is a member class
and applies to \<Nested> if \<Nested> is a static class).  It's not legal
to write an annotation on the outer class of a static nested class, because
neither annotations nor instantiations of the outer class affect the static
nested class.

Similar arguments apply when annotating \<package.Outer.Nested>.

\item
An ``error: package ... does not exist'' or ``error: cannot find symbol''
about classes in your own project or its dependencies means that you have
left your own project or its dependencies off the classpath when you
invoked the compiler.

\end{itemize}


\subsectionAndLabel{Unexpected type-checking results}{common-problems-typechecking}

This section describes possible problems that can lead the type-checker to
give unexpected results.


\begin{itemize}
\item
  If the Checker Framework is unable to verify a property that you know is
  true, then you should formulate a proof about why the property is true.
  Your proof depends on some set of facts about the program and its
  operation.  State them completely; for example, don't write ``the field
  \<f> cannot be null when execution reaches line 22'', but justify
  \emph{why} the field cannot be null.

  Once you have written down your proof, translate each fact into a Java
  annotation.

  If you are unable to express some aspect of your proof as an annotation,
  then the type system is not capable of reproducing your proof.  You might
  need to find a different proof, or extend the type system to be more
  expressive, or suppress the warning.

  If you are able to express your entire proof as annotations, then look at
  the Checker Framework error messages.  One possibility is that the errors
  indicate that your proof was incomplete or incorrect.  Maybe your proof
  implicitly depended on some fact you didn't write down, such as ``method
  \<m> has no side effects.''  In this case, you should revise your proof
  and add more annotations to your Java code.  Another possibility is that
  your proof is incorrect, and the errors indicate where.  Another
  possibility is that there is a bug in the type-checker.  In this case,
  you should report it to the maintainers, giving your proof and explaining
  why the type-checker should be able to make the same inferences that you did.

  Recall that the Checker Framework does modular verification,
  one procedure at a time; it observes the specifications, but not the
  implementations, of other methods.

  Also see Section~\ref{handling-warnings}, which explains this same
  methodology in different words.

\item
If a checker seems to be ignoring the annotation on a method, then it is
possible that the checker is reading the method's signature from its
\code{.class} file, but the \code{.class} file was not created by a Java 8
or later compiler.
You can check whether the annotations actually appear in the
\code{.class} file by using the \code{javap} tool.

If the annotations do not appear in the \code{.class} file, here are two
ways to solve the problem:
\begin{itemize}
\item
  Re-compile the method's class with the Checker Framework compiler.  This will
  ensure that the type annotations are written to the class file, even if
  no type-checking happens during that execution.
\item
  Pass the method's file explicitly on the command line when type-checking,
  so that the compiler reads its source code instead of its \code{.class}
  file.
\end{itemize}

\item
If a checker issues a warning about a property that it accepted (or that
was checked) on a previous line, then probably there was a side-effecting
method call in between that could invalidate the property.  For example, in
this code:

\begin{Verbatim}
if (currentOutgoing != null && !message.isCompleted()) {
    currentOutgoing.continueBuffering(message);
}
\end{Verbatim}

\noindent
the Nullness Checker will issue a warning on the second line:
\begin{Verbatim}
warning: [dereference.of.nullable] dereference of possibly-null reference currentOutgoing
    currentOutgoing.continueBuffering(message);
    ^
\end{Verbatim}

If \<currentOutgoing> is a field rather than a local variable, and
\<isCompleted()> is not a pure method, then a null pointer
dereference can occur at the given location, because \<isCompleted()> might set
the field \<currentOutgoing> to \<null>.

If you want to communicate that
isCompleted() does not set the field \<currentOutgoing> to \<null>, you can use
\<\refqualclass{dataflow/qual}{Pure}>,
\<\refqualclass{dataflow/qual}{SideEffectFree}>,
or \<\refqualclass{checker/nullness/qual}{EnsuresNonNull}> on the
declaration of \<isCompleted()>; see Sections~\ref{type-refinement-purity}
and~\ref{nullness-method-annotations}.


\item
If a checker issues a type-checking error for a call that the library's
documentation states is correct, then maybe that library method has not yet
been annotated, so default annotations are being used.

To solve the problem, add the missing annotations to the library (see
Chapter~\ref{annotating-libraries}).  Depending on the checker, the
annotations might be expressed in the form of stub files (which appear
together with the checker's source code, such as in file
\code{checker/src/org/checkerframework/checker/interning/jdk8.astub} for the
Interning Checker) or in the form of annotated libraries (which appear
under \code{checker/jdk/}, such as at \code{checker/jdk/nullness/src/} for
the Nullness Checker.

\item
If the compiler reports that it cannot find a method from the JDK or
another external library, then maybe the stub file for that class
is incomplete.

To solve the problem, add the missing annotations to the library, as
described in the previous item.

The error might take one of these forms:

\begin{Verbatim}
method sleep in class Thread cannot be applied to given types
cannot find symbol: constructor StringBuffer(StringBuffer)
\end{Verbatim}

\item
If you get an error related to a bounded type parameter and a literal such
as \<null>, the problem may be missing defaulting.  Here is an example:

\begin{Verbatim}
mypackage/MyClass.java:2044: warning: incompatible types in assignment.
      T retval = null;
                 ^
  found   : null
  required: T extends @MyQualifier Object
\end{Verbatim}

\noindent
A value that can be assigned to a variable of type \<T extends @MyQualifier
Object> only if that value is of the bottom type, since the bottom type is
the only one that is a subtype of every subtype of \<T extends @MyQualifier
Object>.  The value \<null> satisfies this for the Java type system, and it
must be made to satisfy it for the pluggable type system as well.  The
typical way to address this is to call \<addStandardLiteralQualifiers> on the \<LiteralTreeAnnotator>.

\item
An error such as

\begin{Verbatim}
MyFile.java:123: error: incompatible types in argument.
                        myModel.addElement("Scanning directories...");
                                           ^
  found   : String
  required: ? extends Object
\end{Verbatim}

\noindent
may stem from use of raw types.  (``\<String>'' might be a different type
and might have type annotations.)  If your declaration was

\begin{Verbatim}
  DefaultListModel myModel;
\end{Verbatim}

\noindent
then it should be
\begin{Verbatim}
  DefaultListModel<String> myModel;
\end{Verbatim}

Running the regular Java compiler with the \<-Xlint:unchecked> command-line
option will help you to find and fix problems such as raw types.


\item
The error

\begin{Verbatim}
error: annotation type not applicable to this kind of declaration
    ... List<@NonNull String> ...
\end{Verbatim}

\noindent
indicates that you are using a definition of \<@NonNull> that is a
declaration annotation, which cannot be used in that syntactic location.
For example, many legacy annotations such as those listed in
Figure~\ref{fig-nullness-refactoring} are declaration annotations.  You can
fix the problem by instead using a definition of \<@NonNull> that is a type
annotation, such as the Checker Framework's annotations; often this only
requires changing an \<import> statement.


\item
If Eclipse gives the warning

\begin{Verbatim}
The annotation @NonNull is disallowed for this location
\end{Verbatim}

\noindent
then you have the wrong version of the \<org.eclipse.jdt.annotation>
classes.  Eclipse includes two incompatible versions of these annotations.
You want the one with a name like
\<org.eclipse.jdt.annotation\_2.0.0.....jar>, which you can find in the
\<plugins> subdirectory under the Eclipse installation directory.
Add this .jar file to your build path.


\item
When one formal parameter's annotation references another formal
parameter's name, as in this constructor:

\begin{smaller}
\begin{Verbatim}
public String(char value[], @IndexFor("value") int offset, @IndexOrHigh("value") int count) { ... }
\end{Verbatim}
\end{smaller}

\noindent
you will get an error such as

\begin{smaller}
\begin{Verbatim}[]
[expression.unparsable.type.invalid] Expression in dependent type annotation invalid:
Use "#1" rather than "value"
\end{Verbatim}
\end{smaller}

Section~\ref{java-expressions-as-arguments} explains that you need to use
a different syntax to refer to a formal parameter:

\begin{smaller}
\begin{Verbatim}
public String(char value[], @IndexFor("#1") int offset, @IndexOrHigh("#1") int count) { ... }
\end{Verbatim}
\end{smaller}


\end{itemize}


\subsectionAndLabel{Unexpected compilation output when running javac without a pluggable type-checker}{common-problems-running-javac}

On rare occasions, javac may issue an error when compiling against the
Checker Framework's annotated JDK that you do not get when using the
regular JDK\@.  (Recall that the Checker Framework compiler uses the
annotated JDK\@.)  This may occur even when you are \emph{not} running any
annotation processor.  The error is:

\begin{Verbatim}
  unchecked method invocation: method myMethod in class C is applied to given types
\end{Verbatim}

The reason for this is that there are some wildcards in the annotated JDK
that have been given an explicit upper bound --- they have been changed
from, for example, \code{List<?>} to \code{List<? extends Object>}.  The
JDK treats these two types as identical in almost all respects.  However,
they have a different representation in bytecode.  More importantly,
\code{List<?>} is reifiable but \code{List<? extends Object>} is not; this
means that the compiler permits uses of the former in some locations where
it issues a warning for the latter.  You can suppress the warning.

A message of the form

\begin{Verbatim}
  error: annotation values must be of the form 'name=value'
        @LTLengthOf("firstName", "lastName") int index;
                    ^
\end{Verbatim}

\noindent
is caused by incorrect Java syntax.  When you supply a set of multiple
values as an annotation argument, you need to put curly braces around them:

\begin{Verbatim}
        @LTLengthOf({"firstName", "lastName"}) int index;
\end{Verbatim}

A message of the form

\begin{Verbatim}
  Error: cannot find symbol
\end{Verbatim}

\noindent
for an annotation type that is imported, and is a applied to a
statically-imported enum, is caused by a javac bug, unrelated to the
Checker Framework.  See
\url{https://bugs.openjdk.java.net/browse/JDK-7101822} and \url{https://bugs.openjdk.java.net/browse/JDK-8169095}.
% Also see https://github.com/typetools/checker-framework/issues/1304


\sectionAndLabel{How to report problems (bug reporting)}{reporting-bugs}

If you have a problem with any checker, or with the Checker Framework,
please file a bug at
\url{https://github.com/typetools/checker-framework/issues}.
(First, check whether there is an existing bug report for that issue.)
If the problem is with an incorrect or missing annotation on a library,
including the JDK, see Section~\ref{reporting-bugs-annotated-libraries}.

Alternately (especially if your communication is not a bug report), you can
send mail to checker-framework-dev@googlegroups.com.
We welcome suggestions, annotated libraries, bug fixes, new
features, new checker plugins, and other improvements.

Please ensure that your bug report is clear and that it is complete.
Otherwise, we may be unable to understand it or to reproduce it, either of
which would prevent us from helping you.  Your bug report will be most
helpful if you:

% If you update this, also update ../../.github/ISSUE_TEMPLATE
\begin{itemize}
\item
  Add \code{-version -verbose -AprintAllQualifiers}
  to the javac options.  This causes the compiler to output
  debugging information, including its version number.
\item
  Indicate exactly what you did.  Don't skip any steps, and don't merely
  describe your actions in words.  Show the exact commands by attaching a
  file or using cut-and-paste from your command shell.  Always include
  plaintext, not just a screenshot.  Try to reproduce the problem from the
  command line as well as from an IDE or within a build system; that helps
  to indicate whether the problem is with the IDE or build system.
\item
  Include all files that are necessary to reproduce the problem.  This
  includes every file that is used by any of the commands you reported, and
  possibly other files as well.  Please attach the files, rather than
  pasting their contents into the body of your bug report or email message,
  because some mailers mangle formatting of pasted text.

  If you
  encountered a problem while using tool integration such as
  Maven integration, then try to reproduce the problem from the
  command line as well --- this will indicate whether the problem is with
  the checker itself or with the tool integration.  If you use an invasive
  annotation processor such as Lombok, then try to repoduce the problem
  without it --- this will indicate whether the problem is in the Checker
  Framework proper or in its interaction with Lombok.

  If you cannot share your code, create a new, small test case.  (This is
  helpful even if your code is not secret!)  The progress tracing options
  (Section~\ref{creating-debugging-options-progress}) can be helpful in
  determining which file the Checker Framework was processing when it
  crashed.
\item
  Indicate exactly what the result was by attaching a file or using
  cut-and-paste from your command shell (don't merely describe it in
  words, don't use a screenshot, and don't provide just part of the output).
\item
  If the problem is not a crash, then
  indicate what you expected the result to be, since a bug is a difference
  between desired and actual outcomes.  Also, please indicate \textbf{why}
  you expected that result --- explaining your reasoning can help you
  understand how your reasoning is different than the checker's and which
  one is wrong.  Remember that the checker reasons modularly and
  intraprocedurally:  it examines one method at a time, using only the
  method signatures of other methods.
\item
  Indicate what you have already done to try to understand the problem.
  Did you do any additional experiments?  What parts of the manual did
  read, and what else did you search for in the manual?  Without this
  information, the maintainers may give you redundant suggestions.
\end{itemize}

A particularly useful format for a test case is as a new file, or a diff to
an existing file, for the existing Checker Framework test suite.  For
instance, for the Nullness
Checker, see directory \<checker-framework/checker/tests/nullness/>.
But, please report your bug even if you do not report it in this format.

When reporting bugs, please focus on realistic scenarios and well-written
code.  We are sure that you can make up artificial code that stymies the
type-checker!  Those aren't a good use of your time to report nor the
maintainers' time to evaluate and fix.


\subsectionAndLabel{Problems with annotated libraries}{reporting-bugs-annotated-libraries}

Sometimes, a checker will report a warning because a library is not
annotated or because the library contains incorrect annotations.
Please do not open GitHub issues for these.
Instead, we appreciate pull requests to help us improve the annotations.
Alternatively or in the interim, you can use stub files as described in
Section~\ref{stub}.

If the library is annotated but has some incorrect or missing annotations,
then please open a pull request that adds the annotations.
\begin{itemize}
\item
  Non-JDK libraries:  You can find the annotated source in
  \url{https://github.com/typetools/}.
  If the library does not exist there, then it has no annotations yet.
  You can fork it, add annotations,
  and propose that your annotated version be moved into
  \url{https://github.com/typetools/}.
\item
  JDK:  You need to open two pull requests, because there are two versions of the
  annotated JDK.
  \begin{itemize}
  \item JDK 8: The annotated JDK source is in the
    \ahref{https://github.com/typetools/checker-framework}{Checker Framework
      GitHub repository}, either in a subdirectory of
    \ahref{https://github.com/typetools/checker-framework/tree/master/checker/jdk}{\<checker/jdk>}
    or in files named \<jdk.astub> in the checker's implementation directory.
  \item
    JDK 11: The annotated JDK source is in \url{https://github.com/typetools/jdk}.
  \end{itemize}
\end{itemize}

For either approach, please see \chapterpageref{annotating-libraries} for
tips about writing library annotations.

Thanks for your contribution to the annotated libraries!


\sectionAndLabel{Building from source}{build-source}

The Checker Framework release (Section~\ref{installation}) contains
everything that most users need, both to use the distributed checkers and
to write your own checkers.  This section describes how to compile its
binaries from source.  You will be using the latest development version of
the Checker Framework, rather than an official release.

% Doing
% so permits you to examine and modify the implementation of the distributed
% checkers and of the checker framework.  It may also help you to debug
% problems more effectively.

Note the JDK requirements (Section~\ref{installation}).


\subsectionAndLabel{Install prerequisites}{building-prerequisites}

You need to install several packages in order to build the Checker
Framework.
Follow the instructions for your operating system.
If your OS is not listed, adapt the instructions for an existing OS;
for example, other Linux distributions will be similar to Ubuntu.

\begin{description}
\item[Ubuntu]
  Run the following commands:

% Keep this up to date with ../../checker/bin-devel/Dockerfile-ubuntu-jdk11-plus
\begin{Verbatim}
sudo apt-get -qqy update
sudo apt-get -qqy install \
 openjdk-11-jdk \
 ant cpp git gradle jq libcurl3-gnutls \
 make maven mercurial python3-pip python3-requests unzip wget \
 dia hevea imagemagick latexmk librsvg2-bin maven rsync \
 texlive-font-utils texlive-fonts-recommended \
 texlive-latex-base texlive-latex-extra texlive-latex-recommended
pip3 install html5validator
\end{Verbatim}

  You may have to answer questions about which time zone your computer is in.

\item[Mac OS]
  If you employ \ahref{https://brew.sh}{homebrew} to install packages, run
  the following commands:

\begin{Verbatim}
brew update
brew install git ant hevea maven mercurial librsvg unzip make
brew cask install java
brew cask install mactex
\end{Verbatim}

Make a \<latex> directory and copy \<hevea.sty> file into it (you may need to update the version number \<2.31>):

\begin{Verbatim}
mkdir -p $HOME/Library/texmf/tex/latex
cp -p /usr/local/Cellar/hevea/2.31/lib/hevea/hevea.sty $HOME/Library/texmf/tex/latex/
\end{Verbatim}

Note: If copy permission is denied, try \<sudo>.

Also set the \<JAVA\_HOME> environment variable in your \<.bashrc> file;
for example,

\begin{Verbatim}
export JAVA_HOME=/Library/Java/JavaVirtualMachines/jdk1.8.0_144.jdk/Contents/Home
\end{Verbatim}


\item[Windows]
  To build on Windows 10,
  run \<bash> to obtain a version of
  Ubuntu (provided by the Windows Subsystem for Linux) and follow the Ubuntu
  instructions.

% To build on other versions of Windows,
% here is an \emph{incomplete} list of needed prerequisites:
% \begin{itemize}
% \item
%   Install MSYS to obtain the \<cp> and \<make> commands.
% \end{itemize}

\end{description}


\subsectionAndLabel{Obtain the source}{building-obtain-source}

Obtain the latest source code from the version control repository:

\begin{Verbatim}
git clone https://github.com/typetools/checker-framework.git checker-framework
export CHECKERFRAMEWORK=`pwd`/checker-framework
\end{Verbatim}
% $ to unconfuse Emacs LaTeX mode

You might want to add an \<export CHECKERFRAMEWORK=...> line to your
\<.bashrc> file.

% Why is this necessary?  What goes wrong if it is not set?  Can I avoid
% the need to set it?  It's used for:
%  * the location of tools.jar, below.
%  * the default location of CTSYM, in checker/jdk/Makefile.
Set the \<JAVA\_HOME> environment variable to the location of your JDK
8 or JDK 11 installation (not the JRE installation, and not JDK 7 or earlier).
(The \<JAVA\_HOME> environment
variable might already be set, because it is needed for Ant to work.)

\begin{description}
\item[Ubuntu]
If you use the bash shell, put the following command in your
\code{.bashrc} file.  (This might not work if \<java> refers to an executable
in the JRE rather than in the JDK, but you need the JDK installed to build
the Checker Framework anyway.)
% Can someone give a simpler command?
%BEGIN LATEX
\begin{smaller}
%END LATEX
\begin{Verbatim}
  export JAVA_HOME=${JAVA_HOME:-$(dirname $(dirname $(dirname $(readlink -f $(/usr/bin/which java)))))}
\end{Verbatim}
%BEGIN LATEX
\end{smaller}
%END LATEX

\item[Mac OS X 10.5 or later]
  Add one of the following two commands in your \code{.bash\_profile} or
  \code{.profile} file according to the version of your JDK.
\begin{Verbatim}
  export JAVA_HOME=$(/usr/libexec/java_home -v 1.8)
  export JAVA_HOME=$(/usr/libexec/java_home -v 1.9)
\end{Verbatim}

\end{description}

\subsectionAndLabel{Build the Checker Framework}{building}

% Building (compiling) the checkers and framework from source creates the
% \code{checker.jar} file.  A pre-compiled \code{checker.jar} is included
% in the distribution, so building it is optional.  It is mostly useful for
% people who are developing compiler plug-ins (type-checkers).  If you only
% want to \emph{use} the compiler and existing plug-ins, it is sufficient to
% use the pre-compiled version.

\begin{enumerate}

\item
Run \code{./gradlew cloneAndBuildDependencies} to build the Checker Framework dependencies:

\begin{Verbatim}
  cd $CHECKERFRAMEWORK
  ./gradlew cloneAndBuildDependencies
\end{Verbatim}
% $ to unconfuse Emacs LaTeX mode

\item
Run \code{./gradlew assemble} to build the Checker Framework:

\begin{Verbatim}
  cd $CHECKERFRAMEWORK
  ./gradlew assemble
\end{Verbatim}
% $ to unconfuse Emacs LaTeX mode

\item
Once it is built, you may wish to put the Checker Framework's \<javac>
even earlier in your \<PATH>:

\begin{Verbatim}
export PATH=$CHECKERFRAMEWORK/checker/bin:${PATH}
\end{Verbatim}

The Checker Framework's \code{javac} ensures that all required
libraries are on your classpath and boot classpath, but is otherwise
identical to the Type Annotations compiler.

Putting the Checker Framework's \<javac> earlier in your \<PATH> will
ensure that the Checker Framework's version is used.

\item
If you are developing a checker within the Checker Framework, there is
a developer version of \<javac> in the \<bin-devel> directory. This
version will use compiled classes from \<dataflow/build>,
\<javacutil/build>, \<framework/build>,
and \<checker/build> in the \<checker-framework> directory instead of
the compiled jar files, and by default will print stack traces for all
errors.

To use it, set your \<PATH> to use \<javac> in the \<bin-devel> directory:

\begin{Verbatim}
export PATH=$CHECKERFRAMEWORK/checker/bin-devel:${PATH}
\end{Verbatim}

The developer version of \<javac> allows you to not have to rebuild
the jar files after every code change, in turn allowing you to test
your changes faster. Source files can be compiled using command \<./gradlew
compileJava>, or can be automatically compiled by
an IDE such as Eclipse.

\item Test that everything works:

  \begin{itemize}

  \item Run \code{./gradlew allTests}:
\begin{Verbatim}
  cd $CHECKERFRAMEWORK
  ./gradlew allTests
\end{Verbatim}
% $ to unconfuse Emacs LaTeX mode

  \item Run the Nullness Checker examples (see
    Section~\refwithpage{nullness-example}).

  \end{itemize}

\end{enumerate}


\subsectionAndLabel{Build the Checker Framework Manual (this document)}{building-manual}

\begin{enumerate}
\item
Install needed packages; see Section~\ref{building-prerequisites} for
instructions.

\item
Run \code{make} in the \code{docs/manual} directory to build both the PDF and HTML versions of the manual.
\end{enumerate}


\subsectionAndLabel{Code style, IDE configuration, pull requests, etc.}{building-developer-manual}

Please see the
\href{https://rawgit.com/typetools/checker-framework/master/docs/developer/developer-manual.html}{Checker Framework Developer Manual}.


\subsectionAndLabel{Enable continuous integration builds}{building-ci}

A continuous integration system runs tests every time you
push a commit to GitHub.

If you have forked any of the projects rather than just creating a clone,
then we recommend that you enable CI builds,
so that you learn quickly of any errors that creep into your fork.

Follow the
\ahref{https://docs.microsoft.com/en-us/azure/devops/pipelines/create-first-pipeline?view=azure-devops}{Azure
  Pipelines getting started directions}.

To save time, by default the CI jobs download a pre-built version of
the JDK rather than building the JDK from the sources in the Checker
Framework repository.  This means that if you make a change to the
annotated JDK, your tests will fail.
To fix your tests, follow the instructions at
\url{https://github.com/typetools/annotated-libraries}.


\subsubsectionAndLabel{Debugging continuous integration builds}{building-ci-debug}

If a continuous integration job is failing, you can reproduce the problem locally.
The CI jobs all run within Docker containers.
Install Docker on your local computer, then perform commands like the
following to get a shell within Docker:

\begin{Verbatim}
docker pull mdernst/cf-ubuntu-jdk8
docker run -it mdernst/cf-ubuntu-jdk8 /bin/bash
\end{Verbatim}

Then, you can run arbitrary commands, including those that appear in the
CI configuration files.


\sectionAndLabel{Contributing fixes (creating a pull request)}{pull-request}

Please see the
\ahref{https://rawgit.com/typetools/checker-framework/master/docs/developer/developer-manual.html#pull-requests}{pull
  requests} section of the Developer Manual.
Thanks in advance for your contributions!


\sectionAndLabel{Publications}{publications}

Here are two technical papers about the Checker Framework itself:

\begin{itemize}
\item
``Practical pluggable types for Java''~\cite{PapiACPE2008}
(ISSTA 2008, \myurl{https://homes.cs.washington.edu/~mernst/pubs/pluggable-checkers-issta2008.pdf})
describes the design and implementation of the Checker Framework.
The paper also describes case
studies in which the Nullness, Interning, Javari, and IGJ Checkers found
previously-unknown errors in real software.
The case studies also yielded new insights about type systems.

\item
``Building and using pluggable
type-checkers''~\cite{DietlDEMS2011}
(ICSE 2011, \myurl{https://homes.cs.washington.edu/~mernst/pubs/pluggable-checkers-icse2011.pdf})
discusses further experience with the Checker Framework, increasing the
number of lines of verified code to 3 million.  The case studies are of the
Fake Enum, Signature String, Interning, and Nullness Checkers.
The paper also evaluates the ease
of pluggable type-checking with the Checker Framework:  type-checkers
were easy to write, easy for novices to use, and effective in finding
errors.
\end{itemize}

Here are some papers about type systems that were implemented and evaluated
using the Checker Framework:

\begin{description}
\item[Nullness (Chapter~\ref{nullness-checker})]
See the two papers about the Checker Framework, described above.

\item[Rawness initialization (Section~\ref{initialization-rawness-checker})]
``Inference of field initialization'' (ICSE 2011, \myurl{https://homes.cs.washington.edu/~mernst/pubs/initialization-icse2011-abstract.html})
describes inference for the Rawness Initialization Checker.

\item[Interning (Chapter~\ref{interning-checker})]
See the two papers about the Checker Framework, described above.

\item[Locking (Chapter~\ref{lock-checker})]
``Locking discipline inference and checking'' (ICSE 2016,
\myurl{https://homes.cs.washington.edu/~mernst/pubs/locking-inference-checking-icse2016-abstract.html})
describes the Lock Checker.

\item[Fake enumerations, type aliases, and typedefs (Chapter~\ref{fenum-checker})]
See the ICSE 2011 paper about the Checker Framework, described above.

\item[Regular expressions (Chapter~\ref{regex-checker})]
``A type system for regular expressions''~\cite{SpishakDE2012} (FTfJP 2012, \myurl{https://homes.cs.washington.edu/~mernst/pubs/regex-types-ftfjp2012-abstract.html})
            describes the Regex Checker.

\item[Format Strings (Chapter~\ref{formatter-checker})]
``A type system for format strings''~\cite{WeitzKSE2014} (ISSTA 2014, \myurl{https://homes.cs.washington.edu/~mernst/pubs/format-string-issta2014-abstract.html})
            describes the Format String Checker.

\item[Signature strings (Chapter~\ref{signature-checker})]
See the ICSE 2011 paper about the Checker Framework, described above.

\item[GUI Effects (Chapter~\ref{guieffect-checker})]
``JavaUI: Effects for controlling UI object access''~\cite{GordonDEG2013} (ECOOP 2013, \myurl{https://homes.cs.washington.edu/~mernst/pubs/gui-thread-ecoop2013-abstract.html})
            describes the GUI Effect Checker.

\item
``Verification games: Making verification fun'' (FTfJP 2012, \myurl{https://homes.cs.washington.edu/~mernst/pubs/verigames-ftfjp2012-abstract.html})
            describes a general inference approach that, at the time, had only been implemented for the Nullness Checker (Section~\ref{nullness-checker}).

\item[Thread locality (Section~\ref{loci-thread-locality-checker})]
``Loci: Simple thread-locality for Java''~\cite{WrigstadPMZV2009} (ECOOP 2009,
\myurl{http://janvitek.org/pubs/ecoop09.pdf})

\item[Security (Section~\ref{sparta-checker})]
``Static analysis of implicit control flow: Resolving Java reflection and
  Android intents''~\cite{BarrosJMVDdAE2015} (ASE 2015,
  \myurl{https://homes.cs.washington.edu/~mernst/pubs/implicit-control-flow-ase2015-abstract.html})
  describes the SPARTA toolset and information flow type-checker.

``Boolean formulas for the static identification of injection attacks in
  Java''~\cite{ErnstLMSS2015} (LPAR 2015, \myurl{https://homes.cs.washington.edu/~mernst/pubs/detect-injections-lpar2015-abstract.html})

\item[\href{https://ece.uwaterloo.ca/~wdietl/ownership/}{Generic Universe
    Types} (Section~\ref{gut-checker})]
``Tunable static inference for Generic Universe Types'' (ECOOP 2011, \myurl{https://homes.cs.washington.edu/~mernst/pubs/tunable-typeinf-ecoop2011-abstract.html})
            describes inference for the Generic Universe Types type system.

Another implementation of Universe Types and \href{http://www.cs.rpi.edu/~huangw5/cf-inference/}{ownership types} is  described in
``Inference and checking of object ownership''~\cite{HuangDME2012} (ECOOP 2012, \myurl{https://homes.cs.washington.edu/~mernst/pubs/infer-ownership-ecoop2012-abstract.html}).

\item[Approximate data (Section~\ref{enerj-checker})]
``EnerJ: Approximate Data Types for Safe and General Low-Power Computation''~\cite{SampsonDFGCG2011} (PLDI 2011, \myurl{https://homes.cs.washington.edu/~luisceze/publications/Enerj-pldi2011.pdf})

\item[Information flow and tainting (Section~\ref{sparta-checker})]
``Collaborative Verification of Information Flow
for a High-Assurance App Store''~\cite{ErnstJMDPRKBBHVW2014} (CCS 2014, \myurl{https://homes.cs.washington.edu/~mernst/pubs/infoflow-ccs2014.pdf}) describes the SPARTA information flow type system.

\item[IGJ and OIGJ immutability (Section~\ref{igj-checker})]
``Object and reference immutability using Java generics''~\cite{ZibinPAAKE2007} (ESEC/FSE 2007, \myurl{https://homes.cs.washington.edu/~mernst/pubs/immutability-generics-fse2007-abstract.html})
and
``Ownership and immutability in generic Java''~\cite{ZibinPLAE2010} (OOPSLA 2010, \myurl{https://homes.cs.washington.edu/~mernst/pubs/ownership-immutability-oopsla2010-abstract.html})
            describe the IGJ and OIGJ immutability type systems.
For further case studies, also see the ISSTA 2008 paper about the Checker
Framework, described above.

\item[Javari immutability (Section~\ref{javari-checker})]
``Javari: Adding reference immutability to Java''~\cite{TschantzE2005} (OOPSLA 2005, \myurl{https://homes.cs.washington.edu/~mernst/pubs/ref-immutability-oopsla2005-abstract.html})
            describes the Javari type system.
For inference, see
``Inference of reference immutability''~\cite{QuinonezTE2008} (ECOOP 2008, \myurl{https://homes.cs.washington.edu/~mernst/pubs/infer-refimmutability-ecoop2008-abstract.html})
and
``Parameter reference immutability: Formal definition, inference tool, and comparison''~\cite{ArtziQKE2009} (J.ASE 2009, \myurl{https://homes.cs.washington.edu/~mernst/pubs/mutability-jase2009-abstract.html}).
For further case studies, also see the ISSTA 2008 paper about the Checker
Framework, described above.

\item[ReIm immutability]
% TODO:  (Section~\ref{reim-checker})
``ReIm \& ReImInfer: Checking and inference of reference immutability and method purity''~\cite{HuangMDE2012} (OOPSLA 2012, \myurl{https://homes.cs.washington.edu/~mernst/pubs/infer-refimmutability-oopsla2012-abstract.html})
            describes the ReIm immutability type system.

\end{description}

In addition to these papers that discuss use the Checker Framework
directly, other academic papers use the Checker Framework in their
implementation or evaluation.
Most educational use of the Checker
Framework is never published, and most commercial use of the Checker
Framework is never discussed publicly.

(If you know of a paper or other use that is not listed here, please inform
the Checker Framework developers so we can add it.)


\sectionAndLabel{Credits and changelog}{credits}

Differences from previous versions of the checkers and framework can be found
in the \code{changelog.txt} file.  This file is included in the
Checker Framework distribution and is also available on the web at
\myurl{https://checkerframework.org/changelog.txt}.

Developers who have contributed code to the Checker Framework include
\input{contributors.tex}
In addition, too many users to list have provided valuable feedback, which
has improved the toolset's design and implementation.
Thanks for your help!


\sectionAndLabel{License}{license}

Two different licenses apply to different parts of the Checker Framework.
\begin{itemize}
\item
The Checker Framework itself is licensed under the GNU General Public License
(GPL), version 2, with the classpath exception.
The GPL is the same license that OpenJDK is licensed
under.  Just as compiling your code with javac does not infect your code
with the GPL, type-checking your code with the Checker Framework does not
infect your code with the GPL\@.  Running the Checker Framework during
development has no effect on your intellectual property or licensing.  If
you want to ship the Checker Framework as part of your product, then your
product must be licensed under the GPL\@.
\item
The more permissive MIT License applies
to code that you might want to include in your own
program, such as the annotations and run-time utility classes.
\end{itemize}
\noindent
For details, see file
\ahref{https://raw.githubusercontent.com/typetools/checker-framework/master/LICENSE.txt}{\<LICENSE.txt>}.



% LocalWords:  jsr unsetting plugins langtools zipfile cp plugin Nullness txt
% LocalWords:  nullness classpath NonNull MyObject javac uref changelog MyEnum
% LocalWords:  subtyping containsKey proc classfiles SourceChecker javap jdk
% LocalWords:  MyFile buildfiles ClassName JRE java jsr308 bootclasspath
%  LocalWords:  extJavac ZipFile AnoPrintErrorStack AprintAllQualifiers Jlint
%  LocalWords:  Telmo Correa Papi NoSuchFieldError ZipException Xlint A1
%  LocalWords:  FileNotFoundException MyQualifier ImplicitFor A2 A3 JDKs
%  LocalWords:  StaticNestedClass StaticNested ConfusingAnnotation pre yml
%%  LocalWords:  CHECKERFRAMEWORK currentOutgoing isCompleted ElementType
%%  LocalWords:  EnsuresNonNull devel javacutil stubparser rsvg Regex IGJ
%%  LocalWords:  JavaUI EnerJ App CCS ReIm ReImInfer Anatoly Kupriyanov
%%  LocalWords:  Asumu Takikawa Brotherston McArthur Luo Bayne Coblenz Lai
%%  LocalWords:  Barros Athaydes Ren Oblak Heule Steph Trask Stalnaker
%%  LocalWords:  toolset's typechecking LiteralKind reifiable plaintext
%%  LocalWords:  astub homebrew hevea cloneAndBuildDependencies allTests
%%  LocalWords:  compileJava typedefs LPAR Tunable OIGJ sudo