docs/manual/troubleshooting.tex

\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://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.  Note that if you are running under Java 8,
\<\$CHECKERFRAMEWORK/bin/javac -version> prints ``javac (version info
not available)'' because it uses the Error Prone compiler which does not
provide version information.

\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{Verbatim}
error: Annotation processor 'org.checkerframework.checker.signedness.SignednessChecker' 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
% 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.

\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
(all on one line),
then either give the JVM more memory when running the Checker Framework, or
split your files and methods into smaller ones, or both.

\item
Versions of \ahref{https://errorprone.info/}{Error Prone} before 2.4.0 are
incompatible with the Checker Framework.  Those versions of Error Prone
use an outdated version of the Checker Framework's dataflow analysis
library, which conflicts with the Checker Framework itself.

If you wish to use both Error Prone and the Checker Framework, then use
Error Prone version 2.4.0 or later.
If you cannot upgrade to Error Prone 2.4.0 or later, there is a way to
still use both tools.  The
\ahreforurl{https://github.com/kelloggm/checkerframework-gradle-plugin\#incompatibility-with-error-prone}{Gradle
  plugin documentation} shows how to do so if you use the Gradle build
system.

\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 \<pakkage.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.
  \begin{itemize}
  \item
    Perhaps your proof was incomplete or incorrect.  Your proof might
    depend 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.
  \item
    Perhaps your proof is incorrect, and the errors indicate where.
  \item
    Perhaps 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.
  \end{itemize}

  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}).  The
annotations might appear in stub files (which appear
in an \code{.astub} file together with the checker's source code)
or in the form of annotated libraries (which appear
in \url{https://github.com/typetools/}).

\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] 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}


\item
\label{false-positive-in-dead-code}
  The Checker Framework can issue false positive warnings in dead code.  An
  example is

\begin{smaller}
\begin{Verbatim}
  void m() {
    String t = "";
    t.toString();
    try {
    } catch (Throwable e) {
        t.toString(); // Nullness Checker issues spurious (dereference.of.nullable)
    }
\end{Verbatim}
\end{smaller}

\item
  If the Checker Framework issues an error or warning that you cannot
  reproduce using a smaller test case, then try running the Checker
  Framework with the \<-AatfDoNotCache> command-line argument.  If the
  Checker Framework behaves differently with and without that command-line
  argument, then there is a bug related to its internal caches.  Please
  report that bug at
  \url{https://github.com/typetools/checker-framework/issues}.

\end{itemize}


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

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}


\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}.
You can also use the issue tracker to make suggestions and feature
requests.  We also welcome pull requests with annotated libraries, bug
fixes, new features, new checkers, 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 should include at
least the following 4 parts: commands, inputs, outputs, and expectation.

% If you update this, also update ../../.github/ISSUE_TEMPLATE
\begin{description}
\item[Commands]
  Provide one or more commands that can be pasted into a command shell to
  reproduce the problem.

  In the simplest case, you will provide one command of
  the form \<javac -processor ... MyFile.java>.  In more complex cases, it
  might be a set of commands clone a repository, check out a branch, and
  run a build command.  Include commands to install software and set
  environment variables if necessary.

  If you encountered the problem in an IDE, reproduce it from the command
  line; if you cannot, report the bug to the IDE integration.

  It can be helpful to add \\
  \code{-version -Aversion -AprintGitProperties -verbose -AprintVerboseGenerics} \\
  to the javac options.  This causes the
  compiler to output debugging information, including its version number.

\item[Inputs]
  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.  This is not necessary if the commands you
  provided obtain the code that is type-checked.

  If you cannot share your code, create a new, small test case.  (A small
  test case is helpful even if your code is not secret!)  If the Checker
  Framework crashed, 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.

  \emph{Minimization:}
  If your command invokes a build system such as Gradle or Maven, it can be
  helpful to the maintainers if you are able to reduce it to a single
  \<javac> invocation on a single file.
  This also rules out the possibility that the problem is with the build system
  integration rather than the checker itself.
  If you use an invasive
  annotation processor such as Lombok, then try to reproduce the problem
  without it --- this will indicate whether the problem is in the Checker
  Framework proper or in its interaction with Lombok.

\item[Output]
  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[Expectation]
  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 reveal
  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.

  It can also be helpful to indicate what you have already done to try to
  understand the problem.  Did you do any additional experiments?  What
  parts of the manual did you read, and what else did you search for in the
  manual?  Without this information, the maintainers may give you redundant
  suggestions or may waste time re-doing work you have already done.
\end{description}

% 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}

If a checker reports a warning because a library contains \emph{incorrect} annotations,
then please open a pull request that adds the annotations.  If the
library's maintainers have added annotations, make a pull request to them.
If the Checker Framework maintainers have added annotations,
you can find the annotated source in \url{https://github.com/typetools/}.

If a checker reports a warning because a library is \emph{not
annotated}, please do not open a GitHub issue.
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}.

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.

% 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.
Put the setting of the \<JAVA\_HOME> environment variable in a startup file
such as \<.bash\_profile> or \<.bashrc>, if \<JAVA\_HOME> is not already
set appropriately.  It must be the location of your JDK 8 or JDK 11
installation (not the JRE installation, and not JDK 7 or earlier).
You may need to log out and log back in for the setting to take effect.

\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.

In a startup file, write:
% Can someone give a simpler command?
% Command taken from:
%   https://github.com/typetools/checker-framework/blob/master/checker/bin-devel/build.sh#L19
%BEGIN LATEX
\begin{smaller}
%END LATEX
\begin{Verbatim}
  export JAVA_HOME=${JAVA_HOME:-$(dirname "$(dirname "$(readlink -f "$(which javac)")")")}
\end{Verbatim}
%BEGIN LATEX
\end{smaller}
%END LATEX

\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 tap AdoptOpenJDK/openjdk
brew install --cask adoptopenjdk11
brew install --cask 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>.

In a startup file, write:

\begin{Verbatim}
export JAVA_HOME=$(/usr/libexec/java_home -v 1.11)
\end{Verbatim}
or
\begin{Verbatim}
export JAVA_HOME=/Library/Java/JavaVirtualMachines/adoptopenjdk-11.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.


\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 assemble} to build the Checker Framework:

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

\noindent
Your antivirus program (e.g., Windows Security Virus \& threat protection)
might make the build run very slowly, or might make it seem to stall.  Just
give it time.

\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 javac Java compiler.

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

\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}

We strongly recommend that you enable continuous integration (CI) builds on
your fork of the projects, so that you learn quickly about errors.  See the
\ahref{https://rawgit.com/typetools/checker-framework/master/docs/developer/developer-manual.html\#ci}{CI
  instructions} in the Checker Framework Developer Manual.


\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}{contributing}

We welcome contributions and pull requests.  Section~\ref{build-source}
tells you how to set up your development environment to compile the Checker
Framework, and the
\href{https://rawgit.com/typetools/checker-framework/master/docs/developer/developer-manual.html}{Checker
  Framework Developer Manual} gives more information.

One good way to contribute is to give feedback about your use of the tool.
There is a list
  of potential projects for new contributors at \url{https://rawgit.com/typetools/checker-framework/master/docs/developer/gsoc-ideas.html}.
Or, you can fix a bug that
you have encountered during your use of the Checker Framework.


\subsectionAndLabel{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 Checker Framework Developer Manual.
Thanks in advance for your contributions!

The easiest bugs to fix for a newcomer are
\ahref{https://github.com/typetools/checker-framework/issues?q=is\%3Aopen+is\%3Aissue+label\%3A\%22help+wanted\%22}{labeled
  as ``help wanted''}.

Please do not spam the issue tracker with requests to assign an issue to
you.  If you want to contribute by fixing an issue, just open a pull
request that fixes it.  You can do that even if the issue is already
assigned to someone.

Please do not spam the issue tracker asking how to get started fixing a
bug.  If you have concrete questions, please ask them and we will be happy
to assist you.  If you don't know how to get started fixing a particular
bug, then you should contribute to the project in other ways.  Thanks!


\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{docs/CHANGELOG.md} file.  This file is included in the
Checker Framework distribution and is also available on the web at
\myurl{https://checkerframework.org/CHANGELOG.md}.

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 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 ci
%%  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 allTests AatfDoNotCache Java''
%%  LocalWords:  compileJava typedefs LPAR Tunable OIGJ sudo wanted''
% LocalWords:  addStandardLiteralQualifiers AprintGitProperties checkers''
% LocalWords:  expressions'' strings'' access'' intents'' ownership''
% LocalWords:  Computation'' Store'' generics'' immutability'' purity''
% LocalWords:  comparison''