Checker Framework Gradle Plugin

This plugin configures JavaCompile tasks to use the Checker Framework for pluggable type-checking.

Apply the plugin

Add the following to your build.gradle file:

plugins {
  // Checker Framework pluggable type-checking
  id("org.checkerframework").version("1.0.2")
}

If you are upgrading from plugin version 0.x to 1.x, see the migration guide.

The plugin supports Gradle version 7.3 and later, and it requires Java 17 or later. Although you must compile your project using at least Java 17, the compiled class files can be compatible with, and can run on, any version of Java.

The plugin is compatible with Gradle's configuration cache and with isolated projects.

Configuration

The Checker Framework version

You must specify which version of the Checker Framework to use.

• The Gradle developers recommend modifying two files. Add this to build.gradle:

  checkerFramework {
    version = libs.checker.framework.get().version
  }

  and add this to gradle/libs.versions.toml:

  [libraries]
  checker-framework = "org.checkerframework:checker:4.2.3"

• Alternatively, you can edit just one file. Add this to build.gradle:

  checkerFramework {
    version = "4.2.3"
  }

The special value "local" means to use a locally built version of the Checker Framework, in the directory named by the CHECKERFRAMEWORK environment variable.

The command-line argument -PcfVersion=... (where "..." is a version number or "local") overrides settings in Gradle build files.

Checker Framework jar files

Alternatively, you can directly specify which checker and checker-qual jar files to use. You must also set the Checker Framework version to the special value "dependencies". Put the following in your build.gradle file:

checkerFramework {
  version = "dependencies"
}

ext {
    versions = [
        eisopVersion: "3.49.5-eisop1",
    ]
}

dependencies {
    checkerQual("io.github.eisop:checker-qual:${versions.eisopVersion}")
    checkerFramework("io.github.eisop:checker:${versions.eisopVersion}")
}

Which checkers to run

You must specify which checkers to run, using the checkerFramework.checkers property.

For example, using Groovy syntax in a build.gradle file:

checkerFramework {
  checkers = [
    "org.checkerframework.checker.nullness.NullnessChecker",
    "org.checkerframework.checker.units.UnitsChecker"
  ]
}

The same example, using Kotlin syntax in a build.gradle.kts file:

// In Kotlin, you need to import CheckerFrameworkExtension explicitly:
import org.checkerframework.plugin.gradle.CheckerFrameworkExtension

configure<CheckerFrameworkExtension> {
    checkers = listOf(
        "org.checkerframework.checker.nullness.NullnessChecker",
        "org.checkerframework.checker.units.UnitsChecker"
    )
}

For a list of checkers, see the Checker Framework Manual.

Checker dependencies

If a checker you are running has any dependencies, use a checkerFramework dependency:

dependencies {
    checkerFramework("...")
}

For example, if you are using the Subtyping Checker with custom type qualifiers, you should add a checkerFramework dependency referring to the definitions of the custom qualifiers.

Providing additional options to the compiler

You can set the checkerFramework.extraJavacArgs property to pass additional options to the compiler when running a pluggable type-checker.

For example, to treat all warnings as errors and to use a stub file:

checkerFramework {
  extraJavacArgs = [
    "-Werror",
    "-Astubs=/path/to/my/stub/file.astub"
  ]
}

Whole-program inference

The Checker Framework's wpi2.sh script can infer annotations for your project. If you pass -Pwpi2 to your gradle invocation, then it will use the command-line arguments that wpi2.sh requires. See the Checker Framework manual for details.

Disabling the Checker Framework

You can completely disable the Checker Framework (e.g., when testing something unrelated) either in your build file or from the command line.

In your build file:

checkerFramework {
  skipCheckerFramework = true
}

From the command line, add -PskipCheckerFramework to your Gradle invocation. You can also pass -PskipCheckerFramework=false to enable the Checker Framework even if the configuration has skipCheckerFramework = true. You can also set the skipCheckerFramework project property in a gradle.properties file or via ext; in a multi-project build, see Project properties.

Disabling the Checker Framework for tests

By default, the plugin applies the selected checkers to all JavaCompile targets, including test targets such as testCompileJava.

Here is how to prevent checkers from being applied to test targets:

checkerFramework {
  excludeTests = true
}

A "test target" is one that contains "test" or "Test" as a word. Words are determined using camelCase; underscores (_) also delimit words.

Disabling the Checker Framework for a specific compile task

You can disable the Checker Framework for specific tasks. This can be useful for skipping the Checker Framework on generated code:

tasks.withType(JavaCompile).configureEach {
  // Don't run the checker on generated code.
  if (name.equals("compileMainGeneratedDataTemplateJava")
      || name.equals("compileMainGeneratedRestJava")) {
    options.checkerFrameworkCompile.enabled = false
  }
}

The only configuration available on a per-task basis is enabled.

Multi-project builds

In a project with subprojects, you should apply the plugin to each Java subproject (and to the top-level project, in the unlikely case that it is a Java project). Each subproject should configure the plugin itself, either directly or through a convention plugin. Do not configure the subprojects from the top-level build.gradle file, in a subprojects or allprojects block.

Per-subproject configuration

Apply the plugin in the build.gradle file of each subproject, as if the subproject were a stand-alone project. Use this if the subprojects need different configuration, such as different checkers.

A convention plugin

If the subprojects share configuration, put it in a convention plugin rather than repeating it in each subproject.

Write buildSrc/build.gradle:

plugins {
  id("groovy-gradle-plugin")
}

repositories {
  gradlePluginPortal()
}

dependencies {
  implementation("org.checkerframework:org.checkerframework.gradle.plugin:1.0.2")
}

Write buildSrc/src/main/groovy/my-checkerframework-conventions.gradle:

plugins {
  id("org.checkerframework")
}

repositories {
  mavenCentral()
}

// Change these to the checkers and Checker Framework version that you want.
checkerFramework {
  checkers = ["org.checkerframework.checker.index.IndexChecker"]
  version = "4.2.3"
}

Then each subproject's build.gradle file contains:

plugins {
  id("java-library")
  id("my-checkerframework-conventions")
}

A subproject can override the conventions in its own checkerFramework block. Every project configures only itself, so a convention plugin works with the configuration cache and with isolated projects.

Project properties

Set the cfVersion or skipCheckerFramework project property in the root project's gradle.properties file or on the command line; either one works in every subproject. Setting it via ext in the subproject's own build.gradle file, or in a gradle.properties file in the subproject's own directory, works for that subproject only.

A value given on the command line, as -PcfVersion=... or -PskipCheckerFramework=..., takes precedence over every other way of setting the property, including an assignment to ext in a build script.

Do not set either property in a way that only an ancestor project sees: via ext in the ancestor's build.gradle file, or in a gradle.properties file in the directory of an ancestor other than the root project. A subproject does not inherit such a setting. (Plugin version 1.0.2 and earlier did inherit such a setting. If your build relies on that, move the setting to the root project's gradle.properties file. Otherwise, a subproject uses the checkerFramework block's settings.)

Modules

When running the plugin on a Java project that uses modules, you need to add the annotations to the module path. This is necessary even if you write no annotations in your code, because the Checker Framework inserts inferred annotations into the bytecode.

Add the following to your module-info.java:

requires org.checkerframework.checker.qual;

The addition of requires is typically enough.

If it does not fix your compilation issues, you can additionally add the checker-qual.jar artifact (which contains only annotations) to the module path:

checkerFramework {
  configurations.compileOnly.setCanBeResolved(true)
  extraJavacArgs = [
    "--module-path", configurations.checkerQual.asPath
  ]
}

Lombok compatibility

This plugin automatically interacts with the Lombok Gradle Plugin to delombok your source code before it is passed to the Checker Framework for type-checking. This plugin does not support any other use of Lombok.

For the Checker Framework to work properly on delomboked source code, you must include the following key in your project's lombok.config file:

lombok.addLombokGeneratedAnnotation = true

By default, Lombok suppresses all warnings in the code it generates. If you want to typecheck the code that Lombok generates, set addSuppressWarnings to false:

lombok.addSuppressWarnings = false

Note that doing so will cause all tools (including javac itself) to begin issuing warnings in the code that Lombok generates.

Using a locally built plugin

To use a locally modified version of this plugin:

1. Publish the plugin to your local Maven repository:

   ./gradlew publishToMavenLocal

2. Add the following to the settings.gradle file of the Gradle project in which you want to use the plugin:

   pluginManagement {
       repositories {
           mavenLocal()
           gradlePluginPortal()
       }
   }

Migrating from 0.x to 1.x

If your project uses version 0.x of the Checker Framework Gradle Plugin, you need to make some changes in order to use version 1.x.

1. You must specify a version number.

2. You no longer need to add a checkerFramework dependency or add checker-qual to the compileOnly or testCompileOnly configurations. Remove code like the following:

   dependencies {
     compileOnly("org.checkerframework:checker-qual:${checkerFrameworkVersion}")
     testCompileOnly("org.checkerframework:checker-qual:${checkerFrameworkVersion}")
     checkerFramework("org.checkerframework:checker:${checkerFrameworkVersion}")
   }

3. These options have been removed:

   • suppressLombokWarnings: Use Lombok options to configure interaction with Lombok.

   • skipVersionCheck: There is no longer a version check that might cause a "zip file too large" error. Remove the -PskipVersionCheck command-line argument and remove Gradle code like

     checkerFramework {
       skipVersionCheck = true
     }

   • cfLocal: Set the version to "local" to use a locally built version of the Checker Framework. Change command-line argument -PcfLocal to -PcfVersion=local. (Note: The cfLocal functionality was not an official part of the plugin, but a number of projects use it.)

4. If you want to use a nonstandard Checker Framework jar file (such as that of eisop), see Checker Framework jar files.

Troubleshooting

ClassCastException for a javac class

If you encounter a crash with a ClassCastException referencing some internal javac class, disable incremental compilation in your build using the following code in your checkerFramework configuration block:

checkerFramework {
  incrementalize = false
}

Background: By default, the plugin assumes that all checkers are "isolating incremental annotation processors". This assumption speeds up builds by enabling incremental compilation. Gradle's documentation warns that incremental compilation with the Checker Framework plugin (or any other plugin that uses internal javac APIs) may crash, because Gradle wraps some of those APIs.

Incompatibility with Error Prone 2.3.4 and earlier

To use both Error Prone and the Checker Framework, you need to use Error Prone version 2.4.0 (released in May 2020) or later.