| Interface | Description | 
|---|---|
| AnnotationFormatter | 
 Converts AnnotationMirrors to Strings. 
 | 
| OptionConfiguration | 
 Provides methods for querying the Checker's options. 
 | 
| QualifierKind | 
 Represents a kind of qualifier, which is an annotation class. 
 | 
| QualifierKindHierarchy | 
 This interface holds information about the subtyping relationships between kinds of qualifiers. 
 | 
| StringToJavaExpression | 
 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. | 
| Class | Description | 
|---|---|
| AnnotatedTypes | 
 Utility methods for operating on  
AnnotatedTypeMirror. | 
| AnnotationMirrorMap<V> | 
 The Map interface defines some of its methods with respect to the equals method. 
 | 
| AnnotationMirrorSet | 
 The Set interface defines many methods with respect to the equals method. 
 | 
| CheckerMain | 
 This class behaves similarly to javac. 
 | 
| Contract | 
 A contract represents an annotation on an expression. 
 | 
| Contract.ConditionalPostcondition | 
 Represents a conditional postcondition that must be verified by  
BaseTypeVisitor or one
 of its subclasses. | 
| Contract.Postcondition | 
 A postcondition contract. 
 | 
| Contract.Precondition | 
 A precondition contract. 
 | 
| ContractsFromMethod | 
 A utility class to retrieve pre- and postconditions from a method. 
 | 
| DefaultAnnotationFormatter | 
 A utility for converting AnnotationMirrors to Strings. 
 | 
| DefaultQualifierKindHierarchy | 
 This is the default implementation of  
QualifierKindHierarchy. | 
| DefaultQualifierKindHierarchy.DefaultQualifierKind | 
 The default implementation of  
QualifierKind. | 
| ExecUtil | |
| ExecUtil.Redirection | |
| FieldInvariants | 
 Represents field invariants, which the user states by writing  
@FieldInvariant. | 
| GraphQualifierHierarchy | Deprecated
 See notes in  
MultiGraphQualifierHierarchy about how to convert existing
     subclasses to the new classes. | 
| Heuristics | 
 Utilities for determining tree-based heuristics. 
 | 
| Heuristics.Matcher | 
 A base class for tree-matching algorithms. 
 | 
| Heuristics.OfKind | 
match() returns true if called on a path whose leaf has the given kind (supplied at
 object initialization). | 
| Heuristics.OrMatcher | 
match() returns true if any of the given matchers returns true. | 
| Heuristics.PreceededBy | |
| Heuristics.Within | 
match() returns true if called on a path, any element of which matches the given
 matcher (supplied at object initialization). | 
| Heuristics.WithinTrueBranch | 
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). | 
| JavaExpressionParseUtil | 
 Helper methods to parse a string that represents a restricted Java expression. 
 | 
| JavaParserUtil | 
 Utility methods for working with JavaParser. 
 | 
| JavaParserUtil.StringLiteralConcatenateVisitor | 
 Visitor that combines added String literals, see  
JavaParserUtil.concatenateAddedStringLiterals(com.github.javaparser.ast.Node). | 
| MultiGraphQualifierHierarchy | Deprecated | 
| MultiGraphQualifierHierarchy.MultiGraphFactory | Deprecated
 Use  
ElementQualifierHierarchy instead. | 
| PurityAnnotatedTypeFactory | 
 AnnotatedTypeFactory for the  
PurityChecker. | 
| PurityChecker | 
 Perform purity checking only. 
 | 
| TreePathCacher | 
 TreePathCacher is a TreeScanner that creates and caches a TreePath for a target Tree. 
 | 
| TypeArgumentMapper | 
 Records any mapping between the type parameters of a subtype to the corresponding type parameters
 of a supertype. 
 | 
| VoidVisitorWithDefaultAction | 
 A visitor that visits every node in an AST by default and performs a default action on each node
 after visiting its children. 
 | 
| Enum | Description | 
|---|---|
| AtmCombo | 
 An enum representing the cartesian product of the set of AtmKinds with itself. 
 | 
| Contract.Kind | 
 Enumerates the kinds of contracts. 
 | 
| Exception | Description | 
|---|---|
| JavaExpressionParseUtil.JavaExpressionParseException | 
 An exception that indicates a parse error. 
 |