Package 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:

  • Field Details

    • qualifierArgumentValueElement

      protected final ExecutableElement qualifierArgumentValueElement
      The QualifierArgument.value field/element.

    • factory

      protected final GenericAnnotatedTypeFactory<?,?,?,?> factory
      The factory that this ContractsFromMethod is associated with.

  • Constructor Details

    • ContractsFromMethod

      public ContractsFromMethod(GenericAnnotatedTypeFactory<?,?,?,?> factory)
      Creates a ContractsFromMethod for the given factory.
      Parameters:
      factory - 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.
      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