Package org.checkerframework.checker.calledmethods

Class CalledMethodsVisitor

java.lang.Object

com.sun.source.util.TreeScanner<R,P>

com.sun.source.util.TreePathScanner<R,P>

org.checkerframework.framework.source.SourceVisitor<Void,Void>

org.checkerframework.common.basetype.BaseTypeVisitor<AccumulationAnnotatedTypeFactory>

org.checkerframework.common.accumulation.AccumulationVisitor

org.checkerframework.checker.calledmethods.CalledMethodsVisitor

All Implemented Interfaces:

TreeVisitor<Void,Void>

Direct Known Subclasses:

ResourceLeakVisitor

public class CalledMethodsVisitor
extends AccumulationVisitor

This visitor implements the custom error message "finalizer.invocation". It also supports counting the number of framework build calls.

Nested Class Summary

Nested classes/interfaces inherited from class org.checkerframework.common.basetype.BaseTypeVisitor

BaseTypeVisitor.OverrideChecker

Field Summary

Fields inherited from class org.checkerframework.common.basetype.BaseTypeVisitor

assumePureGetters, atypeFactory, checker, DETERMINISTIC, IMPURE, methodTree, positions, PURE, qualHierarchy, showchecks, SIDE_EFFECT_FREE, TARGET, targetValueElement, typeHierarchy, typeValidator, unusedWhenElement, warnRedundantAnnotations

Fields inherited from class org.checkerframework.framework.source.SourceVisitor

elements, root, trees, treesWithSuppressWarnings, types

Constructor Summary

Constructors

Constructor	Description
CalledMethodsVisitor(BaseTypeChecker checker)	Creates a new CalledMethodsVisitor.

Method Summary

Modifier and Type	Method	Description
protected void	checkExceptionalPostcondition(EnsuresCalledMethodOnExceptionContract postcond, MethodTree tree)	Check if the given postcondition is really ensured by the body of the given method.
void	processMethodTree(MethodTree tree)	Type-check methodTree.
protected void	reportMethodInvocabilityError(MethodInvocationTree tree, AnnotatedTypeMirror found, AnnotatedTypeMirror expected)	Turns some "method.invocation" errors into "finalizer.invocation" errors.
Void	visitAnnotation(AnnotationTree tree, Void p)	Issue an error at every EnsuresCalledMethodsVarargs annotation, because using it is unsound.
Void	visitMethodInvocation(MethodInvocationTree tree, Void p)	Performs a method invocation check.

Methods inherited from class org.checkerframework.common.basetype.BaseTypeVisitor

checkAccess, checkAccessAllowed, checkArguments, checkArrayInitialization, checkConditionalPostcondition, checkConstructorInvocation, checkConstructorResult, checkContract, checkDefaultConstructor, checkExceptionParameter, checkExplicitAnnotationsOnIntersectionBounds, checkExtendsAndImplements, checkExtendsOrImplements, checkFieldInvariantDeclarations, checkMethodInvocability, checkMethodReferenceAsOverride, checkOverride, checkOverride, checkPostcondition, checkPreconditions, checkPurityAnnotations, checkQualifierParameter, checkSuperConstructorCall, checkThisConstructorCall, checkThisOrSuperConstructorCall, checkThrownExpression, checkTypeArguments, checkTypecastRedundancy, checkTypecastSafety, checkVarargs, commonAssignmentCheck, commonAssignmentCheck, commonAssignmentCheck, commonAssignmentCheckEndDiagnostic, commonAssignmentCheckEndDiagnostic, commonAssignmentCheckStartDiagnostic, contractExpressionAndType, createOverrideChecker, createTypeFactory, createTypeFactoryPublic, createTypeValidator, enclosingMemberSelect, enclosingStatement, getExceptionParameterLowerBoundAnnotations, getThrowUpperBoundAnnotations, getTypeFactory, isTypeCastSafe, isValidUse, isValidUse, isValidUse, processClassTree, reportPurityErrors, scan, setRoot, shouldPerformContractInference, shouldSkipUses, shouldWarnAboutIrrelevantJavaTypes, skipReceiverSubtypeCheck, testAnnotationInsertion, testJointJavacJavaParserVisitor, testTypevarContainment, typeCheckVectorCopyIntoArgument, validateType, validateTypeOf, visitAnnotatedType, visitAnnotatedType, visitAssignment, visitCatch, visitClass, visitCompilationUnit, visitCompoundAssignment, visitConditionalExpression, visitEnhancedForLoop, visitIdentifier, visitInstanceOf, visitLambdaExpression, visitMemberReference, visitMethod, visitNewArray, visitNewClass, visitReturn, visitSwitchExpression17, visitThrow, visitTypeCast, visitTypeParameter, visitUnary, visitVariable, warnAboutIrrelevantJavaTypes, warnInvalidPolymorphicQualifier, warnInvalidPolymorphicQualifier, warnRedundantAnnotations

Methods inherited from class org.checkerframework.framework.source.SourceVisitor

visit

Methods inherited from class com.sun.source.util.TreePathScanner

getCurrentPath, scan

Methods inherited from class com.sun.source.util.TreeScanner

reduce, scan, visitArrayAccess, visitArrayType, visitAssert, visitBinary, visitBindingPattern, visitBlock, visitBreak, visitCase, visitContinue, visitDefaultCaseLabel, visitDoWhileLoop, visitEmptyStatement, visitErroneous, visitExports, visitExpressionStatement, visitForLoop, visitGuardedPattern, visitIf, visitImport, visitIntersectionType, visitLabeledStatement, visitLiteral, visitMemberSelect, visitModifiers, visitModule, visitOpens, visitOther, visitPackage, visitParameterizedType, visitParenthesized, visitParenthesizedPattern, visitPrimitiveType, visitProvides, visitRequires, visitSwitch, visitSwitchExpression, visitSynchronized, visitTry, visitUnionType, visitUses, visitWhileLoop, visitWildcard, visitYield

Methods inherited from class java.lang.Object

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

Constructor Details

CalledMethodsVisitor

public CalledMethodsVisitor(BaseTypeChecker checker)

Creates a new CalledMethodsVisitor.

Parameters:

checker - the type-checker associated with this visitor

Method Details

visitAnnotation

public Void visitAnnotation(AnnotationTree tree,
 Void p)

Issue an error at every EnsuresCalledMethodsVarargs annotation, because using it is unsound.

Specified by:

visitAnnotation in interface TreeVisitor<Void,Void>

Overrides:

visitAnnotation in class AccumulationVisitor

processMethodTree

public void processMethodTree(MethodTree tree)

Description copied from class: BaseTypeVisitor

Type-check methodTree. Subclasses should override this method instead of BaseTypeVisitor.visitMethod(MethodTree, Void).

Overrides:

processMethodTree in class BaseTypeVisitor<AccumulationAnnotatedTypeFactory>

Parameters:

tree - the method to type-check

checkExceptionalPostcondition

protected void checkExceptionalPostcondition(EnsuresCalledMethodOnExceptionContract postcond,
 MethodTree tree)

Check if the given postcondition is really ensured by the body of the given method.

Parameters:

postcond - the postcondition to check

tree - the method

visitMethodInvocation

public Void visitMethodInvocation(MethodInvocationTree tree,
 Void p)

Description copied from class: BaseTypeVisitor

Performs a method invocation check.

An invocation of a method, m, on the receiver, r is valid only if:

• passed arguments are subtypes of corresponding m parameters
• r is a subtype of m receiver type
• if m is generic, passed type arguments are subtypes of m type variables

Specified by:

visitMethodInvocation in interface TreeVisitor<Void,Void>

Overrides:

visitMethodInvocation in class BaseTypeVisitor<AccumulationAnnotatedTypeFactory>

reportMethodInvocabilityError

protected void reportMethodInvocabilityError(MethodInvocationTree tree,
 AnnotatedTypeMirror found,
 AnnotatedTypeMirror expected)

Turns some "method.invocation" errors into "finalizer.invocation" errors.

Overrides:

reportMethodInvocabilityError in class BaseTypeVisitor<AccumulationAnnotatedTypeFactory>

Parameters:

tree - the AST node at which to report the error

found - the actual type of the receiver

expected - the expected type of the receiver