All Classes and Interfaces
Class
Description
Ampere.
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.
AbstractCFGVisualizer<V extends AbstractValue<V>,S extends Store<S>,T extends TransferFunction<V,S>>
This abstract class makes implementing a
CFGVisualizer easier.Whether to visualize before or after a block.
A default implementation of the node visitor interface.
This is the super class for a qualifier,
Qualifier or a qualifier variable, QualifierVar.Implements framework support for qualifier polymorphism.
As explained in section 18.1,
the JLS Chapter on type inference use the term "type" to "include type-like syntax that contains
inference variables".
The kind of
AbstractType.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.A constraint the represent additional argument constraints generated from a method or constructor
invocation that is a part of a larger inference problem.
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.
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.
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.
Helper class for determining if a type contains an inference variable.
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.Substitutes references to captured types in
type using
capturedTypeVarToAnnotatedTypeVar.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).BackwardAnalysis<V extends AbstractValue<V>,S extends Store<S>,T extends BackwardTransferFunction<V,S>>
This interface defines a backward analysis, given a control flow graph and a backward transfer
function.
BackwardAnalysisImpl<V extends AbstractValue<V>,S extends Store<S>,T extends BackwardTransferFunction<V,S>>
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.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.
Manages a set of bounds.
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 bound of the form:
G<a1, ..., an> = capture(G<A1, ..., An>).Variables created as a part of a capture bound.
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<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,T extends CFAbstractTransfer<V,S,T>>
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.
CFAbstractTransfer<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,T extends CFAbstractTransfer<V,S,T>>
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.
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.
<LambdaExpression →throws T>: The checked exceptions thrown by the body of the
LambdaExpression are declared by the throws clause of the function type derived from T.
Util for checked exception constraints.
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.
An extended node of type
ExtendedNode.ExtendedNodeType.CONDITIONAL_JUMP.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.
A constraint.
A kind of Constraint.
A set of constraints and the operations that can be performed on them.
Helper class for determining if a type contains an inference variable.
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.
Implements support for
DefaultQualifierForUse and NoDefaultQualifierForUse.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.Implementation of type argument inference.
Default implementation of TypeHierarchy that implements the JLS specification with minor
deviations as outlined by the Checker Framework manual.
Degrees.
A data structure to hold the dependencies between variables.
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.
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.
An
AnnotatedTypeScanner that scans two AnnotatedTypeMirrors simultaneously and
performs DoubleAnnotatedTypeScanner.defaultAction(AnnotatedTypeMirror, AnnotatedTypeMirror) on the pair.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.
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'.
<Expression → T> An expression is compatible in a loose invocation context with type T
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).
Exception thrown when the Java types make it so that false is inferred.
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 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.ForwardAnalysis<V extends AbstractValue<V>,S extends Store<S>,T extends ForwardTransferFunction<V,S>>
This interface defines a forward analysis, given a control flow graph and a forward transfer
function.
ForwardAnalysisImpl<V extends AbstractValue<V>,S extends Store<S>,T extends ForwardTransferFunction<V,S>>
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.
GenericAnnotatedTypeFactory<Value extends CFAbstractValue<Value>,Store extends CFAbstractStore<Value,Store>,TransferFunction extends CFAbstractTransfer<Value,Store,TransferFunction>,FlowAnalysis extends CFAbstractAnalysis<Value,Store,TransferFunction>>
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 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 condition 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.
Factory that creates AbstractTypes.
The result of type argument inferrece.
A type-like structure that contains at least one inference variable, but is not an inference
variable.
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.
InitializationAnnotatedTypeFactory<Value extends CFAbstractValue<Value>,Store extends InitializationStore<Value,Store>,Transfer extends InitializationTransfer<Value,Transfer,Store>,Flow extends CFAbstractAnalysis<Value,Store,Transfer>>
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.InitializationTransfer<V extends CFAbstractValue<V>,T extends InitializationTransfer<V,T,S>,S extends InitializationStore<V,S>>
A transfer function that extends
CFAbstractTransfer and tracks InitializationStores.InitializationVisitor<Factory extends InitializationAnnotatedTypeFactory<Value,Store,?,?>,Value extends CFAbstractValue<Value>,Store extends InitializationStore<Value,Store>>
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.
A method type for an invocation of a method or constructor.
Performs invocation type inference as described in JLS Section
18.5.2.
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 object to pass around for use during invocation type inference.
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.
Visitor that combines added String literals, see
JavaParserUtil.concatenateAddedStringLiterals(com.github.javaparser.ast.Node).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.
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 a 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
OptionalMethods 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
@ParametersName
PerDirectorySuite runs a test class once for each set of parameters returned by its method marked
with
@ParametersName
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.
A type that does not contain any inference variables.
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 wrapper around an
AnnotationMirror.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.
Represents a constraint between two
AbstractType.Class that computes and stores the qualifier upper bounds for type uses.
A
QualifierVar is a variable for a polymorphic qualifier that needs to be viewpoint
adapted at a call site.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.
A result of reduction.
A reduction result that contains a bound set and a constraint set.
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.Resolution finds an instantiation for each variable in a given set of variables.
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.
Static method
SceneToStubWriter.write(org.checkerframework.common.wholeprograminference.scenelib.ASceneWrapper, java.lang.String, org.checkerframework.common.basetype.BaseTypeChecker) writes an AScene to a file in stub file format.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.
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:
An
AnnotatedTypeScanner that scans an AnnotatedTypeMirror and performs some
SimpleAnnotatedTypeScanner.defaultAction on each type.Represents an action to perform on every type.
A simple visitor for
AnnotatedTypeMirrors.SimpleOptionMap is a very basic command-line 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.
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.
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.
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.An implementation of
SwitchExpressionScanner that uses functions passed to the
constructor for SwitchExpressionScanner.FunctionalSwitchExpressionScanner.visitSwitchResultExpression(ExpressionTree, Object) and SwitchExpressionScanner.FunctionalSwitchExpressionScanner.combineResults(Object, Object).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.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.
A mapping from type variables to inference variables.
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.
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 is used as the input type of the individual transfer functions of a ForwardTransferFunction or a BackwardTransferFunction.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.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.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.
Constraints are between either an expression and a type, two types, or an expression and a thrown
type.
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 in 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.
TypeVariableSubstitutor 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.
Represents a constraint between two
AbstractType.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.
A use of an inference variable.
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.
An inference variable.
Applies annotations to variable declaration (providing they are not the use of a TYPE_PARAMETER).
Data structure to stores the bounds of a variable.
Kind of bound.
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.