public static class ContractsUtils.ConditionalPostcondition extends Object
BaseTypeVisitor
or one of its subclasses. Automatically
extracted from annotations with meta-annotation
@ConditionalPostconditionAnnotation
, such as
EnsuresNonNullIf
.Modifier and Type | Field and Description |
---|---|
boolean |
annoResult
The return value for the annotated method that ensures that the
conditional postcondition holds.
|
String |
annotationString
The name of the qualifier class that describes the condition that
must hold.
|
String |
expression
The expression for which the conditional postcondition must hold,
such as
"foo" in
@EnsuresNonNullIf(expression="foo", result=true) . |
Constructor and Description |
---|
ConditionalPostcondition(String expression,
boolean annoResult,
String annotationString) |
public final String expression
"foo"
in
@EnsuresNonNullIf(expression="foo", result=true)
.public final boolean annoResult
@EnsuresNonNullIf(expression="foo", result=false) boolean method()
foo
is guaranteed to be @NonNull
after a call
to method()
if that call returns false
.public final String annotationString