org.checkerframework.framework.util

Class ContractsFromMethod

java.lang.Object

org.checkerframework.framework.util.ContractsFromMethod

public class ContractsFromMethod
extends Object

A utility class to retrieve pre- and postconditions from a method.

See Also:

PreconditionAnnotation, RequiresQualifier, PostconditionAnnotation, EnsuresQualifier, ConditionalPostconditionAnnotation, EnsuresQualifierIf

Field Summary

Fields

Modifier and Type	Field and Description
protected GenericAnnotatedTypeFactory<?,?,?,?>	factory The factory that this ContractsFromMethod is associated with.

Constructor Summary

Constructors

Constructor and Description
ContractsFromMethod(GenericAnnotatedTypeFactory<?,?,?,?> factory) Creates a ContractsFromMethod for the given factory.

Method Summary

Modifier and Type	Method and Description
Set<Contract.ConditionalPostcondition>	getConditionalPostconditions(ExecutableElement methodElement) Returns the conditional postcondition contracts on method methodElement.
Set<Contract>	getContracts(ExecutableElement executableElement) Returns all the contracts on method or constructor executableElement.
Set<Contract.Postcondition>	getPostconditions(ExecutableElement executableElement) Returns the postcondition contracts on executableElement.
Set<Contract.Precondition>	getPreconditions(ExecutableElement executableElement) Returns the precondition 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

factory

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

The factory that this ContractsFromMethod is associated with.

Constructor Detail

ContractsFromMethod

public ContractsFromMethod(GenericAnnotatedTypeFactory<?,?,?,?> factory)

Creates a ContractsFromMethod for the given factory.

Parameters:

factory - the type factory associated with the newly-created ContractsFromMethod

Method Detail

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 precondition contracts on method or constructor executableElement.

Parameters:

executableElement - the method whose contracts to return

Returns:

the precondition contracts on executableElement

getPostconditions

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

Returns the postcondition contracts on executableElement.

Parameters:

executableElement - the method whose contracts to return

Returns:

the postcondition contracts on executableElement

getConditionalPostconditions

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

Returns the conditional postcondition contracts on method methodElement.

Parameters:

methodElement - the method whose contracts to return

Returns:

the conditional postcondition contracts on methodElement