or run

npx @tessl/cli init

Version

Tile

Overview

Evals

Files

docs

concurrency.md constant-value.md contracts.md framework.md index-bounds.md index.md nullness.md optional.md resources.md signedness.md string-format.md units.md

tile.json

tessl/maven-org-checkerframework--checker-qual

Type qualifier annotations for the Checker Framework static analysis tool

Workspace: tessl
Visibility: Public
Created: 3 months ago
Last updated: 3 months ago
Describes: pkg:maven/org.checkerframework/checker-qual@3.49.x

To install, run

npx @tessl/cli install tessl/maven-org-checkerframework--checker-qual@3.49.0

Checker Qual

Checker Qual provides type qualifier annotations for the Checker Framework static analysis tool. It contains 358 annotations organized across 32 packages that enable developers to specify type qualifiers in their Java code for pluggable type-checking, catching potential bugs at compile time through enhanced static analysis.

This Knowledge Tile documents the major annotation categories including nullness checking, bounds validation, concurrency analysis, string format validation, framework meta-annotations, units checking, resource management, method contracts, optional value checking, signedness tracking, and constant value analysis.

Package Information

Package Name: org.checkerframework:checker-qual
Package Type: Maven
Language: Java
Installation:
- Maven: <dependency><groupId>org.checkerframework</groupId><artifactId>checker-qual</artifactId><version>3.49.5</version></dependency>
- Gradle: implementation 'org.checkerframework:checker-qual:3.49.5'

Core Imports

import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.framework.qual.DefaultFor;

For module-based projects:

module mymodule {
    requires org.checkerframework.checker.qual;
}

Basic Usage

import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.index.qual.NonNegative;

public class Example {
    // Method ensures non-null return value
    public @NonNull String getName(@Nullable String input) {
        return input != null ? input : "default";
    }
    
    // Array access with bounds checking
    public void processArray(int @NonNull [] array, @NonNegative int index) {
        if (index < array.length) {
            System.out.println(array[index]);
        }
    }
}

Architecture

Checker Qual is organized into several key areas:

Framework Annotations: Core meta-annotations for defining type qualifier hierarchies and behavior
Checker-Specific Annotations: Domain-specific annotations for nullness, bounds checking, locking, etc.
Common Utilities: Shared annotations used across multiple checkers
Dataflow Annotations: Annotations for method purity and side effects

The annotations work with the Checker Framework's pluggable type system to provide compile-time verification of program properties without runtime overhead.

Capabilities

Nullness Checking

Annotations for preventing null pointer exceptions through static analysis.

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface NonNull {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface Nullable {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface MonotonicNonNull {}

Nullness Annotations

Index and Bounds Checking

Annotations for ensuring array bounds safety and preventing index out of bounds exceptions.

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface NonNegative {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface IndexFor {
    String[] value();
}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface LTLengthOf {
    String[] value();
}

Index and Bounds Annotations

Concurrency and Locking

Annotations for thread safety and lock-based synchronization analysis.

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface GuardedBy {
    String[] value();
}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface LockHeld {}

@Target(ElementType.METHOD)
public @interface Holding {
    String[] value();
}

Concurrency Annotations

String and Format Validation

Annotations for validating string formats, regular expressions, and format strings.

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface Regex {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface Format {
    ConversionCategory[] value();
}

public enum ConversionCategory {
    UNUSED, GENERAL, CHAR, INT, FLOAT, TIME, CHAR_AND_INT, INT_AND_TIME
}

String and Format Annotations

Framework Meta-Annotations

Core annotations for defining type qualifier hierarchies and their behavior.

@Target(ElementType.ANNOTATION_TYPE)
public @interface SubtypeOf {
    Class<? extends Annotation>[] value();
}

@Target(ElementType.ANNOTATION_TYPE)
public @interface DefaultFor {
    TypeUseLocation[] value() default {};
    TypeKind[] typeKinds() default {};
    Class<?>[] types() default {};
}

public enum TypeUseLocation {
    FIELD, LOCAL_VARIABLE, PARAMETER, RETURN, UPPER_BOUND, LOWER_BOUND, OTHERWISE, ALL
}

Framework Annotations

Units and Physical Quantities

Annotations for dimensional analysis and physical unit checking.

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface Length {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface Mass {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface m {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface kg {}

Units Annotations

Resource Management

Annotations for tracking resource lifecycle and ensuring proper cleanup.

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface MustCall {
    String[] value();
}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface CalledMethods {
    String[] value();
}

@Target(ElementType.PARAMETER)
public @interface Owning {}

Resource Management Annotations

Method Contracts and Side Effects

Annotations for specifying method contracts, purity, and side effects.

@Target(ElementType.METHOD)
public @interface Pure {}

@Target(ElementType.METHOD)
public @interface SideEffectFree {}

@Target(ElementType.METHOD)
public @interface EnsuresNonNull {
    String[] value();
}

@Target(ElementType.METHOD)
public @interface RequiresNonNull {
    String[] value();
}

Method Contracts

Optional Value Checking

Annotations for validating Optional container states and preventing empty Optional access.

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface Present {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface MaybePresent {}

@Target(ElementType.METHOD)
public @interface EnsuresPresent {
    String[] value();
}

@Target(ElementType.METHOD)
public @interface RequiresPresent {
    String[] value();
}

Optional Checker

Initialization State Tracking

Annotations for tracking object initialization state during construction.

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface Initialized {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface UnderInitialization {
    Class<?> value() default Object.class;
}

Fake Enumeration (Fenum) Checking

Annotations for creating type-safe enumerations from integer constants.

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface Fenum {
    String value();
}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface SwingCompassDirection {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface AwtColorSpace {}

GUI Thread Safety

Annotations for ensuring GUI operations occur on appropriate threads.

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface UI {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface AlwaysSafe {}

@Target(ElementType.METHOD)
public @interface UIEffect {}

Taint Analysis

Annotations for tracking untrusted data flow and preventing injection attacks.

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface Tainted {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface Untainted {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface PolyTainted {}

Numeric Signedness

Annotations for distinguishing signed and unsigned integer interpretations.

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface Signed {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) 
public @interface Unsigned {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface SignedPositive {}

Signedness Checker

Constant Value Tracking

Annotations for tracking compile-time constant values and ranges of expressions.

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface IntVal {
    long[] value();
}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface StringVal {
    String[] value();
}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface IntRange {
    long from() default Long.MIN_VALUE;
    long to() default Long.MAX_VALUE;
}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface ArrayLen {
    int[] value();
}

Constant Value Checker

Type Definitions

// Core enums used throughout the framework
public enum TypeKind {
    PACKAGE, INT, BOOLEAN, CHAR, DOUBLE, FLOAT, LONG, SHORT, BYTE
}

public enum LiteralKind {
    ALL, BOOLEAN, CHAR, DOUBLE, FLOAT, INT, LONG, NULL, STRING, PRIMITIVE
}

// Common annotation patterns
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@Retention(RetentionPolicy.RUNTIME)
@Documented
public @interface AnnotationTemplate {}