Package org.checkerframework.framework.util

Class Contract.ConditionalPostcondition

java.lang.Object

org.checkerframework.framework.util.Contract

org.checkerframework.framework.util.Contract.ConditionalPostcondition

Enclosing class:

Contract

public static class Contract.ConditionalPostcondition
extends 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.Contract

Contract.ConditionalPostcondition, Contract.Kind, Contract.Postcondition, Contract.Precondition

Field Summary

Fields

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

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

annotation, contractAnnotation, expressionString, kind

Constructor Summary

Constructors

Constructor	Description
ConditionalPostcondition(String expressionString, AnnotationMirror annotation, AnnotationMirror contractAnnotation, boolean resultValue)	Create a new conditional postcondition.

Method Summary

Modifier and Type	Method	Description
boolean	equals(@Nullable Object o)
int	hashCode()
String	toString()

Methods inherited from class org.checkerframework.framework.util.Contract

create, viewpointAdaptDependentTypeAnnotation

Methods inherited from class java.lang.Object

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

Field Details

resultValue

public final boolean resultValue

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() that returns false.

Constructor Details

ConditionalPostcondition

public ConditionalPostcondition(String expressionString,
 AnnotationMirror annotation,
 AnnotationMirror contractAnnotation,
 boolean resultValue)

Create a new conditional postcondition.

Parameters:

expressionString - the Java expression that should have a type qualifier

annotation - the type qualifier that expressionString should have

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

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

Method Details

equals

public boolean equals(@Nullable Object o)

Overrides:

equals in class Contract

hashCode

public int hashCode()

Overrides:

hashCode in class Contract

toString

public String toString()

Overrides:

toString in class Contract