Package org.checkerframework.framework.util

Class Contract

java.lang.Object
org.checkerframework.framework.util.Contract
Direct Known Subclasses:
Contract.ConditionalPostcondition, Contract.Postcondition, Contract.Precondition
public abstract class Contract extends Object
A contract represents an annotation on an expression. It is a precondition, postcondition, or conditional postcondition.
See Also:

  • Field Details

    • expressionString

      public final String expressionString
      The expression for which the condition must hold, such as "foo" in @RequiresNonNull("foo").

      An annotation like @RequiresNonNull({"a", "b", "c"}) would be represented by multiple Contracts.

    • annotation

      public final AnnotationMirror annotation
      The annotation on the type of expression, according to this contract.

    • contractAnnotation

      public final AnnotationMirror contractAnnotation
      The annotation that expressed this contract; used for diagnostic messages.

    • kind

      public final Contract.Kind kind
      The kind of contract: precondition, postcondition, or conditional postcondition.

  • Method Details

    • create

      public static Contract create(Contract.Kind kind, String expressionString, AnnotationMirror annotation, AnnotationMirror contractAnnotation, Boolean ensuresQualifierIf)
      Creates a new Contract.
      Parameters:
      kind - precondition, postcondition, or conditional postcondition
      expressionString - the Java expression that should have a type qualifier
      annotation - the type qualifier that expressionString should have
      contractAnnotation - the pre- or post-condition annotation that the programmer wrote; used for diagnostic messages
      ensuresQualifierIf - the ensuresQualifierIf field, for a conditional postcondition
      Returns:
      a new contract

    • equals

      public boolean equals(@Nullable Object o)
      Overrides:
      equals in class Object

    • hashCode

      public int hashCode()
      Overrides:
      hashCode in class Object

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • viewpointAdaptDependentTypeAnnotation

      public AnnotationMirror viewpointAdaptDependentTypeAnnotation(GenericAnnotatedTypeFactory<?,?,?,?> factory, StringToJavaExpression stringToJavaExpr, @Nullable Tree errorTree)
      Viewpoint-adapt annotation using stringToJavaExpr.

      For example, if the contract is @EnsuresKeyFor(value = "this.field", map = "map"), annotation is @KeyFor("map"). This method applies stringToJava to "map" and returns a new KeyFor annotation with the result.

      Parameters:
      factory - used to get DependentTypesHelper
      stringToJavaExpr - function used to convert strings to JavaExpressions
      errorTree - if non-null, where to report any errors that occur when parsing the dependent type annotation; if null, report no errors
      Returns:
      the viewpoint-adapted annotation, or annotation if it is not a dependent type annotation