org.checkerframework.checker.index.upperbound

Class UpperBoundVisitor

java.lang.Object

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

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

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

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

org.checkerframework.checker.index.upperbound.UpperBoundVisitor

All Implemented Interfaces:

com.sun.source.tree.TreeVisitor<java.lang.Void,java.lang.Void>

public class UpperBoundVisitor
extends BaseTypeVisitor<UpperBoundAnnotatedTypeFactory>

Warns about array accesses that could be too high.

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

atypeFactory, checker, contractsUtils, positions, typeValidator, visitorState

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

elements, root, trees, types

Constructor Summary

Constructors

Constructor and Description
UpperBoundVisitor(BaseTypeChecker checker)

Method Summary

Modifier and Type	Method and Description
protected void	commonAssignmentCheck(AnnotatedTypeMirror varType, com.sun.source.tree.ExpressionTree valueExp, @CompilerMessageKey java.lang.String errorKey) Checks the validity of an assignment (or pseudo-assignment) from a value to a variable and emits an error message (through the compiler's messaging interface) if it is not valid.
java.lang.Void	visitArrayAccess(com.sun.source.tree.ArrayAccessTree tree, java.lang.Void type) When the visitor reaches an array access, it needs to check a couple of things.

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

checkAccess, checkArguments, checkArrayInitialization, checkAssignability, checkConditionalPostcondition, checkConstructorInvocation, checkContract, checkDefaultConstructor, checkExceptionParameter, checkFieldInvariantDeclarations, checkForAnnotatedJdk, checkMethodInvocability, checkMethodReferenceAsOverride, checkOverride, checkOverride, checkPostcondition, checkPreconditions, checkThrownExpression, checkTypeArguments, checkTypecastRedundancy, checkTypecastSafety, checkVarargs, commonAssignmentCheck, commonAssignmentCheck, createOverrideChecker, createTypeFactory, createTypeValidator, enclosingMemberSelect, enclosingStatement, getExceptionParameterLowerBoundAnnotations, getThrowUpperBoundAnnotations, getTypeFactory, isAccessAllowed, isAssignable, isValidUse, isValidUse, isValidUse, isVectorCopyInto, processClassTree, reportPurityErrors, scan, setRoot, shouldSkipUses, skipReceiverSubtypeCheck, testTypevarContainment, typeCheckVectorCopyIntoArgument, validateType, validateTypeOf, visitAnnotation, visitAssignment, visitCatch, visitClass, visitCompilationUnit, visitCompoundAssignment, visitConditionalExpression, visitEnhancedForLoop, visitIdentifier, visitInstanceOf, visitLambdaExpression, visitMemberReference, visitMethod, visitMethodInvocation, visitNewArray, visitNewClass, visitParameterizedType, visitReturn, visitThrow, visitTry, visitTypeCast, visitTypeParameter, visitUnary, visitVariable

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, visitAnnotatedType, visitArrayType, visitAssert, visitBinary, visitBlock, visitBreak, visitCase, visitContinue, visitDoWhileLoop, visitEmptyStatement, visitErroneous, visitExpressionStatement, visitForLoop, visitIf, visitImport, visitIntersectionType, visitLabeledStatement, visitLiteral, visitMemberSelect, visitModifiers, visitOther, visitParenthesized, visitPrimitiveType, visitSwitch, visitSynchronized, visitUnionType, visitWhileLoop, visitWildcard

Methods inherited from class java.lang.Object

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

Constructor Detail

UpperBoundVisitor

public UpperBoundVisitor(BaseTypeChecker checker)

Method Detail

visitArrayAccess

public java.lang.Void visitArrayAccess(com.sun.source.tree.ArrayAccessTree tree,
                                       java.lang.Void type)

When the visitor reaches an array access, it needs to check a couple of things. First, it checks if the index has been assigned a reasonable UpperBound type: only an index with type LTLengthOf(arr) is safe to access arr. If that fails, it checks if the access is still safe. To do so, it checks if the Value Checker knows the minimum length of arr by querying the Value Annotated Type Factory. If the minimum length of the array is known, the visitor can check if the index is less than that minimum length. If so, then the access is still safe. Otherwise, report a potential unsafe access.

Specified by:

visitArrayAccess in interface com.sun.source.tree.TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitArrayAccess in class BaseTypeVisitor<UpperBoundAnnotatedTypeFactory>

commonAssignmentCheck

protected void commonAssignmentCheck(AnnotatedTypeMirror varType,
                                     com.sun.source.tree.ExpressionTree valueExp,
                                     @CompilerMessageKey java.lang.String errorKey)

Description copied from class: BaseTypeVisitor

Checks the validity of an assignment (or pseudo-assignment) from a value to a variable and emits an error message (through the compiler's messaging interface) if it is not valid.

Overrides:

commonAssignmentCheck in class BaseTypeVisitor<UpperBoundAnnotatedTypeFactory>

Parameters:

varType - the annotated type of the lvalue (usually a variable)

valueExp - the AST node for the rvalue (the new value)

errorKey - the error message to use if the check fails (must be a compiler message key, see CompilerMessageKey)