public class UpperBoundTransfer extends IndexAbstractTransfer
analysissequentialSemantics| Constructor and Description |
|---|
UpperBoundTransfer(CFAnalysis analysis) |
| Modifier and Type | Method and Description |
|---|---|
protected void |
refineGT(Node left,
AnnotationMirror leftAnno,
Node right,
AnnotationMirror rightAnno,
CFStore store)
The implementation of the algorithm for refining a > test.
|
protected void |
refineGTE(Node left,
AnnotationMirror leftAnno,
Node right,
AnnotationMirror rightAnno,
CFStore store)
If an LTL is greater than or equal to something, it must also be LTL.
|
protected TransferResult<CFValue,CFStore> |
strengthenAnnotationOfEqualTo(TransferResult<CFValue,CFStore> res,
Node firstNode,
Node secondNode,
CFValue firstValue,
CFValue secondValue,
boolean notEqualTo)
Refine the annotation of
secondNode if the annotation secondValue is less
precise than firstvalue. |
TransferResult<CFValue,CFStore> |
visitAssignment(AssignmentNode node,
TransferInput<CFValue,CFStore> in) |
isArrayLengthFieldAccess, visitGreaterThan, visitGreaterThanOrEqual, visitLessThan, visitLessThanOrEqualaddInformationFromPreconditions, finishValue, finishValue, getTypeFactoryOfSubchecker, getValueFromFactory, getValueWithSameAnnotations, initialStore, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, setFixedInitialStore, splitAssignments, usesSequentialSemantics, visitArrayAccess, visitCase, visitClassName, visitConditionalNot, visitEqualTo, visitFieldAccess, visitLocalVariable, visitMethodInvocation, visitNarrowingConversion, visitNode, visitNotEqual, visitObjectCreation, visitReturn, visitStringConcatenateAssignment, visitStringConversion, visitTernaryExpression, visitThisLiteral, visitVariableDeclaration, visitWideningConversionvisitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThisLiteral, visitInstanceOf, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitNumericalSubtraction, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, visitUnsignedRightShift, visitValueLiteralclone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, waitvisitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThisLiteral, visitInstanceOf, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitNumericalSubtraction, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, visitUnsignedRightShiftpublic UpperBoundTransfer(CFAnalysis analysis)
public TransferResult<CFValue,CFStore> visitAssignment(AssignmentNode node, TransferInput<CFValue,CFStore> in)
visitAssignment in interface NodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>visitAssignment in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>protected TransferResult<CFValue,CFStore> strengthenAnnotationOfEqualTo(TransferResult<CFValue,CFStore> res, Node firstNode, Node secondNode, CFValue firstValue, CFValue secondValue, boolean notEqualTo)
CFAbstractTransfersecondNode if the annotation secondValue is less
precise than firstvalue. This is possible, if secondNode is an expression
that is tracked by the store (e.g., a local variable or a field).strengthenAnnotationOfEqualTo in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>res - the previous resultnotEqualTo - if true, indicates that the logic is flipped (i.e., the information is
added to the elseStore instead of the thenStore) for a not-equal
comparison.null.protected void refineGT(Node left, AnnotationMirror leftAnno, Node right, AnnotationMirror rightAnno, CFStore store)
refineGT in class IndexAbstractTransferprotected void refineGTE(Node left, AnnotationMirror leftAnno, Node right, AnnotationMirror rightAnno, CFStore store)
refineGTE in class IndexAbstractTransfer