Package org.checkerframework.common.wholeprograminference

Class WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos

java.lang.Object
org.checkerframework.common.wholeprograminference.WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos
All Implemented Interfaces:
DeepCopyable<WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos>
Enclosing class:
WholeProgramInferenceJavaParserStorage
public class WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos extends Object implements DeepCopyable<WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos>
Stores the JavaParser node for a method or constructor and the annotations that have been inferred about its parameters and return type.

  • Field Details

    • declaration

      public final com.github.javaparser.ast.body.CallableDeclaration<?> declaration
      Wrapped method or constructor declaration.

  • Constructor Details

    • CallableDeclarationAnnos

      public CallableDeclarationAnnos(com.github.javaparser.ast.body.CallableDeclaration<?> declaration)
      Creates a wrapper for the given method or constructor declaration.
      Parameters:
      declaration - method or constructor declaration to wrap

  • Method Details

    • deepCopy

      public WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos deepCopy()
      Description copied from interface: DeepCopyable
      Returns a deep copy of this. A deep copy is equal to the original, but side effects to either object are not visible in the other. A deep copy may share immutable state with the original.

      The run-time class of the result is identical to the run-time class of this. The deep copy is equal to this (per equals() if the object's class does not use reference equality as Object.equals() does).

      Specified by:
      deepCopy in interface DeepCopyable<WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos>
      Returns:
      a deep copy of this

    • getParameterTypeInitialized

      public AnnotatedTypeMirror getParameterTypeInitialized(AnnotatedTypeMirror type, int index, AnnotatedTypeFactory atf)
      Returns the inferred type for the parameter at the given index. If necessary, initializes the AnnotatedTypeMirror for that location using type and atf to a wrapper around the base type for the parameter.
      Parameters:
      type - type for the parameter at index, used for initializing the returned AnnotatedTypeMirror the first time it's accessed
      atf - the annotated type factory of a given type system, whose type hierarchy will be used
      index - index of the parameter to return the inferred annotations of
      Returns:
      an AnnotatedTypeMirror containing all annotations inferred for the parameter at the given index

    • getParameterType

      public @Nullable AnnotatedTypeMirror getParameterType(int index)
      Returns the inferred type for the parameter at the given index, or null if there's no parameter at the given index or there's no inferred type for that parameter.
      Parameters:
      index - index of the parameter to return the inferred annotations of
      Returns:
      an AnnotatedTypeMirror containing all annotations inferred for the parameter at the given index, or null if there's no parameter at index or if there's not inferred annotations for that parameter

    • addDeclarationAnnotationToFormalParameter

      public boolean addDeclarationAnnotationToFormalParameter(AnnotationMirror annotation, int index)
      Adds a declaration annotation to this parameter and returns whether it was a new annotation.
      Parameters:
      annotation - the declaration annotation to add
      index - index of the parameter
      Returns:
      true if annotation wasn't previously stored for this parameter

    • getReceiverType

      public AnnotatedTypeMirror getReceiverType(AnnotatedTypeMirror type, AnnotatedTypeFactory atf)
      If this wrapper holds a method, returns the inferred type of the receiver. If necessary, initializes the AnnotatedTypeMirror for that location using type and atf to a wrapper around the base type for the receiver type.
      Parameters:
      type - base type for the receiver type, used for initializing the returned AnnotatedTypeMirror the first time it's accessed
      atf - the annotated type factory of a given type system, whose type hierarchy will be used
      Returns:
      an AnnotatedTypeMirror containing all annotations inferred for the receiver type

    • getReturnType

      public AnnotatedTypeMirror getReturnType(AnnotatedTypeMirror type, AnnotatedTypeFactory atf)
      If this wrapper holds a method, returns the inferred type of the return type. If necessary, initializes the AnnotatedTypeMirror for that location using type and atf to a wrapper around the base type for the return type.
      Parameters:
      type - base type for the return type, used for initializing the returned AnnotatedTypeMirror the first time it's accessed
      atf - the annotated type factory of a given type system, whose type hierarchy will be used
      Returns:
      an AnnotatedTypeMirror containing all annotations inferred for the return type

    • getDeclarationAnnotations

      public AnnotationMirrorSet getDeclarationAnnotations()
      Returns the inferred declaration annotations on this executable, or null if there are no annotations.
      Returns:
      the declaration annotations for this callable declaration

    • addDeclarationAnnotation

      public boolean addDeclarationAnnotation(AnnotationMirror annotation)
      Adds a declaration annotation to this callable declaration and returns whether it was a new annotation.
      Parameters:
      annotation - the declaration annotation to add
      Returns:
      true if annotation wasn't previously stored for this callable declaration

    • getPreconditions

      public Map<String,Pair<AnnotatedTypeMirror,AnnotatedTypeMirror>> getPreconditions()
      Returns the inferred preconditions for this callable declaration. The keys of the returned map use the same string formatting as the RequiresQualifier annotation, e.g. "#1" for the first parameter.

      Although the map is immutable, the AnnotatedTypeMirrors within it can be modified, and such changes will be reflected in the receiver CallableDeclarationAnnos object.

      Returns:
      a mapping from Java expression string to pairs of (inferred precondition for the expression, declared type of the expression)
      See Also:

    • getPostconditions

      public Map<String,Pair<AnnotatedTypeMirror,AnnotatedTypeMirror>> getPostconditions()
      Returns the inferred postconditions for this callable declaration. The keys of the returned map use the same string formatting as the EnsuresQualifier annotation, e.g. "#1" for the first parameter.

      Although the map is immutable, the AnnotatedTypeMirrors within it can be modified, and such changes will be reflected in the receiver CallableDeclarationAnnos object.

      Returns:
      a mapping from Java expression string to pairs of (inferred postcondition for the expression, declared type of the expression)
      See Also:

    • getPreconditionsForExpression

      public AnnotatedTypeMirror getPreconditionsForExpression(String expression, AnnotatedTypeMirror declaredType, AnnotatedTypeFactory atf)
      Returns an AnnotatedTypeMirror containing the preconditions for the given expression. Changes to the returned AnnotatedTypeMirror are reflected in this CallableDeclarationAnnos.
      Parameters:
      expression - a string representing a Java expression, in the same format as the argument to a RequiresQualifier annotation
      declaredType - the declared type of expression
      atf - the annotated type factory of a given type system, whose type hierarchy will be used
      Returns:
      an AnnotatedTypeMirror containing the annotations for the inferred preconditions for the given expression

    • getPostconditionsForExpression

      public AnnotatedTypeMirror getPostconditionsForExpression(String expression, AnnotatedTypeMirror declaredType, AnnotatedTypeFactory atf)
      Returns an AnnotatedTypeMirror containing the postconditions for the given expression. Changes to the returned AnnotatedTypeMirror are reflected in this CallableDeclarationAnnos.
      Parameters:
      expression - a string representing a Java expression, in the same format as the argument to a EnsuresQualifier annotation
      declaredType - the declared type of expression
      atf - the annotated type factory of a given type system, whose type hierarchy will be used
      Returns:
      an AnnotatedTypeMirror containing the annotations for the inferred postconditions for the given expression

    • transferAnnotations

      public void transferAnnotations()
      Transfers all annotations inferred by whole program inference for the return type, receiver type, and parameter types for the wrapped declaration to their corresponding JavaParser locations.

    • toString

      public String toString()
      Overrides:
      toString in class Object