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.
    • atypeFactory

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

    • ContractsFromMethod

      public ContractsFromMethod(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.
      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