Package org.checkerframework.framework.util

Class DefaultContractsFromMethod

java.lang.Object

org.checkerframework.framework.util.DefaultContractsFromMethod

All Implemented Interfaces:

ContractsFromMethod

public class DefaultContractsFromMethod
extends Object
implements ContractsFromMethod

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	Description
protected final GenericAnnotatedTypeFactory<?,?,?,?>	atypeFactory	The factory that this ContractsFromMethod is associated with.
protected final ExecutableElement	qualifierArgumentValueElement	The QualifierArgument.value field/element.

Constructor Summary

Constructors

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

Method Summary

Modifier and Type	Method	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 Details

qualifierArgumentValueElement

protected final ExecutableElement qualifierArgumentValueElement

The QualifierArgument.value field/element.

atypeFactory

protected final GenericAnnotatedTypeFactory<?,?,?,?> atypeFactory

The factory that this ContractsFromMethod is associated with.

Constructor Details

DefaultContractsFromMethod

public DefaultContractsFromMethod(GenericAnnotatedTypeFactory<?,?,?,?> atypeFactory)

Creates a ContractsFromMethod for the given factory.

Parameters:

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

Method Details

getContracts

public Set<Contract> getContracts(ExecutableElement executableElement)

Returns all the contracts on method or constructor executableElement.

Specified by:

getContracts in interface ContractsFromMethod

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.

Specified by:

getPreconditions in interface ContractsFromMethod

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.

Specified by:

getPostconditions in interface ContractsFromMethod

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.

Specified by:

getConditionalPostconditions in interface ContractsFromMethod

Parameters:

methodElement - the method whose contracts to return

Returns:

the conditional postcondition contracts on methodElement