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 Summary

Fields

Modifier and Type	Field and Description
com.github.javaparser.ast.body.CallableDeclaration<?>	declaration Wrapped method or constructor declaration.
String	file Path to file containing the declaration.

Constructor Summary

Constructors

Constructor and Description
CallableDeclarationAnnos(com.github.javaparser.ast.body.CallableDeclaration<?> declaration) Creates a wrapper for the given method or constructor declaration.

Method Summary

Modifier and Type	Method and Description
boolean	addDeclarationAnnotation(AnnotationMirror annotation) Adds a declaration annotation to this callable declaration and returns whether it was a new annotation.
Set<AnnotationMirror>	getDeclarationAnnotations() Returns the inferred declaration annotations on this executable, or null if there are no annotations.
@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.
AnnotatedTypeMirror	getParameterTypeInitialized(AnnotatedTypeMirror type, int index, AnnotatedTypeFactory atf) Returns the inferred type for the parameter at the given index.
Map<String,Pair<AnnotatedTypeMirror,AnnotatedTypeMirror>>	getPostconditions() Returns the inferred postconditions for this callable declaration.
AnnotatedTypeMirror	getPostconditionsForExpression(String expression, AnnotatedTypeMirror declaredType, AnnotatedTypeFactory atf) Returns an AnnotatedTypeMirror containing the postconditions for the given expression.
Map<String,Pair<AnnotatedTypeMirror,AnnotatedTypeMirror>>	getPreconditions() Returns the inferred preconditions for this callable declaration.
AnnotatedTypeMirror	getPreconditionsForExpression(String expression, AnnotatedTypeMirror declaredType, AnnotatedTypeFactory atf) Returns an AnnotatedTypeMirror containing the preconditions for the given expression.
AnnotatedTypeMirror	getReceiverType(AnnotatedTypeMirror type, AnnotatedTypeFactory atf) If this wrapper holds a method, returns the inferred type of the receiver.
AnnotatedTypeMirror	getReturnType(AnnotatedTypeMirror type, AnnotatedTypeFactory atf) If this wrapper holds a method, returns the inferred type of the return type.
String	toString()
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.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

declaration

public com.github.javaparser.ast.body.CallableDeclaration<?> declaration

Wrapped method or constructor declaration.

file

public String file

Path to file containing the declaration.

Constructor Detail

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 Detail

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 Set<AnnotationMirror> 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

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