Package org.checkerframework.afu.scenelib.el

Class AMethod

java.lang.Object
org.checkerframework.afu.scenelib.el.AElement
org.checkerframework.afu.scenelib.el.ADeclaration
org.checkerframework.afu.scenelib.el.AMethod
All Implemented Interfaces:
Cloneable
public class AMethod extends ADeclaration
An annotated method; contains bounds, return, parameters, receiver, and throws.

  • Field Details

    • methodSignature

      public final String methodSignature
      The method's simple name followed by its erased signature in JVML format. For example, foo()V or bar(B[I[[Ljava/lang/String;)I.

    • bounds

      public final VivifyingMap<BoundLocation,ATypeElement> bounds
      The method's annotated type parameter bounds.

    • returnType

      public final ATypeElement returnType
      The method's annotated return type. Non-null even if returnTypeMirror is null.

    • receiver

      public final AField receiver
      The method's annotated receiver parameter type.

    • parameters

      public final VivifyingMap<Integer,AField> parameters
      The method's annotated parameters; map key is parameter index, starting at 0.

    • throwsException

      public final VivifyingMap<TypeIndexLocation,ATypeElement> throwsException
      Exceptions that are thrown.

    • preconditions

      public final VivifyingMap<String,AField> preconditions
      Types of expressions at entry to the method. The map key is the string representation of the expression.

    • postconditions

      public final VivifyingMap<String,AField> postconditions
      Types of expressions at exit from the method. The map key is the string representation of the expression.

    • contracts

      public List<Annotation> contracts
      Clients set this before printing the AMethod.

      These annotations are not stored in tlAnnotationsHere because whole-program inference assumes that inferred annotations only become stronger, but these annotations might disappear as other annotations become stronger.

      These annotations are not part of the abstract state of this AMethod (but are derived from it).

    • body

      public ABlock body
      The body of the method.

  • Method Details

    • setFieldsFromMethodElement

      public void setFieldsFromMethodElement(ExecutableElement methodElt)
      Sets return type, type parameters, and formal parameters in this AMethod, from information in the given method element.
      Parameters:
      methodElt - the element whose information to propagate into this

    • getMethodName

      public String getMethodName()
      Returns the method's simple name.
      Returns:
      the method's simple name

    • getTypeParameters

      public List<? extends TypeParameterElement> getTypeParameters()
      Returns the type parameters of this method.
      Returns:
      the list of type parameters

    • setTypeParameters

      public void setTypeParameters(List<? extends TypeParameterElement> typeParameters)
      Set the type parameters of this method.
      Parameters:
      typeParameters - the list of type parameters

    • vivifyAndAddTypeMirrorToParameter

      public AField vivifyAndAddTypeMirrorToParameter(int i, TypeMirror type, Name simpleName)
      Obtain the parameter at the given index, which can be further operated on to e.g. add a type annotation.
      Parameters:
      i - the parameter index (first parameter is zero)
      type - the type of the parameter
      simpleName - the name of the parameter
      Returns:
      an AFieldWrapper representing the parameter

    • vivifyAndAddTypeMirrorToPrecondition

      public AField vivifyAndAddTypeMirrorToPrecondition(String expression, TypeMirror type)
      Obtain information about an expression at method entry. It can be further operated on to e.g. add a type annotation.
      Parameters:
      expression - the expression
      type - the type of the expression
      Returns:
      an AField representing the expression

    • vivifyAndAddTypeMirrorToPostcondition

      public AField vivifyAndAddTypeMirrorToPostcondition(String expression, TypeMirror type)
      Obtain information about an expression at method exit. It can be further operated on to e.g. add a type annotation.
      Parameters:
      expression - the expression
      type - the type of the expression
      Returns:
      an AField representing the expression

    • getReturnTypeMirror

      public TypeMirror getReturnTypeMirror()
      Returns the return type.
      Returns:
      the return type, or null if the return type is unknown or void

    • setReturnTypeMirror

      public void setReturnTypeMirror(@FindDistinct @Nullable TypeMirror returnTypeMirror)
      Set the return type. Does nothing if the argument is null. Errs if called twice with different non-null arguments.
      Parameters:
      returnTypeMirror - the return type

    • getParameters

      public Map<Integer,AField> getParameters()
      Returns the parameters, as a map from parameter index (0-indexed) to representation.
      Returns:
      an immutable copy of the vivified parameters, as a map from index to representation

    • getPreconditions

      public Map<String,AField> getPreconditions()
      Returns the preconditions: annotations that apply to fields at method entry.
      Returns:
      an immutable copy of the vivified preconditions

    • getPostconditions

      public Map<String,AField> getPostconditions()
      Returns the postconditions: annotations that apply to fields at method exit.
      Returns:
      an immutable copy of the vivified postconditions

    • clone

      public AMethod clone()
      Overrides:
      clone in class AElement

    • equals

      public boolean equals(AElement o)
      Description copied from class: AElement
      Returns true if this AElement equals o. This is a slightly faster variant of AElement.equals(Object) for when the argument is statically known to be another nonnull AElement.
      Overrides:
      equals in class AElement
      Parameters:
      o - the AElement to compare to
      Returns:
      true if this is equal to o

    • hashCode

      public int hashCode()
      Overrides:
      hashCode in class ADeclaration

    • isEmpty

      public boolean isEmpty()
      Description copied from class: AElement
      Returns true if this AElement is empty.
      Overrides:
      isEmpty in class ADeclaration
      Returns:
      true iff this is empty

    • prune

      public void prune()
      Description copied from class: AElement
      Removes empty subelements of this AElement depth-first.
      Overrides:
      prune in class ADeclaration

    • toString

      public String toString()
      Overrides:
      toString in class ADeclaration

    • accept

      public <R, T> R accept(ElementVisitor<R,T> v, T t)
      Specified by:
      accept in class ADeclaration