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 2.1 and 2.2.
1. The programmer writes annotations, such as @NonNull and @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 Chapter 35.) It is possible to
annotate only part of your code: see Section 2.4.6.
2. The checker reports whether the program contains any erroneous code — that is, code that is inconsistent with the annotations.
This chapter is structured as follows:
• Section 2.1: How to write annotations
• Section 2.2: How to run a checker
• Section 2.3: What the checker guarantees
• Section 2.4: Tips about writing annotations
Additional topics that apply to all checkers are covered later in the manual:
• Chapter 33: Advanced type system features
• Chapter 34: Suppressing warnings
• Chapter 36: Annotating libraries
• Chapter 37: How to create a new checker
• Chapter 39: Integration with external tools
There is a tutorial that walks you through using the Checker Framework on the command line.
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:
@Interned String intern(){...}// return value int compareTo(@NonNull String other){...}// parameter String toString(@Tainted MyClass this){...}// receiver ("this" parameter) @NonNull List<@Interned String> messages; // generics: non-null list of interned Strings @Interned String @NonNull [] messages; // arrays: non-null array of interned Strings myDate = (@Initialized Date) beingConstructed; // cast
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 33.7.
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.
To run a checker, run the compiler javac as usual, but either pass the -processor plugin_class command-line option, or use auto-discovery as described in Section 2.2.3. (If your
project already uses auto-discovery for some annotation processor, such as AutoValue, then you should use auto-discovery.) Two concrete examples of using -processor to run the Nullness Checker are
javac -processor nullness MyFile.java
javac -processor org.checkerframework.checker.nullness.NullnessChecker MyFile.java
where javac is as specified in Section 39.6.
You can also run a checker from within your favorite IDE or build system. See Chapter 39 for details about build tools such as Ant (Section 39.3), Buck (Section 39.5), Bazel (Section 39.4), Gradle (Section 39.9), Maven (Section 39.13), and sbt (Section 39.15); IDEs such as Eclipse (Section 39.8), IntelliJ IDEA (Section 39.10), NetBeans (Section 39.14), and tIDE (Section 39.16); 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 Java files of yours, if they are more recent than the corresponding .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 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 -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.
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 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 Chapter 36.)
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/src/main/resources/, then pass the command-line option
-Astubs=checker.jar/stubfilename.astub. The “checker.jar” should be literal — don’t provide a path. This special syntax only works for “checker.jar”.
The annotated libraries that are provided as class files appear in the org.checkerframework.annotatedlib group in the Maven Central Repository. The annotated
library has identical behavior to the upstream, unannotated version; the source code is identical other than added annotations. (Some of the annotated libraries are bcel, commons-csv, commons-io, guava, and java-getopt.)
To use an annotated library:
• If your project stores .jar files locally, then download the .jar file from the Maven Central Repository.
• 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
api("org.apache.bcel:bcel:6.3.1")
api("commons-io:commons-io:2.8")
to
api("org.checkerframework.annotatedlib:bcel:6.3.1")
api("org.checkerframework.annotatedlib:commons-io:2.8.0.1")
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 open an issue requesting that the org.checkerframework.annotatedlib version be updated.
There is one special case. If an .astub file is shipped with the Checker Framework in checker/src/main/resources/, then you can use -Astubs=checker.jar/stubfilename.astub. The “checker.jar” should be literal — don’t provide
a path. (This special syntax only works for “checker.jar”.)
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
-ANullnessChecker_lint=redundantNullComparison
-Aorg.checkerframework.checker.guieffect.GuiEffectChecker_lint=debugSpew
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.
Unsound checking: ignore some errors
• -AsuppressWarnings Suppress all errors and warnings matching the given key; see Section 34.3.
• -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 34.4.
• -AskipDefs, -AonlyDefs Suppress all errors and warnings within the definition of given classes — or everywhere except within the definition of given classes. See Section 34.5.
• -AskipFiles, -AonlyFiles Suppress all errors and warnings within given files or directories/folders — or everywhere except within given files or directories/folders. See Section 34.6.
• -AassumeSideEffectFree, -AassumeDeterministic, -AassumePure, -AassumePureGetters Unsoundly assume that every method is side-effect-free, deterministic, or both; or that every getter method is pure. See Section 23.4 and Section 33.7.5.
• -AassumeAssertionsAreEnabled, -AassumeAssertionsAreDisabled Whether to assume that assertions (Java assert statements) are enabled or disabled; see Section 33.7.6.
• -AignoreRangeOverflow Ignore the possibility of overflow for range annotations such as @IntRange; see Section 24.4.
• -Awarns Treat checker errors as warnings. If you use this, you may wish to also supply -Xmaxwarns 10000, because by default javac prints at most 100 warnings. If you use this, don’t supply -Werror, which is a javac argument to halt compilation if a
warning is issued.
• -AignoreInvalidAnnotationLocations Ignore annotations in bytecode that have invalid annotation locations.
More sound (strict) checking: enable errors that are disabled by default
• -AcheckPurityAnnotations Check the bodies of methods and constructors marked @SideEffectFree, @Deterministic, and @Pure to ensure the method or constructor
satisfies the annotation. By default, the Checker Framework unsoundly trusts the annotation. See Section 33.7.5.
• -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 33.1.
• -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 32.1.6 and Section 33.1.
• -AuseConservativeDefaultsForUncheckedCode Enables conservative defaults, and suppresses all type-checking warnings, in unchecked code. Takes arguments “source,bytecode”. “-source,-bytecode” is the (unsound) default setting.
– “bytecode” specifies whether the checker should apply conservative defaults to bytecode (that is, to already-compiled libraries); see Section 33.5.6.
– Outside the scope of any relevant @AnnotatedFor annotation, “source” specifies whether conservative default annotations are applied to source code and suppress all
type-checking warnings; see Section 36.4.
• -AconcurrentSemantics Whether to assume concurrent semantics (field values may change at any time) or sequential semantics; see Section 40.4.6.
• -AignoreRawTypeArguments=false Do not ignore subtype tests for type arguments that were inferred for a raw type. See Section 32.1.1.
• -processor org.checkerframework.common.initializedfields.InitializedFieldsChecker,... Ensure that all fields are initialized by the constructor. See Chapter 27.
Type-checking modes: enable/disable functionality
• -Alint Enable or disable optional checks; see Section 34.7.
• -AwarnRedundantAnnotations Warn about redundant annotations. A warning is issued if an explicitly written annotation is the same as the default annotation for that location. This feature does not warn about all redundant annotations, only some.
• -AsuggestPureMethods Suggest methods that could be marked @SideEffectFree, @Deterministic, or @Pure; see Section 33.7.5.
• -AresolveReflection Determine the target of reflective calls, and perform more precise type-checking based on that information; see Chapter 26. -AresolveReflection=debug causes
debugging information to be output.
• -Ainfer=outputformat Output suggested annotations for method signatures and fields. These annotations may reduce the number of type-checking errors on subsequent type-checking runs. This option is typically used by whole-program inference (WPI; see Section 35.2) rather than by programmers. 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.
• -AinferOutputDirectory The directory into which to write inference output (e.g., .ajava files). It defaults to build/whole-program-inference. When using a build system (e.g., Gradle), the default may be interpreted relative to a build system directory (e.g.,
$HOME/.gradle/workers) rather than the project root directory, so you may need to provide an absolute path.
• -AinferOutputOriginal When outputting .ajava files when running with -Ainfer=ajava, also output a copy of the original file with no inferred annotations, but with the formatting of a .ajava file, to permit use of diff to view the inferred
annotations. Must be combined with -Ainfer=ajava.
• -AshowSuppressWarningsStrings With each warning, show all possible strings to suppress that warning.
• -AwarnUnneededSuppressions Issue an unneeded.suppression warning for each @SuppressWarnings that did not suppress a warning issued by the checker. This only warns about @SuppressWarnings strings that contain a checker name other than
"allcheckers" (for syntax, Section 34.1.1). The -ArequirePrefixInWarningSuppressions command-line argument ensures that all @SuppressWarnings
strings contain a checker name. An unneeded.suppression warning can be suppressed only by @SuppressWarnings("unneeded.suppression") or @SuppressWarnings("checkername:unneeded.suppression"), not by
@SuppressWarnings("checkername") and not by a partial message key such as @SuppressWarnings("suppression").
• -AwarnUnneededSuppressionsExceptions=regex disables -AwarnUnneededSuppressions for @SuppressWarnings strings that contain a match for the regular expression. Most users don’t need this.
• -ArequirePrefixInWarningSuppressions Require that the string in a warning suppression annotation begin with a checker name. Otherwise, the warning suppression annotation does not suppress any warnings. For example, if this command-line option is supplied, then
@SuppressWarnings("assignment") has no effect, but @SuppressWarnings("nullness:assignment") does.
• -AshowPrefixInWarningMessages When issuing an error or warning, prefix the warning suppression key by the checker name. For instance, output “error: [nullness:assignment] ...” instead of “error: [assignment]”. This makes it easy to tell, from the suppression key only, which checker issued the
error or warning.
Partially-annotated libraries
• -Astubs List of stub files or directories; see Section 36.5.1.
• -AstubWarnIfNotFound, -AstubNoWarnIfNotFound, -AstubWarnIfNotFoundIgnoresClasses, -AstubWarnIfRedundantWithBytecode, -AstubWarnNote Warn about problems with stub files; see Section 36.5.7.
• -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 36.5.2.
• -AuseConservativeDefaultsForUncheckedCode=source Outside the scope of any relevant @AnnotatedFor annotation, use conservative default annotations and
suppress all type-checking warnings; see Section 36.4.
Debugging
• -AprintAllQualifiers, -AprintVerboseGenerics, -Anomsgtext, -Aonelinemsg, -AdumpOnErrors, -AexceptionLineSeparator Amount of detail in messages; see Section 37.12.1.
• -Adetailedmsgtext Format of diagnostic messages; see Section 37.12.2.
• -Aignorejdkastub, -ApermitMissingJdk, -AparseAllJdk, -AstubDebug Stub and JDK libraries; see Section 37.12.3.
• -Afilenames, -Ashowchecks, -AshowWpiFailedInferences Progress tracing; see Section 37.12.4.
• -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 37.12.5.
• -Aflowdotdir, -Averbosecfg, -Acfgviz Draw a visualization of the CFG (control flow graph); see Section 37.12.6.
• -AresourceStats, -AatfDoNotCache, -AatfCacheSize Miscellaneous debugging options; see Section 37.12.7.
• -AslowTypecheckingSeconds=N Print a warning for any program construct, such as a method or class, whose type-checking takes more than N seconds (default 45). Often, generic type inference is the slowest part of type-checking, and you can significantly speed up type-checking by explicitly
writing a few generic type arguments.
• -Aversion Print the Checker Framework version.
• -AprintGitProperties Print information about the git repository from which the Checker Framework was compiled.
Some checkers support additional options, which are described in that checker’s manual section. For example, -Aquals tells the Subtyping Checker (see Chapter 30) and the Fenum Checker (see Chapter 9) which annotations to check.
Here are some standard javac command-line options that you may find useful. Many of them contain “processor” or “proc”, because in javac jargon, a checker is an “annotation processor”.
• -processor Names the checker to be run; see Sections 2.2 and 2.2.4. 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.
• -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 30.2) and classes that define
statically-executable methods used by the Constant Value Checker (see Section 24.2.2).
• -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 2.2.3.
• -implicit:class Suppresses warnings about implicitly compiled files (not named on the command line); see Section 39.3.
• -J Supply an argument to the JVM that is running javac; for example, -J-Xmx4g to increase its maximum heap size.
• -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.
“Auto-discovery” makes the javac compiler always run an annotation processor, such as a checker plugin, without explicitly passing the -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. (Alternately, if you prefer to use a
-processor command-line argument, you will need to specify all annotation processors, including ones that used to be auto-discovered.)
To enable auto-discovery, place a configuration file named 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:
org.checkerframework.checker.nullness.NullnessChecker
org.checkerframework.checker.interning.InterningChecker
You can disable this auto-discovery mechanism by passing the -proc:none command-line option to javac, which disables all annotation processing including all pluggable type-checking.
Ordinarily, javac’s -processor flag requires fully-qualified class names. When using the Checker Framework javac wrapper (Section 39.6), you may omit the package name and the
Checker suffix. The following three commands are equivalent:
javac -processor org.checkerframework.checker.nullness.NullnessChecker MyFile.java javac -processor NullnessChecker MyFile.java javac -processor nullness MyFile.java
This feature also works when multiple checkers are specified. Their names are separated by commas, with no surrounding space. For example:
javac -processor NullnessChecker,RegexChecker MyFile.java javac -processor nullness,regex MyFile.java
This feature does not apply to javac @argfiles.
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 3) guarantees lack of null pointer exceptions (Java NullPointerException). More precisely, it guarantees that expressions whose type is annotated with @NonNull never evaluate to null, and it forbids other expressions from being dereferenced.
As another example, the Interning Checker (Chapter 6) guarantees that correct equality tests are performed. More precisely, it guarantees that every expression whose type is an @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.
• 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:
– Code compiled without the -processor switch. This includes external libraries supplied as a .class file and native methods (because the implementation is not Java code, it cannot be checked).
– Code compiled with the -AskipUses, -AonlyUses, -AskipDefs, -AonlyDefs, -AskipFiles, or -AonlyFiles command-line arguments (see Chapter 34).
– Dynamically generated code, such as code generated by Spring or MyBatis. Its bytecode is directly generated and run, not compiled by javac and not visible to the Checker Framework.
In each of these cases, any 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.
• You can suppress warnings, such as via the @SuppressWarnings annotation (Chapter 34). If you do so incorrectly, the checker’s guarantee no longer holds.
• 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 2.2.2. You can supply a command-line argument to make the Checker Framework sound for each of these cases.
• Specific checkers may have other limitations; see their documentation for details.
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:
@Nullable Object x = ...;
x.toString(); // warning
x.toString(); // no warning
The second call to toString cannot possibly throw a null pointer exception — 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.)
If you find that a checker fails to issue a warning that it should, then please report a bug (see Section 41.2).
Section 36.1 gives additional tips that are specific to annotating a third-party library.
Before you run a checker, annotate the code, based on its documentation. Then, run the checker to uncover bugs in the code or the documentation.
Don’t do the opposite, which is to run the checker and then add annotations according to the warnings issued. This approach is less systematic, so you may overlook some annotations. It often leads to confusion and poor results. It leads users to make changes not for any principled reason, but to “make the type-checker happy”, even when the changes are in conflict with the documentation or the code. Also see “Annotations are a specification”, below.
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.
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 34.4 and 34.5 give ways to skip checking of some files, directories, or packages. Section 2.4.6 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 40.1.2).
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 2.4.3 and 2.4.4 give more tips about writing specifications.
For each class, read its Javadoc. For instance, if you are adding annotations for the Nullness Checker (Chapter 3), 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 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 callers. 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. 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 callers, 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 36 tells you how to annotate libraries that your code uses. Section 2.4.5 and Chapter 34 tell you what to do when you are unable to eliminate checker warnings by adding annotations.
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 List; use parameterized types like List<String> instead (Section 32.1.1). 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.
• Do not annotate local variables unless necessary. The checker infers annotations for local variables (see Section 33.7). 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).
• Do not write annotations that are redundant with defaults. For example, when checking nullness (Chapter 3), the default annotation is @NonNull, in most locations other than some type bounds (Section 33.5.3). 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:
// The below code increments variable i by adding 1 to it. i++;
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.
• 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 2.4.5 discusses what to do when a checker issues a warning about your code.
You should use annotations to specify normal behavior. The annotations indicate all the values that you want to flow to a reference — not every value that might possibly flow there if your program has a bug.
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:
/** @throws NullPointerException if arg is null */
void m1(Object arg) {
arg.toString();
...
}
Therefore, the type of arg should be @NonNull Object — you can write this as just Object, because @NonNull is the default. The Nullness Checker (Chapter 3) prevents null
pointer exceptions by warning you whenever a client passes a value that might cause m1 to crash.
Here is another method:
/** @throws NullPointerException if arg is null */
void m2(Object arg) {
Objects.requireNonNull(arg);
...
}
Method m2 behaves just like m1 in that it throws NullPointerException if a client passes null. Therefore, their specifications should be identical (the formal parameter type is annotated with @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 null as an argument. Examples include:
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)
org.junit.jupiter.api.Assert.assertNotNull(Object)
Their formal parameter types are 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 @Nullable because passing 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.
Optional example Another example is the Optional Checker (Chapter 5) and the orElseThrow() method. The goal of the Optional Checker is to ensure that the program does not crash due to use of a non-present
Optional value. Therefore, the receiver of orElseThrow() is annotated as @Present, and the Optional Checker issues an error if the client calls
orElseThrow() on a @MaybePresent value. (For details, see Section 5.3.)
Permitting crashes in some called methods 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.
• The -AskipUses command-line argument (Section 34.4) skips checking all method calls to one or more classes.
• A stub file (Section 36.5) can override the library’s annotations, for one or more methods.
As a special case, if you want the Nullness Checker to prevent most null pointer exceptions in your code, but to permit null pointer exceptions at nullness assertion methods, you can pass -Astubs=permit-nullness-assertion-exception.astub.
• 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.
If a method can possibly throw an exception because its parameter is null, then that parameter’s type should be @NonNull, which guarantees that the type-checker will issue a warning for every client use that has the potential to cause an exception. Don’t write
@Nullable on the parameter just because there exist some executions that don’t necessarily throw an exception.
An annotation indicates a guarantee that a client can depend upon. A subclass is not permitted to weaken the contract; for example, if a method accepts null as an argument, then every overriding definition must also accept null. A subclass is permitted to
strengthen the contract; for example, if a method does not accept null as an argument, then an overriding definition is permitted to accept null.
As a bad example, consider an erroneous @Nullable annotation in com/google/common/collect/Multiset.java (the annotation was subsequently changed to the more correct @ParametricNullness):
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);
There exist implementations of Multiset that permit null elements, and implementations of Multiset that do not permit null elements. A client with a variable Multiset ms does not know which variety of Multiset ms refers to. However, the
@Nullable annotation promises that ms.add(null, 1) is permissible. (Recall from Section 2.4.3 that annotations should indicate normal behavior.)
If parameter element on line 141 were to be annotated, the correct annotation would be @NonNull. Suppose a client has a reference to the same Multiset ms. The only way the client can be sure not to throw an exception is to pass only non-null elements to
ms.add(). A particular class that implements Multiset could declare add to take a @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-null value to
add(), and may also pass null.
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
class MyNullPermittingMultiset implements Multiset<@Nullable Object> { ... }
class MyNullProhibitingMultiset implements Multiset<@NonNull Object> { ... }
or, more generally, as
class MyNullPermittingMultiset<E extends @Nullable Object> implements Multiset<E> { ... }
class MyNullProhibitingMultiset<E extends @NonNull Object> implements Multiset<E> { ... }
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 E in Multiset.
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:
There is a bug in your code, such as a possible null dereference. Fix your code to prevent that crash.
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 Chapter 36).
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. (Recall that the checker works modularly: when type-checking a method m, it relies on the types and signatures of variables and methods used by m,
but not the initialization expressions or the method bodies.)
If possible, rewrite your code to be simpler for the checker to analyze; this is likely to make it easier for people to understand, too. If that is not possible, suppress the warning (see Chapter 34); 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.
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 41.1.4 and Chapter 41, Troubleshooting. In particular, Section 41.1.4 explains this same methodology in different words.)
Step 1: Explain correctness: write a proof Write an explanation of why your code is correct and why 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, such as 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).
Step 2: Translate the proof into annotations Here are some examples of the translation.
• If your proof includes “variable x is never null at run time”, then annotate x’s type with @NonNull.
• If your proof includes “method foo always returns a legal regular expression”, then annotate foo’s return type with @Regex.
• 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 @PolyNull.
• If your proof includes “method processOptions has already been called and it set field tz1”, then annotate processOptions’s declaration with @EnsuresNonNull("tz1").
• If your proof includes “method isEmpty returned false, so its argument must have been non-null”, then annotate isEmpty’s declaration with @EnsuresNonNullIf(expression="#1",result=false).
• If your proof includes “method m has no side effects”, then annotate m’s declaration with @SideEffectFree.
• If your proof includes “each call to method m returns the same value”, then annotate m’s declaration with @Deterministic.
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 Chapter 36.
Don’t omit any parts of your proof. When the Checker Framework analyzes a method, it examines only the signature/specification (not the implementation) 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 indices might be
null”. In this case, you have two choices. First, you can suppress the warning (Chapter 34); be sure to write a comment explaining your reasoning for suppressing the warning. You may wish to submit a
feature request (Section 41.2) 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.
Step 3: Re-run the checker 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 (Chapter 34). 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 41.2).
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. 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 3) will warn whenever an unannotated method result is used in a non-null context:
@NonNull Object myvar = unannotated_method(); // WARNING: unannotated_method may return null
If the call can return null, you should fix the bug in your program by removing the @NonNull annotation in your own program.
If the call never returns null, you have two choices: annotate the library or suppress warnings.
1. To annotate the library:
• 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 @SuppressWarnings annotation (Section 34.1) or
not running the checker on that file, for example via the -AskipDefs command-line option (Section 34.5).
• To annotate a library whose source code you do not have or cannot change, see Chapter 36.
2. To suppress all warnings related to uses of unannotated_method, use the -AskipUses command-line option (Section 34.4). Beware: a carelessly-written regular expression may suppress more warnings
than you intend.