Package org.checkerframework.common.wholeprograminference

Class WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos

java.lang.Object
org.checkerframework.common.wholeprograminference.WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos
Enclosing class:
WholeProgramInferenceJavaParserStorage
public class WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos extends Object
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

    • 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

    • 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 - declaration annotation to add
      Returns:
      true if annotation wasn't previously stored for this callable declaration

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

    • getPreconditions

      public Map<String,Pair<AnnotatedTypeMirror,AnnotatedTypeMirror>> getPreconditions()
      Returns the inferred preconditions for this callable declaration.
      Returns:
      a mapping from expression string to pairs of (inferred precondition, declared type). The keys of this map use the same string formatting as the RequiresQualifier annotation, e.g. "#1" for the first parameter.

    • getPostconditions

      public Map<String,Pair<AnnotatedTypeMirror,AnnotatedTypeMirror>> getPostconditions()
      Returns the inferred postconditions for this callable declaration.
      Returns:
      a mapping from expression string to pairs of (inferred postcondition, declared type). The keys of this map use the same string formatting as the EnsuresQualifier annotation, e.g. "#1" for the first parameter.

    • getPreconditionsForExpression

      public AnnotatedTypeMirror getPreconditionsForExpression(String expression, AnnotatedTypeMirror declaredType, AnnotatedTypeFactory atf)
      Returns an AnnotatedTypeMirror containing the preconditions for the given expression.
      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.
      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