All Classes and Interfaces

Class
Description
Ampere.
A constraint of the form: A 《 F or F 》 A
A2FReducer takes an A2F constraint that is not irreducible (@see AFConstraint.isIrreducible) and reduces it by one step.
AbstractAnalysis<V extends AbstractValue<V>,S extends Store<S>,T extends TransferFunction<V,S>>
Implementation of common features for BackwardAnalysisImpl and ForwardAnalysisImpl.
A worklist is a priority queue of blocks in which the order is given by depth-first ordering to place non-loop predecessors ahead of successors.
Implements all methods from AtmComboVisitor.
This abstract class makes implementing a CFGVisualizer easier.
Whether to visualize before or after a block.
A default implementation of the node visitor interface.
Implements framework support for qualifier polymorphism.
This class is an abstract annotation processor designed to be a convenient superclass for concrete "type processors", processors that require the type information in the processed source.
An abstract value used in the org.checkerframework.dataflow analysis.
Units of acceleration.
This class only contains boilerplate code to permit AccumulationValue's accumulatedValues functionality to interact with the rest of an accumulation type system.
An annotated type factory for an accumulation checker.
An accumulation checker is one that accumulates some property: method calls, map keys, etc.
The alias analyses that an accumulation checker can support.
This class is boilerplate, to enable the logic in AccumulationValue.
The default transfer function for an accumulation checker.
AccumulationValue holds additional information about accumulated facts ("values", not to be confused with "Value" in the name of this class) that cannot be stored in the accumulation type, because they are not a refinement of that type.
The visitor for an accumulation checker.
Utility that generates @AnnotatedFor class annotations.
AFConstraint represent the initial constraints used to infer type arguments for method invocations and new class invocations.
AFReducer implementations reduce AFConstraints into one or more "simpler" AFConstraints until these constraints are irreducible.
An aggregate checker that packages multiple checkers together.
A specialized variant of CheckerFrameworkPerDirectoryTest for testing the Whole Program Inference feature of the Checker Framework, which is tested by running pairs of these tests: a "generation test" (of this class) to do inference using the -Ainfer option, and a "validation test" (of class AinferValidatePerDirectoryTest) to check that files typecheck after those inferences are taken into account.
A specialized variant of CheckerFrameworkPerDirectoryTest for testing the Whole Program Inference feature of the Checker Framework, which is tested by running pairs of these tests: a "generation test" (of class AinferGeneratePerDirectoryTest) to do inference using the -Ainfer option, and a "validation test" (of this class) to check that files typecheck after those inferences are taken into account.
Annotated type factory for the Aliasing Checker.
Aliasing type system -- used to identify expressions that definitely have no aliases.
Type refinement is treated in the usual way, except that at (pseudo-)assignments the RHS may lose its type refinement, before the LHS is type-refined.
This visitor ensures that every constructor whose result is annotated as @Unique does not leak aliases.
Annotation to override the UI effect on a class, and make a field or method safe for non-UI code to use.
Analysis<V extends AbstractValue<V>,S extends Store<S>,T extends TransferFunction<V,S>>
This interface defines a dataflow analysis, given a control flow graph and a transfer function.
In calls to Analysis#runAnalysisFor, whether to return the store before or after the given node.
The direction of an analysis instance.
AnalysisResult<V extends AbstractValue<V>,S extends Store<S>>
An AnalysisResult represents the result of a org.checkerframework.dataflow analysis by providing the abstract values given a node or a tree.
Units of measure for angles.
Indicates that this class has been annotated for the given type system.
Changes each parameter type to be the GLB of the parameter type and visited type.
AnnotatedTypeCopier is a visitor that deep copies an AnnotatedTypeMirror exactly, including any lazily initialized fields.
Duplicates annotated types and replaces components according to a replacement map.
AnnotatedTypeCopier maintains a mapping of typeVisited => copyOfTypeVisited When a reference, typeVisited, is encountered again, it will use the recorded reference, copyOfTypeVisited, instead of generating a new copy of typeVisited.
The methods of this class take an element or AST node, and return the annotated type as an AnnotatedTypeMirror.
The type for an instantiated generic method or constructor.
Converts an AnnotatedTypeMirror mirror into a formatted string.
Represents an annotated type in the Java programming language, including: standard types: primitive types, declared types (class and interface types), array types, type variables, and the null type wildcard type arguments executable types (their signature and return types) pseudo-types corresponding to packages and to the keyword void
Represents Array types in java.
Represents a declared type (whether class or interface).
Represents a type of an executable.
Represents an intersection type.
A pseudo-type used where no actual type is appropriate.
Represents the null type.
Represents a primitive type.
Represents a type variable.
 
Represents a wildcard type argument.
Represents upper and lower bounds, each an AnnotatedTypeMirror.
Replaces or adds all the annotations in the parameter with the annotations from the visited type.
Utility methods for operating on AnnotatedTypeMirror.
An AnnotatedTypeScanner visits an AnnotatedTypeMirror and all of its child AnnotatedTypeMirrors and performs some function depending on the kind of type.
Reduces two results into a single result.
A visitor of annotated types, in the style of the visitor design pattern.
Builds an annotation mirror that may have some values.
This class assists the AnnotatedTypeFactory by reflectively looking up the list of annotation class names in each checker's qual directory, and then loading and returning it as a set of annotation classes.
This class contains static methods that convert between Annotation and AnnotationMirror.
Given two ASTs representing the same Java file that may differ in annotations, tests if they have the same annotations.
Holds information about types parsed from annotation files (stub files or ajava files).
This class has three static methods.
The result of calling AnnotationFileParser.parse: the annotated types and declaration annotations from the file.
An exception indicating a problem while parsing an annotation file.
Information about a record component: its type, and whether there was an accessor in the stubs for that component.
Information about a record from a stub file.
Interface for sources of stub data.
Stores a collection of annotation files.
Utility class for annotation files (stub files and ajava files).
The types of files that can contain annotations.
Converts AnnotationMirrors to Strings.
The Map interface defines some of its methods with respect to the equals method.
The Set interface defines many methods with respect to the equals method.
Methods for converting a AnnotationMirror into a JavaParser AnnotationExpr, namely annotationMirrorToAnnotationExpr.
An implementation of AnnotationProvider returns annotations on Java AST elements.
An annotation processor for counting the annotations in a program and for listing the potential locations of annotations.
A visitor that adds all annotations from a AnnotatedTypeMirror to the corresponding JavaParser type, including nested types like array components.
A utility class for working with annotations.
Units of areas.
An array access.
A node for an array access:
JavaExpression for array creations.
A node for new array creation.
An annotation indicating the length of an array or a string.
An expression with this type evaluates to an array or a string whose length is in the given range.
A node representing an array type used in an expression such as a field access.
An identifier or primitive type, followed by any number of array square brackets.
scene-lib (from the Annotation File Utilities) doesn't provide enough information to usefully print stub files: it lacks information about what is and is not an enum, about the base types of variables, and about formal parameter names.
A node for the AssertionError when an assertion fails or when a method call marked AssertMethod fails.
AssertMethod is a method annotation that indicates that a method throws an exception if the value of a boolean argument is false.
Indicates that if the method returns a non-null value, then the value expressions are also non-null.
A node for an assignment:
An enum representing the cartesian product of the set of AtmKinds with itself.
Visitor interface for all pair-wise combinations of AnnotatedTypeMirrors.
AutoValue support for the Called Methods Checker.
Basic alpha compositing rules for combining source and destination colors to achieve blending and transparency effects with graphics and images (see AlphaComposite for more details).
Color space tags to identify the specific color space of a Color object or, via a ColorModel object, of an Image, a BufferedImage, or a GraphicsDevice (see ColorSpace for more details).
AwtCursorType.
Line alignments in a flow layout (see FlowLayout for more details).
This interface defines a backward analysis, given a control flow graph and a backward transfer function.
An implementation of a backward analysis to solve a org.checkerframework.dataflow problem given a control flow graph and a backward transfer function.
Interface of a backward transfer function for the abstract interpretation used for the backward flow analysis.
A factory that extends GenericAnnotatedTypeFactory to use the default flow-sensitive analysis as provided by CFAnalysis.
A class for functionality common to multiple type-checkers that are used by the Index Checker.
An abstract SourceChecker that provides a simple SourceVisitor implementation that type-checks assignments, pseudo-assignments such as parameter passing and method invocation, and method overriding.
A visitor to validate the types in a tree.
A SourceVisitor that performs assignment and pseudo-assignment checking, method invocation checking, and assignability checking.
An AnnotationProvider that is independent of any type hierarchy.
Process the types in an AST in a trivial manner, with hooks for derived classes to actually do something.
Represents a binary name as defined in the Java Language Specification, section 13.1.
Represents a primitive type name or a binary name.
Represents a string that is a BinaryName, an InternalForm, and a ClassGetName.
JavaExpression for binary operations.
A node for a binary expression.
A node for the bitwise or logical (single bit) and operation:
A node for the bitwise complement operation:
A node for the bitwise or logical (single bit) or operation:
A node for the bitwise or logical (single bit) xor operation:
Represents a basic block in a control flow graph.
The types of basic blocks.
Base class of the Block implementation hierarchy.
A node for a boolean literal:
An annotation indicating the possible values for a bool type.
A special annotation intended solely for representing the bottom type in the qualifier hierarchy.
The bottom type for the Returns Receiver Checker's type system.
The bottom type in the Constant Value type system.
BoundsInitializer creates AnnotatedTypeMirrors (without annotations) for the bounds of type variables and wildcards.
Exception type indicating a bug in the framework.
Provides hooks to add CalledMethods annotations to code generated by a builder framework like Lombok or AutoValue.
A utility class of static methods used in supporting builder-generation frameworks.
The playground for busy expression analysis.
A busy expression store contains a set of busy expressions represented by nodes.
A busy expression transfer function
BusyExprValue class contains a BinaryOperationNode.
 
Degree Centigrade (Celsius).
A deprecated variant of CalledMethods.
If an expression has type @CalledMethods({"m1", "m2"}), then methods m1 and m2 have definitely been called on its value.
The analysis for the Called Methods Checker.
The annotated type factory for the Called Methods Checker.
The bottom type for the Called Methods type system.
The Called Methods Checker tracks the methods that have definitely been called on an object.
This annotation represents a predicate on @CalledMethods annotations.
A transfer function that accumulates the names of methods called.
This visitor implements the custom error message "finalizer.invocation".
Canonical names have the same syntactic form as fully-qualified names.
This is a string that is a valid canonical name and a valid binary name.
Either a CanonicalName or the empty string.
This is a string that is a valid canonical name and a valid binary name or primitive type.
A node for a case in a switch statement.
A CatchMarkerNode is a marker node for the beginning or end of a catch block.
Candela (unit of luminance).
CFAbstractAnalysis is an extensible org.checkerframework.dataflow analysis for the Checker Framework that tracks the annotations using a flow-sensitive analysis.
A triple of field, value corresponding to the annotations on its declared type, value of its initializer.
A store for the Checker Framework analysis.
The default analysis transfer function for the Checker Framework.
An implementation of an abstract value used by the Checker Framework org.checkerframework.dataflow analysis.
The default org.checkerframework.dataflow analysis used in the Checker Framework.
A control-flow graph builder (see CFGBuilder) that knows about the Checker Framework annotations and their representation as AnnotatedTypeMirrors.
A specialized phase-one CFG builder, with a few modifications that make use of the type factory.
This annotation is for comments related to the Checker Framework.
Builds the control flow graph of some Java code (either a method, or an arbitrary statement).
Generate the control flow graph of a given method in a given class.
The result of the CFG process, contains the control flow graph when successful.
Class that performs phase one of the translation process.
Holds the elements of an AssertMethod annotation.
Class that performs phase three of the translation process.
A simple wrapper object that holds a basic block and allows to set one of its successors.
Class that performs phase two of the translation process.
Launcher to generate the DOT or String representation of the control flow graph of a given method in a given class.
Options for running analysis on files.
CFGVisualizer<V extends AbstractValue<V>,S extends Store<S>,T extends TransferFunction<V,S>>
Perform some visualization on a control flow graph.
The default store used in the Checker Framework.
The default transfer function used in the Checker Framework.
The TreeBuilder permits the creation of new AST Trees using the non-public Java compiler API TreeMaker.
The default abstract value used in the Checker Framework: a set of annotations and a TypeMirror.
A node for a character literal.
Compiles all test files in a test directory together.
Compiles all test files individually.
A specialized variant of CheckerFrameworkPerDirectoryTest for testing the Whole Program Inference feature of the Checker Framework, which is tested by running pairs of these tests: a "generation test" (of class AinferGeneratePerDirectoryTest) to do inference using the -Ainfer option, and a "validation test" (of class AinferValidatePerDirectoryTest) to check that files typecheck after those inferences are taken into account.
This class behaves similarly to javac.
This represents a Class<T> object whose run-time value is equal to or a subtype of one of the arguments.
A node representing a class declaration that occurs within a method, for example, an anonymous class declaration.
The type representation used by the Class.getName(), Class.forName(String), and Class.forName(String, boolean, ClassLoader) methods.
The format produced by the Class.getSimpleName() method.
A ClassName represents either a class literal or the occurrence of a class as part of a static field access or static method invocation.
A node representing a class name used in an expression such as a static method invocation.
Applies the annotations present for a class type parameter onto an AnnotatedTypeVariable.
This represents a Class<T> object where the set of possible values of T is known at compile time.
A type factory for the @ClassVal and @ClassBound annotations.
The bottom type in the ClassVal type system.
The ClassVal Checker provides a sound estimate of the binary name of Class objects.
A visitor to verify validity of @ClassVal annotations.
Determines the nullness type of calls to Collection.toArray().
Utility methods related to Java Collections.
Method declaration annotation that indicates a method has a specification like compareTo() or compare().
CompilationResult represents the output of the compiler after it is run.
A string that is definitely a compiler message key.
The bottom type in the Compiler Message Key type system.
A PropertyKeyATF that uses CompilerMessageKey to annotate the keys.
A PropertyKeyChecker for the compiler message keys that are used in the Checker Framework.
A node for a conditional and expression:
Represents a conditional basic block.
Implementation of a conditional basic block.
A node for a conditional not expression:
A node for a conditional or expression:
A meta-annotation that indicates that an annotation E is a conditional postcondition annotation, i.e., E is a type-specialized version of EnsuresQualifierIf or EnsuresQualifierIf.List.
Implementation of a TransferResult with two non-exceptional stores.
 
 
Run constant propagation for a specific file and create a PDF of the CFG.
A store that records information about constant values.
 
ConstraintMap holds simplified versions of the TUConstraints for ALL type variable for which we are inferring an argument.
Converts a set of TUConstraints into a ConstraintMap.
A contract represents an annotation on an expression.
Represents a conditional postcondition that must be verified by BaseTypeVisitor or one of its subclasses.
Enumerates the kinds of contracts.
A postcondition contract.
A precondition contract.
A utility class to retrieve pre- and postconditions from a method.
A control flow graph (CFG for short) of a single method.
Elements of this enumeration are used in a Format annotation to indicate the valid types that may be passed as a format parameter.
A marker annotation, written on a class declaration, that signifies that one or more of the class's type parameters can be treated covariantly.
Indicates that the method resets the expression's must-call type to its declared type.
A wrapper annotation that makes the CreatesMustCallFor annotation repeatable.
This interface should be implemented by all type factories that can provide an ExecutableElement for CreatesMustCallFor and CreatesMustCallFor.List.
Utility methods to convert targets of @CreatesMustCallFor annotations to JavaExpressions.
Electric current.
A ListTreeAnnotator implementation that additionally outputs debugging information.
A helper class that puts the declaration annotations from a method declaration back into the corresponding Elements, so that they get stored in the bytecode by the compiler.
A node for a deconstrutor pattern.
Deprecated.
use org.plumelib.util.DeepCopyable
Represents a mapping from an Annotation to a TypeUseLocation it should be applied to during defaulting.
An AnnotatedTypeFormatter used by default by all AnnotatedTypeFactory (and therefore all annotated types).
A scanning visitor that prints the entire AnnotatedTypeMirror passed to visit.
A utility for converting AnnotationMirrors to Strings.
A meta-annotation applied to the declaration of a type qualifier.
Adds annotations to a type based on the use of a type.
Utility class for applying the annotations inferred by dataflow to a given type.
An implementation of JointJavacJavaParserVisitor where process methods do nothing.
Applied to a declaration of a package, type, method, variable, etc., specifies that the given annotation should be the default.
A wrapper annotation that makes the DefaultQualifier annotation repeatable.
Declaration annotation applied to type declarations to specify the qualifier to be added to unannotated uses of the type.
Indicates that the annotated qualifier is the default qualifier in the qualifier hierarchy: it applies if the programmer writes no explicit qualifier and no other default has been specified for the location.
This is the default implementation of QualifierKindHierarchy.
The default implementation of QualifierKind.
Default implementation of AbstractQualifierPolymorphism.
Default implementation of ReflectionResolver.
An implementation of TypeArgumentInference that mostly follows the process outlined in JLS7 See the JLS 7: JLS §5.12.2.7
Default implementation of TypeHierarchy that implements the JLS specification with minor deviations as outlined by the Checker Framework manual.
Degrees.
Helper class for creating dependent type annotation error strings.
A class that helps checkers use qualifiers that are represented by annotations with Java expression strings.
Standardizes Java expressions in annotations and also viewpoint-adapts field accesses.
A DetachedVarSymbol represents a variable that is not part of any AST Tree.
A method is called deterministic if it returns the same value (according to ==) every time it is called with the same arguments and in the same environment.
A DiagMessage is a kind, a message key, and arguments.
The kinds of errors that can be encountered during typechecking.
An annotation indicating the possible values for a String type.
This is an annotation processor that does nothing.
DOTCFGVisualizer<V extends AbstractValue<V>,S extends Store<S>,T extends TransferFunction<V,S>>
Generate a graph description in the DOT language of a control graph.
This is a string that is a valid fully qualified name and a valid binary name.
This is a string that is a valid fully qualified name and a valid binary name or primitive type.
A visitor that visits two JavaParser ASTs simultaneously that almost match.
A node for a double literal.
 
An annotation indicating the possible values for a double or float type.
An effect -- either UIEffect, PolyUIEffect, or SafeEffect.
 
Utility methods for adding the annotations that are stored in an Element to the type that represents that element (or a use of that Element).
Utility methods for adding the annotations that are stored in an Element to the type that represents that element (or a use of that Element).
An ERROR TypeKind was found.
Exception indicating an invalid location for an annotation was found.
A QualifierHierarchy where qualifiers may be represented by annotations with elements.
Utility methods for analyzing Elements.
A postcondition contract that a method calls the given method on the given expression when that method throws an exception.
Indicates that the method, if it terminates successfully, always invokes the given methods on the given expressions.
A wrapper annotation that makes the EnsuresCalledMethods annotation repeatable.
Indicates that the method, if it terminates with the given result, invokes the given methods on the given expressions.
A wrapper annotation that makes the EnsuresCalledMethodsIf annotation repeatable.
Indicates that the method, if it terminates by throwing an Exception, always invokes the given methods on the given expressions.
A wrapper annotation that makes the EnsuresCalledMethodsOnException annotation repeatable.
Indicates that the method, if it terminates successfully, always invokes the given methods on all of the arguments passed in the varargs position.
A method postcondition annotation indicates which fields the method definitely initializes.
A wrapper annotation that makes the EnsuresInitializedFields annotation repeatable.
Indicates that the value expressions evaluate to a value that is a key in all the given maps, if the method terminates successfully.
A wrapper annotation that makes the EnsuresKeyFor annotation repeatable.
Indicates that the given expressions evaluate to a value that is a key in all the given maps, if the method returns the given result (either true or false).
A wrapper annotation that makes the EnsuresKeyForIf annotation repeatable.
Indicates that the given expressions are held if the method terminates successfully.
A wrapper annotation that makes the EnsuresLockHeld annotation repeatable.
Indicates that the given expressions are held if the method terminates successfully and returns the given result (either true or false).
A wrapper annotation that makes the EnsuresLockHeldIf annotation repeatable.
Indicates that the value expressions evaluate to an integer whose value is less than the lengths of all the given sequences, if the method terminates successfully.
A wrapper annotation that makes the EnsuresLTLengthOf annotation repeatable.
Indicates that the given expressions evaluate to an integer whose value is less than the lengths of all the given sequences, if the method returns the given result (either true or false).
A wrapper annotation that makes the EnsuresLTLengthOfIf annotation repeatable.
Indicates that the value of the given expression is a sequence containing at least the given number of elements, if the method returns the given result (either true or false).
A wrapper annotation that makes the EnsuresMinLenIf annotation repeatable.
Indicates that the value expressions are non-null just after a method call, if the method terminates successfully.
A wrapper annotation that makes the EnsuresNonNull annotation repeatable.
Indicates that the given expressions are non-null, if the method returns the given result (either true or false).
* A wrapper annotation that makes the EnsuresNonNullIf annotation repeatable.
Indicates that the expression evaluates to a non-empty Optional, if the method terminates successfully.
Indicates that the given expressions of type Optional<T> are present, if the method returns the given result (either true or false).
A wrapper annotation that makes the EnsuresPresentIf annotation repeatable.
A postcondition annotation to indicate that a method ensures that certain expressions have a certain type qualifier once the method has successfully terminated.
A wrapper annotation that makes the EnsuresQualifier annotation repeatable.
A conditional postcondition annotation to indicate that a method ensures that certain expressions have a certain qualifier once the method has terminated, and if the result is as indicated by result.
A wrapper annotation that makes the EnsuresQualifierIf annotation repeatable.
An annotation indicating the possible values for an enum type.
EqualitiesSolver infers type arguments for targets using the equality constraints in ConstraintMap.
Compares two annotated type mirrors for structural equality using only the primary annotations and underlying types of the two input types and their component types.
Method declaration annotation that indicates a method has a specification like equals().
A node for an equality check:
EquivalentAtmComboScanner is an AtmComboVisitor that accepts combinations that are identical in TypeMirror structure but might differ in contained AnnotationMirrors.
Represents a basic block that contains exactly one Node which can throw an exception.
Implementation of ExceptionBlock.
Utilities for executing external processes.
 
After this visitor visits a tree, ExpectedTreesVisitor.getTrees() returns all the trees that should match with some JavaParser node.
A node for a reference to 'this'.
A node for an expression that is used as a statement.
An extended node can be one of several things (depending on its type): NODE: NodeHolder.
Extended node types (description see above).
A constraint of the form: F 《 A or A 》 F
F2AReducer takes an F2A constraint that is not irreducible (@see AFConstraint.isIrreducible) and reduces it by one step.
The bottom type in the initialization type system.
A generic fake enumeration qualifier that is parameterized by a name.
The type factory for the Fenum Checker.
The bottom type in the Fenum type system.
The main checker class for the Fake Enum Checker.
The top of the fake enumeration type hierarchy.
An unqualified type.
The visitor for Fenum Checker.
A FieldAccess represents a field access.
A node for a field access, including a method accesses:
Represents a field descriptor (JVM type format) as defined in the Java Virtual Machine Specification, section 4.3.2.
Represents a field descriptor (JVM type format) for a primitive as defined in the Java Virtual Machine Specification, section 4.3.2.
Represents a field descriptor for a primitive or for an array whose base type is primitive or in the unnamed package.
Specifies that a field's type, in the class on which this annotation is written, is a subtype of its declared type.
Represents field invariants, which the user states by writing @FieldInvariant.
File-based implementation of AnnotationFileResource.
This formal parameter annotation indicates that the method searches for the given value, using reference equality (==).
A constraint of the form: F = A or A = F
FIsAReducer takes an FIsA constraint that is not irreducible (@see AFConstraint.isIrreducible) and reduces it by one step.
A node for the floating-point division:
A node for the floating-point remainder:
A node for a float literal.
 
A utility class to support fluent API generators so the checker can add @This annotations on method return types when a generator has been used.
Units of force.
A formal parameter, represented by its 1-based index.
This annotation, attached to a String type, indicates that the String may be passed to Formatter.format and similar methods.
The bottom type in the Format String type system.
Annotation for a method that takes a printf-style format string as an argument followed by arguments for that format string.
If this annotation is attached to a Formatter.format-like method, then the first parameter of type String is treated as a format string for the following arguments.
Adds Format to the type of tree, if it is a String or char literal that represents a satisfiable format.
A type-checker plug-in for the Format qualifier that finds syntactically invalid formatter calls.
 
This class provides a collection of utilities to ease working with syntax trees that have something to do with Formatters.
Describes the ways a format method may be invoked.
A wrapper around a value of type E, plus an ExpressionTree location.
Whenever a format method invocation is found in the syntax tree, checks are performed as specified in the Format String Checker manual.
This class provides a collection of utilities to ease working with format strings.
 
 
Annotation for methods like Class.forName.
This interface defines a forward analysis, given a control flow graph and a forward transfer function.
An implementation of a forward analysis to solve a org.checkerframework.dataflow problem given a control flow graph and a forward transfer function.
Interface of a forward transfer function for the abstract interpretation used for the forward flow analysis.
An extension of binary name format to represent primitives and arrays.
If a method is annotated with this declaration annotation, then its signature is not written in a stub file and the method is not declared in source.
If a method is annotated with this declaration annotation, then its signature was read from a stub file.
A sequence of dot-separated identifiers, followed by any number of array square brackets.
A node for member references and lambdas.
Gram.
A factory that extends AnnotatedTypeFactory to optionally use flow-sensitive qualifier inference.
Track the state of org.checkerframework.dataflow analysis scanning for each class tree in the compilation unit.
Annotation for methods like Object.getClassName.
Annotation for methods like Class.getConstructor, whose signature is:
@MethodVal(classname=c, methodname="<init>", params=p) Constructor<T> method(Class<c> this, Object... params)
Annotation for methods like Class.getMethod and Class.getDeclaredMethod, whose signature is:
{@link MethodVal}(classname=c, methodname=m, params=p) Method getMyMethod(Class<c> this, String m, Object... params)
A class used to determine the greatest lower bounds for a set of AnnotatedTypeMirrors.
A node for the greater than comparison:
A node for the greater than or equal comparison:
The annotated expression evaluates to an integer greater than or equal to -1.
Indicates that a thread may dereference the value referred to by the annotated variable only if the thread holds all the given lock expressions.
The bottom type in the GuardedBy type system.
It is unknown what locks guard the value referred to by the annotated variable.
If a variable x has type @GuardSatisfied, then all lock expressions for x's value are held.
The GUI Effect Checker.
Annotated type factory for the GUI Effect Checker.
Require that only UI code invokes code with the UI effect.
Hour.
Computes the hashcode of an AnnotatedTypeMirror using the underlying type and primary annotations and the hash code of component types of AnnotatedTypeMirror.
This is a declaration annotation that applies to type declarations and packages.
The annotated sequence contains a subsequence that is equal to the value of some other expression.
Utilities for determining tree-based heuristics.
A base class for tree-matching algorithms.
match() returns true if called on a path whose leaf has the given kind (supplied at object initialization).
match() returns true if any of the given matchers returns true.
 
match() returns true if called on a path, any element of which matches the given matcher (supplied at object initialization).
match() returns true if called on a path whose leaf is within the "then" clause of an if whose conditon matches the matcher (supplied at object initialization).
Indicates a method precondition: the specified expressions must be held when the annotated method is invoked.
 
A type-checker that enforces (and finds the violations of) two properties: Only localized output gets emitted to the user Only localizable keys (i.e.
This annotation is used internally to annotate I18nFormatUtil.hasFormat() and similar methods.
Elements of this enumeration are used in a I18nFormat annotation to indicate the valid types that may be passed as a format parameter.
This annotation, attached to a String type, indicates that the String may be passed to MessageFormat.format.
The bottom type in the Internationalization Format String type system.
This annotation indicates that when a string of the annotated type is passed as the first argument to MessageFormat.format(String, Object...), then the expression that is an argument to the annotation can be passed as the remaining arguments, in varargs style.
Adds I18nFormat to the type of tree, if it is a String or char literal that represents a satisfiable format.
A type-checker plug-in for the qualifier that finds syntactically invalid i18n-formatter calls (MessageFormat.format()).
The transfer function for the Internationalization Format String Checker.
This class provides a collection of utilities to ease working with syntax trees that have something to do with I18nFormatters.
Describe the format annotation type.
Whenever a method with I18nFormatFor annotation is invoked, it will perform the format string verification.
This class provides a collection of utilities to ease working with i18n format strings.
This annotation, attached to a String type, indicates that if the String is passed to MessageFormat.format(String, Object...), an exception will result.
This annotation is used internally to annotate ResourceBundle.getString(java.lang.String) indicating the checker to check if the given key exist in the translation file and annotate the result string with the correct format annotation according to the corresponding key's value.
A type-checker that checks that only localized Strings are visible to the user.
The top qualifier.
This annotation is used internally to annotate I18nFormatUtil.isFormat().
An identifier.
An identifier or a primitive type.
This annotation can be used two ways:
Represents all of the information needed to execute the Javac compiler for a given set of test files.
A node to model the implicit this, e.g., in a field access.
Impure is a method annotation that means the method might have side effects and/or might be nondeterministic.
This class provides methods shared by the Index Checker's internal checkers in their transfer functions.
A type checker for preventing out-of-bounds accesses on fixed-length sequences, such as arrays and strings.
An integer that can be used to index any of the given sequences.
Given a Tree or other construct, this class has methods to query whether it is a particular method call.
An integer that, for each of the given sequences, is either a valid index or is equal to the sequence's length.
An integer that is either -1 or is a valid index for each of the given sequences.
This struct contains all of the information that the refinement functions need.
A collection of utility functions used by several Index Checker subcheckers.
Represents the result from inferring type arguments.
When one of the constraint solvers infers that a the target has a given type/target in ALL qualifier hierarchies or that given an additional set of annotations that we know the target must hold we have covered all hierarchies then it creates an InferredValue to represent this inference.
Indicates that a corresponding target was inferred to be the field "target" in the hierarchies not overridden by additionalAnnotations.
Indicates that a corresponding target was inferred to be the field "type" in all hierarchies.
This annotation is an alias for MustCall that applies to the type on which it is written and all of its subtypes.
A meta-annotation that specifies if a declaration annotation should be inherited.
The annotated type factory for the freedom-before-commitment type-system.
Tracks whether a value is initialized (all its fields are set), and checks that values are initialized before being used.
A store that extends CFAbstractStore and additionally tracks which fields of the 'self' reference have been initialized.
A transfer function that extends CFAbstractTransfer and tracks InitializationStores.
The visitor for the freedom-before-commitment type-system.
This type qualifier belongs to the freedom-before-commitment initialization tracking type-system.
Indicates which fields have definitely been initialized.
The annotated type factory for the Initialized Fields Checker.
The bottom type qualifier for the Initialized Fields type system.
The Initialized Fields Checker.
Accumulates the names of fields that are initialized.
This program inserts annotations from an ajava file into a Java file.
A node for the instanceof operator:
A node for the integer division:
A node for an integer literal.
 
A node for the integer remainder:
The syntax for binary names that appears in a class file, as defined in the JVM Specification, section 4.2.
Miscellaneous static utility methods.
Indicates that a variable has been interned, i.e., that the variable refers to the canonical representation of an object.
Indicates that no other value is equals() to the given value.
An AnnotatedTypeFactory that accounts for the properties of the Interned type system.
A type-checker plug-in for the Interned qualifier that finds (and verifies the absence of) equality-testing and interning errors.
Typechecks source code for interning violations.
Method declaration annotation used to indicate that this method may be invoked on an uninterned object and that it returns an interned object.
An expression with this type evaluates to an integral value (byte, short, char, int, or long) in the given range.
An expression with this type is exactly the same as an IntRange annotation whose from field is -1 and whose to field is Integer.MAX_VALUE.
An expression with this type is exactly the same as an IntRange annotation whose from field is 0 and whose to field is Integer.MAX_VALUE.
An expression with this type is exactly the same as an IntRange annotation whose from field is 1 and whose to field is Integer.MAX_VALUE.
An annotation indicating the possible values for a byte, short, char, int, or long type.
This annotation, attached to a String type, indicates that the string is not a legal format string.
A meta-annotation indicating that an annotation is a type qualifier that should not be visible in output.
Annotation for methods like Method.invoke, whose signature is:
Object method({@link MethodVal}(classname=c, methodname=m, params=p) Method this, Object obj, Object... args)
Adds annotations to types that are not relevant specified by the RelevantJavaTypes on a checker.
JarEntry-based implementation of AnnotationFileResource.
An annotation processor for counting a few specific aspects about the size of Java code: The number of type parameter declarations and uses.
This class reads expected javac diagnostics from a single file.
This class represents a Java expression and its type.
An annotation to use on an element of a dependent type qualifier to specify which elements of the annotation should be interpreted as Java expressions.
This class calls JavaExpressionConverter.convert(JavaExpression) on each subexpression of the JavaExpression and returns a new JavaExpression built from the result of calling convert on each subexpression.
Optimize the given JavaExpression.
Helper methods to parse a string that represents a restricted Java expression.
An exception that indicates a parse error.
A simple scanner for JavaExpression.
A simple visitor for JavaExpression.
Utility methods for working with JavaParser.
Process Java source files in a directory to produce, in-place, minimal stub files.
A visitor that processes javac trees and JavaParser nodes simultaneously, matching corresponding nodes.
A JointJavacJavaParserVisitor that visits all javac trees with their corresponding JavaParser nodes and performs some default action on each pair.
Kelvin (unit of temperature).
Indicates that the value assigned to the annotated variable is a key for at least the given map(s).
Boilerplate code to glue together all the parts the KeyFor dataflow classes.
 
The bottom type in the Map Key type system.
For the following initializations we wish to propagate the annotations from the left-hand side to the right-hand side or vice versa:
KeyForPropagator is used to move nested KeyFor annotations in type arguments from one side of a pseudo-assignment to the other.
 
 
A type-checker for determining which values are keys for which maps.
KeyForTransfer ensures that java.util.Map.put and containsKey cause the appropriate @KeyFor annotation to be added to the key.
KeyForValue holds additional information about which maps this value is a key for.
Kilogram.
Kilometer.
Square kilometer.
Cubic kilometer.
Kilometer per hour.
Kilonewton.
A label is used to refer to other extended nodes using a mapping from labels to extended nodes.
A node for the single expression body of a single-expression lambda.
This annotation is used on a formal parameter to indicate that the parameter may be returned, but it is not otherwise leaked.
A node for bitwise left shift operations:
Units of length.
An integer that, for each of the given sequences, is equal to the sequence's length.
An annotation indicating the relationship between values with a byte, short, char, int, or long type.
The type factory for the Less Than Checker.
The bottom type in the LessThan type system.
An internal checker that estimates which expression's values are less than other expressions' values.
A node for the less than comparison:
A node for the less than or equal comparison:
Implements 3 refinement rules: 1.
The top qualifier for the LessThan type hierarchy.
The visitor for the Less Than Checker.
ListTreeAnnotator is a TreeVisitor that executes a list of TreeAnnotator for each tree visited.
ListTypeAnnotator is a TypeAnnotator that executes a list of TypeAnnotator for each type visited.
Specifies kinds of literal trees.
Adds annotations to a type based on the contents of a tree.
The playground of live variable analysis.
A LiveVarNode contains a CFG node, which can only be a LocalVariableNode or FieldAccessNode.
A live variable store contains a set of live variables represented by nodes.
A live variable transfer function.
Indicates that the String is a key into a property file or resource bundle containing Localized Strings.
A PropertyKeyATF that uses LocalizableKey to annotate the keys.
The bottom type in the Internationalization type system.
A type-checker that checks that only valid localizable keys are used when using localizing methods (e.g.
Indicates that the String type has been localized and formatted for the target output locale.
A local variable.
A node for a local variable or a parameter:
The analysis class for the lock type system.
LockAnnotatedTypeFactory builds types with @LockHeld and @LockPossiblyHeld annotations.
The Lock Checker.
Indicates that an expression is used as a lock and the lock is known to be held on the current thread.
The method neither acquires nor releases locks, nor do any of the methods that it calls.
Indicates that an expression is not known to be LockHeld.
The Lock Store behaves like CFAbstractStore but requires the ability to insert exact annotations.
LockTransfer handles constructors, initializers, synchronized methods, and synchronized blocks.
A TreeAnnotator implementation to apply special type introduction rules to string concatenations, binary comparisons, and new array instantiations.
The LockVisitor enforces the special type-checking rules described in the Lock Checker manual chapter.
Lombok support for the Called Methods Checker.
A node for a long literal.
 
Implements the introduction rules for the Lower Bound Checker.
The bottom type of the lower bound type system.
A type-checker for preventing fixed-length sequences such as arrays or strings from being accessed with values that are too low.
Implements dataflow refinement rules based on tests: <, >, ==, and their derivatives.
The annotated expression evaluates to value that might be -2 or lower.
Implements the actual checks to make sure that array accesses aren't too low.
The annotated expression evaluates to an integer whose value is less than or equal to the lengths of all the given sequences.
The annotated expression evaluates to an integer whose value is less than the lengths of all the given sequences.
The annotated expression evaluates to an integer whose value is at least 2 less than the lengths of all the given sequences.
Units of luminance.
Meter.
Square meter.
Cubic meter.
A taglet for processing the @checker_framework.manual javadoc block tag, which inserts references to the Checker Framework manual into javadoc.
MarkerNodes are no-op Nodes used for debugging information.
Units of mass.
An annotation indicating the possible values for a String type.
An expression with this type might have an alias.
Temporary type qualifier:
The Optional container may or may not contain a value.
The method, or one of the methods it calls, might release locks that were held prior to the method being called.
A node for a method access, including a receiver:
Adds annotations from element to the return type, formal parameter types, type parameters, and throws clauses of the AnnotatedExecutableType type.
A call to a @Deterministic method.
Represents a method descriptor (JVM representation of method signature) as defined in the Java Virtual Machine Specification, section 4.3.3.
A node for method invocation.
Applies the annotations present for a method type parameter onto an AnnotatedTypeVariable.
This represents a set of Method or Constructor values.
AnnotatedTypeFactory for the MethodVal Checker.
The bottom type in the MethodVal type system.
The MethodVal Checker provides a sound estimate of the signature of Method objects.
 
Minute.
The value of the annotated expression is a sequence containing at least the given number of elements.
A specialization of FieldInvariant for specifying the minimum length of an array.
MixedUnits is the result of multiplying or dividing units, where no more specific unit is known from a UnitsRelations implementation.
Millimeter.
Square millimeter.
Cubic millimeter.
Mole (unit of Substance).
Indicates that once the field (or variable) becomes non-null, it never becomes null again.
A meta-annotation that indicates that a qualifier indicates that an expression goes monotonically from a type qualifier T to another qualifier S.
A QualifierHierarchy where qualifiers may be represented by annotations with elements, but most of the qualifiers do not have elements.
Meter per second.
Meter per second squared.
An expression of type @MustCall({"m1", "m2"}) may be obligated to call m1() and/or m2() before it is deallocated, but it is not obligated to call any other methods.
This polymorphic annotation represents an either-or must-call obligation.
The annotated type factory for the Must Call Checker.
This typechecker ensures that @MustCall annotations are consistent with one another.
This class implements the annotation inference algorithm for the Resource Leak Checker.
This copy of the Must Call Checker is identical, except that it does not load the stub files that treat unconnected sockets as @MustCall({}).
Transfer function for the must-call type system.
Primitive types always have no must-call obligations.
The top qualifier in the Must Call type hierarchy.
The visitor for the Must Call Checker.
Newton.
A node for the narrowing primitive conversion operation.
The annotated expression is between -1 and -a.length - 1, inclusive, for each sequence a listed in the annotation.
Annotation for methods like Constructor.newInstance, whose signature is:
T method(MethodVal(classname=c, methodname="<init>", params=p) Constructor this, Object... args)
A type that represents a newly-constructed object.
A node in the abstract representation used for Java code inside a basic block.
Declaration annotation applied to type declarations to specify that the annotation on the type declaration should not be applied to unannotated uses of the type.
A utility class to operate on a given Node.
A visitor for a Node tree.
A QualifierHierarchy where no qualifier has arguments; that is, no qualifier is represented by an annotation with elements.
This annotation is used on a formal parameter to indicate that the parameter is not leaked (stored in a location that could be accessed later) nor returned by the method body.
The annotated expression evaluates to an integer greater than or equal to 0.
If an expression's type is qualified by @NonNull, then the expression never evaluates to null.
This is a declaration annotation that applies to type declarations.
An annotation speculatively used by Lombok's lombok.config checkerframework = true option.
A node for the not equal comparison:
A declaration annotation for fields that indicates that a client might observe the field storing values that are Initialized, UnderInitialization, or UnknownInitialization, regardless of the initialization type annotation on the field's type.
Annotation indicating that ownership should not be transferred to the annotated parameter, field, or method's call sites, for the purposes of Must Call checking.
Nullable is a type annotation that makes no commitments about whether the value is null.
A node for the unary 'nullchk' operation (generated by the Java compiler):
A node for the null literal.
The analysis class for the non-null type system (serves as factory for the transfer function, stores and abstract values.
The annotated type factory for the nullness type-system.
Nullness doesn't call propagation on binary and unary because the result is always @Initialized (the default qualifier).
A DefaultAnnotatedTypeFormatter that prints null literals without their annotations.
 
An implementation of the nullness type-system, parameterized by an initialization type-system for safe initialization.
Behaves like InitializationStore, but additionally tracks whether PolyNull is known to be NonNull or Nullable (or not known to be either).
Transfer function for the non-null type system.
Utility class for the Nullness Checker.
Behaves just like CFValue, but additionally tracks whether at this point PolyNull is known to be NonNull or Nullable (or not known to be either)
The visitor for the nullness type-system.
 
Utility routines for manipulating numbers.
A node for the numerical addition:
A node for the unary minus operation:
A node for the numerical multiplication:
A node for the unary plus operation:
A node for the numerical subtraction:
A node for new object creation.
Dependent type helper for array offset expressions.
An offset equation is 2 sets of Java expression strings, one set of added terms and one set of subtracted terms, and a single integer constant.
Utility class providing every method in Optional, but written for possibly-null references rather than for the Optional type.
OptionalAnnotatedTypeFactory for the Optional Checker.
The bottom type qualifier for the Optional Checker.
A type-checker that prevents misuse of the Optional class.
An method annotation for methods that create an Optional
Methods whose receiver is an Optional and return a non-optional.
Methods whose receiver is an Optional and return an Optional.
The transfer function for the Optional Checker.
This is a utility class for the Optional Checker.
The OptionalVisitor enforces the Optional Checker rules.
Provides methods for querying the Checker's options.
Annotation indicating that ownership should be transferred to the annotated element for the purposes of Must Call checking.
A node representing a package name used in an expression such as a constructor invocation.
Deprecated.
use org.plumelib.util.IPair
Adds annotations to one formal parameter of a method or lambda within a method.
A node for a parameterized type occurring in an expression:
Indicates a String that is not a syntactically valid regular expression.
PerDirectorySuite runs a test class once for each set of javaFiles returned by its method marked with @Parameters
Name
PerDirectorySuite runs a test class once for each set of parameters returned by its method marked with @Parameters
Name
A wrapper object to pass around the result of phase one.
A polymorphic qualifier for the fake enum type system.
A polymorphic qualifier for the Lower Bound and Upper Bound type systems.
Polymorphic qualifier for the Initialized Fields type system.
A polymorphic qualifier for the Interning type system.
A polymorphic qualifier for the Map Key (@KeyFor) type system.
Syntactic sugar for both @PolyValue and @PolySameLen.
A polymorphic qualifier for the Lower Bound type system.
A meta-annotation that indicates that an annotation is a polymorphic type qualifier.
The polymorphic qualifier for the Must Call type system.
A polymorphic qualifier for the non-null type system.
A polymorphic qualifier for the Optional type system.
A polymorphic qualifier for the Regex type system.
A polymorphic qualifier for the SameLen type system.
A polymorphic qualifier for the Signature type system.
A polymorphic qualifier for the signedness type system.
A polymorphic qualifier for the Tainting type system.
Annotation for the polymorphic-UI effect.
Annotation for the polymorphic effect on methods, or on field accesses.
Annotation for the polymorphic type declaration.
A polymorphic qualifier for the units-of-measure type system implemented by the Units Checker.
A polymorphic qualifier for the Upper Bound type system.
A polymorphic qualifier for the Constant Value Checker.
The annotated expression evaluates to an integer greater than or equal to 1.
A meta-annotation that indicates that an annotation E is a postcondition annotation, i.e., E is a type-specialized version of EnsuresQualifier or of EnsuresQualifier.List.
A meta-annotation that indicates that an annotation R is a precondition annotation, i.e., R is a type-specialized version of RequiresQualifier.
SI prefixes.
The Optional container definitely contains a (non-null) value.
A primitive type.
A node representing a primitive type used in an expression such as a field access.
PropagationTreeAnnotator adds qualifiers to types where the resulting type is a function of an input type, e.g.
PropagationTypeAnnotator adds qualifiers to types where the qualifier to add should be transferred from one or more other types.
Indicates that the String type can be used as key in a property file or resource bundle.
This AnnotatedTypeFactory adds PropertyKey annotations to String literals that contain values from lookupKeys.
The bottom type in the PropertyKeyChecker (and associated checkers) qualifier hierarchy.
A type-checker that checks that only valid keys are used to access property files and resource bundles.
Pure is a method annotation that means both SideEffectFree and Deterministic.
 
The type of purity.
AnnotatedTypeFactory for the PurityChecker.
A visitor that determines the purity (as defined by SideEffectFree, Deterministic, and Pure) of a statement or expression.
Perform purity checking only.
Helper class to keep PurityChecker's interface clean.
Result of the PurityChecker.
An annotation intended solely for representing an unqualified type in the qualifier hierarchy for the Purity Checker.
A utility class for working with the SideEffectFree, Deterministic, and Pure annotations.
An annotation to use on an element of a contract annotation to indicate that the element specifies the value of an argument of the qualifier.
Determines the default qualifiers on a type.
Specifies whether the type variable or wildcard has an explicit upper bound (UPPER), an explicit lower bound (LOWER), or no explicit bounds (UNBOUNDED).
A meta-annotation that indicates what qualifier should be given to literals.
Represents multiple type qualifier hierarchies.
Represents a kind of qualifier, which is an annotation class.
This interface holds information about the subtyping relationships between kinds of qualifiers.
Interface to implement qualifier polymorphism.
Class that computes and stores the qualifier upper bounds for type uses.
Radians.
The Range class models a 64-bit two's-complement integral interval, such as all integers between 1 and 10, inclusive.
A ReachingDefinitionNode contains a CFG node, which can only be a AssignmentNode.
The playground for reaching definition analysis.
A reaching definition store contains a set of reaching definitions represented by ReachingDefinitionNode
The reaching definition transfer function.
Interface for reflection resolvers that handle reflective method calls such as Method.invoke(Object, Object...) or Constructor.newInstance(Object...).
Evaluates expressions (such as method calls and field accesses) at compile time, to determine whether they have compile-time constant values.
If a type is annotated as @Regex(n), then the run-time value is a regular expression with n capturing groups.
Adds Regex to the type of tree, in the following cases: a String or char literal that is a valid regular expression concatenation of two valid regular expression values (either String or char) or two partial regular expression values that make a valid regular expression when concatenated.
The bottom type in the Regex type system.
A type-checker plug-in for the Regex qualifier that finds syntactically invalid regular expressions.
The transfer function for the Regex Checker.
Utility methods for regular expressions, most notably for testing whether a string is a regular expression.
A checked version of PatternSyntaxException.
A type-checking visitor for the Regex type system.
A regular basic block that contains a sequence of Nodes.
Implementation of a regular basic block.
Implementation of a TransferResult with just one non-exceptional store.
The method maintains a strictly nondecreasing lock held count on the current thread for any locks that were held prior to the method call.
An annotation on a SourceChecker subclass to specify which Java types are processed by the checker.
Process Java source files to remove annotations that ought to be inferred.
Report all calls of a method that has this annotation, including calls of methods that override this method.
The Report Checker performs semantic searches over a program, for example, to find all methods that override a specific method, all classes that inherit from a specific class, or all uses of do-while-loops (and not also while loops!).
Report all instantiations of a class/interface that has this annotation, including any subclass.
Report all types that extend/implement a type that has this annotation.
Report all methods that override a method with this annotation.
Report all read or write access to a field with this annotation.
An annotation intended solely for representing an unqualified type in the qualifier hierarchy for the Report Checker.
Report all uses of a type that has this annotation.
 
Report all write accesses to a field with this annotation.
Indicates a method precondition: when the method is invoked, the specified expressions must have had the specified methods called on them.
A wrapper annotation that makes the RequiresCalledMethods annotation repeatable.
Indicates a method precondition: the method expects the specified expressions to be non-null when the annotated method is invoked.
A wrapper annotation that makes the RequiresNonNull annotation repeatable.
Indicates a method precondition: the specified expressions of type Optional must be present (i.e., non-empty) when the annotated method is invoked.
A wrapper annotation that makes the RequiresPresent annotation repeatable.
A precondition annotation to indicate that a method requires certain expressions to have a certain qualifier at the time of the call to the method.
A wrapper annotation that makes the RequiresQualifier annotation repeatable.
A utility class to find symbols corresponding to string references (identifiers).
This variant of CFAnalysis extends the set of ignored exception types.
The type factory for the Resource Leak Checker.
The entry point for the Resource Leak Checker.
The transfer function for the resource-leak extension to the called-methods type system.
The visitor for the Resource Leak Checker.
A node for a return statement:
Attach this annotation to a method with the following properties: The first parameter is a format string.
A deprecated variant of org.checkerframework.common.returnsreceiver.qual.This.
The type factory for the Returns Receiver Checker.
Entry point for the Returns Receiver Checker.
The visitor for the Returns Receiver Checker.
A second (1/60 of a minute).
Annotation for the concrete safe effect on methods, or on field accesses.
Class declaration annotation to make methods default to @AlwaysSafe.
An expression whose type has this annotation evaluates to a value that is a sequence, and that sequence has the same length as the given sequences.
The SameLen Checker is used to determine whether there are multiple fixed-length sequences (such as arrays or strings) in a program that share the same length.
The bottom type in the SameLen type system.
An internal checker that collects information about arrays that have the same length.
The transfer function for the SameLen checker.
This type represents any variable that isn't known to have the same length as another sequence.
 
The Search Index Checker is used to help type the results of calls to the JDK's binary search methods.
The bottom type in the Search Index type system.
An internal checker that assists the Index Checker in typing the results of calls to the JDK's Arrays.binarySearch routine.
The annotated expression evaluates to an integer whose length is between -a.length - 1 and a.length - 1, inclusive, for all sequences a listed in the annotation.
The transfer function for the SearchIndexFor checker.
The top type for the SearchIndex type system.
A set of types.
A node for a short literal.
 
A method is called side-effect-free if it has no visible side-effects, such as setting a field of an object that existed before the method was called.
Accounts for the effects of certain calls to String.replace.
The bottom type in the Signature String type system.
The Signature Checker.
Outputs the method signatures of a class with fully annotated types.
The transfer function for the Signature Checker.
Top qualifier in the type hierarchy.
The value is to be interpreted as signed.
The type factory for the Signedness Checker.
The bottom type in the Signedness type system.
A type-checker that prevents mixing of unsigned and signed values, and prevents meaningless operations on unsigned values.
Client code may interpret the value either as Signed or as Unsigned.
This file contains code to special-case shifts whose result does not depend on the MSB of the first argument, due to subsequent masking or casts.
Provides static utility methods for unsigned values, beyond what is available in the JDK's Unsigned Integer API.
Provides more static utility methods for unsigned values.
The SignednessVisitor enforces the Signedness Checker rules.
The expression's value is in the signed positive range; that is, its most significant bit is zero.
A node for bitwise right shift operations with sign extension:
Represents an action to perform on every type.
A simple visitor for AnnotatedTypeMirrors.
SimpleOptionMap is a very basic Option container.
A basic block that has exactly one non-exceptional successor.
A basic block that has at most one successor.
An abstract annotation processor designed for implementing a source-file checker as an annotation processor (a compiler plug-in).
An AST visitor that provides a variety of compiler utilities and interfaces to facilitate type-checking.
Represents a special basic block; i.e., one of the following: Entry block of a method.
The types of special basic blocks.
The implementation of a SpecialBlock.
Units of speed.
StaticallyExecutable is a method annotation that indicates that the compiler is allowed to run the method at compile time, if all of the method's arguments are compile-time constants.
Store<S extends Store<S>>
A store is used to keep track of the information that the org.checkerframework.dataflow analysis has accumulated at any given point in time.
A flow rule describes how stores flow along one edge between basic blocks.
 
Generate the String representation of a control flow graph.
A node for string concatenation:
A node for the string conversion operation.
A node for an string literal.
This interface is both a functional interface, see StringToJavaExpression.toJavaExpression(String), and also a collection of static methods that convert a string to a JavaExpression at common locations.
An annotation indicating the possible values for a String type.
A visitor used to compare two type mirrors for "structural" equality.
Stores the result of StructuralEqualityComparer for type arguments.
An annotation on a SourceChecker subclass to provide additional stub files that should be used in addition to jdk.astub.
Generates a stub file from a single class or an entire package.
Holds information from HasSubsequence annotations.
Units of substance, such as mole (@mol).
Builds types with annotations from the Substring Index checker hierarchy, which contains the @SubstringIndexFor annotation.
The bottom type in the Substring Index type system.
The Substring Index Checker is an internal checker that assists the Index Checker in typing the results of calls to the JDK's String.indexOf and String.lastIndexOf routines.
The annotated expression evaluates to either -1 or a non-negative integer less than the lengths of all the given sequences.
The top type for the Substring Index type system.
A QualifierHierarchy where, when a qualifier has arguments, the subtype relation is determined by a subset test on the elements (arguments).
A QualifierHierarchy where, when a qualifier has arguments, the subtype relation is determined by a superset test on the elements (arguments).
A meta-annotation to specify all the qualifiers that the given qualifier is an immediate subtype of.
Infers type arguments by using the Greatest Lower Bound computation on the subtype relationships in a constraint map.
THIS CLASS IS DESIGNED FOR USE WITH DefaultTypeHierarchy, DefaultRawnessComparer, and StructuralEqualityComparer ONLY.
 
A checker for type qualifier systems that only checks subtyping relationships.
A node for a reference to 'super'.
When discovering supertypes of an AnnotatedTypeMirror we want to annotate each supertype with the annotations of the subtypes class declaration.
Infers type arguments by using the Least Upper Bound computation on the supertype relationships in a constraint map.
An annotation used to indicate what lint options a checker supports.
An annotation used to indicate what Checker Framework options a checker supports.
Specifies the prefixes or checkernames that suppress warnings issued by this checker.
SwingBoxOrientation.
SwingCompassDirection.
SwingElementOrientation.
SwingHorizontalOrientation.
SwingSplitPaneOrientation.
SwingTextOrientation.
Vertical orientations for the title text of a TitledBorder.
Justifications for the title text of a TitledBorder.
SwingVerticalOrientation.
A node for a switch expression.
A class that visits each result expression of a switch expression and calls SwitchExpressionScanner.visitSwitchResultExpression(ExpressionTree, Object) on each result expression.
This represents the start and end of a synchronized code block.
SyntheticArrays exists solely to fix AnnotatedTypeMirrors that need to be adapted from Array type to a specific kind of array.
Utility class for handling System.getProperty(String) and related invocations.
This file contains basic utility functions.
Metric ton.
Denotes a possibly-tainted value: at run time, the value might be tainted or might be untainted.
Annotated type factory for the Tainting Checker.
A type-checker plug-in for the Tainting type system qualifier that finds (and verifies the absence of) trust bugs.
Visitor for the TaintingChecker.
TargetConstraints represents the set of all TUConstraints for which target was the type parameter, i.e.
 
Remember these are constraints in which the target is the subtype.
 
NOTE: This meta-annotation is not currently enforced.
Units of temperature.
TerminatesExecution is a method annotation that indicates that a method terminates the execution of the program.
A node for a conditional expression:
A configuration for running CheckerFrameworkTests or running the TypecheckExecutor.
Used to create an instance of TestConfiguration.
Represents an expected error/warning message in a Java test file or an error/warning reported by the Javac compiler.
Represents a list of TestDiagnostics, which was read from a one line of a file.
A set of utilities and factory methods useful for working with TestDiagnostics.
Defines the path to the directory which holds test java files.
Utilities for testing.
Write @This on the return type of a method that always returns its receiver ( this).
A node for a reference to 'this', either implicit or explicit.
A use of this.
A node for exception throws:
Units of time.
A constraint of the form: T = U
Convert a JAIF file plus a stub file into index files (JAIFs).
Interface of a transfer function for the abstract interpretation used for the flow analysis.
TransferInput<V extends AbstractValue<V>,S extends Store<S>>
TransferInput is used as the input type of the individual transfer functions of a ForwardTransferFunction or a BackwardTransferFunction.
TransferResult<V extends AbstractValue<V>,S extends Store<S>>
TransferResult is used as the result type of the individual transfer functions of a TransferFunction.
TreeAnnotator is an abstract SimpleTreeVisitor to be used with ListTreeAnnotator.
The TreeBuilder permits the creation of new AST Trees using the non-public Java compiler API TreeMaker.
A utility class for displaying the structure of the AST of a program.
 
A utility class for parsing Java expression snippets, and converting them to proper Javac AST nodes.
TreePathCacher is a TreeScanner that creates and caches a TreePath for a target Tree.
Utility methods for obtaining or analyzing a javac TreePath.
A utility class for pretty-printing the AST of a program.
A visitor that performs some default action on a tree and then all of its children.
Utility methods for analyzing a javac Tree.
This is a duplication of com.sun.tools.javac.tree.JCTree.JCMemberReference.ReferenceKind, which is not part of the supported javac API.
This class contains util methods for reflective accessing Tree classes and methods that were added after Java 11.
Utility methods for accessing BindingPatternTree methods.
Utility methods for accessing CaseTree methods.
Utility methods for accessing ConstantCaseLabelTree methods.
Utility methods for accessing DeconstructionPatternTree methods.
Utility methods for accessing InstanceOfTree methods.
Utility methods for accessing PatternCaseLabelTree methods.
Utility methods for accessing SwitchExpressionTree methods.
Utility methods for accessing YieldTree methods.
A constraint of the form: T <: U
A constraint of the form: T :> U
Subclasses of TUConstraint represent constraints between a type parameter, whose type arguments are being inferred, and the types used to do that inference.
Moves annotations in a JavaParser AST from declaration position onto the types they correspond to.
A collection of helper methods related to type annotation handling.
TypeAnnotator is an abstract AnnotatedTypeScanner to be used with ListTypeAnnotator.
Miscellaneous utilities to help in type argument inference.
Instances of TypeArgumentInference are used to infer the types of method type arguments when no explicit arguments are provided.
Records any mapping between the type parameters of a subtype to the corresponding type parameters of a supertype.
A node for the cast operator:
Used by the Checker Framework test suite to run the framework and generate a test result.
Represents the test results from typechecking one or more Java files using the given TestConfiguration.
Apply annotations to a declared type based on its declaration.
Compares AnnotatedTypeMirrors for subtype relationships.
Presents formatted type information for various AST trees in a class.
Specifies kinds of types.
A utility class that helps with TypeKinds.
The type of primitive conversion: narrowing, widening, or same.
A testing class that can be used to test TypeElement.
Stores any explicit annotation in AnnotatedTypeMirrors.
Prints the types of the class and all of its enclosing fields, methods, and inner classes.
A helper class that puts the annotations from an AnnotatedTypeMirrors back into the corresponding Elements, so that they get stored in the bytecode by the compiler.
A utility class that helps with TypeMirrors.
Exception type indicating a mistake by a type system built using the Checker Framework.
Specifies the locations to which a DefaultQualifier annotation applies.
TypeValidator ensures that a type for a given tree is valid both for the tree and the type system that is being used to check the tree.
TypeVariableSusbtitutor replaces type variables from a declaration with arguments to its use.
Apply annotations to the use of a type parameter declaration.
TypeVisualizer prints AnnotatedTypeMirrors as a directed graph where each node is a type and an arrow is a reference.
Abstraction for Upper Bound annotations.
The less-than-length-of qualifier (@LTLengthOf).
Represents an integer value that is known at compile time.
The top type qualifier.
Annotation for the UI effect.
Annotation for the concrete UI effect on methods, or on field accesses.
Package annotation to make all classes within a package @UIType.
Class declaration annotation to make methods default to @UI.
JavaExpression for unary operations.
A node for a postfix or an unary expression.
This type qualifier indicates that an object is (definitely) in the process of being constructed/initialized.
Represents an abstract syntax tree of type Tree that underlies a given control flow graph.
If the underlying AST is a lambda.
If the underlying AST is a method.
If the underlying AST is a statement or expression.
The kinds of underlying ASTs.
An expression with this type has no aliases.
Annotated type factory for the Units Checker.
UnitsQualifierKindHierarchy.
Formats units-of-measure annotations.
Format the error printout of any units qualifier that uses Prefix.one.
 
 
The bottom type in the Units type system.
Units Checker main class.
Define the relation between a base unit and the current unit.
Specify the class that knows how to handle the meta-annotated unit when put in relation (plus, multiply, ...) with another unit.
Interface that is used to specify the relation between units.
Default relations between SI units.
A helper class for UnitsRelations, providing numerous methods which help process Annotations and Annotated Types representing various units.
Utility methods to generate annotated types and to convert between them.
Units visitor.
Stands for any expression that the Dataflow Framework lacks explicit support for.
Represents a Class object whose run-time value is not known at compile time.
A String that might or might not be a compiler message key.
The top qualifier.
This type qualifier indicates how much of an object has been fully initialized.
The top qualifier for the Interning Checker.
Used internally by the type system; should never be written by a programmer.
Indicates that the String type has an unknown localizable key property.
Indicates that the String type has unknown localization properties.
Represents a Method or Constructor expression whose run-time value is not known at compile time.
Indicates that the String type has an unknown property key property.
Represents the top of the Regex qualifier hierarchy.
The value's signedness is not known to the Signedness Checker.
The top type for the Returns Receiver Checker's type system.
UnknownUnits is the top type of the type hierarchy.
UnknownVal is a type annotation indicating that the expression's value is not known at compile type.
A special annotation intended solely for representing an unqualified type in the qualifier hierarchy, as an argument to SubtypeOf.value(), in a type qualifier declaration.
The value is to be interpreted as unsigned.
A node for bitwise right shift operations with zero extension:
Denotes a reference that is untainted, i.e.
Declares that the field may not be accessed if the receiver is of the specified qualifier type (or any supertype).
UnusedAbstractValue is an AbstractValue that is not involved in any lub computation during dataflow analysis.
Implements the introduction rules for the Upper Bound Checker.
The bottom type in the Upper Bound type system.
A type-checker for preventing arrays from being accessed with values that are too high.
A meta-annotation applied to the declaration of a type qualifier.
A literal value.
Contains the transfer functions for the upper bound type system, a part of the Index Checker.
A variable not known to have a relation to any sequence length.
Warns about array accesses that could be too high.
Exception type indicating a mistake by an end user in using the Checker Framework, such as incorrect command-line arguments.
Class declaration to indicate the class does not override equals(Object), and therefore a.equals(b) and a == b behave identically.
AnnotatedTypeFactory for the Value type system.
The Constant Value Checker is a constant propagation analysis: for each variable, it determines whether that variable's value can be known at compile time.
Utility methods for the Value Checker.
JavaExpression for literals.
A node for a literals that have some form of value: integer literal long literal char literal string literal float literal double literal boolean literal null literal
The transfer class for the Value Checker.
Visitor for the Constant Value type system.
Applies annotations to variable declaration (providing they are not the use of a TYPE_PARAMETER).
A node for a variable declaration, including local variables and fields:
This class has methods to viewpoint-adapt JavaExpression by replacing ThisReference and FormalParameter expressions with the given JavaExpressions.
A visitor that visits every node in an AST by default and performs a default action on each node after visiting its children.
Units of volume.
Interface for recording facts at (pseudo-)assignments.
The kinds of output that whole-program inference can produce.
This is the primary implementation of WholeProgramInference.
This is an implementation of WholeProgramInferenceStorage that stores annotations directly with the JavaParser node corresponding to the annotation's location.
This class stores annotations using scenelib objects.
Maps the WholeProgramInferenceScenesStorage.aTypeElementToString(org.checkerframework.afu.scenelib.el.ATypeElement) representation of an ATypeElement and its TypeUseLocation to a set of names of annotations.
Stores annotations from whole-program inference.
A node for the widening primitive conversion operation.