Package 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 java.lang.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	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	Description
javax.lang.model.element.AnnotationMirror	annotation	The annotation on the type of expression, according to this contract.
javax.lang.model.element.AnnotationMirror	contractAnnotation	The annotation that expressed this contract; used for diagnostic messages.
java.lang.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	Description
static Contract	create(Contract.Kind kind, java.lang.String expressionString, javax.lang.model.element.AnnotationMirror annotation, javax.lang.model.element.AnnotationMirror contractAnnotation, java.lang.Boolean ensuresQualifierIf)	Creates a new Contract.
boolean	equals(@Nullable java.lang.Object o)
int	hashCode()
java.lang.String	toString()
javax.lang.model.element.AnnotationMirror	viewpointAdaptDependentTypeAnnotation(GenericAnnotatedTypeFactory<?,?,?,?> factory, StringToJavaExpression stringToJavaExpr, @Nullable com.sun.source.tree.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 java.lang.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 javax.lang.model.element.AnnotationMirror annotation

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

contractAnnotation

public final javax.lang.model.element.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,
                              java.lang.String expressionString,
                              javax.lang.model.element.AnnotationMirror annotation,
                              javax.lang.model.element.AnnotationMirror contractAnnotation,
                              java.lang.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 java.lang.Object o)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

viewpointAdaptDependentTypeAnnotation

public javax.lang.model.element.AnnotationMirror viewpointAdaptDependentTypeAnnotation(GenericAnnotatedTypeFactory<?,?,?,?> factory,
                                                                                       StringToJavaExpression stringToJavaExpr,
                                                                                       @Nullable com.sun.source.tree.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