Package org.checkerframework.framework.util

Class ContractsFromMethod

java.lang.Object

org.checkerframework.framework.util.ContractsFromMethod

public class ContractsFromMethod
extends java.lang.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	Description
protected GenericAnnotatedTypeFactory<?,?,?,?>	atypeFactory	The factory that this ContractsFromMethod is associated with.
protected javax.lang.model.element.ExecutableElement	qualifierArgumentValueElement	The QualifierArgument.value field/element.

Constructor Summary

Constructors

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

Method Summary

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

qualifierArgumentValueElement

protected final javax.lang.model.element.ExecutableElement qualifierArgumentValueElement

The QualifierArgument.value field/element.

atypeFactory

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

The factory that this ContractsFromMethod is associated with.

Constructor Detail

ContractsFromMethod

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

Creates a ContractsFromMethod for the given factory.

Parameters:

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

Method Detail

getContracts

public java.util.Set<Contract> getContracts(javax.lang.model.element.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 java.util.Set<Contract.Precondition> getPreconditions(javax.lang.model.element.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 java.util.Set<Contract.Postcondition> getPostconditions(javax.lang.model.element.ExecutableElement executableElement)

Returns the postcondition contracts on executableElement.

Parameters:

executableElement - the method whose contracts to return

Returns:

the postcondition contracts on executableElement

getConditionalPostconditions

public java.util.Set<Contract.ConditionalPostcondition> getConditionalPostconditions(javax.lang.model.element.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