org.checkerframework.checker.index.inequality

Class LessThanTransfer

java.lang.Object

org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<TransferResult<V,S>,TransferInput<V,S>>

org.checkerframework.framework.flow.CFAbstractTransfer<CFValue,CFStore,CFTransfer>

org.checkerframework.framework.flow.CFTransfer

org.checkerframework.checker.index.IndexAbstractTransfer

org.checkerframework.checker.index.inequality.LessThanTransfer

All Implemented Interfaces:

TransferFunction<CFValue,CFStore>, NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

public class LessThanTransfer
extends IndexAbstractTransfer

Implements 3 refinement rules:

• 1. if left > right, right has type @LessThan("left")
• 2. if left ≥ right, right has type @LessThan("left + 1")
• 3. if 0 < right, left - right has type @LessThan("left")

These are implemented generally, so they also apply to e.g. < and ≤ comparisons.

Field Summary

Fields inherited from class org.checkerframework.framework.flow.CFAbstractTransfer

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor and Description
LessThanTransfer(CFAnalysis analysis)

Method Summary

Modifier and Type	Method and Description
protected void	refineGT(Node left, AnnotationMirror leftAnno, Node right, AnnotationMirror rightAnno, CFStore store, TransferInput<CFValue,CFStore> in) Case 1.
protected void	refineGTE(Node left, AnnotationMirror leftAnno, Node right, AnnotationMirror rightAnno, CFStore store, TransferInput<CFValue,CFStore> in) Case 2.
TransferResult<CFValue,CFStore>	visitNumericalSubtraction(NumericalSubtractionNode n, TransferInput<CFValue,CFStore> in) Case 3.

Methods inherited from class org.checkerframework.checker.index.IndexAbstractTransfer

visitGreaterThan, visitGreaterThanOrEqual, visitLessThan, visitLessThanOrEqual

Methods inherited from class org.checkerframework.framework.flow.CFAbstractTransfer

addInformationFromPreconditions, finishValue, finishValue, getValueFromFactory, getValueWithSameAnnotations, initialStore, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, setFixedInitialStore, splitAssignments, strengthenAnnotationOfEqualTo, usesSequentialSemantics, visitArrayAccess, visitAssignment, visitCase, visitClassName, visitConditionalNot, visitEqualTo, visitFieldAccess, visitLambdaResultExpression, visitLocalVariable, visitMethodInvocation, visitNarrowingConversion, visitNode, visitNotEqual, visitObjectCreation, visitReturn, visitStringConcatenateAssignment, visitStringConversion, visitTernaryExpression, visitThisLiteral, visitVariableDeclaration, visitWideningConversion

Methods inherited from class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor

visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitClassDeclaration, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThisLiteral, visitInstanceOf, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, visitUnsignedRightShift, visitValueLiteral

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.checkerframework.dataflow.cfg.node.NodeVisitor

visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitClassDeclaration, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThisLiteral, visitInstanceOf, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, visitUnsignedRightShift

Constructor Detail

LessThanTransfer

public LessThanTransfer(CFAnalysis analysis)

Method Detail

refineGT

protected void refineGT(Node left,
                        AnnotationMirror leftAnno,
                        Node right,
                        AnnotationMirror rightAnno,
                        CFStore store,
                        TransferInput<CFValue,CFStore> in)

Case 1.

Specified by:

refineGT in class IndexAbstractTransfer

refineGTE

protected void refineGTE(Node left,
                         AnnotationMirror leftAnno,
                         Node right,
                         AnnotationMirror rightAnno,
                         CFStore store,
                         TransferInput<CFValue,CFStore> in)

Case 2.

Specified by:

refineGTE in class IndexAbstractTransfer

visitNumericalSubtraction

public TransferResult<CFValue,CFStore> visitNumericalSubtraction(NumericalSubtractionNode n,
                                                                 TransferInput<CFValue,CFStore> in)

Case 3.

Specified by:

visitNumericalSubtraction in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

Overrides:

visitNumericalSubtraction in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>