\htmlhr
\chapterAndLabel{Introduction}{introduction}

The Checker Framework enhances Java's type system to make it more powerful
and useful.
This lets software developers detect and
prevent errors in their Java programs.

A ``checker'' is a tool that warns you about certain errors or gives you a
guarantee that those errors do not occur.
The Checker Framework comes with checkers for specific types of errors:

\begin{enumerate}

\item
  \ahrefloc{nullness-checker}{Nullness Checker} for null pointer errors
  (see \chapterpageref{nullness-checker})
\item
  \ahrefloc{initialization-checker}{Initialization Checker} to ensure all
  fields are set in the constructor (see
  \chapterpageref{initialization-checker})
\item
  \ahrefloc{map-key-checker}{Map Key Checker} to track which values are
  keys in a map (see \chapterpageref{map-key-checker})
\item
  \ahrefloc{optional-checker}{Optional Checker} for errors in using the
  \sunjavadoc{java.base/java/util/Optional.html}{Optional} type (see
  \chapterpageref{optional-checker})
\item
  \ahrefloc{interning-checker}{Interning Checker} for errors in equality
  testing and interning (see \chapterpageref{interning-checker})
\item
  \ahrefloc{lock-checker}{Lock Checker} for concurrency and lock errors
  (see \chapterpageref{lock-checker})
\item
  \ahrefloc{index-checker}{Index Checker} for array accesses
  (see \chapterpageref{index-checker})
\item
  \ahrefloc{fenum-checker}{Fake Enum Checker} to allow type-safe fake enum
  patterns and type aliases or typedefs (see \chapterpageref{fenum-checker})
\item
  \ahrefloc{tainting-checker}{Tainting Checker} for trust and security errors
  (see \chapterpageref{tainting-checker})
\item
  \ahrefloc{regex-checker}{Regex Checker} to prevent use of syntactically
  invalid regular expressions (see \chapterpageref{regex-checker})
\item
  \ahrefloc{formatter-checker}{Format String Checker} to ensure that format
  strings have the right number and type of \<\%> directives (see
  \chapterpageref{formatter-checker})
\item
  \ahrefloc{i18n-formatter-checker}{Internationalization Format String Checker}
  to ensure that i18n format strings have the right number and type of
  \<\{\}> directives (see \chapterpageref{i18n-formatter-checker})
\item
  \ahrefloc{propkey-checker}{Property File Checker} to ensure that valid
  keys are used for property files and resource bundles (see
  \chapterpageref{propkey-checker})
\item
  \ahrefloc{i18n-checker}{Internationalization Checker} to
  ensure that code is properly internationalized (see
  \chapterpageref{i18n-checker})
% The Compiler Message Key Checker is neither here nor in the advanced
% type system features chapter because it is really meant for
% Checker Framework developers and as sample code, and is not meant
% for Checker Framework users at large.
\item
  \ahrefloc{signature-checker}{Signature String Checker} to ensure that the
  string representation of a type is properly used, for example in
  \<Class.forName> (see \chapterpageref{signature-checker})
\item
  \ahrefloc{guieffect-checker}{GUI Effect Checker} to ensure that non-GUI
  threads do not access the UI, which would crash the application
  (see \chapterpageref{guieffect-checker})
\item
  \ahrefloc{units-checker}{Units Checker} to ensure operations are
  performed on correct units of measurement
  (see \chapterpageref{units-checker})
\item
  \ahrefloc{signedness-checker}{Signedness Checker} to
  ensure unsigned and signed values are not mixed
  (see \chapterpageref{signedness-checker})
\item
  \ahrefloc{aliasing-checker}{Aliasing Checker} to identify whether
  expressions have aliases (see \chapterpageref{aliasing-checker})
\item
  \ahrefloc{purity-checker}{Purity Checker} to identify whether
  methods have side effects (see \chapterpageref{purity-checker})
\item
  \ahrefloc{constant-value-checker}{Constant Value Checker} to determine
  whether an expression's value can be known at compile time
  (see \chapterpageref{constant-value-checker})
\item
  \ahrefloc{reflection-resolution}{Reflection Checker} to determine
  whether an expression's value (of type \<Method> or \<Class>) can be known at compile time
  (see \chapterpageref{reflection-resolution})
\item
  \ahrefloc{subtyping-checker}{Subtyping Checker} for customized checking without
  writing any code (see \chapterpageref{subtyping-checker})
% \item
%   \ahrefloc{typestate-checker}{Typestate checker} to ensure operations are
%   performed on objects that are in the right state, such as only opened
%   files being read (see \chapterpageref{typestate-checker})
\item
  \ahrefloc{third-party-checkers}{Third-party checkers} that are distributed
  separately from the Checker Framework
  (see \chapterpageref{third-party-checkers})

\end{enumerate}

\noindent
These checkers are easy to use and are invoked as arguments to \<javac>.


The Checker Framework also enables you to write new checkers of your
own; see Chapters~\ref{subtyping-checker} and~\ref{creating-a-checker}.


\sectionAndLabel{How to read this manual}{how-to-read-this-manual}

If you wish to get started using some particular type system from the list
above, then the most effective way to read this manual is:

\begin{itemize}
\item
  Read all of the introductory material
  (Chapters~\ref{introduction}--\ref{using-a-checker}).
\item
  Read just one of the descriptions of a particular type system and its
  checker (Chapters~\ref{nullness-checker}--\ref{third-party-checkers}).
\item
  Skim the advanced material that will enable you to make more effective
  use of a type system
  (Chapters~\ref{polymorphism}--\ref{troubleshooting}), so that you will
  know what is available and can find it later.  Skip
  Chapter~\ref{creating-a-checker} on creating a new checker.
\end{itemize}


\sectionAndLabel{How it works:  Pluggable types}{pluggable-types}

The Checker Framework supports adding
pluggable type systems to the Java language in a backward-compatible way.
Java's built-in type-checker finds and prevents many errors --- but it
doesn't find and prevent \emph{enough} errors.  The Checker Framework lets you
run an additional type-checker as a plug-in to the javac compiler.  Your
code stays completely backward-compatible:  your code compiles with any
Java compiler, it runs on any JVM, and your coworkers don't have to use the
enhanced type system if they don't want to.  You can check only part of
your program.  Type inference tools exist to help you annotate your
code; see \chapterpageref{type-inference-to-annotate}.


A type system designer uses the Checker Framework to define type qualifiers
and their semantics, and a
compiler plug-in (a ``checker'') enforces the semantics.  Programmers can
write the type qualifiers in their programs and use the plug-in to detect
or prevent errors.  The Checker Framework is useful both to programmers who
wish to write error-free code, and to type system designers who wish to
evaluate and deploy their type systems.



% This manual is organized as follows.
% \begin{itemize}
% \item Chapter~\ref{introduction} overviews the Checker Framework and
%   describes how to \ahrefloc{installation}{install} it (Chapter~\ref{installation}).
% \item Chapter~\ref{using-a-checker} describes how to \ahrefloc{using-a-checker}{use a checker}.
% \item
%   The next chapters are user manuals for the \ahrefloc{nullness-checker}{Nullness}
%   (Chapter~\ref{nullness-checker}), \ahrefloc{interning-checker}{Interning}
%   (Chapter~\ref{interning-checker}), and \ahrefloc{subtyping-checker}{Basic}
%   (Chapter~\ref{subtyping-checker}) checkers.
% \item Chapter~\ref{annotating-libraries} describes an approach for \ahrefloc{annotating-libraries}{annotating external
% libraries}.
% \item Chapter~\ref{creating-a-checker} describes how to
%   \ahrefloc{creating-a-checker}{write a new checker} using the Checker Framework.
% \end{itemize}






This document uses the terms ``checker'', ``checker plugin'',
``type-checking compiler plugin'', and ``annotation processor'' as
synonyms.

\sectionAndLabel{Installation}{installation}

This section describes how to install the Checker Framework.
\begin{itemize}
\item
If you use a build system that automatically downloads dependencies,
such as Gradle or Maven, \textbf{no installation is necessary}; just see
\chapterpageref{external-tools}.
\item
If you wish to try the Checker Framework without installing it, use the
\href{http://eisop.uwaterloo.ca/live/}{Checker Framework Live Demo} webpage.
\item
This section describes how to install the Checker Framework from its
distribution.  The Checker Framework release contains everything that you
need, both to run checkers and to write your own checkers.
\item
Alternately, you can build the latest development version from source
(Section~\refwithpage{build-source}).
\end{itemize}


\textbf{Requirement:}
% Keep in sync with build.gradle and SourceChecker.init.
You must have \textbf{JDK 8} or \textbf{JDK 11} installed.
(The Checker Framework should work with any JDK 8--12, but we only test with JDK 8 and JDK 11.)

The installation process is simple!  It has two required steps and one
optional step.
\begin{enumerate}
\item
  Download the Checker Framework distribution:
  %BEGIN LATEX
  \\
  %END LATEX
  \url{https://checkerframework.org/checker-framework-3.2.0.zip}

\item
  Unzip it to create a \code{checker-framework} directory.

\item
  \label{installation-configure-step}%
  Configure your IDE, build system, or command shell to include the Checker
  Framework on the classpath.  Choose the appropriate section of
  Chapter~\ref{external-tools}.


\end{enumerate}

That's all there is to it!  Now you are ready to start using the checkers.

We recommend that you work through the
\ahreforurl{https://checkerframework.org/tutorial/}{Checker
Framework tutorial}, which walks you through how to use the Checker
Framework on
the command line (Nullness, Regex, and Tainting Checkers).
There is also a
\ahreforurl{https://github.com/glts/safer-spring-petclinic/wiki}{Nullness Checker
tutorial} by David B\"urgin; the setup instructions are out of date, but
you can read through the steps.

Section~\ref{example-use} walks you through a simple example.  More detailed
instructions for using a checker appear in Chapter~\ref{using-a-checker}.



\sectionAndLabel{Example use:  detecting a null pointer bug}{example-use}

This section gives a very simple example of running the Checker Framework.
There is also a \ahreforurl{https://checkerframework.org/tutorial/}{tutorial}
that gives more extensive instructions for using the Checker Framework
on the command line,
and a
\ahreforurl{https://github.com/glts/safer-spring-petclinic/wiki}{Nullness Checker
tutorial} by David B\"urgin.

% To run a checker on a source file, just compile as usual, but pass the
% \<-processor> flag to the compiler.
%
% For instance, if you usually run the javac compiler like
% this:
%
% \begin{Verbatim}
%   javac Foo.java Bar.java
% \end{Verbatim}
%
% \noindent
% then you will instead a command line such as:
%
% \begin{alltt}
%   javac \textbf{-processor NullnessChecker} Foo.java Bar.java
%   javac \textbf{-processor RegexChecker} Foo.java Bar.java
% \end{alltt}
%
% \noindent
% but take note that the \code{javac} command must refer to the
% Checker Framework compiler (see Section~\ref{javac-wrapper}).
%
% If you usually do your coding within an IDE, you will need to configure
% the IDE; see Chapter~\ref{external-tools}.


\begin{enumerate}
\item
  Let's consider this very simple Java class.  The local variable \<ref>'s type is
  annotated as \refqualclass{checker/nullness/qual}{NonNull}, indicating that \<ref> must be a reference to a
  non-null object.  Save the file as \<GetStarted.java>.

\begin{Verbatim}
import org.checkerframework.checker.nullness.qual.*;

public class GetStarted {
    void sample() {
        @NonNull Object ref = new Object();
    }
}
\end{Verbatim}

\item
  Run the Nullness Checker on the class.
  You can do that from the command line or from an IDE:

\begin{enumerate}
\item
  From the command line, run this command:

%BEGIN LATEX
\begin{smaller}
%END LATEX
\begin{alltt}
  \emph{javac} -processor org.checkerframework.checker.nullness.NullnessChecker GetStarted.java
\end{alltt}
%BEGIN LATEX
\end{smaller}
%END LATEX

\noindent
where \emph{\code{javac}} is set as in Section~\ref{javac-wrapper}.

\item
  To compile within your IDE, you must have customized it to use the
  Checker Framework compiler and to pass the extra arguments (see
  Chapter~\ref{external-tools}).
\end{enumerate}

  The compilation should complete without any errors.

\item
  Let's introduce an error now.  Modify \<ref>'s assignment to:
\begin{alltt}
  @NonNull Object ref = \textbf{null};
\end{alltt}

\item
  Run the Nullness Checker again, just as before.  This run should emit
  the following error:
\begin{Verbatim}
GetStarted.java:5: incompatible types.
found   : @Nullable <nulltype>
required: @NonNull Object
        @NonNull Object ref = null;
                              ^
1 error
\end{Verbatim}

\end{enumerate}

The type qualifiers (e.g., \<@NonNull>) are permitted anywhere
that you can write a type, including generics and casts; see
Section~\ref{writing-annotations}.  Here are some examples:

\begin{alltt}
  \underline{@Interned} String intern() \ttlcb{} ... \ttrcb{}             // return value
  int compareTo(\underline{@NonNull} String other) \ttlcb{} ... \ttrcb{}  // parameter
  \underline{@NonNull} List<\underline{@Interned} String> messages;     // non-null list of interned Strings
\end{alltt}


\htmlhr
\chapterAndLabel{Using a checker}{using-a-checker}

A pluggable type-checker enables you to detect certain bugs in your code,
or to prove that they are not present.  The verification happens at compile
time.


Finding bugs, or verifying their absence, with a checker plugin is a two-step process, whose steps are
described in Sections~\ref{writing-annotations} and~\ref{running}.

\begin{enumerate}

\item The programmer writes annotations, such as \refqualclass{checker/nullness/qual}{NonNull} and
  \refqualclass{checker/interning/qual}{Interned}, that specify additional information about Java types.
  (Or, the programmer uses an inference tool to automatically insert
  annotations in his code:  see Section~\ref{nullness-inference}.)
  It is possible to annotate only part of your code:  see
  Section~\ref{unannotated-code}.

\item The checker reports whether the program contains any erroneous code
  --- that is, code that is inconsistent with the annotations.

\end{enumerate}

This chapter is structured as follows:
\begin{itemize}
\item Section~\ref{writing-annotations}: How to write annotations
\item Section~\ref{running}:  How to run a checker
\item Section~\ref{checker-guarantees}: What the checker guarantees
\item Section~\ref{tips-about-writing-annotations}: Tips about writing annotations
\end{itemize}

Additional topics that apply to all checkers are covered later in the manual:
\begin{itemize}
\item Chapter~\ref{advanced-type-system-features}: Advanced type system features
\item Chapter~\ref{suppressing-warnings}: Suppressing warnings
\item Chapter~\ref{legacy-code}: Handling legacy code
\item Chapter~\ref{annotating-libraries}: Annotating libraries
\item Chapter~\ref{creating-a-checker}: How to create a new checker
\item Chapter~\ref{external-tools}: Integration with external tools
\end{itemize}


Finally, there is a
\ahreforurl{https://checkerframework.org/tutorial/}{tutorial}
that walks you through using the Checker Framework on the
command line, and a separate
\ahreforurl{https://github.com/glts/safer-spring-petclinic/wiki}{Nullness
  Checker tutorial} by David B\"urgin.

% The annotations have to be on your classpath even when you are not using
% the -processor, because of the existence of the import statement for
% the annotations.


\sectionAndLabel{Writing annotations}{writing-annotations}

The syntax of type annotations in Java is specified by
the Java Language Specification (Java SE 8 edition).
% \href{https://checkerframework.org/jsr308/}{JSR 308}~\cite{JSR308-2008-09-12}.

Java 5 defines declaration annotations such as \<@Deprecated>, which apply
to a class, method, or field, but do not apply to the method's return type
or the field's type.  They are typically written on their own line in the
source code.

Java 8 defines type annotations, which you write immediately before any
use of a type, including in generics and casts.  Because array levels are
types and receivers have types, you can also write type annotations on
them.  Here are a few examples of type annotations:

%BEGIN LATEX
\begin{smaller}
%END LATEX
\begin{alltt}
  \underline{@Interned} String intern() \ttlcb{} ... \ttrcb{}               // return value
  int compareTo(\underline{@NonNull} String other) \ttlcb{} ... \ttrcb{}    // parameter
  String toString(\underline{@Tainted} MyClass this) \ttlcb{} ... \ttrcb{}  // receiver ("this" parameter)
  \underline{@NonNull} List<\underline{@Interned} String> messages;       // generics:  non-null list of interned Strings
  \underline{@Interned} String \underline{@NonNull} [] messages;          // arrays:  non-null array of interned Strings
  myDate = (\underline{@Initialized} Date) beingConstructed;  // cast
\end{alltt}
%BEGIN LATEX
\end{smaller}
%END LATEX

You only need to write annotations on method signatures, fields, and some type arguments.
Most annotations within method bodies are inferred for you; for more details,
see  Section~\ref{type-refinement}.

\sectionAndLabel{Running a checker}{running}

To run a checker plugin, run the compiler \code{javac} as usual,
but either pass the \code{-processor \emph{plugin\_class}} command-line
option, or use auto-discovery as described in
Section~\ref{checker-auto-discovery}.
A concrete example of using \code{-processor} to run the Nullness Checker is:

\begin{Verbatim}
  javac -processor nullness MyFile.java
\end{Verbatim}

\noindent
where \<javac> is as specified in Section~\ref{javac-wrapper}.

You can also run a checker from within your favorite IDE or build system.  See
Chapter~\ref{external-tools} for details about build tools such as
Ant (Section~\ref{ant-task}),
Buck (Section~\ref{buck}),
Gradle (Section~\ref{gradle}), and
Maven (Section~\ref{maven});
IDEs such as
IntelliJ IDEA (Section~\ref{intellij}),
Eclipse (Section~\ref{eclipse}),
NetBeans (Section~\ref{netbeans}),
and
tIDE (Section~\ref{tide});
and about customizing other IDEs and build tools.

The checker is run on only the Java files that javac compiles.
This includes all Java files specified on the command line (or
created by another annotation processor).  It may also include other of
your Java files (but not if a more recent \code{.class} file exists).
Even when the checker does not analyze a class (say, the class was
already compiled, or source code is not available), it does check
the \emph{uses} of those classes in the source code being compiled.

You can always compile the code without the \code{-processor}
command-line option, but in that case no checking of the type
annotations is performed.  Furthermore, only explicitly-written annotations
are written to the \<.class> file; defaulted annotations are not, and this
will interfere with type-checking of clients that use your code.
Therefore, it is strongly recommended that whenever you are creating
\<.class> files that will be distributed or compiled against, you run the
type-checkers for all the annotations that your have written.


\subsectionAndLabel{Using annotated libraries}{annotated-libraries-using}

When your code uses a library that is not currently being compiled, the
Checker Framework looks up the library's annotations in its class files.

Some projects are already distributed with type annotations by their
maintainers, so you do not need to do anything special.
Over time, this should become more common.

For some other libraries, the Checker Framework developers have provided an
annotated version of the library.
The annotated libraries appear in
\ahref{https://search.maven.org/search?q=org.checkerframework.annotatedlib}{the
  \<org.checkerframework.annotatedlib> group in the Central Repository}.
The annotated library has \emph{identical} behavior to the upstream,
unannotated version; the source code is identical other than the
annotations are different, so the only difference is with respect to
pluggable type-checking of clients.

(Some of the annotated libraries are
% This list appears here to make it searchable/discoverable.
bcel,
commons-csv,
commons-io,
guava,
and
java-getopt.
If the library you are interested in does not appear
\ahref{https://search.maven.org/search?q=org.checkerframework.annotatedlib}{in
  the Central Repository}, you can contribute by annotating it, which will
help you and all other Checker Framework users; see
\chapterpageref{annotating-libraries}.)

To use an annotated library:

\begin{itemize}
\item
If your project stores \<.jar> files locally, then
\ahref{https://search.maven.org/search?q=org.checkerframework.annotatedlib}{download
  the \<.jar> file from the Central Repository}.

\item
If your project manages dependencies using a tool such as Gradle or Maven,
then update your buildfile to use the \<org.checkerframework.annotatedlib>
group.  For example, in \<build.gradle>, change

\begin{Verbatim}
  api group: 'org.apache.bcel', name: 'bcel', version: '6.3.1'
  api group: 'commons-io', name: 'commans-io', version: '2.6'
\end{Verbatim}

\noindent
to

\begin{Verbatim}
  api group: 'org.checkerframework.annotatedlib', name: 'bcel', version: '6.3.1'
  api group: 'org.checkerframework.annotatedlib', name: 'commons-io', version: '2.6.0.1'
\end{Verbatim}

\noindent
Use the same version number.  (Sometimes you will use a slightly larger
number, if the Checker Framework developers have improved the type
annotations since the last release by the upstream maintainers.)  If a
newer version of the upstream library is available but that version is not
available in \<org.checkerframework.annotatedlib>, then
\ahrefloc{reporting-bugs}{open an issue} requesting that the
\<org.checkerframework.annotatedlib> version be updated.
\end{itemize}

%% This is for paranoid users.
% During type-checking, you should use the
% annotated version of the library to improve type-checking results (to issue
% fewer false positive warnings).  When doing ordinary compilation or while
% running your code, you can use either the annotated library or the regular
% distributed version of the library --- they behave identically.

There are two special cases.
\begin{itemize}
\item
The annotated JDK is automatically put on your
classpath; you don't have to do anything special for it.
\item
For the Javadoc classes in the JDK's \<com.sun.javadoc> package,
% are not exposed by ct.sym and therefore cannot be part of an
% annotated JDK
use the stub file \<checker/resources/javadoc.astub> by using \<-Astubs=checker.jar/javadoc.astub>.
% Note: that this syntax only works for checker.jar.
\end{itemize}


\subsectionAndLabel{Distributing your annotated project}{distributing}

  The distributed
  \<.jar> files can be used for pluggable type-checking of client code.
  The \<.jar> files are only compatible with a Java 8
  % or later
  JVM.
  Developers perform pluggable type-checking in-house to detect errors and
  verify their absence.
  When you create \<.class> files, run each relevant type system.
  Create the distributed \<.jar> files from those \<.class> files.


\subsectionAndLabel{Summary of command-line options}{checker-options}

You can pass command-line arguments to a checker via javac's standard \<-A>
option (``\<A>'' stands for ``annotation'').  All of the distributed
checkers support the following command-line options.
Each checker may support additional command-line options; see the checker's
documentation.

% This list should be kept in sync with file
% framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java

Unsound checking: ignore some errors
\begin{itemize}
\item \<-AsuppressWarnings>
  Suppress all errors and warnings matching the given key; see
  Section~\ref{suppresswarnings-command-line}.
\item \<-AskipUses>, \<-AonlyUses>
  Suppress all errors and warnings at all uses of a given class --- or at all
  uses except those of a given class.  See Section~\ref{askipuses}.
\item \<-AskipDefs>, \<-AonlyDefs>
  Suppress all errors and warnings within the definition of a given class
  --- or everywhere except within the definition of a given class.  See
  Section~\ref{askipdefs}.
\item \<-AassumeSideEffectFree>, \<-AassumeDeterministic>, \<-AassumePure>
  Unsoundly assume that every method is side-effect-free, deterministic, or
  both; see
  Section~\ref{type-refinement-purity}.
\item \<-AassumeAssertionsAreEnabled>, \<-AassumeAssertionsAreDisabled>
  Whether to assume that assertions are enabled or disabled; see Section~\ref{type-refinement-assertions}.
\item \<-AignoreRangeOverflow>
  Ignore the possibility of overflow for range annotations such as
  \<@IntRange>; see Section~\ref{value-checker-overflow}.
\item \<-Awarns>
  Treat checker errors as warnings.  If you use this, you may wish to also
  supply \code{-Xmaxwarns 10000}, because by default \<javac> prints at
  most 100 warnings.  If you use this, don't supply \code{-Werror},
  which is a javac argument to halt compilation if a warning is issued.
\item \<-AignoreInvalidAnnotationLocations>
  Ignore annotations in bytecode that have invalid annotation locations.
\end{itemize}

\label{unsound-by-default}
More sound (strict) checking: enable errors that are disabled by default
\begin{itemize}
\item \<-AcheckPurityAnnotations>
  Check the bodies of methods marked
  \refqualclass{dataflow/qual}{SideEffectFree},
  \refqualclass{dataflow/qual}{Deterministic},
  and \refqualclass{dataflow/qual}{Pure}
  to ensure the method satisfies the annotation.  By default,
  the Checker Framework unsoundly trusts the method annotation.  See
  Section~\ref{type-refinement-purity}.
\item \<-AinvariantArrays>
  Make array subtyping invariant; that is, two arrays are subtypes of one
  another only if they have exactly the same element type.  By default,
  the Checker Framework unsoundly permits covariant array subtyping, just
  as Java does.  See Section~\ref{invariant-arrays}.
\item \<-AcheckCastElementType>
  In a cast, require that parameterized type arguments and array elements
  are the same.  By default, the Checker Framework unsoundly permits them
  to differ, just as Java does.  See Section~\ref{covariant-type-parameters}
  and Section~\ref{invariant-arrays}.
\item \<-AuseDefaultsForUncheckedCode>
  Enables/disables unchecked code defaults.  Takes arguments ``source,bytecode''.
  ``-source,-bytecode'' is the (unsound) default setting.
  ``bytecode'' specifies
  whether the checker should apply unchecked code defaults to
  bytecode (that is, to already-compiled libraries); see
  Section~\ref{defaults-classfile}.
  Outside the scope of any relevant
  \refqualclass{framework/qual}{AnnotatedFor} annotation, ``source'' specifies whether unchecked code
  default annotations are applied to source code and suppress all type-checking warnings; see
  Section~\ref{compiling-libraries}.
\item \<-AconcurrentSemantics>
  Whether to assume concurrent semantics (field values may change at any
  time) or sequential semantics; see Section~\ref{faq-concurrency}.
\item \<-AconservativeUninferredTypeArguments>
  Whether an error should be issued if type arguments could not be inferred and
  whether method type arguments that could not be inferred should use
  conservative defaults.
  By default, such type arguments are (largely) ignored in later
  checks.
  Passing this option uses a conservative value instead.
  See \href{https://github.com/typetools/checker-framework/issues/979}{Issue
  979}.
\item \<-AignoreRawTypeArguments=false>
  Do not ignore subtype tests for type arguments that were inferred for a
  raw type. Must also use \<-AconservativeUninferredTypeArguments>.  See
  Section~\ref{generics-raw-types}.
\end{itemize}

Type-checking modes:  enable/disable functionality
\begin{itemize}
\item \<-Alint>
  Enable or disable optional checks; see Section~\ref{lint-options}.
\item \<-AsuggestPureMethods>
  Suggest methods that could be marked
  \refqualclass{dataflow/qual}{SideEffectFree},
  \refqualclass{dataflow/qual}{Deterministic},
  or \refqualclass{dataflow/qual}{Pure}; see
  Section~\ref{type-refinement-purity}.
\item \<-AresolveReflection>
  Determine the target of reflective calls, and perform more precise
  type-checking based no that information; see
  Chapter~\ref{reflection-resolution}.  \<-AresolveReflection=debug> causes
  debugging information to be output.
\item \<-Ainfer>
  Output suggested annotations for method signatures and fields.
  These annotations may reduce the number of type-checking
  errors when running type-checking in the future; see
  Section~\ref{whole-program-inference}.
\item \<-AshowSuppressWarningKeys>
  With each warning, show all possible keys to suppress that warning.
\item \<-AwarnUnneededSuppressions>
  Issue a warning if a \<@SuppressWarnings> did not suppress a warning
  issued by the checker.  This may issue false positive warnings about
  \<@SuppressWarnings> keys without a \<\emph{checkername}:> prefix
  (Section~\ref{suppresswarnings-annotation-syntax}).  You can use the
  \<-ArequirePrefixInWarningSuppressions> command-line argument to ensure
  your \<@SuppressWarnings> always use a \<\emph{checkername}:> prefix.
\item \<-ArequirePrefixInWarningSuppressions>
  Require that the key in a warning suppression annotation begin with a checker
  warning suppression key.  Otherwise, the suppress warning annotation does not
  suppress any warnings.  For example, if this command-line option is
  supplied, then \<@SuppressWarnings("assignment.type.incompatible")> has no effect, but
  \<@SuppressWarnings("nullness:assignment.type.incompatible")> does.
\end{itemize}

Partially-annotated libraries
\begin{itemize}
% \item \<-AprintUnannotatedMethods>
%   List library methods that need to be annotated; see
%   Section~\ref{annotating-libraries}.
\item \<-Astubs>
  List of stub files or directories; see Section~\ref{stub-using}.
\item \<-AstubWarnIfNotFound>
  Warn if a stub file entry could not be found; see Section~\ref{stub-using}.
\item \<-AstubWarnIfNotFoundIgnoresClasses>
  Don't warn about missing classes (only methods and fields) even when \<-AwarnIfNotFound> is true.
%% Uncomment when https://tinyurl.com/cfissue/2759 is fixed.
% \item \<-AstubWarnIfOverwritesBytecode>
%   Warn if a stub file entry overwrite bytecode information; see
%   Section~\ref{stub-using}.
\item \<-AstubWarnIfRedundantWithBytecode>
  Warn if a stub file entry is redundant with bytecode information; see
  Section~\ref{stub-using}.
% This item is repeated above:
\item \<-AuseDefaultsForUncheckedCode=source>
  Outside the scope of any relevant
  \refqualclass{framework/qual}{AnnotatedFor} annotation, use unchecked code
  default annotations and suppress all type-checking warnings; see
  Section~\ref{compiling-libraries}.
\end{itemize}

Debugging
\begin{itemize}
\item
 \<-AprintAllQualifiers>,
 \<-AprintVerboseGenerics>,
 \<-Adetailedmsgtext>,
 \<-Anomsgtext>
Amount of detail in messages; see Section~\ref{creating-debugging-options-detail}.

\item
 \<-Aignorejdkastub>,
 \<-ApermitMissingJdk>,
 \<-AstubDebug>
Stub and JDK libraries; see Section~\ref{creating-debugging-options-libraries}.

\item
 \<-Afilenames>,
 \<-Ashowchecks>,
 \<-AshowInferenceSteps>
Progress tracing; see Section~\ref{creating-debugging-options-progress}.

\item
\<-AoutputArgsToFile>
Output the compiler command-line arguments to a file.  Useful when the
command line is generated and executed by a tool, such as a build system.
This produces a standalone command line that can be executed independently
of the tool that generated it (such as a build system).
That command line makes it easier to reproduce, report, and debug issues.
For example, the command line can be modified to enable attaching a debugger.
See Section~\ref{creating-debugging-options-output-args}.

\item
 \<-Aflowdotdir>,
 \<-Averbosecfg>,
 \<-Acfgviz>
 Draw a visualization of the CFG (control flow graph); see
 Section~\ref{creating-debugging-dataflow-graph}.

\item
 \<-AresourceStats>,
 \<-AatfDoNotCache>,
 \<-AatfCacheSize>
Miscellaneous debugging options; see Section~\ref{creating-debugging-options-misc}.

\item
 \<-AprintGitProperties>
Print information about the git repository from which the Checker Framework
was compiled.

\end{itemize}


\noindent
Some checkers support additional options, which are described in that
checker's manual section.
% Search for "@SupportedOptions" in the implementation to find them all.
For example, \<-Aquals> tells
the Subtyping Checker (see Chapter~\ref{subtyping-checker}) and the Fenum Checker
(see Chapter~\ref{fenum-checker}) which annotations to check.


Here are some standard javac command-line options that you may find useful.
Many of them contain the word ``processor'', because in javac jargon, a
checker is an ``annotation processor''.

\begin{itemize}
\item \<-processor> Names the checker to be
  run; see Sections~\ref{running} and~\ref{shorthand-for-checkers}.
  May be a comma-separated list of multiple checkers.  Note that javac
  stops processing an indeterminate time after detecting an error.  When
  providing multiple checkers, if one checker detects any error, subsequent
  checkers may not run.
\item \<-processorpath> Indicates where to search for the
  checker; should also contain any qualifiers used by the Subtyping
  Checker; see Section~\ref{subtyping-example}
\item \<-proc:>\{\<none>,\<only>\} Controls whether checking
  happens; \<-proc:none>
  means to skip checking; \<-proc:only> means to do only
  checking, without any subsequent compilation; see
  Section~\ref{checker-auto-discovery}
\item \<-implicit:class> Suppresses warnings about implicitly compiled files
  (not named on the command line); see Section~\ref{ant-task}
\item \<-J> Supply an argument to the JVM that is running javac;
  for example, \<-J-Xmx2500m> to increase its maximum heap size
\item \<-doe> To ``dump on error'', that is, output a stack trace
  whenever a compiler warning/error is produced. Useful when debugging
  the compiler or a checker.
\end{itemize}

The Checker Framework does not support \<-source 1.7> or earlier.  You must
supply \<-source 1.8> or later, or no \<-source> command-line argument,
when running \<javac>.


\subsectionAndLabel{Checker auto-discovery}{checker-auto-discovery}

``Auto-discovery'' makes the \code{javac} compiler always run a checker
plugin, even if you do not explicitly pass the \code{-processor}
command-line option.  This can make your command line shorter, and ensures
that your code is checked even if you forget the command-line option.

\begin{sloppypar}
To enable auto-discovery, place a configuration file named
\code{META-INF/services/javax.annotation.processing.Processor}
in your classpath.  The file contains the names of the checker plugins to
be used, listed one per line.  For instance, to run the Nullness Checker and the
Interning Checker automatically, the configuration file should contain:
\end{sloppypar}

%BEGIN LATEX
\begin{smaller}
%END LATEX
\begin{Verbatim}
  org.checkerframework.checker.nullness.NullnessChecker
  org.checkerframework.checker.interning.InterningChecker
\end{Verbatim}
%BEGIN LATEX
\end{smaller}
%END LATEX

You can disable this auto-discovery mechanism by passing the
\code{-proc:none} command-line option to \<javac>, which disables all
annotation processing including all pluggable type-checking.

%% Auto-discovering all the distributed checkers by default would be
%% problematic:  the nullness and mutability checkers would issue lots of
%% errors for unannotated code, and that would be irritating.  So, leave it
%% up to the user to enable auto-discovery.  1.

\subsectionAndLabel{Shorthand for built-in checkers}{shorthand-for-checkers}

% TODO: this feature only works for our javac script, not when using
% the standard javac. Should this be explained?

Ordinarily, javac's \code{-processor} flag requires fully-qualified class names.
When running a built-in checker, you may
omit the package name and the \<Checker> suffix.
The following three commands are equivalent:

\begin{alltt}
  javac -processor \textbf{org.checkerframework.checker.nullness.NullnessChecker} MyFile.java
  javac -processor \textbf{NullnessChecker} MyFile.java
  javac -processor \textbf{nullness} MyFile.java
\end{alltt}

This feature also works when multiple checkers are specified.
Their names are separated by commas, with no surrounding space.
For example:

\begin{alltt}
  javac -processor NullnessChecker,RegexChecker MyFile.java
  javac -processor nullness,regex MyFile.java
\end{alltt}

This feature does not apply to Javac \href{https://docs.oracle.com/javase/7/docs/technotes/tools/windows/javac.html#commandlineargfile}{@argfiles}.


\sectionAndLabel{What the checker guarantees}{checker-guarantees}

A checker can guarantee that a particular property holds throughout the
code.  For example, the Nullness Checker (Chapter~\ref{nullness-checker})
guarantees that every expression whose type is a \refqualclass{checker/nullness/qual}{NonNull} type never
evaluates to null.  The Interning Checker (Chapter~\ref{interning-checker})
guarantees that every expression whose type is an \refqualclass{checker/interning/qual}{Interned} type
evaluates to an interned value.  The checker makes its guarantee by
examining every part of your program and verifying that no part of the
program violates the guarantee.

There are some limitations to the guarantee.


\begin{itemize}

\item
  A compiler plugin can check only those parts of your program that you run
  it on.  If you compile some parts of your program without running the
  checker, then there is no guarantee that the entire program satisfies the
  property being checked.  Some examples of un-checked code are:

  \begin{itemize}
  \item
    Code compiled without the \code{-processor} switch, including any
    external library supplied as a \code{.class} file.
  \item
    Code compiled with the \code{-AskipUses}, \code{-AonlyUses}, \code{-AskipDefs} or \code{-AonlyDefs}
    properties (see Chapter~\ref{suppressing-warnings}).
  \item
    Suppression of warnings, such as via the \code{@SuppressWarnings}
    annotation (see Chapter~\ref{suppressing-warnings}).
  \item
    Native methods (because the implementation is not Java code, it cannot
    be checked).
  \end{itemize}

  In each of these cases, any \emph{use} of the code is checked --- for
  example, a call to a native method must be compatible with any
  annotations on the native method's signature.
  However, the annotations on the un-checked code are trusted; there is no
  verification that the implementation of the native method satisfies the
  annotations.

\item
  The Checker Framework is, by default, unsound in a few places where a
  conservative analysis would issue too many false positive warnings.
  These are listed in Section~\ref{unsound-by-default}.
  You can supply a command-line argument to make the Checker Framework
  sound for each of these cases.

%% This isn't an unsoundness in the Checker Framework:  for any type system
%% that does not include a conservative library annotation for
%% Method.invoke, it is a bug in that particular type-checker.
% \item
%   Reflection can violate the Java type system, and
%   the checkers are not sophisticated enough to reason about the possible
%   effects of reflection.  Similarly, deserialization and cloning can
%   create objects that could not result from normal constructor calls, and
%   that therefore may violate the property being checked.

\item
  Specific checkers may have other limitations; see their documentation for
  details.

\end{itemize}

A checker can be useful in finding bugs or in verifying part of a
program, even if the checker is unable to verify the correctness of an
entire program.

In order to avoid a flood of unhelpful warnings, many of the checkers avoid
issuing the same warning multiple times.  For example, in this code:

\begin{Verbatim}
  @Nullable Object x = ...;
  x.toString();                 // warning
  x.toString();                 // no warning
\end{Verbatim}

\noindent
In this case, the second call to \<toString> cannot possibly throw a null
pointer warning --- \<x> is non-null if control flows to the second
statement.
In other cases, a checker avoids issuing later warnings with the same cause
even when later code in a method might also fail.
This does not
affect the soundness guarantee, but a user may need to examine more
warnings after fixing the first ones identified.  (More often, at least in
our experience to date, a single fix corrects all the warnings.)

% It might be worthwhile to permit a user to see every warning --- though I
% would not advocate this setting for daily use.

If you find that a checker fails to issue a warning that it
should, then please report a bug (see Section~\ref{reporting-bugs}).


\sectionAndLabel{Tips about writing annotations}{tips-about-writing-annotations}

Section~\ref{library-tips} gives additional tips that are
specific to annotating a third-party library.


\subsectionAndLabel{Write annotations before you run a checker}{annotate-before-checking}

Before you run a checker, annotate the code, based on its documentation.
Then, run the checker to uncover bugs in the code or the documentation.

Don't do the opposite, which is to run the checker and then add annotations
according to the warnings issued.  This approach is less systematic, so you
may overlook some annotations.  It often leads to confusion and poor
results.  It leads users to make changes not for any principled reason, but
to ``make the type-checker happy'', even when the changes are in conflict
with the documentation or the code.  Also see ``Annotations
are a specification'', below.


\subsectionAndLabel{How to get started annotating legacy code}{get-started-with-legacy-code}

Annotating an entire existing program may seem like a daunting task.  But,
if you approach it systematically and do a little bit at a time, you will
find that it is manageable.

\subsubsectionAndLabel{Start small}{get-started-start-small}

Start small.  Focus on one specific property that matters to you; in
other words, run just one checker rather than multiple ones.  You may
choose a different checker for different programs.
Focus on
the most mission-critical or error-prone part of your code; don't try to
annotate your whole program at first.

It is easiest to add annotations if you know the code or the
code contains documentation; you will find that you spend most of your time
understanding the code, and very little time actually writing annotations
or running the checker.

When annotating, be systematic; we recommend
annotating an entire class at a time (not just some of the methods)
so that you don't lose track of your work or redo work.  For example,
working class-by-class avoids confusion about whether an unannotated type
means you determined that the default is desirable, or it means you didn't
yet examine that type.
You may find it helpful to start annotating the leaves of the call tree ---
that is,
start with methods/classes/packages that have few dependencies on other
code or, equivalently, start with code that a lot of your other code
depends on.  For example, within a package annotate supertypes before you
annotated classes that extend or implement them.
The reason for this rule is that it is
easiest to annotate a class if the code it depends on has already been
annotated.

Don't overuse pluggable type-checking.  If the regular Java type system can
verify a property using Java subclasses, then that is a better choice than
pluggable type-checking (see Section~\ref{faq-typequals-vs-subtypes}).


\subsubsectionAndLabel{Annotations are a specification}{get-started-annotations-are-a-specification}

When you write annotations, you are writing a specification, and you should
think about them that way.  Start out by understanding the program so that
you can write an accurate specification.
Sections~\ref{annotate-normal-behavior}
and~\ref{annotations-are-a-contract} give more tips about writing
specifications.

For each class, read its Javadoc.  For instance, if you are adding
annotations for the Nullness Checker (Section~\ref{nullness-checker}), then
you can search the documentation for ``null'' and then add \<@Nullable>
anywhere appropriate.  For now, just annotate signatures and fields; there is no
need to annotate method bodies.  The only reason to even
\emph{read} the method bodies yet is to determine signature annotations for
undocumented methods ---
for example, if the method returns null, you know its return type should be
annotated \<@Nullable>, and a parameter that is compared against \<null>
may need to be annotated \<@Nullable>.

After you have annotated all the signatures, run the checker.
Then, fix bugs in code and add/modify annotations as necessary.
% If signature annotations are necessary, then you may want
% to fix the documentation that did not indicate the property; but this isn't
% strictly necessary, since the annotations that you wrote provide that
% documentation.
Don't get discouraged if you see many type-checker warnings at first.
Often, adding just a few missing annotations will eliminate many warnings,
and you'll be surprised how fast the process goes overall.

You may wonder about the effect of adding a given annotation (that is, of
changing the specification for a given method or class):  how many
other specification changes (added annotations) will it require, and will
it conflict with other code?  It's best to reason about the desired design,
but you can also do an experiment.
Suppose you are considering adding an annotation to a method parameter.
One approach is to manually examine all callees.
A more automated approach is to save the checker
output before adding the annotation, and to compare it to the checker
output after adding the annotation.  This helps you to focus on the
specific consequences of your change.

Chapter~\ref{annotating-libraries} tells you how to annotate libraries that
your code uses.  Section~\ref{handling-warnings} and
Chapter~\ref{suppressing-warnings} tell you what to do when you are unable
to eliminate checker warnings by adding annotations.


\subsubsectionAndLabel{Write good code}{get-started-write-good-code}

Avoid complex code, which is more error-prone.  If you write your code to
be simple and clean enough for the type-checker to verify, then it will
also be easier for programmers to understand.

Your code should compile cleanly under the regular Java compiler.  If you
are not willing to write code that type-checks in Java, then there is
little point in using an even more powerful, restrictive type system.  As a
specific example, your code should not use raw types like \code{List}; use
parameterized types like \code{List<String>} instead
(Section~\ref{generics-raw-types}).

Do not write unnecessary annotations.
\begin{itemize}
\item
  Do not annotate local variables unless necessary.  The checker infers
  annotations for local variables (see Section~\ref{type-refinement}).
  Usually, you only need to annotate fields and method signatures.  You
  should add annotations inside method bodies only if the checker is unable
  to infer the correct annotation (usually on type arguments or array
  element types, rather than
  on top-level types).
  % or if
  % you need to suppress a warning (see Chapter~\ref{suppressing-warnings}).

\item
  Do not write annotations that are redundant with defaults.  For example,
  when checking nullness (\chapterpageref{nullness-checker}), the default
  annotation is \<@NonNull>, in most locations other than some type bounds
  (Section~\ref{climb-to-top}).  When you are starting out, it might seem
  helpful to write redundant annotations as a reminder, but that's like
  when beginning programmers write a comment about every simple piece of
  code:

\begin{Verbatim}
// The below code increments variable i by adding 1 to it.
i++;
\end{Verbatim}

  As you become comfortable with pluggable type-checking, you will find
  redundant annotations to be distracting clutter, so avoid putting them in
  your code in the first place.

\item
  Avoid writing \<@SuppressWarnings> annotations unless there is no
  alternative.  It is tempting to think that your code is right and the
  checker's warnings are false positives.  Sometimes they are, but slow
  down and convince yourself of that before you dismiss them.
  Section~\ref{handling-warnings} discusses what to do when a checker
  issues a warning about your code.

\end{itemize}


\subsectionAndLabel{Annotations indicate non-exceptional behavior}{annotate-normal-behavior}

You should use annotations to specify \emph{normal} behavior.  The
annotations indicate all the values that you \emph{want} to flow to a
reference --- not every value that might possibly flow there if your
program has a bug.

As an example, the goal of the Nullness Checker is to guarantee that your
program does not crash due to a null value.  In a method like this:

\begin{Verbatim}
  /** @throws IllegalArgumentException if arg is null */
  void m(Object arg) {
    if (arg == null) {
      throw new IllegalArgumentException();
    }
    ...
  }
\end{Verbatim}

\noindent
the program crashes if \<null> is passed.  Therefore, the type of \<arg>
should be \<@NonNull Object> (which you can write as just \<Object> due to
defaulting).  The Nullness Checker (\chapterpageref{nullness-checker})
will warn whenever a client passes a
value that might cause m to crash.  If you wrote the type of the formal
parameter as \<@Nullable Object>, the Nullness Checker would permit clients
to make calls that lead to a crash.


Many methods are guaranteed to throw an exception if they are passed \code{null}
as an argument.  Examples include

\begin{Verbatim}
  java.lang.Double.valueOf(String)
  java.lang.String.contains(CharSequence)
  org.junit.Assert.assertNotNull(Object)
  com.google.common.base.Preconditions.checkNotNull(Object)
\end{Verbatim}

\refqualclass{checker/nullness/qual}{Nullable} (see Section~\ref{nullness-annotations})
might seem like a reasonable annotation for the parameter,
for two reasons.  First, \code{null} is a legal argument with a
well-defined semantics:  throw an exception.  Second, \code{@Nullable}
describes a possible program execution:  it might be possible for
\code{null} to flow there, if your program has a bug.

% (Checking for such a bug is the whole purpose of the \code{assertNotNull}
% and \code{checkNotNull} methods.)

However, it is never useful for a programmer to pass \code{null}.  It is
the programmer's intention that \code{null} never flows there.  If
\code{null} does flow there, the program will not continue normally
(whether or not it throws a NullPointerException).

Therefore, you should specify such parameters as
\refqualclass{checker/nullness/qual}{NonNull}, indicating
the intended use of the method.  When you specify the parameter as the \code{@NonNull}
annotation, the checker is able to issue compile-time warnings about
possible run-time exceptions, which is its purpose.  Specifying the parameter
as \code{@Nullable} would suppress such warnings, which is undesirable.
(Since \code{@NonNull} is the default, you don't have to write anything in
the source code to specify the parameter as non-null.  You are allowed to
write a redundant \code{@NonNull} annotation, but it is discouraged.)

% This is only an issue for code with unchecked, trusted annotations such as
% library methods; if the method is type-checked, then the type-checker
% warnings will lead you to leave the formal parameter as the default, which
% means \<@NonNull>.
If a method can possibly throw an exception because its parameter
is \<null>, then that parameter's type should be \<@NonNull>, which
guarantees that the type-checker will issue a warning for every client
use that has the potential to cause an exception.  Don't write
\<@Nullable> on the parameter just because there exist some executions that
don't necessarily throw an exception.

% (The note at
% http://google-collections.googlecode.com/svn/trunk/javadoc/com/google/common/base/Preconditions.html
% argues that the parameter could be marked as @Nullable, since it is
% possible for null to flow there at run time.  However, since that is an
% erroneous case, the annotation would be counterproductive rather than
% useful.)

Another example is the Optional Checker (\chapterpageref{optional-checker})
and the \<orElseThrow> method.
The goal of the Optional Checker is to ensure that the program does not
crash due to use of a non-present Optional value.  Therefore, the receiver
of
\sunjavadoc{java.base/java/util/Optional.html\#orElseThrow()}{orElseThrow} is annotated as
\ahref{https://checkerframework.org/api/org/checkerframework/checker/optional/qual/Present.html}{\<@Present>},
and the optional Checker issues a warning if the client calls
\<orElseThrow> on a \<@MaybePresent> value.


\subsectionAndLabel{Subclasses must respect superclass annotations}{annotations-are-a-contract}

An annotation indicates a guarantee that a client can depend upon.  A subclass
is not permitted to \emph{weaken} the contract; for example,
if a method accepts \code{null} as an argument, then every overriding
definition must also accept \code{null}.
A subclass is permitted to \emph{strengthen} the contract; for example,
if a method does \emph{not} accept \code{null} as an argument, then an
overriding definition is permitted to accept \code{null}.

\begin{sloppypar}
As a bad example, consider an erroneous \code{@Nullable} annotation in
\href{https://github.com/google/guava/blob/master/guava/src/com/google/common/collect/Multiset.java\#L129}{\code{com/google/common/collect/Multiset.java}}:
\end{sloppypar}

\begin{Verbatim}
101  public interface Multiset<E> extends Collection<E> {
...
122    /**
123     * Adds a number of occurrences of an element to this multiset.
...
129     * @param element the element to add occurrences of; may be {@code null} only
130     *     if explicitly allowed by the implementation
...
137     * @throws NullPointerException if {@code element} is null and this
138     *     implementation does not permit null elements. Note that if {@code
139     *     occurrences} is zero, the implementation may opt to return normally.
140     */
141    int add(@Nullable E element, int occurrences);
\end{Verbatim}

There exist implementations of Multiset that permit \code{null} elements,
and implementations of Multiset that do not permit \code{null} elements.  A
client with a variable \code{Multiset ms} does not know which variety of
Multiset \code{ms} refers to.  However, the \code{@Nullable} annotation
promises that \code{ms.add(null, 1)} is permissible.  (Recall from
Section~\ref{annotate-normal-behavior} that annotations should indicate
normal behavior.)

If parameter \code{element} on line 141 were to be annotated, the correct
annotation would be \code{@NonNull}.  Suppose a client has a reference to
same Multiset \code{ms}.  The only way the client can be sure not to throw an exception is to pass
only non-\code{null} elements to \code{ms.add()}.  A particular class
that implements Multiset could declare \code{add} to take a
\code{@Nullable} parameter.  That still satisfies the original contract.
It strengthens the contract by promising even more:  a client with such a
reference can pass any non-\code{null} value to \code{add()}, and may also
pass \code{null}.

\textbf{However}, the best annotation for line 141 is no annotation at all.
The reason is that each implementation of the Multiset interface should
specify its own nullness properties when it specifies the type parameter
for Multiset.  For example, two clients could be written as

\begin{Verbatim}
  class MyNullPermittingMultiset implements Multiset<@Nullable Object> { ... }
  class MyNullProhibitingMultiset implements Multiset<@NonNull Object> { ... }
\end{Verbatim}

\noindent
or, more generally, as

\begin{Verbatim}
  class MyNullPermittingMultiset<E extends @Nullable Object> implements Multiset<E> { ... }
  class MyNullProhibitingMultiset<E extends @NonNull Object> implements Multiset<E> { ... }
\end{Verbatim}

Then, the specification is more informative, and the Checker Framework is
able to do more precise checking, than if line 141 has an annotation.

It is a pleasant feature of the Checker Framework that in many cases, no
annotations at all are needed on type parameters such as \code{E} in \<MultiSet>.


\subsectionAndLabel{What to do if a checker issues a warning about your code}{handling-warnings}

When you run a type-checker on your code, it is likely to issue warnings or
errors.  Don't panic!  There are three general causes for the warnings:

\begin{itemize}
\item
  There is a bug in your code, such as a possible null dereference.  Fix
  your code to prevent that crash.

\item
  The annotations are too strong (they are incorrect) or too weak (they
  are imprecise).  Improve the
  annotations, usually by writing more annotations in order to better
  express the specification.
  Only write annotations that accurately describe the intended behavior of
  the software --- don't write inaccurate annotations just for the purpose
  of eliminating type-checker warnings.

  Usually you need to improve the annotations in your source code.
  Sometimes you need to improve annotations in a library that your program
  uses (see \chapterpageref{annotating-libraries}).

\item
  There is a weakness in the type-checker.  Your code is safe --- it never
  suffers the error at run time --- but the checker cannot prove this fact.
  If possible, rewrite your code to be simpler for the checker to analyze;
  this is likely to make it easier for people to understand, too.
  If that is not possible, suppress the warning (see
  Chapter~\ref{suppressing-warnings}); be sure to include a code
  comment explaining how you know the code is correct even though the
  type-checker cannot deduce that fact.

  (Do not add an \<if> test that can never fail, just to suppress a
  warning.  Adding a gratuitous \<if> clutters the code and confuses
  readers, who will assume that every \<if> condition can evaluate to true
  or false.  It can be acceptable to add an \<if> test that throws a
  descriptive error message.)
\end{itemize}

For each warning issued by the checker, you need to determine which of the
above categories it falls into.  Here is an effective methodology to do so.
It relies mostly on manual code examination, but you may also find it
useful to write test cases for your code or do other kinds of analysis, to
verify your reasoning.

\begin{enumerate}
\item
  Write an explanation of why your code is correct and it
  never suffers the error at run time.  In other words, this is an English proof
  that the type-checker's warning is incorrect.

  Don't skip any steps in your proof.
  (For example, don't write an unsubstantiated claim such as ``\<x> is
  non-null here''; instead, give a justification.)
  Don't let your reasoning rely on
  facts that you do not write down explicitly.  For example, remember that
  calling a method might change the values of object fields; your proof
  might need to state that certain methods have no side effects.

  If you cannot write a proof, then there is a bug
  in your code (you should fix the bug) or your code is too complex for you
  to understand (you should improve its documentation and/or design).

\item
  Translate the proof into annotations.  Here are some examples.

  \begin{itemize}
  \item
    If your proof includes ``variable \<x> is never \<null>
    at run time'', then annotate <x>'s type with
    \refqualclass{checker/nullness/qual}{NonNull}.
  \item
    If your proof
    includes ``method \<foo> always returns a legal regular expression'',
    then annotate \<foo>'s return type with
    \refqualclass{checker/regex/qual}{Regex}.
  \item
    If your proof includes ``if method \<join>'s first argument is
    non-null, then \<join> returns a non-null result'', then annotate
    \<join>'s first parameter and return type with
    \refqualclass{checker/nullness/qual}{PolyNull}.
  \item
    If your proof includes ``method \<processOptions> has already been called and it
    set field \<tz1>'', then annotate \<processOptions>'s declaration with
    \refqualclasswithparams{checker/nullness/qual}{EnsuresNonNull}{"tz1"}.
  \item
    If your proof includes ``method \<isEmpty> returned false, so its
    argument must have been non-null'', then annotate \<isEmpty>'s
    declaration with
    \refqualclasswithparams{checker/nullness/qual}{EnsuresNonNullIf}{expression="\#1",result=false}.
  \end{itemize}
  All of these are examples of correcting weaknesses in the annotations you wrote.
  The Checker Framework provides many other powerful annotations; you may
  be surprised how many proofs you can express in annotations.
  If you need to annotate a method that is defined in a
  library that your code uses, see \chapterpageref{annotating-libraries},
  Annotating Libraries.

  If there are complex facts in your proof that cannot be expressed as
  annotations, then that is a weakness in the type-checker.  For example,
  the Nullness Checker cannot express ``in list \<lst>, elements stored at
  even indices are always non-\<null>, but elements stored at odd elements
  might be \<null>.''  In this case, you have two choices.
  %
  First, you can suppress the warning
  (\chapterpageref{suppressing-warnings}); be sure to write a comment
  explaining your reasoning for suppressing the warning.  You may wish to
  submit a feature request (Section~\ref{reporting-bugs}) asking for
  annotations that handle your use case.
  %
  Second, you can rewrite the code to make the proof simpler;
  in the above example, it might be better to use a list of pairs
  rather than a heterogeneous list.

\item
  At this point, all the steps in your proof have been formalized as
  annotations.  Re-run the checker and repeat the process for any new or
  remaining warnings.

  If every step of your proof can be expressed in annotations, but the
  checker cannot make one of the deductions (it cannot follow one of the
  steps), then that is a weakness in the type-checker.  First, double-check
  your reasoning.  Then, suppress the warning, along with a comment
  explaining your reasoning (\chapterpageref{suppressing-warnings}).
  The comment is an excerpt from your English proof, and the proof guides
  you to the best place to suppress the warning.
  Finally, please submit a bug report so that the checker can be improved
  in the future (Section~\ref{reporting-bugs}).

\end{enumerate}

If you have trouble understanding a Checker Framework warning message, you
can search for its text in this manual.  Also see
Section~\ref{common-problems-typechecking} and
Chapter~\ref{troubleshooting}, Troubleshooting.
In particular, Section~\ref{common-problems-typechecking} explains this
same methodology in different words.


% LocalWords:  NonNull zipfile processor classfiles annotationname javac htoc
% LocalWords:  SuppressWarnings un skipUses java plugins plugin TODO cp io
% LocalWords:  nonnull langtools sourcepath classpath OpenJDK pre jsr lst
% LocalWords:  Djsr qual Alint javac's dotequals nullable supertype JLS Papi
% LocalWords:  deserialization Mahmood Telmo Correa changelog txt nullness ESC
% LocalWords:  Nullness unselect checkbox unsetting PolyNull typedefs arg
% LocalWords:  bashrc IDE xml buildfile PolymorphicQualifier enum API elts INF
% LocalWords:  type-checker proc discoverable Xlint util QualifierDefaults Foo
% LocalWords:  DefaultQualifier SoyLatte GetStarted Formatter bcel csv
% LocalWords:  Dcheckers Warski MyClass ProcessorName compareTo toString myDate
% LocalWords:  int XDTA newdir Awarns signedness urgin bytecodes gradle
% LocalWords:  subpackages bak tIDE Multiset NullPointerException AskipUses
% LocalWords:  html JCIP MultiSet Astubs Afilenames Anomsgtext Ashowchecks tex
% LocalWords:  Aquals processorpath regex RegEx Xmaxwarns Xbootclasspath com
% LocalWords:  IntelliJ assertNotNull checkNotNull Goetz antipattern subclassed
% LocalWords:  callees Xmx unconfuse fenum propkey forName jsr308 Djsr308
% LocalWords:  bootclasspath AonlyUses AskipDefs AonlyDefs AcheckPurityAnnotations
% LocalWords:  AsuppressWarnings AassumeSideEffectFree Adetailedmsgtext
% LocalWords:  AignoreRawTypeArguments AsuggestPureMethods ApermitMissingJdk
% LocalWords:  AassumeAssertionsAreEnabled AassumeAssertionsAreDisabled
% LocalWords:  AconcurrentSemantics AstubWarnIfNotFound AnoPrintErrorStack
% LocalWords:  AprintAllQualifiers Aignorejdkastub AstubDebug Aflowdotdir
% LocalWords:  AresourceStats jls r78 JDKs i18n AignoreRangeOverflow L129
% LocalWords:  AinvariantArrays AcheckCastElementType formatter pathname
% LocalWords:  typedef guieffect Gradle jdk8 javadoc MyFile argfiles tz1
% LocalWords:  AshowSuppressWarningKeys AoutputArgsToFile RegexChecker
% LocalWords:  NullnessChecker commandlineargfile AnnotatedFor Xmx2500m
% LocalWords:  AsafeDefaultsForUnannotatedBytecode Signedness Werror
% LocalWords:  AuseSafeDefaultsForUnannotatedSourceCode beingConstructed
% LocalWords:  AuseDefaultsForUncheckedCode AresolveReflection Ainfer
% LocalWords:  AconservativeUninferredTypeArguments Averbosecfg Acfgviz
% LocalWords:  AstubWarnIfOverwritesBytecode AprintVerboseGenerics
% LocalWords:  AatfDoNotCache AatfCacheSize IntRange AwarnIfNotFound
% LocalWords:  AwarnUnneededSuppressions AshowInferenceSteps BHCJEIBB
% LocalWords:  AstubWarnIfNotFoundIgnoresClasses processOptions getopt
% LocalWords:  EnsuresNonNull EnsuresNonNullIf checkername orElseThrow
% LocalWords:  ArequirePrefixInWarningSuppressions MaybePresent
% LocalWords:  AignoreInvalidAnnotationLocations AprintGitProperties
% LocalWords:  AstubWarnIfRedundantWithBytecode