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 A postcondition contract.
static class	ContractsUtils.Precondition A precondition contract.

Field Summary

Fields

Modifier and Type	Field and Description
protected GenericAnnotatedTypeFactory<?,?,?,?>	factory The factory that this ContractsUtils is associated with.
protected static ContractsUtils	instance The currently-used ContractsUtils object.

Method Summary

Modifier and Type	Method and Description
java.util.Set<ContractsUtils.ConditionalPostcondition>	getConditionalPostconditions(javax.lang.model.element.ExecutableElement methodElement) Returns the 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

The currently-used ContractsUtils object. This class is NOT a singleton: this value can change.

factory

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

The factory that this ContractsUtils is associated with.

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 the conditional postconditions on the method methodElement.