org.checkerframework.framework.util

Class Contract

java.lang.Object

org.checkerframework.framework.util.Contract

Direct Known Subclasses:

Contract.ConditionalPostcondition, Contract.Postcondition, Contract.Precondition

public abstract class Contract
extends Object

A contract represents an annotation on an expression. It is a precondition, postcondition, or conditional postcondition.

See Also:

Contract.Precondition, Contract.Postcondition, Contract.ConditionalPostcondition

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	Contract.ConditionalPostcondition Represents a conditional postcondition that must be verified by BaseTypeVisitor or one of its subclasses.
static class	Contract.Kind Enumerates the kinds of contracts.
static class	Contract.Postcondition A postcondition contract.
static class	Contract.Precondition A precondition contract.

Field Summary

Fields

Modifier and Type	Field and Description
AnnotationMirror	annotation The annotation on the type of expression, according to this contract.
AnnotationMirror	contractAnnotation The annotation that expressed this contract; used for diagnostic messages.
String	expressionString The expression for which the condition must hold, such as "foo" in @RequiresNonNull("foo").
Contract.Kind	kind The kind of contract: precondition, postcondition, or conditional postcondition.

Method Summary

Modifier and Type	Method and Description
static Contract	create(Contract.Kind kind, String expressionString, AnnotationMirror annotation, AnnotationMirror contractAnnotation, Boolean ensuresQualifierIf) Creates a new Contract.
boolean	equals(@Nullable Object o)
int	hashCode()
String	toString()
AnnotationMirror	viewpointAdaptDependentTypeAnnotation(GenericAnnotatedTypeFactory<?,?,?,?> factory, StringToJavaExpression stringToJavaExpr, @Nullable Tree errorTree) Viewpoint-adapt annotation using stringToJavaExpr.

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

expressionString

public final String expressionString

The expression for which the condition must hold, such as "foo" in @RequiresNonNull("foo").

An annotation like @RequiresNonNull({"a", "b", "c"}) would be represented by multiple Contracts.

annotation

public final AnnotationMirror annotation

The annotation on the type of expression, according to this contract.

contractAnnotation

public final AnnotationMirror contractAnnotation

The annotation that expressed this contract; used for diagnostic messages.

kind

public final Contract.Kind kind

The kind of contract: precondition, postcondition, or conditional postcondition.

Method Detail

create

public static Contract create(Contract.Kind kind,
                              String expressionString,
                              AnnotationMirror annotation,
                              AnnotationMirror contractAnnotation,
                              Boolean ensuresQualifierIf)

Creates a new Contract.

Parameters:

kind - precondition, postcondition, or conditional postcondition

expressionString - the Java expression that should have a type qualifier

annotation - the type qualifier that expressionString should have

contractAnnotation - the pre- or post-condition annotation that the programmer wrote; used for diagnostic messages

ensuresQualifierIf - the ensuresQualifierIf field, for a conditional postcondition

Returns:

a new contract

equals

public boolean equals(@Nullable Object o)

Overrides:

equals in class Object

hashCode

public int hashCode()

Overrides:

hashCode in class Object

toString

public String toString()

Overrides:

toString in class Object

viewpointAdaptDependentTypeAnnotation

public AnnotationMirror viewpointAdaptDependentTypeAnnotation(GenericAnnotatedTypeFactory<?,?,?,?> factory,
                                                              StringToJavaExpression stringToJavaExpr,
                                                              @Nullable Tree errorTree)

Viewpoint-adapt annotation using stringToJavaExpr.

For example, if the contract is @EnsuresKeyFor(value = "this.field", map = "map"), annotation is @KeyFor("map"). This method applies stringToJava to "map" and returns a new KeyFor annotation with the result.

Parameters:

factory - used to get DependentTypesHelper

stringToJavaExpr - function used to convert strings to JavaExpressions

errorTree - if non-null, where to report any errors that occur when parsing the dependent type annotation; if null, report no errors

Returns:

the viewpoint-adapted annotation, or annotation if it is not a dependent type annotation