The Checker Framework enhances Java’s type system to make it more powerful and useful. This lets software developers detect and prevent errors in their Java programs.
A “checker” is a compile-time tool that warns you about certain errors or gives you a guarantee that those errors do not occur. The Checker Framework comes with checkers for specific types of errors:
1. Nullness Checker for null pointer errors (see Chapter 3)
2. Initialization Checker to ensure all @NonNull fields are set in the constructor (see Section 3.8)
3. Map Key Checker to track which values are keys in a map (see Chapter 4)
4. Optional Checker for errors in using the Optional type (see Chapter 5)
5. Interning Checker for errors in equality testing and interning (see Chapter 6)
6. Called Methods Checker for the builder pattern (see Chapter 7)
7. Resource Leak Checker for ensuring that resources are disposed of properly (see Chapter 8)
8. Fake Enum Checker to allow type-safe fake enum patterns and type aliases or typedefs (see Chapter 9)
9. Tainting Checker for trust and security errors (see Chapter 12)
10. SQL Quotes Checker to mitigate SQL injection attacks (see Chapter 13)
11. Lock Checker for concurrency and lock errors (see Chapter 10)
12. Index Checker for array accesses (see Chapter 11)
13. Regex Checker to prevent use of syntactically invalid regular expressions (see Chapter 14)
14. Format String Checker to ensure that format strings have the right number and type of % directives (see Chapter 15)
15. Internationalization Format String Checker to ensure that i18n format strings have the right number and type of {} directives (see
Chapter 16)
16. Property File Checker to ensure that valid keys are used for property files and resource bundles (see Chapter 17)
17. Internationalization Checker to ensure that code is properly internationalized (see Section 17.2)
18. Signature String Checker to ensure that the string representation of a type is properly used, for example in Class.forName (see Chapter 18)
19. GUI Effect Checker to ensure that non-GUI threads do not access the UI, which would crash the application (see Chapter 19)
20. Units Checker to ensure operations are performed on correct units of measurement (see Chapter 20)
21. Signedness Checker to ensure unsigned and signed values are not mixed (see Chapter 21)
22. Modifiability Checker to warn about a possible UnsupportedOperationException at run time when modifying a collection (see Chapter 22)
23. Purity Checker to identify whether methods have side effects (see Chapter 23)
24. Constant Value Checker to determine whether an expression’s value can be known at compile time (see Chapter 24)
25. Reflection Checker to determine whether an expression’s value (of type Method or Class) can be known at compile time (see Chapter 26)
26. Initialized Fields Checker to ensure all fields are set in the constructor (see Chapter 27)
27. Aliasing Checker to identify whether expressions have aliases (see Chapter 28)
28. Must Call Checker to over-approximate the methods that should be called on an object before it is de-allocated (see Chapter 29)
29. Subtyping Checker for customized checking without writing any code (see Chapter 30)
30. Third-party checkers that are distributed separately from the Checker Framework (see Chapter 31)
These checkers are easy to use and are invoked as arguments to javac.
The Checker Framework also enables you to write new checkers of your own; see Chapters 30 and 37.
If you wish to get started using some particular type system from the list above, then the most effective way to read this manual is:
• Read just one of the descriptions of a particular type system and its checker (Chapters 3–31).
• Skim the advanced material that will enable you to make more effective use of a type system (Chapters 32–41), so that you will know what is available and can find it later. Skip Chapter 37 on creating a new checker.
Java’s built-in type-checker finds and prevents many errors — but it doesn’t find and prevent enough errors. The Checker Framework lets you define new type systems and run them as a plug-in to the javac compiler. Your code stays completely backward-compatible: your code compiles with any Java compiler, it runs on any JVM, and your coworkers don’t have to use the enhanced type system if they don’t want to. You can check part of your program, or the whole thing. Type inference tools exist to help you annotate your code; see Chapter 35.
Most programmers will use type systems created by other people, such as those listed at the start of the introduction (Chapter 1). Some people, called “type system designers”, create new type systems (Chapter 37). The Checker Framework is useful both to programmers who wish to write error-free code, and to type system designers who wish to evaluate and deploy their type systems.
This document uses the terms “checker” and “type-checking compiler plugin” as synonyms.
This section describes how to install the Checker Framework.
• If you use a build system that automatically downloads dependencies, such as Gradle or Maven, no installation is necessary; just see Chapter 39.
• If you wish to try the Checker Framework without installing it, use the Checker Framework Live Demo webpage.
• This section describes how to install the Checker Framework from its distribution. The Checker Framework release contains everything that you need, both to run checkers and to write your own checkers.
• Alternately, you can build the latest development version from source (Section 41.3).
Requirement: You must have a JDK (version 17 or later) installed.
The installation process has two required steps and one optional step.
1. Download the Checker Framework distribution: https://checkerframework.org/checker-framework-4.3.0.zip
For example, on Unix you can run: wget https://checkerframework.org/checker-framework-4.3.0.zip
2. Unzip it to create a checker-framework-4.3.0 directory.
For example, on Unix you can run: unzip checker-framework-4.3.0.zip
3. Configure your IDE, build system, or command shell to include the Checker Framework on the classpath. Choose the appropriate section of Chapter 39.
Now you are ready to start using the checkers.
We recommend that you work through the Checker Framework tutorial, which demonstrates the Nullness, Regex, and Tainting Checkers.
Section 1.4 walks you through a simple example. More detailed instructions for using a checker appear in Chapter 2.
The Checker Framework is released on a monthly schedule. The minor version (the middle number in the version number) is incremented if there are any incompatibilities with the previous version, including in user-visible behavior or in methods that a checker implementation might call.
This section gives a very simple example of running the Checker Framework. There is also a tutorial that you can work along with.
Let’s consider this very simple Java class. The local variable ref’s type is annotated as @NonNull, indicating that ref must be a reference to a non-null
object. Save the file as GetStarted.java.
import org.checkerframework.checker.nullness.qual.*;
public class GetStarted {
void sample() {
@NonNull Object ref = new Object();
}
}
If you run the Nullness Checker (Chapter 3), the compilation completes without any errors.
Now, introduce an error. Modify ref’s assignment to:
@NonNull Object ref = null;
If you run the Nullness Checker again, it emits the following error:
GetStarted.java:5: incompatible types.
found : @Nullable <nulltype>
required: @NonNull Object
@NonNull Object ref = null;
^
1 error
This is a trivially simple example. Even an unsound bug-finding tool like SpotBugs or Error Prone could have detected this bug. The Checker Framework’s analysis is more powerful than those tools and detects more code defects than they do.
Type qualifiers such as @NonNull are permitted anywhere that you can write a type, including generics and casts; see Section 2.1. Here are some examples:
@Interned String intern(){...}// return value int compareTo(@NonNull String other){...}// parameter @NonNull List<@Interned String> messages; // non-null list of interned Strings