org.checkerframework.framework.util

Class ContractsUtils

java.lang.Object

org.checkerframework.framework.util.ContractsUtils

public class ContractsUtils
extends Object

A utility class to handle pre- and postconditions.

See Also:

PreconditionAnnotation, RequiresQualifier, PostconditionAnnotation, EnsuresQualifier, ConditionalPostconditionAnnotation, EnsuresQualifierIf

Field Summary

Fields

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

Method Summary

Modifier and Type	Method and Description
Set<Contract.ConditionalPostcondition>	getConditionalPostconditions(ExecutableElement methodElement) Returns the contracts on method methodElement.
Set<Contract>	getContracts(ExecutableElement executableElement) Returns all the contracts on method or constructor executableElement.
static ContractsUtils	getInstance(GenericAnnotatedTypeFactory<?,?,?,?> factory) Returns an instance of the ContractsUtils class for the given factory.
Set<Contract.Postcondition>	getPostconditions(ExecutableElement executableElement) Returns the contracts on executableElement.
Set<Contract.Precondition>	getPreconditions(ExecutableElement executableElement) Returns the contracts on method or constructor executableElement.

Methods inherited from class java.lang.Object

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

Field Detail

instance

protected static @InternedDistinct 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 for the given factory. Also sets it as the currently-used ContractsUtils object.

Parameters:

factory - the factory to create a ContractsUtils for

Returns:

a ContractsUtils for the given factory

getContracts

public Set<Contract> getContracts(ExecutableElement executableElement)

Returns all the contracts on method or constructor executableElement.

Parameters:

executableElement - the method or constructor whose contracts to retrieve

Returns:

the contracts on executableElement

getPreconditions

public Set<Contract.Precondition> getPreconditions(ExecutableElement executableElement)

Returns the contracts on method or constructor executableElement.

Parameters:

executableElement - the method whose contracts to return

Returns:

the contracts on executableElement

getPostconditions

public Set<Contract.Postcondition> getPostconditions(ExecutableElement executableElement)

Returns the contracts on executableElement.

Parameters:

executableElement - the method whose contracts to return

Returns:

the contracts on executableElement

getConditionalPostconditions

public Set<Contract.ConditionalPostcondition> getConditionalPostconditions(ExecutableElement methodElement)

Returns the contracts on method methodElement.

Parameters:

methodElement - the method whose contracts to return

Returns:

the contracts on methodElement