org.checkerframework.framework.util

Class ContractsUtils.Contract

java.lang.Object

org.checkerframework.framework.util.ContractsUtils.Contract

Direct Known Subclasses:

ContractsUtils.ConditionalPostcondition, ContractsUtils.Postcondition, ContractsUtils.Precondition

Enclosing class:

ContractsUtils

public abstract static class ContractsUtils.Contract
extends java.lang.Object

A contract represents an annotation on an expression, along with the kind: precondition, postcondition, or conditional postcondition.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	ContractsUtils.Contract.Kind

Field Summary

Fields

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

Constructor Summary

Constructors

Constructor and Description
Contract(java.lang.String expression, javax.lang.model.element.AnnotationMirror annotation, javax.lang.model.element.AnnotationMirror contractAnnotation, ContractsUtils.Contract.Kind kind) Creates a new Contract.

Method Summary

Modifier and Type	Method and Description
boolean	equals(java.lang.Object o)
int	hashCode()

Methods inherited from class java.lang.Object

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

Field Detail

expression

public final java.lang.String expression

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

annotation

public final javax.lang.model.element.AnnotationMirror annotation

The annotation that must be on the type of expression as part of this contract.

contractAnnotation

public final javax.lang.model.element.AnnotationMirror contractAnnotation

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

kind

public final ContractsUtils.Contract.Kind kind

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

Constructor Detail

Contract

public Contract(java.lang.String expression,
                javax.lang.model.element.AnnotationMirror annotation,
                javax.lang.model.element.AnnotationMirror contractAnnotation,
                ContractsUtils.Contract.Kind kind)

Creates a new Contract.

Parameters:

expression - the Java expression that should have a type qualifier

annotation - the type qualifier that expression should have

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

kind - precondition, postcondition, or conditional postcondition

Method Detail

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object