Constant Value Annotations

/**
 * Indicates the possible values for a byte, short, char, int, or long type.
 * At run time, the expression evaluates to one of the annotation's arguments.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE})
@SubtypeOf({UnknownVal.class})
public @interface IntVal {
    /** The values that the expression might evaluate to. */
    long[] value();
}

import org.checkerframework.common.value.qual.IntVal;

public class IntValExample {
    // Variable can only be 1, 2, or 3
    @IntVal({1, 2, 3}) int validMonth;
    
    // Method returns specific values
    public @IntVal({200, 404, 500}) int getResponseCode() {
        return 200; // Must be one of the declared values
    }
    
    // Parameter must be specific values
    public void setStatus(@IntVal({0, 1, 2}) int status) {
        // Safe to use without range checking
        this.status = status;
    }
}

/**
 * Indicates the possible values for a String type.
 * At run time, the expression evaluates to one of the annotation's arguments.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE})
@SubtypeOf({UnknownVal.class})
public @interface StringVal {
    /** The values that the expression might evaluate to. */
    String[] value();
}

import org.checkerframework.common.value.qual.StringVal;

public class StringValExample {
    // Configuration values
    @StringVal({"development", "staging", "production"}) String environment;
    
    // Method returns specific strings
    public @StringVal({"success", "failure", "pending"}) String getStatus() {
        return "success";
    }
    
    // Compile-time verification of switch statements
    public void handleMode(@StringVal({"read", "write", "append"}) String mode) {
        switch (mode) {
            case "read": return readFile();
            case "write": return writeFile();
            case "append": return appendFile();
            // No default needed - all cases covered
        }
    }
}

/**
 * An expression with this type evaluates to an integral value in the given range.
 * The bounds are inclusive.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE})
@SubtypeOf(UnknownVal.class)
public @interface IntRange {
    /**
     * Smallest value in the range, inclusive.
     * Defaults to Long.MIN_VALUE (or appropriate min for the type).
     */
    long from() default Long.MIN_VALUE;
    
    /**
     * Largest value in the range, inclusive.
     * Defaults to Long.MAX_VALUE (or appropriate max for the type).
     */
    long to() default Long.MAX_VALUE;
}

import org.checkerframework.common.value.qual.IntRange;

public class IntRangeExample {
    // Month values (1-12)
    @IntRange(from = 1, to = 12) int month;
    
    // Percentage values (0-100)
    @IntRange(from = 0, to = 100) int percentage;
    
    // Method with range constraints
    public void setVolume(@IntRange(from = 0, to = 10) int volume) {
        // Safe to use without bounds checking
        this.volume = volume;
    }
    
    // Array index that's within bounds
    public char getChar(String text, @IntRange(from = 0, to = 9) int index) {
        return text.charAt(index); // Safe if text.length() >= 10
    }
}

/**
 * Indicates the length of an array or a string.
 * At run time, the expression evaluates to an array or string whose length
 * is one of the annotation's arguments.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE})
@SubtypeOf({UnknownVal.class})
public @interface ArrayLen {
    /** The possible lengths of the array. */
    int[] value();
}

import org.checkerframework.common.value.qual.ArrayLen;

public class ArrayLenExample {
    // Fixed-size arrays
    int @ArrayLen(3) [] coordinates = new int[3]; // x, y, z
    String @ArrayLen({1, 2, 4, 8}) [] powerOfTwoArray;
    
    // Method returning fixed-length array
    public String @ArrayLen(2) [] getNameParts() {
        return new String[]{"First", "Last"};
    }
    
    // Safe array access
    public void processFixedArray(int @ArrayLen(5) [] data) {
        // Safe - array is guaranteed to have 5 elements
        for (int i = 0; i < 5; i++) {
            System.out.println(data[i]);
        }
    }
}

/**
 * Indicates the possible values for a boolean type.
 * At run time, the expression evaluates to one of the annotation's arguments.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE})
@SubtypeOf({UnknownVal.class})
public @interface BoolVal {
    /** The values that the expression might evaluate to. */
    boolean[] value();
}

/**
 * Indicates the possible values for a double type.
 * At run time, the expression evaluates to one of the annotation's arguments.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE})
@SubtypeOf({UnknownVal.class})
public @interface DoubleVal {
    /** The values that the expression might evaluate to. */
    double[] value();
}

/**
 * Indicates that an array or string has a length at least equal to the given value.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE})
@SubtypeOf({UnknownVal.class})
public @interface MinLen {
    /** The minimum length of the array or string. */
    int value();
}

/**
 * Indicates that an enum type may be one of the specified values.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE})
@SubtypeOf({UnknownVal.class})
public @interface EnumVal {
    /** The enum constants that the expression might evaluate to. */
    String[] value();
}

/**
 * UnknownVal is a type annotation indicating that the expression's value
 * is not known at compile time. This is the default/top qualifier.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE})
@SubtypeOf({})
@DefaultQualifierInHierarchy
@InvisibleQualifier
public @interface UnknownVal {}

// Import statements for using constant value annotations
import org.checkerframework.common.value.qual.IntVal;
import org.checkerframework.common.value.qual.StringVal;
import org.checkerframework.common.value.qual.IntRange;
import org.checkerframework.common.value.qual.ArrayLen;
import org.checkerframework.common.value.qual.BoolVal;
import org.checkerframework.common.value.qual.DoubleVal;
import org.checkerframework.common.value.qual.MinLen;
import org.checkerframework.common.value.qual.EnumVal;
import org.checkerframework.common.value.qual.UnknownVal;