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

Type qualifier annotations for the Checker Framework static analysis tool

—

Pending

Overview

Eval results

Files

Framework Annotations

Name: tessl/maven-org-checkerframework--checker-qual
Author: tessl

Framework annotations are meta-annotations used to define type qualifier hierarchies and their behavior in the Checker Framework. These annotations control how type qualifiers are applied, inherited, and interact with each other.

Capabilities

Type Hierarchy Definition

Annotations for defining subtype relationships between qualifiers.

/**
 * Specifies the supertypes of the annotated qualifier in the type hierarchy
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.ANNOTATION_TYPE)
public @interface SubtypeOf {
    Class<? extends Annotation>[] value();
}

/**
 * Indicates that the annotated qualifier is the default qualifier in its hierarchy
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.ANNOTATION_TYPE)
public @interface DefaultQualifierInHierarchy {}

/**
 * Makes a qualifier polymorphic, adapting based on context
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.ANNOTATION_TYPE)
public @interface PolymorphicQualifier {
    Class<? extends Annotation> value() default Annotation.class;
}

Usage Examples:

import org.checkerframework.framework.qual.*;

// Define a simple hierarchy: @Trusted > @Untrusted
@SubtypeOf({})
@DefaultQualifierInHierarchy
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface Trusted {}

@SubtypeOf(Trusted.class)
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface Untrusted {}

// Polymorphic qualifier that adapts based on context
@PolymorphicQualifier(Trusted.class)
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface PolyTrust {}

// Usage in code
public class TrustExample {
    public @PolyTrust String process(@PolyTrust String input) {
        return input.trim(); // Preserves trust level
    }
    
    public void example() {
        @Trusted String trusted = "safe input";
        @Untrusted String untrusted = getUserInput();
        
        @Trusted String result1 = process(trusted);     // Stays @Trusted
        @Untrusted String result2 = process(untrusted); // Stays @Untrusted
    }
}

Default Qualifier Application

Annotations that control where qualifiers are applied by default.

/**
 * Specifies that the given annotation should be the default for specified locations
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.ANNOTATION_TYPE)
public @interface DefaultFor {
    TypeUseLocation[] value() default {};
    TypeKind[] typeKinds() default {};
    Class<?>[] types() default {};
    String[] names() default {};
    String[] namesExceptions() default {};
}

/**
 * Applies the specified qualifier to types in the current package or class by default
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.PACKAGE, ElementType.TYPE})
@InheritedAnnotation
public @interface DefaultQualifier {
    Class<? extends Annotation> value();
    TypeUseLocation[] locations() default {TypeUseLocation.ALL};
}

/**
 * Locations where type qualifiers can be applied
 */
public enum TypeUseLocation {
    FIELD,
    LOCAL_VARIABLE,
    RESOURCE_VARIABLE,
    EXCEPTION_PARAMETER,
    RECEIVER,
    PARAMETER,
    RETURN,
    CONSTRUCTOR_RESULT,
    LOWER_BOUND,
    EXPLICIT_LOWER_BOUND,
    IMPLICIT_LOWER_BOUND,
    UPPER_BOUND,
    EXPLICIT_UPPER_BOUND,
    IMPLICIT_UPPER_BOUND,
    OTHERWISE,
    ALL
}

/**
 * Java type kinds for qualifier targeting
 */
public enum TypeKind {
    PACKAGE, INT, BOOLEAN, CHAR, DOUBLE, FLOAT, LONG, SHORT, BYTE
}

Usage Examples:

import org.checkerframework.framework.qual.*;

// Apply @NonNull by default to all method returns
@DefaultFor(value = TypeUseLocation.RETURN)
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface NonNull {}

// Apply @Tainted by default to all String types
@DefaultFor(types = String.class)
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface Tainted {}

// Apply @Initialized by default to primitive types
@DefaultFor(typeKinds = {TypeKind.INT, TypeKind.BOOLEAN, TypeKind.CHAR})
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface Initialized {}

// Package-level default qualifier
@DefaultQualifier(value = NonNull.class, locations = {TypeUseLocation.PARAMETER, TypeUseLocation.RETURN})
package com.example.safe;

import org.checkerframework.framework.qual.DefaultQualifier;

Literal and Value Association

Annotations that associate qualifiers with literal values.

/**
 * Associates a qualifier with specific literal kinds
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.ANNOTATION_TYPE)
public @interface QualifierForLiterals {
    LiteralKind[] value();
}

/**
 * Types of literals that can be associated with qualifiers
 */
public enum LiteralKind {
    ALL,
    BOOLEAN,
    CHAR,
    DOUBLE,
    FLOAT,
    INT,
    LONG,
    NULL,
    STRING,
    PRIMITIVE
}

/**
 * Implicitly applies the qualifier for specified literal kinds
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.ANNOTATION_TYPE)
public @interface ImplicitFor {
    LiteralKind[] literals() default {};
    Class<?>[] types() default {};
    TypeKind[] typeKinds() default {};
}

Usage Examples:

import org.checkerframework.framework.qual.*;

// String literals are automatically @Interned
@QualifierForLiterals(LiteralKind.STRING)
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface Interned {}

// Null literals are automatically @Nullable
@QualifierForLiterals(LiteralKind.NULL)
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface Nullable {}

// Primitive types are implicitly @NonNull
@ImplicitFor(typeKinds = {TypeKind.INT, TypeKind.BOOLEAN, TypeKind.CHAR})
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface NonNull {}

// Usage
public class LiteralExample {
    public void example() {
        @Interned String s1 = "hello";    // Automatically @Interned
        @Nullable String s2 = null;       // Automatically @Nullable
        @NonNull int i = 42;              // Automatically @NonNull
    }
}

Qualifier Restrictions and Targeting

Annotations that control where and how qualifiers can be applied.

/**
 * Restricts the locations where a qualifier can be applied
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.ANNOTATION_TYPE)
public @interface TargetLocations {
    TypeUseLocation[] value();
}

/**
 * Specifies relevant Java types for a checker
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.ANNOTATION_TYPE)
public @interface RelevantJavaTypes {
    Class<?>[] value();
}

/**
 * Prevents the default qualifier from being applied to uses of this type
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.ANNOTATION_TYPE)
public @interface NoDefaultQualifierForUse {}

/**
 * Makes a qualifier invisible to users (for internal framework use)
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.ANNOTATION_TYPE)
public @interface InvisibleQualifier {}

Usage Examples:

import org.checkerframework.framework.qual.*;

// Qualifier only applies to method parameters and returns
@TargetLocations({TypeUseLocation.PARAMETER, TypeUseLocation.RETURN})
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface MethodOnly {}

// Checker only analyzes String and StringBuilder types
@RelevantJavaTypes({String.class, StringBuilder.class})
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface StringQualifier {}

// Don't apply default qualifiers to this annotation's uses
@NoDefaultQualifierForUse
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface SpecialCase {}

// Internal framework annotation, not visible to users
@InvisibleQualifier
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface InternalOnly {}

Method Contract Annotations

Framework support for method contracts and specifications.

/**
 * Method postcondition: ensures the specified condition after method execution
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresQualifier {
    String[] expression();
    Class<? extends Annotation> qualifier();
}

/**
 * Conditional method postcondition
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresQualifierIf {
    String[] expression();
    Class<? extends Annotation> qualifier();
    boolean result();
}

/**
 * Method precondition: requires the specified condition when method is called
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface RequiresQualifier {
    String[] expression();
    Class<? extends Annotation> qualifier();
}

Usage Examples:

import org.checkerframework.framework.qual.*;

public class ContractExample {
    private String data;
    
    @EnsuresQualifier(expression = "data", qualifier = NonNull.class)
    public void initialize(String value) {
        this.data = value; // Postcondition: data is @NonNull
    }
    
    @EnsuresQualifierIf(expression = "data", qualifier = NonNull.class, result = true)
    public boolean isInitialized() {
        return data != null; // If returns true, data is @NonNull
    }
    
    @RequiresQualifier(expression = "data", qualifier = NonNull.class)
    public void processData() {
        System.out.println(data.length()); // Precondition: data must be @NonNull
    }
    
    public void safeUsage() {
        initialize("hello");
        processData(); // Safe - postcondition ensures data is @NonNull
        
        if (isInitialized()) {
            // Safe - conditional postcondition ensures data is @NonNull
            System.out.println("Data: " + data);
        }
    }
}

Advanced Framework Features

Additional framework annotations for complex type system features.

/**
 * Indicates that a qualifier has parameters
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.ANNOTATION_TYPE)
public @interface HasQualifierParameter {}

/**
 * Associates stub files with a qualifier
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE, ElementType.PACKAGE})
public @interface StubFiles {
    String[] value();
}

/**
 * Validates Java expressions in annotations
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.ANNOTATION_TYPE)
public @interface JavaExpression {}

/**
 * Specifies field invariants
 */
@Target(ElementType.FIELD)
@Retention(RetentionPolicy.RUNTIME)
public @interface FieldInvariant {
    String[] qualifier();
    String[] field();
}

/**
 * Specifies covariance for type parameters
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.TYPE)
public @interface Covariant {
    int[] value();
}

/**
 * Specifies contravariance for type parameters
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.TYPE)
public @interface Contravariant {
    int[] value();
}

Usage Examples:

import org.checkerframework.framework.qual.*;

// Parameterized qualifier
@HasQualifierParameter
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface KeyFor {
    String[] value(); // Parameter: which maps this is a key for
}

// Class with covariant type parameter
@Covariant(0) // First type parameter is covariant
public class Producer<T> {
    public T produce() { /* ... */ return null; }
}

// Class with contravariant type parameter
@Contravariant(0) // First type parameter is contravariant
public class Consumer<T> {
    public void consume(T item) { /* ... */ }
}

// Field invariant example
public class InvariantExample {
    @FieldInvariant(qualifier = "NonNull", field = "items")
    private List<String> items = new ArrayList<>();
    
    public void addItem(String item) {
        items.add(item); // Invariant ensures items is always @NonNull
    }
}

// Stub files association
@StubFiles("mylib.astub")
package com.example.mylib;

Utility Annotations

Supporting annotations for framework functionality.

/**
 * Marks elements as unused for warning suppression
 */
@Target({ElementType.TYPE, ElementType.FIELD, ElementType.METHOD, ElementType.PARAMETER,
         ElementType.CONSTRUCTOR, ElementType.LOCAL_VARIABLE, ElementType.ANNOTATION_TYPE,
         ElementType.PACKAGE, ElementType.TYPE_PARAMETER, ElementType.TYPE_USE})
@Retention(RetentionPolicy.SOURCE)
public @interface Unused {}

/**
 * Comments for documentation
 */
@Target({ElementType.TYPE, ElementType.FIELD, ElementType.METHOD, ElementType.PARAMETER,
         ElementType.CONSTRUCTOR, ElementType.LOCAL_VARIABLE, ElementType.PACKAGE})
@Retention(RetentionPolicy.SOURCE)
public @interface CFComment {
    String value();
}

/**
 * Marks annotations from bytecode
 */
@Target({ElementType.TYPE, ElementType.FIELD, ElementType.METHOD, ElementType.PARAMETER,
         ElementType.CONSTRUCTOR, ElementType.LOCAL_VARIABLE, ElementType.ANNOTATION_TYPE,
         ElementType.PACKAGE})
@Retention(RetentionPolicy.CLASS)
public @interface FromByteCode {}

/**
 * Excludes from whole-program inference
 */
@Target({ElementType.TYPE, ElementType.FIELD, ElementType.METHOD, ElementType.PARAMETER,
         ElementType.CONSTRUCTOR, ElementType.LOCAL_VARIABLE, ElementType.PACKAGE})
@Retention(RetentionPolicy.CLASS)
public @interface IgnoreInWholeProgramInference {}

Usage Examples:

import org.checkerframework.framework.qual.*;

public class UtilityExample {
    @CFComment("This field is for future use")
    @Unused
    private String futureFeature;
    
    @FromByteCode
    public void libraryMethod() {
        // Method signature loaded from bytecode
    }
    
    @IgnoreInWholeProgramInference
    public String experimentalMethod() {
        // Don't infer types for this method
        return "experimental";
    }
}

Reflection and Common Utilities

Additional framework annotations for reflection, aliasing, and value tracking.

/**
 * Class value for reflection operations
 */
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@Retention(RetentionPolicy.RUNTIME)
public @interface ClassVal {
    String[] value();
}

/**
 * Method value for reflection operations
 */
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@Retention(RetentionPolicy.RUNTIME)
public @interface MethodVal {
    String[] className();
    String[] methodName();
    int[] params();
}

/**
 * String literal values
 */
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@Retention(RetentionPolicy.RUNTIME)
public @interface StringVal {
    String[] value();
}

/**
 * Integer literal values
 */
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@Retention(RetentionPolicy.RUNTIME)
public @interface IntVal {
    long[] value();
}

/**
 * Unique reference (no aliasing)
 */
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@Retention(RetentionPolicy.RUNTIME)
public @interface Unique {}

/**
 * Method returns receiver object
 */
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@Retention(RetentionPolicy.RUNTIME)
public @interface This {}

Usage Examples:

import org.checkerframework.common.reflection.qual.*;
import org.checkerframework.common.value.qual.*;
import org.checkerframework.common.aliasing.qual.*;

public class CommonUtilitiesExample {
    // Reflection with known class values
    public void reflectionExample(@ClassVal("java.lang.String") Class<?> clazz) {
        // Safe to cast to String class
        String name = clazz.getName();
    }
    
    // Constant value tracking
    public void processConstant(@StringVal({"success", "failure"}) String status) {
        switch (status) {
            case "success": System.out.println("Operation succeeded"); break;
            case "failure": System.out.println("Operation failed"); break;
        }
    }
    
    // Aliasing control
    public @Unique StringBuilder createBuilder() {
        return new StringBuilder(); // Returns unique reference
    }
    
    // Fluent interface
    public @This StringBuilder append(@This StringBuilder sb, String text) {
        sb.append(text);
        return sb; // Returns the same object
    }
}

Install with Tessl CLI

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

docs

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

framework.md.css-3qkkll{font-size:var(--chakra-font-sizes-sm);font-weight:var(--chakra-font-weights-normal);color:var(--chakra-colors-gray-300);}docs/

Framework Annotations

Capabilities

Type Hierarchy Definition

Default Qualifier Application

Literal and Value Association

Qualifier Restrictions and Targeting

Method Contract Annotations

Advanced Framework Features

Utility Annotations

Reflection and Common Utilities

framework.mddocs/