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, expression, kind

Constructor Summary

Constructors

Constructor and Description
ConditionalPostcondition(java.lang.String expression, boolean annoResult, javax.lang.model.element.AnnotationMirror annotation)

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)

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