When your code uses a library that is not currently being compiled, the Checker Framework looks up the library’s annotations in its class files. Section 2.2.1 tells you how to find and use a version of a library that contains type annotations.
If your code uses a library that does not contain type annotations, then the type-checker has no way to know the library’s behavior. The type-checker makes conservative assumptions about unannotated bytecode. (See Section 33.5.6 for details, an example, and how to override this conservative behavior.) These conservative library annotations invariably lead to checker warnings.
This chapter describes how to eliminate the warnings by adding annotations to the library. (Alternately, the -AskipUses or -AonlyUses command-line option can suppress all warnings related to an unannotated library, or to part of your codebase; see Sections 34.4–34.5.)
You can write annotations for a library, and make them known to a checker, in two ways.
1. Write annotations in a copy of the library’s source code (for instance, in a fork of the library’s GitHub project). In addition to writing annotations, adjust the build system to run pluggable-type-checking when compiling (see Chapter 39). Now, when you compile the library, the resulting .jar file contains type annotations.
When checking a client of the library, put the annotated library’s .jar file on the classpath, as explained in Section 2.2.1.
With this compilation approach, the syntax of the library annotations is validated ahead of time. Thus, this compilation approach is less error-prone, and the type-checker runs faster. You get correctness guarantees about the library in addition to your code.
For instructions, see Section 36.2.
2. Write annotations in a “stub file”, if you do not have access to the source code.
Then, when checking a client of the library, supply the “stub file” textually to the Checker Framework.
This approach does not require you to compile the library source code. A stub file is applicable to multiple versions of a library, so the stub file does not need to be updated when a new version of the library is released, unless the API has changed (such as defining a new class or method).
For instructions, see Section 36.5.
If you annotate a new library (either in its source code or in a stub file), please inform the Checker Framework developers so that your annotated library can be advertised to users of the Checker Framework. Sharing your annotations is useful even if the library is only partially annotated. However, as noted in Sections 2.4.2 and 36.1.4, you should annotate an entire class at a time. You may find type inference tools (Chapter 35) helpful when getting started, but you should always examine their results.
Section 2.4 gives general tips for writing annotations. This section gives tips that are specific to annotating a third-party library.
If you annotate a library that you maintain, you can refactor it to improve its design.
When you annotate a library that you do not maintain, you should only add annotations and, when necessary, documentation of those annotations. You can place the documentation in a Java comment (// or /*...*/) or in a @CFComment annotation.
Do not change the library’s code, which will change its behavior and make the annotated version inconsistent with the unannotated version. (Sometimes it is acceptable to make a refactoring, such as extracting an expression into a new local variable in order to annotate its type or suppress a warning. Perform
refactoring only when you cannot use @AssumeAssertion.)
Do not change publicly-visible documentation, such as Javadoc comments. That also makes the annotated version inconsistent with the unannotated version.
Do not change formatting and whitespace.
Any of these changes would increase the difference between upstream (the original version) and your annotated version. Unnecessary differences make it harder for others to understand what you have done, and they make it harder to pull changes from upstream into the annotated library.
Publicly-visible annotations (including those on public method formal parameters and return types) should be based on the documentation, typically the method’s Javadoc. In other words, your annotations should re-state facts that are in the Javadoc documentation.
Do not add requirements or guarantees beyond what the library author has already committed to. If a project’s Javadoc says nothing about nullness, then you should not assume that the specification forbids or permits null. (If the project’s Javadoc explicitly mentions null everywhere it is permitted, then you can assume it is forbidden elsewhere, where the author omitted those statements.)
If a fact is not mentioned in the documentation, then it is usually an implementation detail. Clients should not depend on implementation details, which are prone to change without notice. (In some cases, you can infer some facts from the implementation, such as that null is permitted for a method’s parameter or return type if the implementation explicitly passes null to the method or the method implementation returns null.)
If there is a fact that you think should be in the library’s documentation but was unintentionally omitted by its authors, then please submit a bug report asking them to update the documentation to reflect this fact. After they do, you can also express the fact as an annotation.
While annotating the library, you may discover bugs or missing/wrong documentation. If you have a documentation improvement or a bug fix, then open a pull request against the upstream version of the library. This will benefit all users of the library. And, once the documentation is updated, you will be able to add annotations that are consistent with the documentation.
If you do not annotate all the files in the library, then use @AnnotatedFor to indicate what files you have annotated.
Whenever you annotate any part of a file, fully annotate the file! That is, write annotations for all the methods and fields, based on their documentation. Here are reasons for this rule:
• If you annotate just part of the file, then users may be surprised that calls to some methods type-check as expected whereas other methods do not (because they have not been annotated).
• Annotating one method or field at a time may lead to inconsistencies between different parts of the file. Different people may make different assumptions, might write annotations in a way that is locally convenient but globally inconsistent, or might not read all the documentation of the class to understand how it works.
• It is only a bit more effort to annotate an entire class than to annotate one method or field. In either case it is usually necessary to understand the entire class’s design and implementation. Once you have done that, you might as well annotate the whole thing.
• If you fully annotate the file, it is possible to type-check the library to verify the annotations. (Even if you do not do this right now, it eases the task in the future.)
Ideally, after you annotate a file, you should type-check the file to verify the correctness and completeness of your annotations.
An alternative is to only annotate method signatures. The alternative is quicker but more error-prone. There is no difference from the point of view of clients, who can only see annotations on public methods and fields. When you compile the library, the type-checker will probably issue warnings; you can supply
-Awarns so that the compiler will still produce .class files.
This section describes how to create an annotated library.
1. See the org.checkerframework.annotatedlib group in the Maven Central Repository to find out whether an annotated version of the library already exists.
• If it exists, but you want to add annotations for a different checker:
Clone its repository from https://github.com/typetools/, and tweak its buildfile to run an additional checker.
• If it does not already exist:
Fork the project. (First, verify that its license permits forking.)
Add a line in its main README to indicate that this is an annotated version of the library. That line should also indicate how to obtain the corresponding upstream version (typically a git tag corresponding to a release), so that others can see exactly what edits you have made.
Adjust the library’s build process, such as an Ant, Gradle, or Maven buildfile (for guidance, see Chapter 39). Every time the build system runs the compiler, it should:
– pass the -AuseConservativeDefaultsForUncheckedCode=source,bytecode command-line option and
– run every pluggable type-checker for which any annotations exist, using -processor TypeSystem1,TypeSystem2,TypeSystem3
You are not adding new build targets, but modifying existing targets. The reason to run every type-checker is to verify the annotations you wrote, and to use appropriate defaults for all unannotated type uses.
2. Annotate some files.
When you annotate a file, annotate the whole thing, not just a few of its methods. Add an @AnnotatedFor({"checkername"})@AnnotatedFor annotation.
3. Build the library.
Because of the changes that you made in step 1, this will run pluggable type-checkers. If there are any compiler warnings, fix them and re-compile.
Now you have a .jar file that you can use while type-checking and at run time.
4. Tell other people about your work so that they can benefit from it.
• Please inform the Checker Framework developers about your new annotated library by opening a pull request or an issue. This will let us add your annotations to a repository in https://github.com/typetools/ and upload a compiled artifact to the Maven Central Repository.
• Optionally, encourage the library’s maintainers to accept your annotations into its main version control repository. This suggestion will be most compelling if you have already reported bugs in the library that were revealed by pluggable type-checking. Once the annotations are in the main version control repository, they will be easier to maintain, the library will obtain the correctness guarantees of pluggable type-checking, and there will be no need to distribute an annotated version of the library.
If the library maintainers do not accept the annotations, then periodically, such as when a new version of the library is released, pull changes from upstream (the library’s main version control system) into your fork, add annotations to any newly-added methods in classes that are annotated with
@AnnotatedFor, rebuild to create an updated .jar file, and inform the Checker Framework developers by opening an issue or a pull request.
When you create a new checker, you need to also supply annotations for parts of the JDK. You can do so either as stub files or in a copy of the JDK source code, as described in Section 37.10. Section 41.2.1 tells how to improve JDK annotations for an existing type system.
If you completely annotate a library, then you can compile it using a pluggable type-checker. You get a guarantee that the library contains no errors (that is, it is consistent with the specifications you wrote).
The rest of this section tells you how to compile a library if you partially annotate it: that is, you write annotations for some of its classes but not others. (There is another type of partial annotation, which is when you annotate method signatures but do not type-check the bodies. See Section 36.1.5.)
Here are two concerns you may have when partially annotating a library:
• Ignoring type-checking errors in unannotated parts of the library. Use the -AskipDefs, -AonlyDefs, -AskipFiles, or -AonlyFiles command-line arguments; see Section 34.5.
• Putting conservative annotations in unannotated parts of the library. The checker needs to use normal defaulting rules (Section 33.5.3) for code you have annotated and conservative defaulting rules (Section 33.5.6) for code you have not yet annotated. This section describes how to do this. You use @AnnotatedFor to indicate which classes you have annotated.
-AuseConservativeDefaultsForUncheckedCode=source,bytecode command-line argument
When compiling a library that is not fully annotated, use command-line argument -AuseConservativeDefaultsForUncheckedCode=source,bytecode. This has the following effect. For classes with @AnnotatedFor for the current checker, the checker applies defaults normally. For
classes without @AnnotatedFor for the current checker, the checker uses conservative defaults (see Section 33.5.6) for any type use with no explicit user-written annotation, and the
checker issues no warnings.
For example, an unannotated method
String concatenate(String p1, String p2)
in a class with a relevant @AnnotatedFor is defaulted normally.
In a class without a relevant @AnnotatedFor, it is interpreted as
@MyTopQualifier String concatenate(@MyBottomQualifier String p1, @MyBottomQualifier String p2)
where @MyTopQualifier is the top qualifier in the hierarchy and @MyBottomQualifier is the bottom qualifier in the hierarchy. These choices are conservative. They are likely to cause many false-positive type-checking errors in client code, which will help you to know which library
methods need annotations. You can then write those library annotations.
The @AnnotatedFor annotation, written on a class, indicates that the class has been annotated for certain type systems. You may write @AnnotatedFor on a class that
contains no explicit annotations from the given type system, if the defaulting rules already give appropriate qualifiers for every type in the class.
For example, @AnnotatedFor( means that the programmer has written annotations for the Nullness and Regular Expression type systems. For any type system other than Nullness or Regex, that {"nullness", "regex"})@AnnotatedFor annotation has no
effect — the checker treats the class as unannotated for that type system. The argument to @AnnotatedFor is not an annotation name, but a checker name.
Whenever you compile a class using the Checker Framework, including when using the -AuseConservativeDefaultsForUncheckedCode=source,bytecode command-line argument, the resulting .class files are fully-annotated; each type use in the .class file has an
explicit type qualifier for any checker that is run.
You use a “stub file” to write annotations for a library, when you cannot edit and recompile the library. A checker uses the annotated signatures at compile time, instead of or in addition to annotations that appear in the library’s .class files.
A stub file cannot override the types of a package-private class, method, or field.
A stub class is Java source code that is allowed to omit certain parts, such as method bodies. Section 36.5.4 describes the stub file format.
Section 36.3 explains how you should choose between creating stub classes and creating an annotated library. Section 36.5.5 describes how to
create stub classes. Section 36.5.1 describes how to use stub classes. These sections illustrate stub classes via the example of creating a @Interned-annotated version of java.lang.String. You don’t need to repeat these steps to handle java.lang.String for the Interning Checker, but you might do something similar for a different class and/or checker.
There are two types of annotation files, which are files containing annotations that can be read by the Checker Framework. This section describes stub files, which are used by programmers and type system designers. Section 36.6 describes ajava files, which are used by tools, such as type inference.
The -Astubs argument causes the Checker Framework to read annotations from annotated stub classes in preference to the unannotated original library classes. For example:
javac -processor org.checkerframework.checker.interning.InterningChecker \
-Astubs=path/to/String.astub:stubs MyFile.java MyOtherFile.java ...
Each stub path entry is a stub file (ending with .astub), directory, or .jar file; specifying a directory or .jar file is equivalent to specifying every file in it whose name ends with .astub. The stub path entries are delimited by
File.pathSeparator (“:” for Linux and Mac, “;” for Windows).
A checker automatically reads some of its own stub files, even without a -Astubs command-line argument; see Section 37.10.
User-supplied stub files override a checker’s built-in stub files and the annotated JDK.
There are three possible sources of information for a given element: source files, stub files, and bytecode files. Usually source files take precedence over the other two, and stub files take precedence over bytecode. In other words:
• If file A.java is being compiled, then by default any stub for class A is ignored. See below for how to change this behavior and respect both types of annotations.
• An unannotated type variable in a stub file is used instead of annotations on a type variable in bytecode.
Use the -AstubWarnIfRedundantWithBytecode command-line option to get a warning whenever a stub file specification is redundant with bytecode annotations.
• If a stub file does not mention a method or field (and no source is available), its annotations are taken from bytecode.
If a method appears in more than one stub file (or twice in the same stub file), then, for each type hierarchy, the last annotation read is used.
The annotated JDK is read as a stub file. You can override JDK annotations by providing your own stub file. If your stub file contains a JDK method m, then no type annotations from the JDK’s m are used. If the JDK’s m contains a declaration annotation @D, it is
used unless your stub file contains a different @D annotation for m.
The command-line option -AmergeStubsWithSource tells the checker to use both source files and stub files. The checker permits only values that are permitted by both the source and stub annotations. (This is called the greatest lower bound, or GLB, of the types.)
As an example of GLB, suppose the source annotation says the value is in the range [1..20] and the stub file says the value is in the range [11..30]. Since both sources of information are trusted, the value must be in the range [11..20]. Equivalently, the GLB of @IntRange(from=1, to=20) and @IntRange(from=11, to=30) is @IntRange(from=11, to=20). As another example, the GLB of @KeyFor({"map1", "map2"}) and @KeyFor({"map2", "map3"}) is @KeyFor({"map1", "map2", "map3"}) since the value is known to be a key for all three maps.
Sometimes, a method’s return type is different in a subclass than in a superclass, even though the subclass inherits (does not define) the method. An example, SecureRandom.nextInt(), is shown below.
To express that method m has a different type in subclass Sub than where m is defined, write a “fake override”: write the method in class Sub in a stub file. The Checker Framework will use that type for m at calls where the receiver’s declared type is
Sub or lower.
In a fake override of m, the formal parameter Java types of the method must be identical to those where m is defined, but you can change its annotations. (The return type and the receiver type can be different.) You may write the name of a formal parameter type in fully-qualified,
partially-qualified, or simple form, and you may omit its type arguments. If a fake override has no annotations on a given type use, that type use is defaulted according to the usual defaulting rules.
This feature currently only works for return types. That is, a fake override changes the return type at certain calls, but formal parameter type annotations on fake overrides have no effect. Type annotations on fake overrides of fields also have no effect. Fake overrides will be able to change formal parameter and field type annotations in a future release of the Checker Framework.
As an example, consider a type system that tracks whether a value is cryptographically secure. @Secure is a subtype of @Insecure. Although SecureRandom does not override Random.nextInt (it overrides the source of randomness instead), you are allowed
to write the following stub file:
package java.util;
class Random {
@Insecure int nextInt();
}
package java.security;
class SecureRandom extends Random {
@Secure int nextInt();
}
Client code behaves as follows:
Random r = ...; SecureRandom sr = ...; @Secure int i1 = r.nextInt(); // error @Secure int i2 = sr.nextInt(); // OK
Every Java file is a valid stub file. However, you can omit information that is not relevant to pluggable type-checking, as explained below; this makes the stub file smaller and easier for people to read and write. The stub file’s extension must be .astub, not .java.
As an illustration, a stub file for the Interning type system (Chapter 6) could be:
import org.checkerframework.checker.interning.qual.Interned;
package java.lang;
@Interned class Class<T> {}
class String {
@Interned String intern();
}
The stub file format is allowed to differ from Java source code in the following ways:
Method bodies: The stub class does not require method bodies for classes; any method body may be replaced by a semicolon (;), as in an interface or abstract method declaration.
Method declarations: You only have to specify the methods that you need to annotate. Any method declaration may be omitted, in which case the checker reads its annotations from the library’s .class files. If you are using a stub class, then often the library is unannotated, but you can use
stub files to override library annotations.
Declaration specifiers: Declaration specifiers (e.g., public, final, volatile) may be omitted.
Return types: The return type of a method does not need to match the real method. In particular, it is valid to use java.lang.Object for every method. This simplifies the creation of stub files.
Multiple classes and packages: The stub file format permits having multiple classes and packages. The packages are separated by a package statement: package my.package;. Each package declaration may occur only once; in other words, all classes from a package must appear together.
Import statements: Imports may appear at the beginning of the file or after any package declaration. An import applies to the whole file. The only required import statements are the ones to import type annotations. Import statements for types are optional. If you omit an import statement for an annotation, occurrences of that annotation are silently ignored; this is a common error in stub files.
When you create a stub file, it is recommended that you validate it by copying the stub file to a file with the .java extension and running the type-checker. This will ensure that your annotations are syntactically valid, are written in the correct locations, and are properly imported. When you run the
type-checker on your annotations, there should not be any stub file that also contains annotations for the class. In particular, if you are type-checking a stub file for a class in the JDK, then you should use the -Aignorejdkastub command-line option.
Every Java file is a stub file. If you have access to the Java file, copy file A.java to A.astub. You can add annotations to the signatures, leaving the method bodies unchanged. The stub file parser silently ignores any annotations that it cannot resolve to a type, so don’t forget the
import statement.
This copy-and-annotate approach retains the original documentation and source code, making it easier for a programmer to double-check the annotations. It also enables creation of diffs, easing the process of upgrading when a library adds new methods. And, the annotations are in a format that the library maintainers can even incorporate.
The downside of the copy-and-annotate approach is that the stub files are larger. This can slow down the Checker Framework, because it parses the stub files each time it runs.
You can minimize source files to speed up parsing them. Use the JavaStubifier to convert, in-place, all .java files in given directories into minimal stub files.
mkdir project-stubs
cp -R project/src project-stubs
java -cp $CHECKERFRAMEWORK/checker/dist/checker.jar org.checkerframework.framework.stub.JavaStubifier project-stubs
find project-stubs -type f -name "*.java" -exec rename 's/.java$/.astub/' {} \;
Supply it a list of directories to process. Replacement happens in-place, so make sure to process a copy of your sources.
You can now provide project-stubs as a stub directory using -Astubs=project-stubs as an additional command-line option.
If you wish to use a single stub file, rather than a stub directory, you can concatenate all the minimized .java files into a single .astub file:
find project-stubs/ -name "*.java" -type f | xargs cat > project.astub
If you do not have access to the library source code, you can create a stub file by hand.
If you have access to the API documentation for the element you wish to annotate, it is often easiest to copy-paste names, types, and signatures from the API documentation. (The API documentation is a .html file that is sometimes colloquially called the “Javadoc”.) This avoids common mistakes
when writing stub files by hand, such as typos in the package name or in a method signature.
Here are steps to write a stub file by hand:
1. Create a file whose name ends in .astub, or use an existing one.
2. Write a package declaration, exactly as if you are writing a Java file for the target class. (If the file already contains a declaration for that package, re-use it by doing the rest of your work under it; don’t write a duplicate package declaration in the file.) Typically, it is easiest to copy-paste the package name from API documentation or from an import statement in the code that you are type-checking, to avoid typos.
3. Write a class declaration header: class followed by the class name. The stub file format does not care whether the enclosing type is a class, interface, etc., so you can write “class” regardless of what kind of type it is.
A common mistake at this stage is that the target method or field may be defined in a superclass of the static type of the class that is actually being used in the code you are trying to analyze. For example, suppose that you are trying to annotate the
drawImage(Image,int,int,int,int,ImageObserver) method of an object whose static type is java.awt.Graphics2D. This method is actually defined in the abstract Graphics class (which is the superclass of Graphics2D), so it needs to appear within
the class Graphics rather than the class Graphics2D in the stub file.
4. Write the element declaration that you wish to annotate, within the class you just created.
For a method, this is the method signature, followed by “;”.
For a field, this is the type, field name, and “;”, without an initializer.
5. Annotate the declaration that you just wrote.
6. Add import statements for any annotations you wrote.
If you are writing stub files but are not writing a checker, you can place the stub files anywhere that is convenient. However, please consider providing your stub files to the checker author, so that other users can also benefit from the stub files you wrote.
Stub files distributed with a checker appear in the same directory as the checker implementation (the *Checker.java file, see Section 37.2). For example, in the Checker Framework they appear in
files such as
checker/src/main/java/org/checkerframework/checker/regex/apache-xerces.astub checker/src/main/java/org/checkerframework/checker/signature/javaparser.astub
If you are distributing stub files with a checker implementation, you must configure your build system to copy the stub files into the distributed jar for your checker. Here are instructions if you are using the Checker Framework Gradle plugin:
• If the stub files appear in the same directory as the checker class, which is a subtype of BaseTypeChecker, use the following build configuration:
sourceSets {
main {
resources {
srcDirs += ['src/main/java']
}
}
}
• If the stub files appear under the src/main/resources/ directory in a subdirectory matching the package of your checker class, the default Gradle build configuration is sufficient.
In either case, recall that a @StubFiles annotation on the checker class lists stub files that are always used. For stub files whose use is optional (for example, because the behavior is
unsound, or unsound except in certain circumstances), users must supply the -Astubs=... command-line option.
If a stub file contains annotations that are used by the framework rather than by any specific checker (such as purity annotations), and you wish to distribute it with the Checker Framework, put the stub file in directory checker/src/main/resources/. You can also do this if the stub file has
annotations for multiple checkers. To use a stub file in directory checker/src/main/resources/, users must supply the -Astubs=checker.jar/stub-file-name.astub command-line option.
By default, the stub parser silently ignores annotations on unknown classes and methods. The stub parser also silently ignores unknown annotations, so don’t forget to import any annotations. Some command-line options make the stub parser issue more warnings:
-AstubWarnIfNotFound-AstubNoWarnIfNotFound
The Checker Framework can issue a “Type not found” warning when a stub file contains a nonexistent element, for example when the stub file mentions a method that the class does not contain. By default, the Checker Framework warns about such problems in a stub file provided on the command line, but does not
warn about built-in stub files. These command-line options turn the warnings on or off (respectively) for all stub files.
The @NoAnnotationFileParserWarning annotation on a package or type in a stub file causes no warning to be issued for that package or type, regardless of the command-line options.
-AstubWarnIfNotFoundIgnoresClasses
Modifies the behavior of -AstubWarnIfNotFound to report only missing methods/fields, but ignore missing classes, even if other classes from the same package are present. Useful if a package spans more than one jar.
-AstubWarnIfRedundantWithBytecodeWarn if a stub file entry is redundant with bytecode information. The warning means that the stub file’s type is the same as the bytecode type, so that entry in the stub file has no effect. You could remove the entry in the stub file to make it shorter, or you could add an annotation to the stub file to make the entry have an effect.
-AstubWarnNote
Issue a “note”, not a warning, for the -AstubWarn* command-line arguments. A warning may prevent further compilation (depending on whether the -Werror command-line argument is passed), but a note permits compilation to proceed.
-AstubDebug
Output debugging messages while parsing stub files, including about unknown classes, methods, and annotations. This overrides the @NoAnnotationFileParserWarning annotation.
When using command-line option -AstubWarnIfNotFound, an error is issued if a stub file has a typo or the API method does not exist.
Fix an error of the form
AnnotationFileParser: Method isLLowerCase(char) not found in type java.lang.Character
by removing the extra “L” in the method name.
Fix an error of the form
AnnotationFileParser: Method enableForegroundNdefPush(Activity,NdefPushCallback)
not found in type android.nfc.NfcAdapter
by removing the method enableForegroundNdefPush(...) from the stub file, because it is not defined in class android.nfc.NfcAdapter in the version of the library you are using.
There are two types of annotation files, which are files containing annotations that can be read by the Checker Framework. Section 36.5 describes stub files, which are used by programmers and type system designers. This section describes
ajava files. Ajava files are primarily read and written by tools, such as whole-program type inference (see Section 35.2). (However, programmers are permitted to write .ajava files.) This section about ajava files
is primarily of interest to the maintainers of such tools.
An ajava file is simply a valid Java source file. The Checker Framework reads its annotations. (This includes annotations that are written on anonymous and local classes — annotations in such locations are ignored in stub files.)
The -Aajava command-line argument works like -Astubs (see Section 36.5.1). It takes a colon-separated list of files and directories containing ajava files, which end in the .ajava extension.
For example:
javac -processor org.checkerframework.checker.interning.InterningChecker \
-Aajava=path/to/String.ajava:ajavadir MyFile.java MyOtherFile.java ...
If there’s an annotation in both a source file and the corresponding ajava file, the Checker Framework uses the greatest lower bound, as with the -AmergeStubsWithSource option.
If the Checker Framework reads both a source file and an ajava file that corresponds to it, then the source file and the ajava file must have a specific relationship to one another, to prevent errors that could occur due to mismatches.
The ajava file must either (1) be found below one of the arguments to -Aajava, in a subdirectory matching its package name, or (2) be unambiguously specified directly with its full path. A pair of .ajava files is specified ambiguously if one of their fully-qualified names is a substring of
the other, and both are specified as .ajava files (rather than being found under directories). For example, if the -Aajava argument was -Aajava= /foo/Bar.ajava: /baz/foo/Bar.ajava, the two .ajava files would be considered ambiguous
and an ambiguous.ajava warning would be issued. Files found under a directory are always unambiguous, because their file structure must match their package name; the solution to an ambiguous.ajava warning is to convert the specific files in the -Aajava argument to
directories.
The ajava file must be named ClassName-checker.qualified.name.ajava where checker.qualified.name is the fully qualified name of the checker that the ajava file’s annotations belong to.
For example, an ajava file with tainting annotations for a class outerpackage.innerpackage.MyClass would be located in a subdirectory outerpackage/innerpackage and it would be named
MyClass-org.checkerframework.checker.tainting.TaintingChecker.ajava.
The ajava file must contain the same source code as the source file, with the following exceptions:
• The two may differ in annotations.
• The two may have different import statements.
• The ajava file may have explicit receivers where the source file doesn’t. If a source file has a method declaration void myMethod(), the ajava file might contain void myMethod(MyClass this) or void myMethod(@Interned MyClass this).
• The ajava file may have explicit type bounds that are implicit in the source file. If a source file has a type argument ?, the ajava file might contain ? extends Object or ? extends @Nullable Object.
The InsertAjavaAnnotations.java program inserts annotations from ajava files into Java files. This can be used to insert the annotations inferred by whole program inference into the source code of a program, similarly to the insert-annotations-to-source script from the Annotation File Utilities project.
Its arguments are a directory containing ajava files and a directory containing Java files. The checker.jar file must be in the classpath. Here is an example invocation:
java -cp $CHECKERFRAMEWORK/checker/dist/checker.jar \
org.checkerframework.framework.ajava.InsertAjavaAnnotations \
<path-to-ajava-files> <path-to-java-files>
Sometimes, it may seem that a checker is treating a library as unannotated even though the library has annotations. The compiler has a flag that may help you in determining which library files are read.
-verbose Outputs information about compile phases — when the compiler reads/parses/attributes/writes any file. Also outputs the classpath and sourcepath paths.
A syntax error in a stub file or the annotated JDK can lead to the file being silently ignored. A typo in an annotation name, or a missing import statement, can lead to annotations being silently ignored.