org.checkerframework.framework.util

Class ContractsUtils.ConditionalPostcondition

java.lang.Object

org.checkerframework.framework.util.ContractsUtils.Contract

org.checkerframework.framework.util.ContractsUtils.ConditionalPostcondition

Enclosing class:

ContractsUtils

public static class ContractsUtils.ConditionalPostcondition
extends ContractsUtils.Contract

Represents a conditional postcondition that must be verified by BaseTypeVisitor or one of its subclasses. Automatically extracted from annotations with meta-annotation @ConditionalPostconditionAnnotation, such as EnsuresNonNullIf.

Nested Class Summary

Nested classes/interfaces inherited from class org.checkerframework.framework.util.ContractsUtils.Contract

ContractsUtils.Contract.Kind

Field Summary

Fields

Modifier and Type	Field and Description
boolean	annoResult The return value for the annotated method that ensures that the conditional postcondition holds.

Fields inherited from class org.checkerframework.framework.util.ContractsUtils.Contract

annotation, contractAnnotation, expression, kind

Constructor Summary

Constructors

Constructor and Description
ConditionalPostcondition(java.lang.String expression, boolean annoResult, javax.lang.model.element.AnnotationMirror annotation, javax.lang.model.element.AnnotationMirror contractAnnotation) Create a new conditional postcondition.

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

annoResult

public final boolean annoResult

The return value for the annotated method that ensures that the conditional postcondition holds. For example, given
@EnsuresNonNullIf(expression="foo", result=false) boolean method()
foo is guaranteed to be @NonNull after a call to method() if that call returns false.

Constructor Detail

ConditionalPostcondition

public ConditionalPostcondition(java.lang.String expression,
                                boolean annoResult,
                                javax.lang.model.element.AnnotationMirror annotation,
                                javax.lang.model.element.AnnotationMirror contractAnnotation)

Create a new conditional postcondition.

Parameters:

expression - the Java expression that should have a type qualifier

annoResult - whether the condition is the method returning true or false

annotation - the type qualifier that expression should have

contractAnnotation - the postcondition annotation that the programmer wrote; used for diagnostic messages

Method Detail

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class ContractsUtils.Contract

hashCode

public int hashCode()

Overrides:

hashCode in class ContractsUtils.Contract