Package org.checkerframework.common.initializedfields

Class InitializedFieldsAnnotatedTypeFactory.InitializedFieldsContractsFromMethod

java.lang.Object

org.checkerframework.framework.util.ContractsFromMethod

org.checkerframework.common.initializedfields.InitializedFieldsAnnotatedTypeFactory.InitializedFieldsContractsFromMethod

Enclosing class:

InitializedFieldsAnnotatedTypeFactory

public class InitializedFieldsAnnotatedTypeFactory.InitializedFieldsContractsFromMethod
extends ContractsFromMethod

A subclass of ContractsFromMethod that adds a postcondition contract to each constructor, requiring that it initializes all fields.

Field Summary

Fields inherited from class org.checkerframework.framework.util.ContractsFromMethod

factory, qualifierArgumentValueElement

Constructor Summary

Constructors

Constructor	Description
InitializedFieldsContractsFromMethod(GenericAnnotatedTypeFactory<?,?,?,?> factory)	Creates an InitializedFieldsContractsFromMethod for the given factory.

Method Summary

Modifier and Type	Method	Description
Set<Contract.Postcondition>	getPostconditions(ExecutableElement executableElement)	Returns the postcondition contracts on executableElement.

Methods inherited from class org.checkerframework.framework.util.ContractsFromMethod

getConditionalPostconditions, getContracts, getPreconditions

Methods inherited from class java.lang.Object

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

Constructor Details

InitializedFieldsContractsFromMethod

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

Creates an InitializedFieldsContractsFromMethod for the given factory.

Parameters:

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

Method Details

getPostconditions

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

Description copied from class: ContractsFromMethod

Returns the postcondition contracts on executableElement.

Overrides:

getPostconditions in class ContractsFromMethod

Parameters:

executableElement - the method whose contracts to return

Returns:

the postcondition contracts on executableElement