org.checkerframework.checker.index.lowerbound

Class LowerBoundVisitor

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

org.checkerframework.checker.index.lowerbound.LowerBoundVisitor

All Implemented Interfaces:

TreeVisitor<java.lang.Void,java.lang.Void>

public class LowerBoundVisitor
extends BaseTypeVisitor<LowerBoundAnnotatedTypeFactory>

Implements the actual checks to make sure that array accesses aren't too low. Will issue a warning if a variable that can't be proved to be either "NonNegative" (i.e. ≥ 0) or "Positive" (i.e. ≥ 1) is used as an array index.

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
LowerBoundVisitor(BaseTypeChecker checker)

Method Summary

Modifier and Type	Method and Description
java.lang.Void	visitArrayAccess(ArrayAccessTree tree, java.lang.Void type)
java.lang.Void	visitNewArray(NewArrayTree tree, java.lang.Void type)

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, 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, visitNewClass, visitParameterizedType, visitReturn, visitThrow, 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, visitTry, visitUnionType, visitWhileLoop, visitWildcard

Methods inherited from class java.lang.Object

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

Constructor Detail

LowerBoundVisitor

public LowerBoundVisitor(BaseTypeChecker checker)

Method Detail

visitArrayAccess

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

Specified by:

visitArrayAccess in interface TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitArrayAccess in class BaseTypeVisitor<LowerBoundAnnotatedTypeFactory>

visitNewArray

public java.lang.Void visitNewArray(NewArrayTree tree,
                                    java.lang.Void type)

Specified by:

visitNewArray in interface TreeVisitor<java.lang.Void,java.lang.Void>

Overrides:

visitNewArray in class BaseTypeVisitor<LowerBoundAnnotatedTypeFactory>