\htmlhr
\chapterAndLabel{Frequently Asked Questions (FAQs)}{faq}

These are some common questions about the Checker Framework and about
pluggable type-checking in general.  Feel free to suggest improvements to
the answers, or other questions to include here.

% Not supported by Hevea, so don't bother; instead do by hand:
% \minitoc

%BEGIN LATEX
~
%END LATEX

%BEGIN LATEX
\newcommand{\faqtocpara}[1]{\paragraph{#1} ~}
%END LATEX
%HEVEA \newcommand{\faqtocpara}[1]{\textbf{#1}}


\noindent
\textbf{Contents:}

\faqtocpara{\ref{faq-motivation-section}: Motivation for pluggable type-checking}
\\ \ref{faq-never-make-type-errors}: I don't make type errors, so would pluggable type-checking help me?
\\ \ref{faq-typequals-vs-subtypes}: Should I use pluggable types (type qualifiers), or should I used Java subtypes?

\faqtocpara{\ref{faq-getting-started-section}: Getting started}
\\ \ref{faq-annotate-existing-program}: How do I get started annotating an existing program?
\\ \ref{faq-first-checker}: Which checker should I start with?
\\ \ref{faq-checker-framework-dev}: How can I join the checker-framework-dev mailing list?

\faqtocpara{\ref{faq-usability-section}: Usability of pluggable type-checking}
\\ \ref{faq-ease-of-use}: Are type annotations easy to read and write?
\\ \ref{faq-code-clutter}: Will my code become cluttered with type annotations?
\\ \ref{faq-slowdown}: Will using the Checker Framework slow down my program?  Will it slow down the compiler?
\\ \ref{faq-shorten-command-line}: How do I shorten the command line when invoking a checker?
\\ \ref{faq-pre-conditions}: Method pre-condition contracts, including formal parameter annotations, make no sense for public methods.

\faqtocpara{\ref{faq-warnings-section}: How to handle warnings}
\\ \ref{faq-handling-warnings}: What should I do if a checker issues a warning about my code?
\\ \ref{faq-interpreting-warnings}: What does a certain Checker Framework warning message mean?
\\ \ref{faq-no-absolute-guarantee}: Can a pluggable type-checker guarantee that my code is correct?
\\ \ref{faq-concurrency}: What guarantee does the Checker Framework give for concurrent code?
\\ \ref{faq-awarns}: How do I make compilation succeed even if a checker issues errors?
\\ \ref{faq-100-warnings}: Why does the checker always say there are 100 errors or warnings?
\\ \ref{faq-type-i-did-not-write}: Why does the Checker Framework report an error regarding a type I have not written in my program?
\\ \ref{faq-same-code-different-behavior}: Why does the Checker Framework accept code on one line but reject it on the next?
\\ \ref{faq-run-time-checking}: How can I do run-time monitoring of properties that were not statically checked?

\faqtocpara{\ref{faq-false-positives-section}: False positive warnings}
\\ \ref{faq-false-positive}: What is a ``false positive'' warning?
\\ \ref{faq-false-positive-extend-checker-framework}: How can I improve the Checker Framework to eliminate a false positive warning?
\\ \ref{faq-infer-fields}: Why doesn't the Checker Framework infer types for fields and method return types?
\\ \ref{faq-relationships-between-variables}: Why doesn't the Checker Framework track relationships between variables?
\\ \ref{faq-path-sensitive}: Why isn't the Checker Framework path-sensitive?

\faqtocpara{\ref{faq-syntax-section}: Syntax of type annotations}
\\ \ref{faq-receiver}: What is a ``receiver''?
\\ \ref{faq-annotation-after-type}: What is the meaning of an annotation after a type, such as \<@NonNull Object @Nullable>?
\\ \ref{faq-array-syntax-meaning}: What is the meaning of array annotations such as \<@NonNull Object @Nullable []>?
\\ \ref{faq-varargs-syntax-meaning}: What is the meaning of varargs annotations such as \<@English String @NonEmpty~...>?
\\ \ref{faq-type-qualifier-on-class-declaration}: What is the meaning of a type qualifier at a class declaration?
\\ \ref{faq-type-qualifier-on-bounds}: How are type qualifiers written on upper and lower bounds?
\\ \ref{faq-no-annotation-on-types-and-declarations}: Why shouldn't a qualifier apply to both types and declarations?
\\ \ref{faq-annotate-fully-qualified-name}: How do I annotate a
fully-qualified type name?
\\ \ref{faq-type-vs-declaration-annotations}: What is the difference between type annotations and declaration annotations?

\faqtocpara{\ref{faq-semantics-section}: Semantics of type annotations}
\\ \ref{faq-typestate}: How can I handle typestate, or phases of my program with different data properties?
\\ \ref{faq-implicit-bounds}: Why are explicit and implicit bounds defaulted differently?
\\ \ref{faq-runtime-retention}: Why are type annotations declared with \<@Retention(RetentionPolicy.RUNTIME)>?

\faqtocpara{\ref{faq-create-a-checker-section}: Creating a new checker}
\\ \ref{faq-create-a-checker}: How do I create a new checker?
\\ \ref{faq-type-properties}: What properties can and cannot be handled by type-checking?
\\ \ref{faq-declarative-syntax-for-type-rules}: Why is there no declarative syntax for writing type rules?

\faqtocpara{\ref{faq-tool-section}: Tool questions}
\\ \ref{faq-pluggable-type-checking}: How does pluggable type-checking work?
\\ \ref{faq-classpath-to-use-annotated-library}: What classpath is needed to use an annotated library?
\\ \ref{faq-classfile-annotations}: Why do \<.class> files contain more annotations than the source code?
\\ \ref{faq-checked-exceptions}: Is there a type-checker for managing checked and unchecked exceptions?

\faqtocpara{\ref{faq-other-tools-section}: Relationship to other tools}
\\ \ref{faq-type-checking-vs-bug-detectors}: Why not just use a bug detector (like FindBugs or Error Prone)?
\\ \ref{faq-eclipse}: How does the Checker Framework compare with Eclipse's Null Analysis?
\\ \ref{faq-nullaway}: How does the Checker Framework compare with NullAway?
\\ \ref{faq-optional}: How does the Checker Framework compare with the JDK's \<Optional> type?
\\ \ref{faq-jml}: How does pluggable type-checking compare with JML?
\\ \ref{faq-checker-framework-part-of-java}: Is the Checker Framework an official part of Java?
\\ \ref{faq-jsr-305}: What is the relationship between the Checker Framework and JSR 305?
\\ \ref{faq-jsr-308}: What is the relationship between the Checker Framework and JSR 308?


\sectionAndLabel{Motivation for pluggable type-checking}{faq-motivation-section}

\subsectionAndLabel{I don't make type errors, so would pluggable type-checking help me?}{faq-never-make-type-errors}

Occasionally, a developer says that he makes no errors that type-checking
could catch, or that any such errors are unimportant because they have low
impact and are easy to fix.  When I investigate the claim, I invariably
find that the developer is mistaken.

Very frequently, the developer has underestimated what type-checking can
discover.  Not every type error leads to an exception being thrown; and
even if an exception is thrown, it may not seem related to classical types.
Remember that a type system can discover
null pointer dereferences,
incorrect side effects,
security errors such as information leakage or SQL injection,
partially-initialized data,
wrong units of measurement,
and many other errors.
Every programmer makes errors sometimes and works with other people
who do.
Even where type-checking does not discover a
problem directly, it can indicate code with bad smells, thus revealing
problems, improving documentation, and making future maintenance easier.

There are other ways to discover errors, including extensive testing and
debugging.  You should continue to use these.
But type-checking is a good complement to these.  Type-checking is more
effective for some problems, and less effective for other problems.  It can
reduce (but not eliminate) the time and effort that you spend on other
approaches.  There are many important errors that type-checking and other
automated approaches cannot find; pluggable type-checking gives you more
time to focus on those.


\subsectionAndLabel{Should I use pluggable types (type qualifiers), or should I used Java subtypes?}{faq-typequals-vs-subtypes}

% Old labels, for backward compatibility.  Don't use them any longer.
\label{when-to-use-type-qualifiers}
\label{faq-qualifiers-vs-subclasses}

In brief, use subtypes when you can, and use type qualifiers when you cannot
use subtypes.

For some programming tasks, you can use either a Java subtype (interfaces
or subclasses) or a type
qualifier.  As an example, suppose that your code currently uses \code{String} to
represent an address.  You could use Java subclasses by creating a new
\code{Address} class and refactor your code to use it, or you could use
type qualifiers by creating an \code{@Address} annotation and applying it
to some uses of \code{String} in your code.  As another example, suppose
that your code currently uses \code{MyClass} in two different ways that
should not interact with one another.  You could use Java subclasses by
changing MyClass into an interface or abstract class, defining two
subclasses, and ensuring that neither subclass ever refers to the other
subclass nor to the parent class.

If  Java subclasses solve your problem, then that is probably better.
We do not encourage you to use type qualifiers as a poor substitute for
classes.  An advantage of using classes is that the Java type-checker
runs every time you compile your code;
by contrast, it is possible to forget to run the pluggable
type-checker.  However, sometimes type qualifiers are a
better choice; here are some reasons:

\begin{description}

\item[Backward compatibility]
Using a new class may make your code incompatible with existing libraries or
clients.  Brian Goetz expands on this issue in an article on the
pseudo-typedef antipattern~\cite{Goetz2006:typedef}.  Even if compatibility
is not a concern, a code change may introduce bugs, whereas adding
annotations does not change the run-time behavior.  It is possible to add
annotations to existing code, including code you do not maintain or cannot
change.  For code that strictly cannot be changed, you
can write library annotations (see Chapter~\ref{annotating-libraries}).

\item[Broader applicability]
Type annotations can be applied to primitives and to final classes such as
\code{String}, which cannot be subclassed.

\item[Richer semantics and new supertypes]
Type qualifiers permit you to remove operations, with a compile-time
guarantee.  More
generally, type qualifiers permit creating a new supertype, not just a
subtype, of an existing Java type.

\item[More precise type-checking]
The Checker Framework is able to verify the correctness of code that the
Java type-checker would reject.  Here are a few examples.
\begin{itemize}
\item
  It uses a dataflow analysis to determine a more precise type for
  variables after conditional tests or assignments.
\item
  It treats certain Java constructs more precisely, such as
  reflection (see Chapter~\ref{reflection-resolution}).
\item
  It includes special-case logic for type-checking specific methods, such
  as the Nullness Checker's treatment of \code{Map.get}.
\end{itemize}


\item[Efficiency]
  Type qualifiers have no run-time representation.  Therefore, there is no
  space overhead for separate classes or for wrapper classes for
  primitives.  There is no run-time overhead for due to extra dereferences
  or dynamic dispatch for methods that could otherwise be statically
  dispatched.

\item[Less code clutter]
  The programmer does not have to convert primitive types to wrappers,
  which would make the code both uglier and slower.  Thanks to defaults and
  type inference (Section~\ref{defaults}),
  you may be able to write and think in terms of the
  original Java type, rather than having to explicitly write one of the
  subtypes in all locations.

\end{description}


For more details, see Section~\ref{faq-typequals-vs-subtypes}.



\sectionAndLabel{Getting started}{faq-getting-started-section}

\subsectionAndLabel{How do I get started annotating an existing program?}{faq-annotate-existing-program}

See Section~\ref{get-started-with-legacy-code}.


\subsectionAndLabel{Which checker should I start with?}{faq-first-checker}

You should start with a property that matters to you.  Think about what
aspects of your code cause the most errors, or cost the most time during
maintenance, or are the most common to be incorrectly-documented.  Focusing
on what you care about will give you the best benefits.

When you first start out with the Checker Framework, it's usually best to
get experience with an existing type-checker before you write your own new
checker.

Many users are tempted to start with the
\ahrefloc{nullness-checker}{Nullness Checker} (see
\chapterpageref{nullness-checker}), since null pointer errors are common
and familiar.  The Nullness Checker works very well, but be warned of three
facts that make the absence of null pointer exceptions challenging to
verify.

\begin{enumerate}
\item
  Dereferences happen throughout your codebase, so there are a lot of
  potential problems.  By contrast, fewer lines of code are related to
  locking, regular expressions, etc., so those properties are easier to
  check.
\item
  Programmers use \<null> for many different purposes.  More seriously,
  programmers write run-time tests against \<null>, and those are difficult
  for any static analysis to capture.
\item
  The Nullness Checker interacts with initialization and map keys.
\end{enumerate}

If null pointer exceptions are most important to you, then by all means use
the Nullness Checker.  But if you just want to try \emph{some}
type-checker, there are others that are easier to use.

We do not recommend indiscriminately running all the checkers on your code.
The reason is that each one has a cost --- not just at compile time, but
also in terms of code clutter and human time to maintain the annotations.
If the property is important to you, is difficult for people to reason
about, or has caused problems in the past, then you should run that
checker.  For other properties, the benefits may not repay the effort to
use it.  You will be the best judge of this for your own code, of course.

%You might want to avoid some type-checkers when you are first starting out.
Some of the third-party checkers (see
\chapterpageref{third-party-checkers})
have known bugs that limit their
usability.  (Report the ones that affect you, so the developers
will prioritize fixing them.)


\subsectionAndLabel{How can I join the checker-framework-dev mailing list?}{faq-checker-framework-dev}

The \code{checker-framework-dev@googlegroups.com} mailing list is for
Checker Framework developers.  Anyone is welcome to
\href{https://groups.google.com/forum/#!forum/checker-framework-dev}{join
  \code{checker-framework-dev}}, after they have had several pull requests
accepted.

Anyone is welcome to send mail to the
\code{checker-framework-dev@googlegroups.com} mailing list --- for
implementation details it is generally a better place for discussions than
the general \code{checker-framework-discuss@googlegroups.com} mailing list,
which is for user-focused discussions.

Anyone is welcome to
\href{https://groups.google.com/forum/#!forum/checker-framework-discuss}{join
  \code{checker-framework-discuss@googlegroups.com}} and send mail to it.


\sectionAndLabel{Usability of pluggable type-checking}{faq-usability-section}

\subsectionAndLabel{Are type annotations easy to read and write?}{faq-ease-of-use}

% This FAQ also appears in the JSR 308 FAQ.
% When I update one, also update the other.

The papers
\href{https://homes.cs.washington.edu/~mernst/pubs/pluggable-checkers-issta2008-abstract.html}{``Practical
  pluggable types for Java''}~\cite{PapiACPE2008}
and
\href{https://homes.cs.washington.edu/~mernst/pubs/pluggable-checkers-icse2011-abstract.html}{``Building
  and using pluggable type-checkers''}~\cite{DietlDEMS2011}
discuss case studies in
which programmers
found type annotations to be natural to read and write.  The code
continued to feel like Java, and the type-checking errors were easy to
comprehend and often led to real bugs.

You don't have to take our word for it, though.  You can try the
Checker Framework for yourself.

The difficulty of adding and verifying annotations depends on your program.
If your program is well-designed and -documented, then skimming the
existing documentation and writing type annotations is extremely easy.
Otherwise, you may find yourself spending a lot of time trying to
understand, reverse-engineer, or fix bugs in your program, and then just a
moment writing a type annotation that describes what you discovered.  This
process inevitably improves your code.  You must decide whether it is a
good use of your time.  For code that is not causing trouble now and is
unlikely to do so in the future (the code is bug-free, and you do not
anticipate changing it or using it in new contexts), then the
effort of writing type annotations for it may not be justified.


\subsectionAndLabel{Will my code become cluttered with type annotations?}{faq-code-clutter}

% This FAQ also appears in the JSR 308 FAQ.
% When I update one, also update the other.

In summary:  annotations do not clutter code; they are used much
less frequently than generic types, which Java programmers find acceptable;
and they reduce the overall volume of documentation that a codebase needs.

As with any language feature, it is possible to write ugly code that
over-uses annotations.  However, in normal use, very few annotations need
to be written.  Figure 1 of the paper
\href{https://homes.cs.washington.edu/~mernst/pubs/pluggable-checkers-issta2008-abstract.html}{Practical
  pluggable types for Java}~\cite{PapiACPE2008} reports data for over
350,000 lines of type-annotated code:

\begin{itemize}
\item
    1 annotation per 62 lines for nullness annotations (\<@NonNull>, \<@Nullable>, etc.)
    % (/ (+ 4640 3961 10798) (+ 107 35 167))
\item
    1 annotation per 1736 lines for interning annotations (\<@Interned>)
    % (/ 224048 129)
\end{itemize}

% ICSE 2011 paper says:
% Signature String Checker: less than 1 annotation per 500 lines of code

These numbers are for annotating existing code.  New code that
is written with the type annotation system in mind is cleaner and more
correct, so it requires even fewer annotations.

Each annotation that a programmer writes replaces a sentence or phrase of
English descriptive text that would otherwise have been written in the
Javadoc.  So, use of annotations actually reduces the overall size of the
documentation, at the same time as making it machine-processable
and less ambiguous.


\subsectionAndLabel{Will using the Checker Framework slow down my program?  Will it slow down the compiler?}{faq-slowdown}

Using the Checker Framework has no impact on the execution of your program:
the compiler emits the identical bytecodes as the Java 8
compiler and so there is no run-time effect.  Because there is no run-time
representation of type qualifiers, there is no way to use reflection to
query the qualifier on a given object, though you can use reflection to
examine a class/method/field declaration.

Using the Checker Framework does increase compilation time.  In theory it
should only add a few percent overhead, but our current implementation
can double the compilation time --- or more, if you run many pluggable
type-checkers at once.  This is especially true if you run pluggable
type-checking on every file (as we recommend) instead of just on the ones
that have recently changed.
Nonetheless, compilation with pluggable type-checking still feels like
compilation, and you can do it as part of your normal development process.


\subsectionAndLabel{How do I shorten the command line when invoking a checker?}{faq-shorten-command-line}

\begin{sloppypar}
The compile options to javac can be long to type; for example,
\code{javac -processor org.checkerframework.checker.nullness.NullnessChecker ...}.
See Section~\ref{checker-auto-discovery} for a way to avoid the need for
the \code{-processor} command-line option.
\end{sloppypar}


\subsectionAndLabel{Method pre-condition contracts, including formal parameter annotations, make no sense for public methods}{faq-pre-conditions}

Some people go further and say that pre-condition contracts make no sense
for any method.  This objection is sometimes stated as, "A method parameter
should never be annotated as \<@NonNull>.  A client could pass any value at
all, so the method implementation cannot depend on the value being
non-null.  Furthermore, if a client passes an illegal value, it is the
method's responsibility to immediately tell the client about the illegal
value."

Here is an example that invalidates this general argument.  Consider a
binary search routine.  Its specification requires that clients pass in a
sorted array.

%BEGIN LATEX
\begin{smaller}
%END LATEX
\begin{Verbatim}
  /** Return index of the search key, if it is contained it the sorted array a; otherwise ... */
  int binarySearch(Object @Sorted [] a, Object key)
\end{Verbatim}
%BEGIN LATEX
\end{smaller}
%END LATEX

The \<binarySearch> routine is fast --- it runs in O(log n) time where n is
the length of the array.  If the routine had to validate that its input
array is sorted, then it would run in O(n) time, negating all benefit of
binary search.  In other words, \<binarySearch> should \emph{not} validate
its input!

The nature of a contract is that if the \emph{caller} violates its
responsibilities by passing bad values, then the \emph{callee} is absolved
of its responsibilities.  It is polite for the callee to try to provide a
useful diagnostic to the misbehaving caller (for example, by raising a
particular exception quickly), but it is \emph{not} required.  In such a
situation, the callee has the flexibility to do anything that is
convenient.

In some cases a routine has a \emph{complete} specification:  the contract
permits the caller to pass any value, and the callee is required to throw
particular exceptions for particular inputs.  This approach is common for
public methods, but it is not required and is not always the right thing.
As explained in section~\ref{annotate-normal-behavior}, even when a method
has a complete specification, the annotations should indicate normal
behavior:  behavior that will avoid exceptions.



\sectionAndLabel{How to handle warnings and errors}{faq-warnings-section}

\subsectionAndLabel{What should I do if a checker issues a warning about my code?}{faq-handling-warnings}

For a discussion of this issue, see Section~\ref{handling-warnings}.


\subsectionAndLabel{What does a certain Checker Framework warning message mean?}{faq-interpreting-warnings}

Read the error message first; sometimes that is enough to clarify it.

Search through this manual for the text of the warning message or for words
that appear in it.

If nothing else explains it, then ask on the
\href{https://groups.google.com/forum/#!forum/checker-framework-discuss}{mailing
  list}.  Be sure to say what you think it means or what specific part does
not make sense to you, and what you have already done to try to understand it.


\subsectionAndLabel{Can a pluggable type-checker guarantee that my code is correct?}{faq-no-absolute-guarantee}

Each checker looks for certain errors.  You can use multiple checkers to
detect more errors in your code, but you will never have a guarantee that
your code is completely bug-free.

If the type-checker issues no warning, then you have a guarantee that your
code is free of some particular error.  There are some limitations to the
guarantee.

Most importantly, if you run a pluggable checker on only part of a program, then
you only get a guarantee that those parts of the program are error-free.
For example, suppose you have type-checked a framework that clients
are intended to extend.  You should recommend that clients
run the pluggable checker.  There is no way to force users to do so, so you
may want to retain dynamic checks or use other mechanisms to detect errors.

Section~\ref{checker-guarantees} states other limitations to a checker's
guarantee, such as regarding concurrency.  Java's type system is also
unsound in certain situations, such as for arrays and casts (however, the
Checker Framework is sound for arrays and casts).  Java uses dynamic checks
is some places it is unsound, so that errors are thrown at run time.  The
pluggable type-checkers do not currently have built-in dynamic checkers to
check for the places they are unsound.
Writing dynamic checkers would be an interesting and valuable project.

Other types of dynamism in a Java application do not jeopardize the
guarantee, because the type-checker is conservative.  For example, at a
method call, dynamic dispatch chooses some implementation of the method,
but it is impossible to know at compile time which one it will be.  The
type-checker gives a guarantee no matter what implementation of the method
is invoked.

% This paragraph is weak.

Even if a pluggable checker cannot give an ironclad
guarantee of correctness, it is still useful.  It can find errors,
exclude certain types of possible problems (e.g., restricting the
possible class of problems), improve documentation, and increase confidence
in your software.


\subsectionAndLabel{What guarantee does the Checker Framework give for concurrent code?}{faq-concurrency}

The Lock Checker (see Chapter~\ref{lock-checker}) offers a way to detect
and prevent certain concurrency errors.


By default, the Checker Framework assumes that the code that it is checking
is sequential:  that is, there are no concurrent accesses from another
thread.  This means that the Checker Framework is unsound for concurrent
code, in the sense that it may fail to issue a warning about errors that
occur only when the code is running in a concurrent setting.
For example, the Nullness Checker issues no warning for this
code:

\begin{Verbatim}
  if (myobject.myfield != null) {
    myobject.myfield.toString();
  }
\end{Verbatim}

\noindent
This code is safe when run on its own.
However, in the presence of multithreading, the call to \<toString> may
fail because another thread may set \<myobject.myfield> to \<null> after
the nullness check in the \<if> condition, but before the \<if> body is
executed.

If you supply the \<-AconcurrentSemantics> command-line option, then the
Checker Framework assumes that any field can be changed at any time.  This
limits the amount of type refinement
(Section~\ref{type-refinement}) that the Checker Framework can do.


% If you are concerned about concurrency, then the ``fix''
% of putting data in a local variable doesn't fix the problem,
% just masks it from one particular checker.  This is bad style and may make
% debugging harder rather than easier.
%
% For instance, suppose you have
%
% if (x.val != null) {
%   x.val = x.val + 1;
% }
%
% which can suffer a null pointer exception if another thread nulls out
% x.val.  The underlying problem is the possible concurrency error:  the user
% should have used locks or some other mechanism to protect access to x.val.
%
% Changing this to
%
% myval = x.val;
% if (myval != null) {
%   x.val = myval + 1;
% }
%
% does not fix the concurrency error, because no locking has been introduced.
% The code still has a data race that can lose updates or corrupt data
% structures.  The code has been transformed so that the Nullness Checker
% does not issue a warning, but this is scant comfort since the code is no
% more correct than it was before.
%
% If you want to detect concurrency errors, then it is better to use a
% correct checker that is concurrency-aware, rather than an unsound one that
% encourages incorrect workarounds.  Another way to put this is that a static
% checker should encourage better overall design, not just different bad
% designs.


\subsectionAndLabel{How do I make compilation succeed even if a checker issues errors?}{faq-awarns}

Section~\ref{running} describes the \<-Awarns> command-line
option that turns checker errors into warnings, so type-checking errors
will not cause \<javac> to exit with a failure status.


\subsectionAndLabel{Why does the checker always say there are 100 errors or warnings?}{faq-100-warnings}

By default, javac only reports the first 100 errors or warnings.
Furthermore, once javac encounters an error, it doesn't try compiling any
more files (but does complete compilation of all the ones that it has
started so far).

To see more than 100 errors or warnings, use the javac options \<-Xmaxerrs>
and \<-Xmaxwarns>.  To convert Checker Framework errors into warnings so
that javac will process all your source files, use the option \<-Awarns>.
See Section~\ref{running} for more details.


\subsectionAndLabel{Why does the Checker Framework report an error regarding a type I have not written in my program?}{faq-type-i-did-not-write}

Sometimes, a Checker Framework warning message will mention a type you have
not written in your program.  This is typically because a default has been
applied where you did not write a type; see Section~\ref{defaults}.  In
other cases, this is because type refinement has given an
expression a more specific type than you wrote or than was defaulted; see
Section~\ref{type-refinement}.
Note that an invocation of an impure method may cause the loss of all
information that was determined via type refinement; see
Section~\ref{type-refinement-purity}.


\subsectionAndLabel{Why does the Checker Framework accept code on one line but reject it on the next?}{faq-same-code-different-behavior}

Sometimes, the Checker Framework permits code on one line, but rejects the
same code a few lines later:

\begin{Verbatim}
  if (myField != null) {
    myField.hashCode();   // no warning
    someMethod();
    myField.hashCode();   // warning about potential NullPointerException
  }
\end{Verbatim}

The reason is explained in the section on type refinement
(Section~\ref{type-refinement}), which also tells how to specify the side
effects of \<someMethod> (Section~\ref{type-refinement-purity}).


\subsectionAndLabel{How can I do run-time monitoring of properties that were not statically checked?}{faq-run-time-checking}

Some properties are not checked statically (see
Chapter~\ref{suppressing-warnings} for reasons that code might not be
statically checked).  In such cases, it would be desirable to check the
property dynamically, at run time.
Currently, the Checker Framework has no support for adding code to perform
run-time checking.

Adding such support would be an interesting and valuable project.
An example would be an option that causes the Checker Framework to
automatically insert a run-time check anywhere that static checking is
suppressed.
% such as casts
If you
are able to add run-time verification functionality, we would gladly
welcome it as a contribution to the Checker Framework.

Some checkers have library methods that you can explicitly insert in your
source code.
Examples include the Nullness Checker's
\refmethod{checker/nullness}{NullnessUtil}{castNonNull}{-T-} method (see
Section~\ref{suppressing-warnings-with-assertions}) and the Regex Checker's
\<RegexUtil> class (see Section~\ref{regexutil-methods}).
But, it would be better to have more general support that does not require
the user to explicitly insert method calls.


\sectionAndLabel{False positive warnings}{faq-false-positives-section}


\subsectionAndLabel{What is a ``false positive'' warning?}{faq-false-positive}

A ``false positive'' is when the tool reports a potential problem, but the
code is actually correct and will never violate the given property at run
time.

The Checker Framework aims to be sound; that is, if the Checker Framework
does not report any possible errors, then your code is correct.

Every sound tool suffers false positive errors.
Wherever the Checker Framework issues an error, you can think of it as
saying, ``I can't prove this code is safe,'' but the code might be safe for
some complex, tricky reason that is beyond the capabilities of its
analysis.

If you are sure that the warning is a false positive, you have several
options.
Perhaps you just need to write annotations, especially on method signatures
but perhaps within method bodies as well.
Sometimes you can rewrite the code in a clearer way that the Checker
Framework can verify, and that might be easier for people to understand, too.
If these don't work, then you can suppress the warning
(Section~\ref{handling-warnings}).
You also might want to report
the false positive in the Checker Framework issue tracker
(Section~\ref{reporting-bugs}), if it appears in real-world, well-written code.
%
Finally, you could improve the Checker Framework to make it more
precise, so that it does not suffer that false positive (see
Section~\ref{faq-false-positive-extend-checker-framework}).


\subsectionAndLabel{How can I improve the Checker Framework to eliminate a false positive warning?}{faq-false-positive-extend-checker-framework}

As noted in Section~\ref{faq-false-positive}, \emph{every} sound analysis
tool suffers false positives.

For any given false positive warning, it is theoretically possible to
improve the Checker Framework to eliminate it.  (But, it's theoretically
impossible to eliminate all false positives.  That is, there
will always exist some programs that don't go wrong at run time but for
which the Checker Framework issues a warning.)

Some improvements affect the implementation of the type system; they do not
add any new types.  Such an improvement is invisible to users, except that
the users suffer fewer false positive warnings.  This type of improvement
to the type checker's implementation is often worthwhile.

Other improvements change the type system or add a new type system.
Defining new types is a powerful way to improve precision, but it is costly
too.  A simpler type system is easier for users to understand, less likely
to contain bugs, and more efficient.

By design, each type system in the Checker Framework has limited
expressiveness.  Our goal is to implement enough functionality to handle
common, well-written real-world code, not to cover every possible
situation.

When reporting bugs, please focus on realistic scenarios.  We are sure that
you can make up artificial code that stymies the type-checker!  Those bugs
aren't a good use of your time to report nor the maintainers' time to
evaluate and fix.  When reporting a bug, it's very helpful to minimize it
to give a tiny example that is easy to evaluate and fix, but please also
indicate how it arises in real-world, well-written code.


\subsectionAndLabel{Why doesn't the Checker Framework infer types for fields and method return types?}{faq-infer-fields}

Consider the following code.  A programmer can tell that all three
invocations of \<format> are safe --- they never suffer an
\<IllegalFormatException> exception at run time:

\begin{Verbatim}
class MyClass {

  final String field = "%d";

  String method() {
    return "%d";
  }

  void method m() {
    String local = "%d";
    String.format(local, 5);    // Format String Checker verifies the call is safe
    String.format(field, 5);    // Format String Checker warns the call might not be safe
    String.format(method(), 5); // Format String Checker warns the call might not be safe
  }
}
\end{Verbatim}

\noindent
However, the Format String Checker can only verify the first call.  It issues a
false positive warning about the second and third calls.

The Checker Framework can verify all three calls, with no false positive
warnings, if you annotate the type of \<field> and the return type of
\<method> as \<@Format(INT)>.

By default, the Checker Framework infers types for local variables
(Section~\ref{type-refinement}), but not for fields and method return
types.  (The Checker Framework includes a whole-program type inference tool
that infers field and method return types; see
Section~\ref{whole-program-inference}.)
There are several reasons for this design choice.

\begin{description}
\item[Separation of specification from implementation]
  The designer of an API makes certain promises to clients; these are
  codified in the API's specification or contract.  The implementation
  might return a more specific type today, but the designer does not want
  clients to depend on that.  For example, a string might happen to be a
  regular expression because it contains no characters with special meaning
  in regexes, but that is not guaranteed to always be true.  It's better
  for the programmer to explicitly write the intended specification.

\item[Separate compilation]
  To infer types for a non-final method, it is necessary to examine every
  overriding implementation, so that the method's return type annotation is
  compatible with all values that are returned by any overriding
  implementation.  In general, examining all implementations is impossible,
  because clients may override the method.  When possible, it is
  inconvenient to provide all that source code, and it would slow down the
  type-checker.

  A related issue is that determining which values can be returned by a
  method $m$ requires analyzing $m$'s body, which requires analyzing
  all the methods called by $m$, and so forth.  This quickly devolves to
  analyzing the whole program.
  Determining all possible values assigned to a field is equally hard.

  Type-checking is modular --- it works on one procedure at a time,
  examining that procedure and the specifications (not implementations) of
  methods that it calls.  Therefore, type-checking is fast and can work on
  partial programs.  The Checker Framework performs modular type-checking,
  not a whole-program analysis.

\item[Order of compilation]
  When the compiler is called on class \<Client> and class \<Library>, the
  programmer has no control over which class is analyzed first.  When the
  first class is compiled, it has access only to the signature of the other
  class.  Therefore, a programmer would see inconsistent results depending
  on whether \<Client> was compiled first and had access only to the
  declared types of \<Library>, or the \<Library> was compiled first and
  the compiler refined the types of its methods and fields before \<Client>
  looked them up.

\item[Consistent behavior with or without pluggable type-checking]
  The \<.class> files produced with or without pluggable type-checking
  should specify the same types for all public fields and methods.  If
  pluggable type-checking changed the those types, then users would be
  confused.  Depending on how a library was compiled, pluggable
  type-checking of a client program would give different results.

\end{description}

% In the future, the Checker Framework may infer types for final fields; if
% programmers see inconsistent results, they should write types explicitly.


\subsectionAndLabel{Why doesn't the Checker Framework track relationships between variables?}{faq-relationships-between-variables}

The Checker Framework estimates the possible run-time value of each
variable, as expressed in a type system.  In general, the Checker Framework
does estimate relationships between two variables, except for specific
relationships listed in Section~\ref{java-expressions-as-arguments}.

For example, the Checker Framework does not track which variables are equal
to one another.  The Nullness Checker issues a warning, ``dereference of
possibly-null reference y'', for expression \<y.toString()>:

\begin{Verbatim}
void nullnessExample1(@Nullable Object x) {
    Object y = x;
    if (x != null) {
      System.out.println(y.toString());
    }
  }
\end{Verbatim}

\noindent
Code that checks one variable and then uses a different variable is
confusing and is often considered poor style.

The Nullness Checker is able to verify the correctness of a small variant
of the program, thanks to type refinement
(Section~\ref{type-refinement}):

\begin{Verbatim}
  void nullnessExample12(@Nullable Object x) {
    if (x != null) {
      Object y = x;
      System.out.println(y.toString());
    }
  }
\end{Verbatim}

The difference is that in the first example, nothing was known about \<x> at
the time \<y> was set to it, and so the Nullness Checker recorded no facts
about \<y>.  In the second example, the Nullness Checker knew that \<x>
was non-null when \<y> was assigned to it.

In the future, the Checker Framework could be enriched by tracking which
variables are equal to one another, a technique called ``copy
propagation''.

This would handle the above examples, but wouldn't handle other examples.
For example, the following code is safe:

\begin{Verbatim}
  void requiresPositive(@Positive int arg) {}

  void intExample1(int x) {
    int y = x*x;
    if (x > 0) {
      requiresPositive(y);
    }
  }

  void intExample2(int x) {
    int y = x*x;
    if (y > 0) {
      requiresPositive(x);
    }
  }
\end{Verbatim}

\noindent
However, the Index Checker (\chapterpageref{index-checker}), which defines the
\refqualclass{checker/index/qual}{Positive} type qualifier, issues warnings
saying that it cannot prove that the arguments are \<@Positive>.

A slight variant of \<intExample1> can be verified:

\begin{Verbatim}
  void intExample1a(int x) {
    if (x > 0) {
      int y = x*x;
      requiresPositive(y);
    }
  }
\end{Verbatim}

\noindent
No variant of \<intExample2> can be verified.  It is not worthwhile to make
the Checker Framework more complex and slow by tracking rich properties
such as arbitrary arithmetic.

As another example of a false positive warning due to arbitrary arithmetic
properties, consider the following code:

\begin{Verbatim}
  void falsePositive2(int arg) {
    Object o;
    if (arg * arg >= arg) { // always true!
      o = new Object();
    }
    o.toString();  // Nullness Checker issues a false positive warning
  }
\end{Verbatim}


\subsectionAndLabel{Why isn't the Checker Framework path-sensitive?}{faq-path-sensitive}

The Checker Framework is not path-sensitive.  That is, it maintains one
estimate for each variable, and it assumes at every branch (such as \<if>
statement) that every choice could be taken.

In the following code, there are two \<if> statements.

\begin{Verbatim}
  void falsePositive1(boolean b) {
    Object o;
    if (b) {
      o = new Object();
    }
    if (b) {
      o.toString();  // Nullness Checker issues a false positive warning
    }
  }
\end{Verbatim}

In general, if code has two \<if> statements in succession, then there are
4 possible paths through the code:  [true, true], [true, false], [false,
  true], and [false, false].  However, for this code only two of those
paths are feasible:  namely, [true, true] and [false, false].

The Checker Framework is not path-sensitive, so it issues a warning.

The lack of path-sensitivity can be viewed as special case of the fact that
the Checker Framework maintains a single estimate for each variable value,
rather than tracking relationships between multiple variables
(Section~\ref{faq-relationships-between-variables}).

Making the Checker Framework path-sensitive would make it more powerful,
but also much more complex and much slower.  We have not yet found this
necessary.


\sectionAndLabel{Syntax of type annotations}{faq-syntax-section}

There is also a separate FAQ for the type annotations syntax
(\url{https://checkerframework.org/jsr308/jsr308-faq.html}).


\subsectionAndLabel{What is a ``receiver''?}{faq-receiver}

The \emph{receiver} of a method is the \<this> formal parameter, sometimes
also called the ``current object''.  Within the method declaration, \<this>
is used to refer to the receiver formal parameter.  At a method call, the
receiver actual argument is written before a period and the method name.

The method \<compareTo> takes \emph{two} formal parameters.  At a call site
like \<x.compareTo(y)>, the two arguments are \<x> and \<y>.  It is
desirable to be able to annotate the types of both of the formal
parameters, and doing so is supported by both Java's type annotations
syntax and by the Checker Framework.

A type annotation on the receiver is treated exactly like a type annotation
on any other formal parameter.  At each call site, the type of the argument
must be a consistent with (a subtype of or equal to) the declaration of the
corresponding formal parameter.  If not, the type-checker issues a warning.

Here is an example.  Suppose that \<@A Object> is a supertype of \<@B
Object> in the following declaration:

\begin{Verbatim}
  class MyClass {
    void requiresA(@A MyClass this) { ... }
    void requiresB(@B MyClass this) { ... }
  }
\end{Verbatim}

\noindent
Then the behavior of four different invocations is as follows:

\begin{Verbatim}
  @A MyClass myA = ...;
  @B MyClass myB = ...;

  myA.requiresA()    // OK
  myA.requiresB()    // compile-time error
  myB.requiresA()    // OK
  myB.requiresB()    // OK
\end{Verbatim}

The invocation \<myA.requiresB()> does not type-check because the actual
argument's type is not a subtype of the formal parameter's type.

A top-level constructor does not have a receiver.  An inner class
constructor does have a receiver, whose type is the same as the containing
outer class.  The receiver is distinct from the object being constructed.
In a method of a top-level class, the receiver is named \<this>.  In a
constructor of an inner class, the receiver is named \<Outer.this> and the
result is named \<this>.

A method in an anonymous class has a receiver, but it is not possible to
write the receiver in the formal parameter list because there is no name
for the type of \<this>.


\subsectionAndLabel{What is the meaning of an annotation after a type, such as \<@NonNull Object @Nullable>?}{faq-annotation-after-type}

In a type such as \<@NonNull Object @Nullable []>, it may appear that the
\<@Nullable> annotation is written \emph{after} the type \<Object>.  In
fact, \<@Nullable> modifies \<[]>.  See the next FAQ, about array
annotations (Section~\ref{faq-array-syntax-meaning}).


\subsectionAndLabel{What is the meaning of array annotations such as \<@NonNull Object @Nullable []>?}{faq-array-syntax-meaning}

You should parse this as:
(\textbf{\<@NonNull Object>}) (\textbf{\<@Nullable []>}).
Each annotation precedes the component of the type that it qualifies.

Thus,
\<@NonNull Object @Nullable []> is a possibly-null array of non-null
objects.  Note that the first token in the type,
``\<@NonNull>'', applies to the element
type \<Object>, not to the array type as a whole.  The annotation \<@Nullable> applies to the
array (\<[]>).

Similarly,
\<@Nullable Object @NonNull []> is a non-null array of possibly-null
objects.

Some older tools have inconsistent semantics for annotations on array and
varargs elements.  Their semantics is unfortunate and confusing; developers
should convert their code to use type annotations instead.
Section~\ref{declaration-annotations-moved} explains how the Checker
Framework handles declaration annotations in the meanwhile.


\subsectionAndLabel{What is the meaning of varargs annotations such as \<@English String @NonEmpty~...>?}{faq-varargs-syntax-meaning}

Varargs annotations are treated similarly to array annotations.
(A way to remember this is that
when you write a varargs formal parameter such as
\<void method(String... x) \ttlcb\ttrcb>, the Java compiler generates a
method that takes an array of strings; whenever your source code calls the
method with multiple arguments, the Java compiler packages them up into an
array before calling the method.)

Either of these annotations

\begin{Verbatim}
  void method(String @NonEmpty [] x) {}
  void method(String @NonEmpty ... x) {}
\end{Verbatim}

\noindent
applies to the array:  the method takes a non-empty array of strings, or
the varargs list must not be empty.

Either of these annotations

\begin{Verbatim}
  void method(@English String [] x) {}
  void method(@English String ... x) {}
\end{Verbatim}

\noindent.
applies to the element type. The annotation documents that the method takes an array of English strings.


\subsectionAndLabel{What is the meaning of a type qualifier at a class declaration?}{faq-type-qualifier-on-class-declaration}

See Section~\ref{upper-bound-for-use}.


\subsectionAndLabel{How are type qualifiers written on upper and lower bounds?}{faq-type-qualifier-on-bounds}

See Section~\ref{generics-instantiation}.


\subsectionAndLabel{Why shouldn't a qualifier apply to both types and declarations?}{faq-no-annotation-on-types-and-declarations}

It is bad style for an annotation to apply to both types and declarations.
In other words, every annotation should have a \<@Target> meta-annotation,
and the \<@Target> meta-annotation should list either only declaration
locations or only type annotations.  (It's OK for an annotation to target
both \<ElementType.TYPE\_PARAMETER> and \<ElementType.TYPE\_USE>, but no
other declaration location along with \<ElementType.TYPE\_USE>.)

Sometimes, it may seem tempting for an annotation to apply to both type
uses and (say) method declarations.  Here is a hypothetical example:

\begin{quote}
  ``Each \<Widget> type may have a \<@Version> annotation.
  I wish to prove that versions of widgets don't get assigned to
  incompatible variables, and that older code does not call newer code (to
  avoid problems when backporting).

  A \<@Version> annotation could be written like so:

\begin{Verbatim}
  @Version("2.0") Widget createWidget(String value) { ... }
\end{Verbatim}

\<@Version("2.0")> on the method could mean that the \<createWidget> method
only appears in the 2.0 version.  \<@Version("2.0")> on the return type
could mean that the returned \<Widget> should only be used by code that
uses the 2.0 API of \<Widget>.  It should be possible to specify these
independently, such as a 2.0 method that returns a value that allows the
1.0 API method invocations.''
\end{quote}

Both of these are type properties and should be specified with type
annotations.  No method annotation is necessary or desirable.  The best way
to require that the receiver has a certain property is to use a type
annotation on the receiver of the method.  (Slightly more formally, the
property being checked is compatibility between the annotation on the type
of the formal parameter receiver and the annotation on the type of the
actual receiver.)  If you do not know what ``receiver'' means, see
Section~\ref{faq-receiver}.

Another example of a type-and-declaration annotation that represents poor
design is JCIP's \<@GuardedBy> annotation~\cite{Goetz2006}.  As discussed
in Section~\ref{lock-jcip-annotations}, it means two different things when
applied to a field or a method.  To reduce confusion and increase
expressiveness, the Lock Checker (see Chapter~\ref{lock-checker}) uses the
\<@Holding> annotation for one of these meanings, rather than overloading
\<@GuardedBy> with two distinct meanings.


A final example of a type-and-declaration annotation is some \<@Nullable>
or \<@NonNull> annotations that are intended to work both with modern tools
that process type annotations and with old tools that were written before
Java had type annotations.  Such type-and-declaration annotations were a
temporary measure, intended to be used until the tool supported Java 8, and
should not be necessary any longer.


\subsectionAndLabel{How do I annotate a fully-qualified type name?}{faq-annotate-fully-qualified-name}

If you write a fully-qualified type name in your program, then the Java
language requires you to write a type annotation on the simple name part,
such as
\begin{Verbatim}
  entity.hibernate. @Nullable User x;
\end{Verbatim}

If you try to write the type annotation before the entire fully-qualified
name, such as
\begin{Verbatim}
  @Nullable entity.hibernate.User x;  // illegal Java syntax
\end{Verbatim}
\noindent
then you will get an error like one of the following:
\begin{Verbatim}
error: scoping construct for static nested type cannot be annotated
error: scoping construct cannot be annotated with type-use annotation
\end{Verbatim}


\subsectionAndLabel{What is the difference between type annotations and declaration annotations?}{faq-type-vs-declaration-annotations}

Java has two distinct varieties of annotation:  type annotations and
declaration annotations.

A \textbf{type annotation} can be written on any use of a \textbf{type}.
It conceptually creates a new, more specific type.
That is, it describes what values the type represents.

As an example, the \<int> type contains these values: ..., -2, -1, 0, 1, 2, ...  \\
The \<@Positive int> type contains these values:  1, 2, ...   \\
Therefore, \<@Positive int> is a subtype of \<int>.

A \textbf{declaration annotation} can be written on any \textbf{declaration} (a class, method, or variable).  It describes the thing being declared, but does not describe run-time values.  Here are examples of declaration annotations:

\begin{Verbatim}
    @Deprecated    // programmers should not use this class
    class MyClass { ... }

    @Override      // this method overrides a method in a supertype
    void myMethod() { ... }

    @SuppressWarnings(...) // compiler should not warn about the initialization expr
    int myField = INITIALIZATION-EXPRESSION;
\end{Verbatim}

Here are examples that use both a declaration annotation and a type annotation:

\begin{Verbatim}
    @Override
    @Regex String getPattern() { ... }

    @GuardedBy("myLock")
    @NonNull String myField;
\end{Verbatim}

Note that the type annotation describes the value, and the declaration annotation says something about the method or use of the field.

As a matter of style, declaration annotations are written on their own line, and type annotations are written directly before the type, on the same line.


\sectionAndLabel{Semantics of type annotations}{faq-semantics-section}


\subsectionAndLabel{How can I handle typestate, or phases of my program with different data properties?}{faq-typestate}

Sometimes, your program works in phases that have different behavior.  For
example, you might have a field that starts out null and becomes non-null
at some point during execution, such as after a method is called.  You can
express this property as follows:

\begin{enumerate}
\item
Annotate the field type as \refqualclass{checker/nullness/qual}{MonotonicNonNull}.
\item
Annotate the method that sets the field as \refqualclass{checker/nullness/qual}{EnsuresNonNull}\<(">\emph{\<myFieldName>}\<")>.
(If method \<m1> calls method \<m2>, which actually sets the field, then
you would probably write this annotation on both \<m1> and \<m2>.)
\item
Annotate any method that depends on the field being non-null as
\refqualclass{checker/nullness/qual}{RequiresNonNull}\<(">\emph{\<myFieldName>}\<")>.
The type-checker will verify that such a method is only called when the
field isn't null --- that is, the method is only called after the setting
method.
\end{enumerate}

You can also use a typestate checker (see
\chapterpageref{typestate-checker}), but they have not been as extensively
tested.


\subsectionAndLabel{Why are explicit and implicit bounds defaulted differently?}{faq-implicit-bounds}

The following two bits of code have the same semantics under Java, but are
treated differently by the Checker Framework's CLIMB-to-top defaulting
rules (Section~\ref{climb-to-top}):

\begin{Verbatim}
class MyClass<T> { ... }
class MyClass<T extends Object> { ... }
\end{Verbatim}

The difference is the annotation on the upper bound of the type argument
\<T>.  They are treated in the following way.

\begin{Verbatim}
class MyClass<T>                 ==  class MyClass<T extends @TOPTYPEANNO Object>
class MyClass<T extends Object>  ==  class MyClass<T extends @DEFAULTANNO Object>
\end{Verbatim}

\noindent
\<@TOPTYPEANNO> is the top annotation in the type qualifier hierarchy.  For
example, for the nullness type system, the top type annotation is
\<@Nullable>, as shown in Figure~\ref{fig-nullness-hierarchy}.
\<@DEFAULTANNO> is the default annotation for the type system.  For
example, for the nullness type system, the default type annotation is
\<@NonNull>.

In some type systems, the top qualifier and the default are the same.  For
such type systems, the two code snippets shown above are treated the same.
An example is the regular expression type system; see
Figure~\ref{fig-regex-hierarchy}.

The CLIMB-to-top rule reduces the code edits required to annotate an
existing program, and it treats types written in the program consistently.

When a user writes no upper bound, as in
\code{class C<T> \ttlcb\ ... \ttrcb},
then Java permits the class to be instantiated with any type parameter.
The Checker Framework behaves exactly the same, no matter what the default
is for a particular type system --- and no matter whether the user has
changed the default locally.

When a user writes an upper bound, as in
\code{class C<T extends OtherClass> \ttlcb\ ... \ttrcb},
then the Checker Framework treats this occurrence of \<OtherClass> exactly
like any other occurrence, and applies the usual defaulting rules.  Use of
\<Object> is treated consistently with all other types in this location and
all other occurrences of \<Object> in the program.

Here are some style guidelines:
\begin{itemize}
\item
  Omit the \<extends> clause when possible.  To indicate no constraints on
  type qualifiers, write \code{class MyClass<T>} rather than \code{class
    MyClass<T extends @TOPTYPEANNO Object>}.
\item
  When you write an \<Object> upper bound, give an explicit type annotation.
  That is, write \code{class C<T extends @DEFAULTANNO Object>
    \ttlcb\ ... \ttrcb} even though it is equivalent to writing
  \code{class C<T extends Object> \ttlcb\ ... \ttrcb}.

  If you write just \<extends Object>, then someone who is reading the code
  might think that it is irrelevant (which it is in plain Java).  Also,
  some IDEs will suggest removing it.
\end{itemize}


\subsectionAndLabel{Why are type annotations declared with \<@Retention(RetentionPolicy.RUNTIME)>?}{faq-runtime-retention}

Annotations such as \refqualclass{checker/nullness/qual}{NonNull} are
declared with
\<\sunjavadocanno{java.base/java/lang/annotation/Retention.html}{Retention}(RetentionPolicy.\sunjavadoc{java.base/java/lang/annotation/RetentionPolicy.html\#RUNTIME}{RUNTIME})>.  In other words,
these type annotations are available to tools at run time.  Such run-time
tools could check the annotations (like an \<assert> statement), type-check
dynamically-loaded code, check casts and \<instanceof> operations, resolve
reflection more precisely, or other tasks that we have not yet thought of.
Not many such tools exist today, but the annotation designers wanted to
accommodate them in the future.

\<RUNTIME> retention has negligible costs (no run-time dependency, minimal
increase in heap size).

For the purpose of static checking at compile time,
\sunjavadoc{java.base/java/lang/annotation/RetentionPolicy.html\#CLASS}{CLASS}
retention would be sufficient.  Note that
\sunjavadoc{java.base/java/lang/annotation/RetentionPolicy.html\#SOURCE}{SOURCE}
retention would not be sufficient, because of separate compilation: when
type-checking a class, the compiler needs to read the annotations on
libraries that it uses, and separately-compiled libraries are available to
the compiler only as class files.


\sectionAndLabel{Creating a new checker}{faq-create-a-checker-section}

\subsectionAndLabel{How do I create a new checker?}{faq-create-a-checker}

In addition to using the checkers that are distributed with the Checker
Framework, you can write your own checker to check specific properties that
you care about.  Thus, you can find and prevent the bugs that are most
important to you.

Chapter~\ref{creating-a-checker} gives
complete details regarding how to write a checker.  It also suggests places
to look for more help, such as the \href{../api/}{Checker Framework
API documentation (Javadoc)} and the source code of the distributed
checkers.

To whet your interest and demonstrate how easy it is to get started, here
is an example of a complete, useful type-checker.

\begin{Verbatim}
  @SubtypeOf(Unqualified.class)
  @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
  public @interface Encrypted {}
\end{Verbatim}

Section~\ref{subtyping-example} explains this checker and tells
you how to run it.


\subsectionAndLabel{What properties can and cannot be handled by type-checking?}{faq-type-properties}

In theory, any property about a program can be expressed and checked within
a type system.  In practice, types are a good choice for some properties
and a bad choice for others.

A type expresses the set of possible values for an expression.  Therefore,
types are a good choice for any property that is about variable values or
provenance.

Types are a poor choice for expressing properties about timing, such as
that action B will happen within 10 milliseconds of action A.  Types are
not good for verifying the results of calculations; for example, they could
ensure that code always call an \<encrypt> routine in the appropriate
places, but not that the \<encrypt> routine is correctly implemented.
Types are not a good solution for preventing infinite loops, except perhaps
in special cases.


\subsectionAndLabel{Why is there no declarative syntax for writing type rules?}{faq-declarative-syntax-for-type-rules}

A type system implementer can declaratively specify the type qualifier
hierarchy (Section~\ref{creating-declarative-hierarchy}) and the type introduction rules
(Section~\ref{creating-type-introduction}).  However, the Checker
Framework uses a procedural syntax for specifying type-checking
rules (Section~\ref{creating-extending-visitor}).
A declarative syntax might be more concise, more readable, and more
verifiable than a procedural syntax.

We have not found the procedural syntax to be the most important impediment
to writing a checker.

Previous attempts to devise a declarative syntax
for realistic type systems have failed; see a technical
paper~\cite{PapiACPE2008} for a discussion.  When an
adequate syntax exists, then the Checker Framework can be extended to
support it.


\sectionAndLabel{Tool questions}{faq-tool-section}


\subsectionAndLabel{How does pluggable type-checking work?}{faq-pluggable-type-checking}

The Checker Framework enables you to define a new type system.  It finds
errors, or guarantees their absence, by performing type-checking that is
similar to that already performed by the Java compiler.

Type-checking examines each statement of your program in turn, one at a time.
\begin{itemize}
\item
Expressions are processed bottom-up.  Given types for each sub-expression,
the type-checker determines whether the types are legal for the
expression's operator and determines the type of the expression.
% For example, if \<x> has type \<@Positive> and \<y> has type \<@Positive>,
% then the expression \<x + y> also has type @Positive.

\item
An assignment is legal if the type of the right-hand side is a subtype of
the declared type of the left-hand side.

\item
 At a method call, the arguments are legal if they can be assigned to the
 formal parameters (this is called a ``pseudo-assignment'' and it follows
 the normal rules for assignment).  The type of the method call is the
 declared type of the return type, where the method is declared.  If
 the method declaration is not annotated, then a default annotation is
 used.

\item
  Suppose that method \<Sub.m> overrides method \<Super.m>.
  %
  The return type of \<Sub.m> must be equal to or a subtype of the return
  type of \<Super.m> (this is called ``covariance'').
  %
  The type of formal parameter $i$ of \<Sub.m> must be equal to or a
  \emph{super}type of the type of formal parameter $i$ in \<Super.m> (this
  is called ``contravariance'').

\end{itemize}


\subsectionAndLabel{What classpath is needed to use an annotated library?}{faq-classpath-to-use-annotated-library}

Suppose that you distribute a library, which contains Checker Framework
annotations such as \<@Nullable>.  This enables clients of the library to
use the Checker Framework to type-check their programs.  To do so, they
must have the Checker Framework annotations on their classpath, for
instance by using the Checker Framework Compiler.

Clients who do not wish to perform pluggable type-checking do not need to
have the Checker Framework annotations
(\<checker-qual.jar>) in their classpath, either when compiling or running
their programs.

The JVM does not issue a link error if an annotation is not found when a
class is loaded.  (By contrast, the JVM does issue a link error if a
superclass, or a parameter/return/field type, is not found.)
Likewise, there is no problem compiling against a library even if the
library's annotations are not on the classpath.
These are properties of Java, and are not specific to the Checker
Framework's annotations.


\subsectionAndLabel{Why do \<.class> files contain more annotations than the source code?}{faq-classfile-annotations}

You may notice annotations such as \<@Pure> and \<@SideEffectFree> in
compiled \<.class> files even though the source code contains no
annotations.  These annotations are propagated from annotated libraries,
such as the JDK, to your code.

When an overridden method has a side effect annotation, the overriding
method must have one too.  If you do not write one explicitly, the Checker
Framework could issue a warning, or it could automatically add the missing
annotation.  It does the latter, for annotations declared with the
\refqualclass{framework/qual}{InheritedAnnotation} meta-annotation.

In addition, defaulted and inferred type qualifiers are written into
\<.class> files; see Section~\ref{effective-qualifier}.


\subsectionAndLabel{Is there a type-checker for managing checked and unchecked exceptions?}{faq-checked-exceptions}

It is possible to annotate exception types, and any type-checker built on the
Checker Framework enforces that type annotations are consistent between
\<throw> statements and \<catch> clauses that might catch them.

The Java compiler already enforces that all checked exceptions are caught
or are declared to be passed through, so you would use annotations to
express other properties about exceptions.

Checked exceptions are an example of a ``type and effect'' system, which is
like a type system but also accounts for actions/behaviors such as side
effects.  The GUI Effect Checker (\chapterpageref{guieffect-checker}) is a
type-and-effect system that is distributed with the Checker Framework.


\sectionAndLabel{Relationship to other tools}{faq-other-tools-section}


\subsectionAndLabel{Why not just use a bug detector (like FindBugs or Error Prone)?}{faq-type-checking-vs-bug-detectors}

A pluggable type-checker
is a verification tool that prevents or detects all errors of a given
variety.  If it issues no warnings, your code has no errors of a given
variety (for details about the guarantee, see
Section~\ref{checker-guarantees}).

An alternate approach is to use a bug detector such as
\href{https://errorprone.info/}{Error Prone},
\href{http://findbugs.sourceforge.net/}{FindBugs}~\cite{HovemeyerP2004,HovemeyerSP2005},
\href{http://jlint.sourceforge.net/}{Jlint}~\cite{Artho2001}, or
\href{https://pmd.github.io/}{PMD}~\cite{Copeland2005}, or the
tools built into Eclipse (see Section~\ref{faq-eclipse}) and IntelliJ\@.

A pluggable type-checker or verifier
differs from a bug detector in several ways:
\begin{itemize}
\item
  A type-checker reports \emph{all} errors in your code.  If a type-checker
  reports no warnings, then you have a guarantee (a proof) of correctness
  (Section~\ref{faq-no-absolute-guarantee}).

  A bug detector aims to find \emph{some} of the most obvious errors.  Even
  if a bug detector reports no warnings, there may still be errors in your
  code.

\item
  A type-checker requires you to annotate your code with type qualifiers,
  or to run an inference tool that does so for you.  That is, it requires
  you to write a specification, then it verifies that your code meets its
  specification.

  Some bug detectors do not require annotations.  This means that it may be
  easier to get started running a bug detector.  The tool makes guesses
  about the intended behavior of your code, leading to false alarms or
  missed alarms.

\item
  A verification tool may issue more warnings for a programmer to
  investigate.  Some bug detectors internally generate many warnings, then
  use heuristics to discard some of them.  The cost is missed alarms, when
  the tool's heuristics classified the warnings as likely false positives
  and discarded them.

\item
  A type-checker uses a more sophisticated and precise analysis.  For
  example, it can take advantage of method annotations and annotations on
  generic type parameters, such as \code{List<@NonNull String>}.  An
  example specific to the Nullness Checker (Section~\ref{nullness-checker},
  no other tool correctly handles map keys or initialization.

  A bug detector does a more lightweight analysis.  This means that a bug
  detector usually runs faster, giving feedback to the programmer more
  rapidly and avoiding slowdowns.  Its analysis is often narrow, avoiding
  properties that are tricky to reason about or that might lead to false
  alarms.  The cost is missed alarms, when analysis is too weak to find the
  errors.

\item
  Neither type checking nor bug detection subsumes the other.  A
  type-checker finds problems that a bug detector cannot.  A bug detector
  finds problems that a type-checker does not:  there is no need for the
  type-checker to address style rules, when a bug detector is adequate.

  If your code is important to you, it is advantageous to run both types of
  tools.

\end{itemize}

For a case study that compared the nullness analysis of FindBugs, Jlint,
PMD, and the Checker Framework, see section 6 of the paper
\href{https://homes.cs.washington.edu/~mernst/pubs/pluggable-checkers-issta2008.pdf}{``Practical pluggable types for Java''}~\cite{PapiACPE2008}.
The case study was on a well-tested program in daily use.  The Checker
Framework tool found 8 nullness errors (that is, null pointer
dereferences).  None of the other tools found any errors.  A follow-up 10
years later found that Eclipse's and IntelliJ's nullness analyses found 0
and 3 out of the 9 errors that the Nullness Checker found.

The
\href{https://checkerframework.org/jsr308/}{JSR 308}~\cite{JSR308-2008-09-12}
documentation also contains a discussion of related work.


\subsectionAndLabel{How does the Checker Framework compare with Eclipse's null analysis?}{faq-eclipse}

Eclipse comes with a
\href{http://help.eclipse.org/luna/index.jsp?topic=\%2Forg.eclipse.jdt.doc.user\%2Ftasks\%2Ftask-using_null_annotations.htm}{null analysis} that
can detect potential null pointer errors in your code.  Eclipse's built-in
analysis differs from the Checker Framework in several respects.

The Checker Framework's Nullness Checker
(see~\chapterpageref{nullness-checker}) is more precise:  it does a deeper
semantic analysis, so it issues fewer false positives than Eclipse.
Eclipse's nullness analysis is missing many features that the Checker
Framework supports, such as handling of map keys, partially-initialized
objects, method pre- and post-conditions, polymorphism, and a powerful
dataflow analysis.  These are essential for practical verification of
real-world code without poor precision.
Furthermore, Eclipse by default ignores unannotated code (even unannotated
parameters within a method that contains other annotations).
As a result, Eclipse is more useful for bug-finding than for verification,
and that is what the Eclipse documentation recommends.
% See heading "Interpretation of null annotations" under
% http://help.eclipse.org/neon/index.jsp?topic=%2Forg.eclipse.jdt.doc.user%2Ftasks%2Ftask-using_external_null_annotations.htm

Eclipse assumes by default that all code is multi-threaded, which cripples its local
type inference.  (This default can be turned off, however.)
The Checker Framework allows the user to
specify whether code will be run concurrently or not via the
\<-AconcurrentSemantics> command-line option (see
Section~\ref{faq-concurrency}).

The Checker Framework builds on javac, so it is easier to run in
integration scripts or in
environments where not all developers have installed Eclipse.
% It is possible to use ecj as one's compiler:
% https://wiki.eclipse.org/JDT/FAQ#Can_I_use_JDT_outside_Eclipse_to_compile_Java_code.3F

Eclipse handles only nullness properties and is not extensible, whereas the
Checker Framework comes with over 20 type-checkers (for a list,
see~\chapterpageref{introduction}) and is extensible to more properties.

There are also some benefits to Eclipse's null analysis.
It is faster than the Checker Framework, in part because it is less featureful.
It is built into Eclipse, so you do not have to add it to your build scripts.
Its IDE integration is tighter and slicker.

In a case study, the Nullness Checker found 9 errors in a program, and
Eclipse's analysis found 0.


\subsectionAndLabel{How does the Checker Framework compare with NullAway?}{faq-nullaway}

\href{https://github.com/uber/NullAway}{NullAway} is a lightweight, unsound
type-checker whose aim is similar to that of the Nullness Checker
(\chapterpageref{nullness-checker}).  For both tools, the user writes
nullness annotations, and then the tool checks them.

NullAway is faster than the Nullness Checker and requires fewer annotations.

NullAway is unsound:  even if NullAway issues no warnings, your code might
crash with a null pointer exception.  Two differences are that NullAway
makes unchecked assumptions about getter methods and NullAway assumes all
objects are always fully initialized.  NullAway forces all generic
arguments to be non-null, which is not an unsoundness but is less flexible
than the Nullness Checker.


\subsectionAndLabel{How does the Checker Framework compare with the JDK's \<Optional> type?}{faq-optional}

JDK 8 introduced the \sunjavadoc{java.base/java/util/Optional.html}{\code{Optional}}
class, a container that is either empty or contains a non-null value.
The Optional Checker (see Chapter~\ref{optional-checker}) guarantees that
programmers use \<Optional> correctly.

Section~\ref{nullness-vs-optional} explains the relationship between
nullness and \<Optional> and the benefits of each.


\subsectionAndLabel{How does pluggable type-checking compare with JML?}{faq-jml}

\href{http://www.eecs.ucf.edu/~leavens/JML/index.shtml}{JML}, the Java Modeling
Language~\cite{LeavensBR2006:JML}, is a language for writing formal
specifications.

\textbf{JML aims to be more expressive than pluggable type-checking.}
A programmer can write a JML specification that
describes arbitrary facts about program behavior.  Then, the programmer can
use formal reasoning or a theorem-proving tool to verify that the code
meets the specification.  Run-time checking is also possible.
By contrast, pluggable type-checking can express a more limited set of
properties about your program.  Pluggable type-checking annotations are
more concise and easier to understand.

\textbf{JML is not as practical as pluggable type-checking.}
The JML toolset is less mature.  For instance, if your code uses
generics or other features of Java 5, then you cannot use JML.
However, JML has a run-time checker, which the Checker Framework currently
lacks.


\subsectionAndLabel{Is the Checker Framework an official part of Java?}{faq-checker-framework-part-of-java}

The Checker Framework is not an official part of Java.
The Checker Framework relies on
type annotations, which are part of Java 8.  See the
\href{https://checkerframework.org/jsr308/jsr308-faq.html#pluggable-type-checking-in-java}{Type
  Annotations (JSR 308) FAQ} for more details.


\subsectionAndLabel{What is the relationship between the Checker Framework and JSR 305?}{faq-jsr-305}

JSR 305 aimed to define official Java names for some annotations, such as
\<@NonNull> and \<@Nullable>.  However, it did not aim to precisely define
the semantics of those annotations nor to provide a reference
implementation of an annotation processor that validated their use;
as a result, JSR 305 was of limited utility as a specification.
JSR 305 has been abandoned; there has been
no activity by its expert group since
% January
2009.

By contrast, the Checker Framework precisely defines the meaning of a set
of annotations and provides powerful type-checkers that validate them.
However, the Checker Framework is not an official part of the Java
language; it chooses one set of names, but another tool might choose other
names.

In the future, the Java Community Process might revitalize JSR 305 or
create a replacement JSR to standardize the names and
meanings of specific annotations, after there is more experience with their
use in practice.

% JSR 305 didn't specify the semantics of its annotations, and where it did
% they were idiosyncratic --- essentially mimicking the FindBugs tool, but
% not useful for any other defect detection tool.  A revitalization of JSR
% 305 would have to start over from scratch in order to clearly specify a
% semantics that is general and useful for a whole range of tools.
% The Java community does not yet understand all the subtleties well enough
% to set the annotations in stone in the Java specification yet; it is
% better for the community to experiment with different approaches, such as
% those of FindBugs, IntelliJ, Eclipse, and the Checker Framework, so that
% we can come to consensus before deciding on an official set.


The Checker Framework defines annotations \<@NonNull> and \<@Nullable> that
are compatible with annotations defined by JSR 305, FindBugs, IntelliJ, and
other tools; see Section~\ref{nullness-related-work}.


\subsectionAndLabel{What is the relationship between the Checker Framework and JSR 308?}{faq-jsr-308}

JSR 308, also known as the Type Annotations specification, dictates the
syntax of type annotations in Java SE 8:  how they are expressed in the
Java language.

JSR 308 does not define any type annotations such as \<@NonNull>, and it does
not specify the semantics of any annotations.  Those tasks are left to
third-party tools.  The Checker Framework is one such tool.


% LocalWords:  toolset AbstractCollection ConcurrentHashMap NullnessUtil
% LocalWords:  castNonNull createWidget backporting JCIP's GuardedBy Awarns PMD
% LocalWords:  ElementType nullness bytecodes Jlint Hashtable SuppressWarnings
%  LocalWords:  RegexUtil compareTo myA requiresB nullable java myobject
%  LocalWords:  multithreading myfield Regex NonEmpty Xmaxerrs Xmaxwarns
%  LocalWords:  MonotonicNonNull EnsuresNonNull myFieldName pre dev API's
%  LocalWords:  m1 m2 RequiresNonNull AconcurrentSemantics MyQual plugin
%  LocalWords:  MyClass MyMoreRestrictiveQual TOPTYPEANNO DEFAULTANNO api
%%  LocalWords:  OtherClass Goetz antipattern subclassed varargs regexes
%%  LocalWords:  featureful RetentionPolicy instanceof contravariance qual
%%  LocalWords:  NoSuchElementException binarySearch subclasses faq awarns
%%  LocalWords:  intExample1 intExample2 requiresPositive RUNTIME NullAway
%%  LocalWords:  IllegalFormatException typequals typedef runtime nullaway
%%  LocalWords:  covariance InheritedAnnotation someMethod jml jsr