org.checkerframework.framework.util

Class ContractsUtils

java.lang.Object

org.checkerframework.framework.util.ContractsUtils

public class ContractsUtils
extends java.lang.Object

A utility class to handle pre- and postconditions.

See Also:

PreconditionAnnotation, RequiresQualifier, PostconditionAnnotation, EnsuresQualifier, EnsuresQualifierIf

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	ContractsUtils.ConditionalPostcondition Represents a conditional postcondition that must be verified by BaseTypeVisitor or one of its subclasses.
static class	ContractsUtils.Contract A contract represents an annotation on an expression, along with the kind: precondition, postcondition, or conditional postcondition.
static class	ContractsUtils.Postcondition
static class	ContractsUtils.Precondition

Field Summary

Fields

Modifier and Type	Field and Description
protected GenericAnnotatedTypeFactory<?,?,?,?>	factory
protected static ContractsUtils	instance

Method Summary

Modifier and Type	Method and Description
java.util.Set<ContractsUtils.ConditionalPostcondition>	getConditionalPostconditions(javax.lang.model.element.ExecutableElement methodElement) Returns a set of triples (expr, (result, annotation)) of conditional postconditions on the method methodElement.
java.util.List<ContractsUtils.Contract>	getContracts(javax.lang.model.element.ExecutableElement element)
static ContractsUtils	getInstance(GenericAnnotatedTypeFactory<?,?,?,?> factory) Returns an instance of the ContractsUtils class.
java.util.Set<ContractsUtils.Postcondition>	getPostconditions(javax.lang.model.element.ExecutableElement methodElement) Returns the set of postconditions on the method methodElement.
java.util.Set<ContractsUtils.Precondition>	getPreconditions(javax.lang.model.element.Element element) Returns the set of preconditions on the element element.

Methods inherited from class java.lang.Object

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

Field Detail

instance

protected static ContractsUtils instance

factory

protected GenericAnnotatedTypeFactory<?,?,?,?> factory

Method Detail

getInstance

public static ContractsUtils getInstance(GenericAnnotatedTypeFactory<?,?,?,?> factory)

Returns an instance of the ContractsUtils class.

getContracts

public java.util.List<ContractsUtils.Contract> getContracts(javax.lang.model.element.ExecutableElement element)

getPreconditions

public java.util.Set<ContractsUtils.Precondition> getPreconditions(javax.lang.model.element.Element element)

Returns the set of preconditions on the element element.

getPostconditions

public java.util.Set<ContractsUtils.Postcondition> getPostconditions(javax.lang.model.element.ExecutableElement methodElement)

Returns the set of postconditions on the method methodElement.

getConditionalPostconditions

public java.util.Set<ContractsUtils.ConditionalPostcondition> getConditionalPostconditions(javax.lang.model.element.ExecutableElement methodElement)

Returns a set of triples (expr, (result, annotation)) of conditional postconditions on the method methodElement.