introduction.tex

\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 compile-time 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}
% If you update this list, also update the list in advanced-features.tex .

\item
  \ahrefloc{nullness-checker}{Nullness Checker} for null pointer errors
  (see \chapterpageref{nullness-checker})
\item
  \ahrefloc{initialization-checker}{Initialization Checker} to ensure all
  \<@NonNull> 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{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{called-methods-checker}{Called Methods Checker} for
  the builder pattern (see \chapterpageref{called-methods-checker})
\item
  \ahrefloc{resource-leak-checker}{Resource Leak Checker} for ensuring that resources are disposed of properly
  (see \chapterpageref{resource-leak-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{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{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{initialized-fields-checker}{Initialized Fields Checker} to ensure all
  fields are set in the constructor (see
  \chapterpageref{initialization-checker})
\item
  \ahrefloc{aliasing-checker}{Aliasing Checker} to identify whether
  expressions have aliases (see \chapterpageref{aliasing-checker})
\item
  \ahrefloc{must-call-checker}{Must Call Checker} to over-approximate the
  methods that should be called on an object before it is de-allocated (see \chapterpageref{must-call-checker})
\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}

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
define new type systems and run them 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 part of
your program, or the whole thing.  Type inference tools exist to help you annotate your
code; see Section~\ref{type-inference}.

Most programmers will use type systems created by other people, such as
those listed at the start of the introduction (\chapterpageref{introduction}).
Some people, called ``type system designers'', create new type systems
(\chapterpageref{creating-a-checker}).
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 document uses the terms ``checker'' and ``type-checking compiler
plugin'' 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}, \textbf{JDK 11}, or \textbf{JDK 17} installed.
% Possible replacement for the above.
% You must have a supported LTS JDK installed: \textbf{JDK 8}, \textbf{JDK
% 11}, or \textbf{JDK 17}.
The Checker Framework processes code written for any of those versions.
(For running the Checker Framework under other JDK versions, see
Section~\ref{permitUnsupportedJdkVersion}.)

The installation process 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.18.1-eisop1.zip}

\item
  Unzip it to create a \code{checker-framework-\ReleaseVersion{}} 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}

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 demonstrates the Nullness, Regex, and Tainting Checkers.

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

\label{version-number}
The Checker Framework is released on a monthly schedule.  The minor version
(the middle number in the version number) is incremented if there are any
incompatibilities
% Sometimes, we permit trivial incompatibilities, or ones that are unlikely
% to affect users, without changing the minor version.
with the previous version, including in user-visible
behavior or in methods that a checker implementation might call.


\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 you can work along with.

  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}

If you run the Nullness Checker (Chapter~\ref{nullness-checker}), the
compilation completes without any errors.

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

If you run the Nullness Checker again, it emits
  the following error:
\begin{Verbatim}
GetStarted.java:5: incompatible types.
found   : @Nullable <nulltype>
required: @NonNull Object
        @NonNull Object ref = null;
                              ^
1 error
\end{Verbatim}

This is a trivially simple example.  Even an unsound bug-finding tool like
SpotBugs or Error Prone could have detected this bug.  The
Checker Framework's analysis is more powerful than those tools and detects
more code defects than they do.

Type qualifiers such as \<@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 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 infer
  annotations that are consistent with their code:  see Section~\ref{type-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{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}


There is a
\ahreforurl{https://checkerframework.org/tutorial/}{tutorial}
that walks you through using the Checker Framework on the
command line.

% 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{Where to write type annotations}{writing-annotations}

You may write a type annotation 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 type 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}.

The Java Language Specification also defines
declaration annotations, such as \<@Deprecated> and \<@Override>, which apply
to a class, method, or field but do not apply to the method's return type
or the field's type.  They should be written on their own line in the
source code, before the method's signature.


\sectionAndLabel{Running a checker}{running}

To run a checker, 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}.
(If your project already uses auto-discovery for some annotation processor,
such as AutoValue, then you should use auto-discovery.)
Two concretes example of using \code{-processor} to run the Nullness Checker are

\begin{Verbatim}
  javac -processor nullness MyFile.java
  javac -processor org.checkerframework.checker.nullness.NullnessChecker 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}),
Maven (Section~\ref{maven}), and
sbt (Section~\ref{sbt});
IDEs such as
Eclipse (Section~\ref{eclipse}),
IntelliJ IDEA (Section~\ref{intellij}),
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 and those
created by another annotation processor.  It may also include other of
your Java files, if they are more recent than the corresponding \code{.class} file.
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.
Type-checking works modularly and intraprocedurally:  when verifying a
method, it examines only the signature (including annotations) of other
methods, not their implementations.  When analyzing a variable use, it
relies on the type of the variable, not any dataflow outside the current
method that produced the value.

After you compile your code while running a checker, the resulting
\<.class> and \<.jar> files can be used for pluggable type-checking of client code.

If you compile code without the \code{-processor}
command-line option, 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, to create
\<.class> files that will be distributed or compiled against, you should run the
type-checkers for all the annotations that you 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 or
in a stub file.

Some projects are already distributed with type annotations by their
maintainers, so you do not need to do anything special.
An example is all the libraries in \url{https://github.com/plume-lib/}.
Over time, this should become more common.

For some other libraries, the Checker Framework developers have provided an
annotated version of the library, either as a stub file or as compiled class files.
(If some library is not available in either of these forms,
you can contribute by annotating it, which will
help you and all other Checker Framework users; see
\chapterpageref{annotating-libraries}.)

Some stub files are used automatically by a checker, without any action on
your part.  For others, you must pass the \<-Astubs=...> command-line argument.
As a special case, if an \<.astub> file appears in
\<checker/resources/>, then pass the command-line option
use \<-Astubs=checker.jar/\emph{stubfilename.astub}>.
The ``\<checker.jar>'' should be literal --- don't provide a path.
This special syntax only works for ``\<checker.jar>''.
%% There aren't any such libraries at the moment.
% (Examples of such libraries are:
% % This list appears here to make it searchable/discoverable.
% ...
% .)

The annotated libraries that are provided as class files appear in
\ahref{https://search.maven.org/search?q=org.checkerframework.annotatedlib}{the
  \<org.checkerframework.annotatedlib> group in the Maven Central Repository}.
The annotated library has \emph{identical} behavior to the upstream,
unannotated version; the source code is identical other than added
annotations.
%
(Some of the annotated libraries are
% This list appears here to make it searchable/discoverable.
bcel,
commons-csv,
commons-io,
guava,
and
java-getopt.)

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 Maven 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.8'
\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.8.0.1'
\end{Verbatim}

\noindent
Usually 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 is one special case.  If an \<.astub> file is shipped with the
Checker Framework in \<checker/resources/>, then you can
use \<-Astubs=checker.jar/\emph{stubfilename.astub}>.
The ``\<checker.jar>'' should be literal --- don't provide a path.
(This special syntax only works for ``\<checker.jar>''.)


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

To pass an option to only a particular checker,
prefix the option with the canonical or simple name
of a checker, followed by an underscore ``\<\_>''.
Such an option will apply only to a checker with that name or any subclass of that checker.
For example, you can use
\begin{Verbatim}
    -ANullnessChecker_lint=redundantNullComparison
    -Aorg.checkerframework.checker.guieffect.GuiEffectChecker_lint=debugSpew
\end{Verbatim}

\noindent
to pass different lint options to the Nullness and GUI Effect Checkers.  A
downside is that, in this example, the Nullness Checker will issue a
``The following options were not recognized by any processor'' warning
about the second option and the GUI Effect Checker will issue a
``The following options were not recognized by any processor'' warning
about the first option.

% 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 \<-AuseConservativeDefaultsForUncheckedCode>
  Enables conservative defaults, and suppresses all type-checking warnings,
  in unchecked code.  Takes arguments ``source,bytecode''.
  ``-source,-bytecode'' is the (unsound) default setting.
  \begin{itemize}
  \item
  ``bytecode'' specifies
  whether the checker should apply conservative defaults to
  bytecode (that is, to already-compiled libraries); see
  Section~\ref{defaults-classfile}.
  \item
  Outside the scope of any relevant
  \refqualclass{framework/qual}{AnnotatedFor} annotation, ``source'' specifies whether conservative
  default annotations are applied to source code and suppress all type-checking warnings; see
  Section~\ref{compiling-libraries}.
  \end{itemize}
\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}.
\item \<-processor org.checkerframework.common.initializedfields.InitializedFieldsChecker,...>
  Ensure that all fields are initialized by the constructor.  See
  \chapterpageref{initialized-fields-checker}.
\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 on that information; see
  Chapter~\ref{reflection-resolution}.  \<-AresolveReflection=debug> causes
  debugging information to be output.
\item \<-Ainfer=\emph{outputformat}>
  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}.
  Using \<-Ainfer=jaifs> produces \<.jaif> files.
  Using \<-Ainfer=stubs> produces \<.astub> files.
  Using \<-Ainfer=ajava> produces \<.ajava> files.
  You must also supply \<-Awarns>, or the inference output may be incomplete.
\item \<-AshowSuppressWarningsStrings>
  With each warning, show all possible strings to suppress that warning.
\item \<-AwarnUnneededSuppressions>
  Issue a warning if a \<@SuppressWarnings> did not suppress a warning
  issued by the checker.  This only warns about
  \<@SuppressWarnings> strings that contain a checker name
  (Section~\ref{suppresswarnings-annotation-syntax}).  The
  \<-ArequirePrefixInWarningSuppressions> command-line argument ensures
  that all \<@SuppressWarnings> strings contain a checker name.
\item \<-AwarnUnneededSuppressionsExceptions=\emph{regex}> disables
  \<-AwarnUnneededSuppressions> for \<@SuppressWarnings> strings that
  contain a match for the regular expression.  Most users don't need this.
\item \<-ArequirePrefixInWarningSuppressions>
  Require that the string in a warning suppression annotation begin with a checker
  name.  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.
\item \<-ApermitUnsupportedJdkVersion>
  \label{permitUnsupportedJdkVersion}
  Issue a note, rather than a warning, when running the Checker Framework
  on a JDK version that the Checker Framework maintainers do not support.
  The Checker Framework seems to work on all versions of the JDK, from JDK
  8 onward.  However, in the past, Oracle has introduced JDK
  incompatibilities that caused mysterious (to users) failures.  If you
  have a problem while using this command-line argument, please do not
  report it to the Checker Framework maintainers unless you can reproduce
  the problem without this command-line argument.
\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>,
  \<-AstubWarnIfNotFoundIgnoresClasses>,
  %% Uncomment when https://tinyurl.com/cfissue/2759 is fixed.
  %  \<-AstubWarnIfOverwritesBytecode>,
  \<-AstubWarnIfRedundantWithBytecode>,
  \<-AstubWarnNote>,
  Warn about problems with stub files; see Section~\ref{stub-troubleshooting}.

\item \<-AmergeStubsWithSource>
  If both a stub file and a source file for a class are available, trust
  both and use the greatest lower bound of their annotations. The default
  behavior (without this flag) is to ignore types from the stub file if
  source is available. See Section~\ref{stub-multiple-specifications}.
  % note to maintainers: GLB of the two types was chosen to support
  % using this flag in combination with \<-Ainfer=stubs>.

% This item is repeated above:
\item \<-AuseConservativeDefaultsForUncheckedCode=source>
  Outside the scope of any relevant
  \refqualclass{framework/qual}{AnnotatedFor} annotation, use conservative
  default annotations and suppress all type-checking warnings; see
  Section~\ref{compiling-libraries}.

\end{itemize}

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

\item
 \<-Adetailedmsgtext>
Format of diagnostic messages; see Section~\ref{creating-debugging-options-format}.

\item
 \<-Aignorejdkastub>,
 \<-ApermitMissingJdk>,
 \<-AparseAllJdk>,
 \<-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
 \<-Aversion>
Print the Checker Framework version.

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

\item
 \<-AnoJreVersionCheck>
Do not check the JRE version the Checker Framework is running on.
\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.  This should also contain any classes used by type-checkers,
  such as qualifiers used by the Subtyping Checker (see
  Section~\ref{subtyping-example}) and classes that define
  statically-executable methods used by the Constant Value Checker (see
  Section~\ref{constant-value-staticallyexecutable-annotation}).
\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 an
annotation processor, such as a checker
plugin without explicitly passing the \code{-processor}
command-line option.  This can make your command line shorter, and it ensures
that your code is checked even if you forget the command-line option.

If the \<javac> command line specifies any \<-processor> command-line
option, then auto-discovery is disabled.  This means that if your project
currently uses auto-discovery, you should use auto-discovery for the
Checker Framework too.

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


\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 using the Checker Framework javac wrapper (Section~\ref{javac-wrapper}), 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 guarantees two things:  type annotations reflect facts about
run-time values, and illegal operations are not performed.

For example, the Nullness Checker (Chapter~\ref{nullness-checker})
guarantees lack of null pointer exceptions (Java \<NullPointerException>).
More precisely, it guarantees
that expressions whose type is annotated with
\refqualclass{checker/nullness/qual}{NonNull} never evaluate to null,
and it forbids other expressions from being dereferenced.

As another example, the Interning Checker (Chapter~\ref{interning-checker})
guarantees that correct equality tests are performed.
More precisely, it guarantees that
every expression whose type is an \refqualclass{checker/interning/qual}{Interned} type
evaluates to an interned value, and it forbids
\<==>  on other expressions.

The guarantee holds only if you run the checker on every part of your
program and the checker issues no warnings anywhere in the code.
You can also verify just part of your program.

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.  This includes
    external libraries supplied as a \code{.class} file and native methods
    (because the implementation is not Java code, it cannot be checked).
  \item
    Code compiled with the \code{-AskipUses}, \code{-AonlyUses}, \code{-AskipDefs} or \code{-AonlyDefs}
    command-line arguments (see Chapter~\ref{suppressing-warnings}).
  \item
    Dynamically generated code, such as generated by Spring or MyBatis.
    Its bytecode is directly generated and run, not compiled by javac and
    not visible to the Checker Framework.
    % https://github.com/typetools/checker-framework/issues/3139
  \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
  You can suppress warnings, such as via the \code{@SuppressWarnings}
  annotation (\chapterpageref{suppressing-warnings}).  If you do so
  incorrectly, the checker's guarantee no longer holds.

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

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

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

\noindent
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.  (Often,
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
\ahref{#get-started-annotations-are-a-specification}{``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.  While adding annotations, you will spend most of your time
understanding the code, and less time actually writing annotations
or running the checker.

Don't annotate the whole program, but work module by module.
Start annotating classes at the leaves of the call tree ---
that is,
start with classes/packages that have few dependencies on other
code.
Annotate supertypes before you
annotate 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.
Sections~\ref{askipuses} and~\ref{askipdefs} give ways to skip
checking of some files, directories, or packages.
Section~\ref{unannotated-code} gives advice about handling calls from
annotated code into unannotated code.

When annotating, be systematic; we recommend
annotating an entire class or module 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 use
means you determined that the default is desirable, or it means you didn't
yet examine that type use.

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.  Start by annotating signatures and fields, but not
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>.

The specification should state all facts that are relevant to callees.
When checking a method, the checker uses only the specification, not the
implementation, of other methods.  (Equivalently, type-checking is
``modular'' or ``intraprocedural''.)  When analyzing a variable use, the
checker relies on the type of the variable, not any dataflow outside the
current method that produced the value.

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 (assuming that
you understand the code, of course).

It is usually not a good idea to experiment with adding and removing
annotations in order to understand their effect.  It is better to reason
about the desired design.  However, to avoid having to manually examine all
callees, a more automated approach is to save the checker output before
changing an annotation, then compare it to the checker output after
changing the annotation.

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 clear enough for the type-checker to verify, then it will
also be easier for programmers to understand.  When you verify your code, a
side benefit is improving your code's structure.

Your code should compile cleanly under the regular Java compiler.  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}).  If you suppress Java compiler
warnings, then the Checker Framework will issue more warnings, and its
messages will be more confusing.  (Also, if you are not willing to write
code that type-checks in Java, then you might not be willing to use an even
more powerful type system.)

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.


\subsubsectionAndLabel{Methods that crash when passed certain values}{annotate-normal-behavior-always-crash}

\paragraphAndLabel{Nullness example}{annotate-normal-behavior-nullness-example}
As an example, consider the Nullness Checker.  Its goal is to guarantee that your
program does not crash due to a null value.

This method crashes if \<null> is passed to it:

\begin{Verbatim}
  /** @throws NullPointerException if arg is null */
  void m1(Object arg) {
    arg.toString();
    ...
  }
\end{Verbatim}

\noindent
Therefore, the type of \<arg>
should be \<@NonNull Object> (which you can write as just \<Object>, because
\<@NonNull> is the default).  The Nullness Checker (\chapterpageref{nullness-checker})
prevents null pointer exceptions by warning you whenever a client passes a
value that might cause \<m1> to crash.

Here is another method:

\begin{Verbatim}
  /** @throws NullPointerException if arg is null */
  void m2(Object arg) {
    Objects.requireNonNull(arg);
    ...
  }
\end{Verbatim}

Method \<m2> behaves just like \<m1> in that it throws
\<NullPointerException> if a client passes \<null>.  Therefore, their
specifications should be identical (the argument is \<@NonNull>), so the
checker will issue the same warning if a client might pass \<null>.

The same argument applies to any method that is guaranteed to throw an exception
if it receives \code{null} as an argument.  Examples include:

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

Their formal parameter type is annotated as \<@NonNull>, because otherwise the
program might crash.  Adding a call to a method like \<requireNonNull>
never prevents a crash:  your code still crashes, but with a slightly
different stack trace.  In order to prevent all exceptions in your program
caused by null pointers, you need to prevent those thrown by methods including
\<requireNonNull>.

(One might argue that the formal parameter should be annotated as
\refqualclass{checker/nullness/qual}{Nullable} because passing \code{null} has a
well-defined semantics (throw an exception) and such an execution may be
possible if your program has a bug.  However, it is never the programmer's
intent for \<null> to flow there.  Preventing such bugs is the purpose of
the Nullness Checker.)

A method like \<requireNonNull> is useless for making your code correct,
but it does have a benefit:  its stack trace may help developers to track
down the bug.  (For users, the stack trace is scary, confusing, and usually
non-actionable.)  But if you are using the Checker Framework, you can
prevent errors rather than needing extra help in debugging the ones that
occur at run time.


\paragraphAndLabel{Optional example}{annotate-normal-behavior-optional-example}
Another example is the Optional Checker (\chapterpageref{optional-checker})
and the \sunjavadoc{java.base/java/util/Optional.html\#orElseThrow()}{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
\<orElseThrow> is annotated as
\refqualclass{checker/optional/qual}{Present},
and the Optional Checker issues a warning if the client calls
\<orElseThrow> on a \refqualclass{checker/optional/qual}{MaybePresent} value.


\paragraphAndLabel{Permitting crashes in called methods}{annotate-normal-behavior-skip-libraries}
You can make a checker ignore crashes in library code (such as
\<assertNotNull()>) that occur as a result of misuse by your code.
This invalidates the checker's guarantee that your program will not crash.
(Programmers and users typically care about all crashes, no matter which
method is at the top of the call stack when the exception is thrown.)
The checker will still warn you about crashes in your own code.

\begin{itemize}
\item
  The \<-AskipUses> command-line argument (Section~\ref{askipuses}) skips
  checking all method calls to one or more classes.
\item
  A stub file (Section~\ref{stub}) can override the library's annotations,
  for one or more methods.
\item
  Don't type-check clients of the method.  For example, JUnit's
  \<assertNotNull()> is typically called only in test code; its clients are
  the tests.  If you type-check only your main program, then the annotation
  on \<assertNotNull()> is irrelevant.
\end{itemize}


\subsubsectionAndLabel{Methods that sometimes crash when passed certain values}{annotate-normal-behavior-sometimes-crash}

%% TODO: This text should be revised when @NullableWhen or @NonNullWhen is implemented.
% 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 \emph{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.)


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

%% TODO: Revise when @NullableWhen or @NonNullWhen is implemented
\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!
If you have trouble understanding a Checker Framework warning message, you
can search for its text in this manual.
There are three general causes for the warnings:

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

\item[Wrong annotations]
  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[Type-checker weakness]
  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.
  (The checker is not omniscient, and it works modularly:  when type-checking a
  method \<m>, it relies on the types, but not the code, of variables and
  methods used by \<m>.)

  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
  \chapterpageref{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.  A reader should assume that every \<if> condition can evaluate to true
  or false.  There is one exception to this rule:  an \<if> test may have a
  condition that you think will never evaluate to true, if its body just throws a
  descriptive error message.)
\end{description}

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.
(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.)


\paragraphAndLabel{Step 1: Explain correctness:  write a proof}{handling-warnings-step1}
Write an explanation of why your code is correct and it
never suffers the error at run time.  In other words, this is an informal proof
that the type-checker's warning is incorrect.  Write it in natural language
(e.g., English).

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


\paragraphAndLabel{Step 2: Translate the proof into annotations.}{handling-warnings-step2}
Here are some examples of the translation.

\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}.
\item
  If your proof includes ``method \<m> has no side effects'',
  then annotate \<m>'s declaration with
  \refqualclass{dataflow/qual}{SideEffectFree}.
\item
  If your proof includes ``each call to method \<m> returns the same value'',
  then annotate \<m>'s declaration with
  \refqualclass{dataflow/qual}{Deterministic}.
\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}.

Don't omit any parts of your proof.  When the Checker Framework analyzes
a method, it examines only the specifications (not the implementations)
of other methods.

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.

\paragraphAndLabel{Step 3: Re-run the checker}{handling-warnings-step3}
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 informal proof, and the proof guides
you to the best place to suppress the warning.
Please submit a bug report so that the checker can be improved
in the future (Section~\ref{reporting-bugs}).




\subsectionAndLabel{Calls to unannotated code (legacy libraries)}{unannotated-code}

Sometimes, you wish to type-check only part of your program.
You might focus on the most mission-critical or error-prone part of your
code.  When you start to use a checker, you may not wish to annotate
your entire program right away.
% Not having source code is *not* a reason.
You may not have
enough knowledge to annotate poorly-documented libraries that your program uses.
Or, the code you are annotating may call into unannotated libraries.

If annotated code uses unannotated code, then the checker may issue
warnings.  For example, the Nullness Checker (Chapter~\ref{nullness-checker}) will
warn whenever an unannotated method result is used in a non-null context:

\begin{Verbatim}
  @NonNull myvar = unannotated_method();   // WARNING: unannotated_method may return null
\end{Verbatim}

If the call \emph{can} return null, you should fix the bug in your program by
removing the \refqualclass{checker/nullness/qual}{NonNull} annotation in your own program.

If the call \emph{never} returns null, you have two choices:  annotate the library
or suppress warnings.
\begin{enumerate}
\item To annotate the library:
  \begin{itemize}
  \item
    If the unannotated code is in your program, you can write annotations
    but not type-check them yet.  Two ways to prevent the type-checking are
    via a \code{@SuppressWarnings} annotation
    (Section~\ref{suppresswarnings-annotation}) or by not running the
    checker on that file, for example via the \<-AskipDefs> command-line
    option (Section~\ref{askipdefs}).
  \item
    To annotate a library whose source code you do not have or cannot
    change, see Chapter~\ref{annotating-libraries}.
  \end{itemize}
\item To suppress all warnings related to uses of
  \code{unannotated\_method}, use the \code{-AskipUses} command-line option
  (see Section~\ref{askipuses}).  Beware:  a carelessly-written regular
  expression may suppress more warnings than you intend.
\end{enumerate}


% 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 sbt
% LocalWords:  Dcheckers Warski MyClass ProcessorName compareTo toString myDate
% LocalWords:  int XDTA newdir Awarns signedness urgin bytecodes gradle m1
% LocalWords:  subpackages bak tIDE Multiset NullPointerException AskipUses
% LocalWords:  html JCIP MultiSet Astubs Afilenames Anomsgtext Ashowchecks tex
% LocalWords:  Aquals processorpath regex RegEx Xmaxwarns com astub jaifs
% LocalWords:  IntelliJ assertNotNull checkNotNull Goetz antipattern subclassed
% LocalWords:  callees Xmx unconfuse fenum propkey forName de step1 step2
% LocalWords:  bootclasspath AonlyUses AskipDefs AonlyDefs AcheckPurityAnnotations
% LocalWords:  AsuppressWarnings AassumeSideEffectFree Adetailedmsgtext m2
% 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:  AshowSuppressWarningsStrings AoutputArgsToFile RegexChecker
% LocalWords:  NullnessChecker commandlineargfile AnnotatedFor Xmx2500m
% LocalWords:  AsafeDefaultsForUnannotatedBytecode Signedness Werror jaif
% LocalWords:  AuseSafeDefaultsForUnannotatedSourceCode beingConstructed
% LocalWords:  AuseConservativeDefaultsForUncheckedCode AresolveReflection Ainfer
% LocalWords:  AconservativeUninferredTypeArguments Averbosecfg Acfgviz
% LocalWords:  AstubWarnIfOverwritesBytecode AprintVerboseGenerics here''
% LocalWords:  AatfDoNotCache AatfCacheSize IntRange AwarnIfNotFound ajava
% LocalWords:  AwarnUnneededSuppressions AshowInferenceSteps BHCJEIBB
% LocalWords:  AstubWarnIfNotFoundIgnoresClasses processOptions getopt
% LocalWords:  EnsuresNonNull EnsuresNonNullIf checkername orElseThrow
% LocalWords:  ArequirePrefixInWarningSuppressions MaybePresent checker''
% LocalWords:  AignoreInvalidAnnotationLocations AprintGitProperties step3
% LocalWords:  AstubWarnIfRedundantWithBytecode annotation'' AassumePure
% LocalWords:  AassumeDeterministic stubfilename outputformat AparseAllJdk
% LocalWords:  AmergeStubsWithSource MyBatis AdumpOnErrors AutoValue
% LocalWords:  specification'' AwarnUnneededSuppressionsExceptions
% LocalWords:  requireNonNull ApermitUnsupportedJdkVersion AstubWarnNote