0
# Framework Annotations
1

2
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.
3

4
## Capabilities
5

6
### Type Hierarchy Definition
7

8
Annotations for defining subtype relationships between qualifiers.
9

10
```java { .api }
11
/**
12
 * Specifies the supertypes of the annotated qualifier in the type hierarchy
13
 */
14
@Documented
15
@Retention(RetentionPolicy.RUNTIME)
16
@Target(ElementType.ANNOTATION_TYPE)
17
public @interface SubtypeOf {
18
    Class<? extends Annotation>[] value();
19
}
20

21
/**
22
 * Indicates that the annotated qualifier is the default qualifier in its hierarchy
23
 */
24
@Documented
25
@Retention(RetentionPolicy.RUNTIME)
26
@Target(ElementType.ANNOTATION_TYPE)
27
public @interface DefaultQualifierInHierarchy {}
28

29
/**
30
 * Makes a qualifier polymorphic, adapting based on context
31
 */
32
@Documented
33
@Retention(RetentionPolicy.RUNTIME)
34
@Target(ElementType.ANNOTATION_TYPE)
35
public @interface PolymorphicQualifier {
36
    Class<? extends Annotation> value() default Annotation.class;
37
}
38
```
39

40
**Usage Examples:**
41

42
```java
43
import org.checkerframework.framework.qual.*;
44

45
// Define a simple hierarchy: @Trusted > @Untrusted
46
@SubtypeOf({})
47
@DefaultQualifierInHierarchy
48
@Target({ElementType.TYPE_USE})
49
@Retention(RetentionPolicy.RUNTIME)
50
public @interface Trusted {}
51

52
@SubtypeOf(Trusted.class)
53
@Target({ElementType.TYPE_USE})
54
@Retention(RetentionPolicy.RUNTIME)
55
public @interface Untrusted {}
56

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

63
// Usage in code
64
public class TrustExample {
65
    public @PolyTrust String process(@PolyTrust String input) {
66
        return input.trim(); // Preserves trust level
67
    }
68
    
69
    public void example() {
70
        @Trusted String trusted = "safe input";
71
        @Untrusted String untrusted = getUserInput();
72
        
73
        @Trusted String result1 = process(trusted);     // Stays @Trusted
74
        @Untrusted String result2 = process(untrusted); // Stays @Untrusted
75
    }
76
}
77
```
78

79
### Default Qualifier Application
80

81
Annotations that control where qualifiers are applied by default.
82

83
```java { .api }
84
/**
85
 * Specifies that the given annotation should be the default for specified locations
86
 */
87
@Documented
88
@Retention(RetentionPolicy.RUNTIME)
89
@Target(ElementType.ANNOTATION_TYPE)
90
public @interface DefaultFor {
91
    TypeUseLocation[] value() default {};
92
    TypeKind[] typeKinds() default {};
93
    Class<?>[] types() default {};
94
    String[] names() default {};
95
    String[] namesExceptions() default {};
96
}
97

98
/**
99
 * Applies the specified qualifier to types in the current package or class by default
100
 */
101
@Documented
102
@Retention(RetentionPolicy.RUNTIME)
103
@Target({ElementType.PACKAGE, ElementType.TYPE})
104
@InheritedAnnotation
105
public @interface DefaultQualifier {
106
    Class<? extends Annotation> value();
107
    TypeUseLocation[] locations() default {TypeUseLocation.ALL};
108
}
109

110
/**
111
 * Locations where type qualifiers can be applied
112
 */
113
public enum TypeUseLocation {
114
    FIELD,
115
    LOCAL_VARIABLE,
116
    RESOURCE_VARIABLE,
117
    EXCEPTION_PARAMETER,
118
    RECEIVER,
119
    PARAMETER,
120
    RETURN,
121
    CONSTRUCTOR_RESULT,
122
    LOWER_BOUND,
123
    EXPLICIT_LOWER_BOUND,
124
    IMPLICIT_LOWER_BOUND,
125
    UPPER_BOUND,
126
    EXPLICIT_UPPER_BOUND,
127
    IMPLICIT_UPPER_BOUND,
128
    OTHERWISE,
129
    ALL
130
}
131

132
/**
133
 * Java type kinds for qualifier targeting
134
 */
135
public enum TypeKind {
136
    PACKAGE, INT, BOOLEAN, CHAR, DOUBLE, FLOAT, LONG, SHORT, BYTE
137
}
138
```
139

140
**Usage Examples:**
141

142
```java
143
import org.checkerframework.framework.qual.*;
144

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

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

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

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

167
import org.checkerframework.framework.qual.DefaultQualifier;
168
```
169

170
### Literal and Value Association
171

172
Annotations that associate qualifiers with literal values.
173

174
```java { .api }
175
/**
176
 * Associates a qualifier with specific literal kinds
177
 */
178
@Documented
179
@Retention(RetentionPolicy.RUNTIME)
180
@Target(ElementType.ANNOTATION_TYPE)
181
public @interface QualifierForLiterals {
182
    LiteralKind[] value();
183
}
184

185
/**
186
 * Types of literals that can be associated with qualifiers
187
 */
188
public enum LiteralKind {
189
    ALL,
190
    BOOLEAN,
191
    CHAR,
192
    DOUBLE,
193
    FLOAT,
194
    INT,
195
    LONG,
196
    NULL,
197
    STRING,
198
    PRIMITIVE
199
}
200

201
/**
202
 * Implicitly applies the qualifier for specified literal kinds
203
 */
204
@Documented
205
@Retention(RetentionPolicy.RUNTIME)
206
@Target(ElementType.ANNOTATION_TYPE)
207
public @interface ImplicitFor {
208
    LiteralKind[] literals() default {};
209
    Class<?>[] types() default {};
210
    TypeKind[] typeKinds() default {};
211
}
212
```
213

214
**Usage Examples:**
215

216
```java
217
import org.checkerframework.framework.qual.*;
218

219
// String literals are automatically @Interned
220
@QualifierForLiterals(LiteralKind.STRING)
221
@Target({ElementType.TYPE_USE})
222
@Retention(RetentionPolicy.RUNTIME)
223
public @interface Interned {}
224

225
// Null literals are automatically @Nullable
226
@QualifierForLiterals(LiteralKind.NULL)
227
@Target({ElementType.TYPE_USE})
228
@Retention(RetentionPolicy.RUNTIME)
229
public @interface Nullable {}
230

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

237
// Usage
238
public class LiteralExample {
239
    public void example() {
240
        @Interned String s1 = "hello";    // Automatically @Interned
241
        @Nullable String s2 = null;       // Automatically @Nullable
242
        @NonNull int i = 42;              // Automatically @NonNull
243
    }
244
}
245
```
246

247
### Qualifier Restrictions and Targeting
248

249
Annotations that control where and how qualifiers can be applied.
250

251
```java { .api }
252
/**
253
 * Restricts the locations where a qualifier can be applied
254
 */
255
@Documented
256
@Retention(RetentionPolicy.RUNTIME)
257
@Target(ElementType.ANNOTATION_TYPE)
258
public @interface TargetLocations {
259
    TypeUseLocation[] value();
260
}
261

262
/**
263
 * Specifies relevant Java types for a checker
264
 */
265
@Documented
266
@Retention(RetentionPolicy.RUNTIME)
267
@Target(ElementType.ANNOTATION_TYPE)
268
public @interface RelevantJavaTypes {
269
    Class<?>[] value();
270
}
271

272
/**
273
 * Prevents the default qualifier from being applied to uses of this type
274
 */
275
@Documented
276
@Retention(RetentionPolicy.RUNTIME)
277
@Target(ElementType.ANNOTATION_TYPE)
278
public @interface NoDefaultQualifierForUse {}
279

280
/**
281
 * Makes a qualifier invisible to users (for internal framework use)
282
 */
283
@Documented
284
@Retention(RetentionPolicy.RUNTIME)
285
@Target(ElementType.ANNOTATION_TYPE)
286
public @interface InvisibleQualifier {}
287
```
288

289
**Usage Examples:**
290

291
```java
292
import org.checkerframework.framework.qual.*;
293

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

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

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

312
// Internal framework annotation, not visible to users
313
@InvisibleQualifier
314
@Target({ElementType.TYPE_USE})
315
@Retention(RetentionPolicy.RUNTIME)
316
public @interface InternalOnly {}
317
```
318

319
### Method Contract Annotations
320

321
Framework support for method contracts and specifications.
322

323
```java { .api }
324
/**
325
 * Method postcondition: ensures the specified condition after method execution
326
 */
327
@Target(ElementType.METHOD)
328
@Retention(RetentionPolicy.RUNTIME)
329
@InheritedAnnotation
330
public @interface EnsuresQualifier {
331
    String[] expression();
332
    Class<? extends Annotation> qualifier();
333
}
334

335
/**
336
 * Conditional method postcondition
337
 */
338
@Target(ElementType.METHOD)
339
@Retention(RetentionPolicy.RUNTIME)
340
@InheritedAnnotation
341
public @interface EnsuresQualifierIf {
342
    String[] expression();
343
    Class<? extends Annotation> qualifier();
344
    boolean result();
345
}
346

347
/**
348
 * Method precondition: requires the specified condition when method is called
349
 */
350
@Target(ElementType.METHOD)
351
@Retention(RetentionPolicy.RUNTIME)
352
@InheritedAnnotation
353
public @interface RequiresQualifier {
354
    String[] expression();
355
    Class<? extends Annotation> qualifier();
356
}
357
```
358

359
**Usage Examples:**
360

361
```java
362
import org.checkerframework.framework.qual.*;
363

364
public class ContractExample {
365
    private String data;
366
    
367
    @EnsuresQualifier(expression = "data", qualifier = NonNull.class)
368
    public void initialize(String value) {
369
        this.data = value; // Postcondition: data is @NonNull
370
    }
371
    
372
    @EnsuresQualifierIf(expression = "data", qualifier = NonNull.class, result = true)
373
    public boolean isInitialized() {
374
        return data != null; // If returns true, data is @NonNull
375
    }
376
    
377
    @RequiresQualifier(expression = "data", qualifier = NonNull.class)
378
    public void processData() {
379
        System.out.println(data.length()); // Precondition: data must be @NonNull
380
    }
381
    
382
    public void safeUsage() {
383
        initialize("hello");
384
        processData(); // Safe - postcondition ensures data is @NonNull
385
        
386
        if (isInitialized()) {
387
            // Safe - conditional postcondition ensures data is @NonNull
388
            System.out.println("Data: " + data);
389
        }
390
    }
391
}
392
```
393

394
### Advanced Framework Features
395

396
Additional framework annotations for complex type system features.
397

398
```java { .api }
399
/**
400
 * Indicates that a qualifier has parameters
401
 */
402
@Documented
403
@Retention(RetentionPolicy.RUNTIME)
404
@Target(ElementType.ANNOTATION_TYPE)
405
public @interface HasQualifierParameter {}
406

407
/**
408
 * Associates stub files with a qualifier
409
 */
410
@Documented
411
@Retention(RetentionPolicy.RUNTIME)
412
@Target({ElementType.TYPE, ElementType.PACKAGE})
413
public @interface StubFiles {
414
    String[] value();
415
}
416

417
/**
418
 * Validates Java expressions in annotations
419
 */
420
@Documented
421
@Retention(RetentionPolicy.RUNTIME)
422
@Target(ElementType.ANNOTATION_TYPE)
423
public @interface JavaExpression {}
424

425
/**
426
 * Specifies field invariants
427
 */
428
@Target(ElementType.FIELD)
429
@Retention(RetentionPolicy.RUNTIME)
430
public @interface FieldInvariant {
431
    String[] qualifier();
432
    String[] field();
433
}
434

435
/**
436
 * Specifies covariance for type parameters
437
 */
438
@Documented
439
@Retention(RetentionPolicy.RUNTIME)
440
@Target(ElementType.TYPE)
441
public @interface Covariant {
442
    int[] value();
443
}
444

445
/**
446
 * Specifies contravariance for type parameters
447
 */
448
@Documented
449
@Retention(RetentionPolicy.RUNTIME)
450
@Target(ElementType.TYPE)
451
public @interface Contravariant {
452
    int[] value();
453
}
454
```
455

456
**Usage Examples:**
457

458
```java
459
import org.checkerframework.framework.qual.*;
460

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

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

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

481
// Field invariant example
482
public class InvariantExample {
483
    @FieldInvariant(qualifier = "NonNull", field = "items")
484
    private List<String> items = new ArrayList<>();
485
    
486
    public void addItem(String item) {
487
        items.add(item); // Invariant ensures items is always @NonNull
488
    }
489
}
490

491
// Stub files association
492
@StubFiles("mylib.astub")
493
package com.example.mylib;
494
```
495

496
### Utility Annotations
497

498
Supporting annotations for framework functionality.
499

500
```java { .api }
501
/**
502
 * Marks elements as unused for warning suppression
503
 */
504
@Target({ElementType.TYPE, ElementType.FIELD, ElementType.METHOD, ElementType.PARAMETER,
505
         ElementType.CONSTRUCTOR, ElementType.LOCAL_VARIABLE, ElementType.ANNOTATION_TYPE,
506
         ElementType.PACKAGE, ElementType.TYPE_PARAMETER, ElementType.TYPE_USE})
507
@Retention(RetentionPolicy.SOURCE)
508
public @interface Unused {}
509

510
/**
511
 * Comments for documentation
512
 */
513
@Target({ElementType.TYPE, ElementType.FIELD, ElementType.METHOD, ElementType.PARAMETER,
514
         ElementType.CONSTRUCTOR, ElementType.LOCAL_VARIABLE, ElementType.PACKAGE})
515
@Retention(RetentionPolicy.SOURCE)
516
public @interface CFComment {
517
    String value();
518
}
519

520
/**
521
 * Marks annotations from bytecode
522
 */
523
@Target({ElementType.TYPE, ElementType.FIELD, ElementType.METHOD, ElementType.PARAMETER,
524
         ElementType.CONSTRUCTOR, ElementType.LOCAL_VARIABLE, ElementType.ANNOTATION_TYPE,
525
         ElementType.PACKAGE})
526
@Retention(RetentionPolicy.CLASS)
527
public @interface FromByteCode {}
528

529
/**
530
 * Excludes from whole-program inference
531
 */
532
@Target({ElementType.TYPE, ElementType.FIELD, ElementType.METHOD, ElementType.PARAMETER,
533
         ElementType.CONSTRUCTOR, ElementType.LOCAL_VARIABLE, ElementType.PACKAGE})
534
@Retention(RetentionPolicy.CLASS)
535
public @interface IgnoreInWholeProgramInference {}
536
```
537

538
**Usage Examples:**
539

540
```java
541
import org.checkerframework.framework.qual.*;
542

543
public class UtilityExample {
544
    @CFComment("This field is for future use")
545
    @Unused
546
    private String futureFeature;
547
    
548
    @FromByteCode
549
    public void libraryMethod() {
550
        // Method signature loaded from bytecode
551
    }
552
    
553
    @IgnoreInWholeProgramInference
554
    public String experimentalMethod() {
555
        // Don't infer types for this method
556
        return "experimental";
557
    }
558
}
559
```
560

561
### Reflection and Common Utilities
562

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

565
```java { .api }
566
/**
567
 * Class value for reflection operations
568
 */
569
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
570
@Retention(RetentionPolicy.RUNTIME)
571
public @interface ClassVal {
572
    String[] value();
573
}
574

575
/**
576
 * Method value for reflection operations
577
 */
578
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
579
@Retention(RetentionPolicy.RUNTIME)
580
public @interface MethodVal {
581
    String[] className();
582
    String[] methodName();
583
    int[] params();
584
}
585

586
/**
587
 * String literal values
588
 */
589
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
590
@Retention(RetentionPolicy.RUNTIME)
591
public @interface StringVal {
592
    String[] value();
593
}
594

595
/**
596
 * Integer literal values
597
 */
598
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
599
@Retention(RetentionPolicy.RUNTIME)
600
public @interface IntVal {
601
    long[] value();
602
}
603

604
/**
605
 * Unique reference (no aliasing)
606
 */
607
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
608
@Retention(RetentionPolicy.RUNTIME)
609
public @interface Unique {}
610

611
/**
612
 * Method returns receiver object
613
 */
614
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
615
@Retention(RetentionPolicy.RUNTIME)
616
public @interface This {}
617
```
618

619
**Usage Examples:**
620

621
```java
622
import org.checkerframework.common.reflection.qual.*;
623
import org.checkerframework.common.value.qual.*;
624
import org.checkerframework.common.aliasing.qual.*;
625

626
public class CommonUtilitiesExample {
627
    // Reflection with known class values
628
    public void reflectionExample(@ClassVal("java.lang.String") Class<?> clazz) {
629
        // Safe to cast to String class
630
        String name = clazz.getName();
631
    }
632
    
633
    // Constant value tracking
634
    public void processConstant(@StringVal({"success", "failure"}) String status) {
635
        switch (status) {
636
            case "success": System.out.println("Operation succeeded"); break;
637
            case "failure": System.out.println("Operation failed"); break;
638
        }
639
    }
640
    
641
    // Aliasing control
642
    public @Unique StringBuilder createBuilder() {
643
        return new StringBuilder(); // Returns unique reference
644
    }
645
    
646
    // Fluent interface
647
    public @This StringBuilder append(@This StringBuilder sb, String text) {
648
        sb.append(text);
649
        return sb; // Returns the same object
650
    }
651
}
652
```