org.checkerframework.checker.index.samelen

Class SameLenTransfer

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.samelen.SameLenTransfer

All Implemented Interfaces:

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

public class SameLenTransfer
extends CFTransfer

The transfer function for the SameLen checker. Contains three cases:

1. 1. "b = new T[a.length]" implies that b is the same length as a.
2. 2. after "if (a.length == b.length)", a and b have the same length.
3. 3. after "if (a == b)", a and b have the same length, if they are arrays or strings.

Field Summary

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

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor and Description
SameLenTransfer(CFAnalysis analysis)

Method Summary

Modifier and Type	Method and Description
protected TransferResult<CFValue,CFStore>	strengthenAnnotationOfEqualTo(TransferResult<CFValue,CFStore> result, Node firstNode, Node secondNode, CFValue firstValue, CFValue secondValue, boolean notEqualTo) Implements the transfer rules for both equal nodes and not-equals nodes.
TransferResult<CFValue,CFStore>	visitAssignment(AssignmentNode node, TransferInput<CFValue,CFStore> in) Handles case 1

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

addInformationFromPreconditions, finishValue, finishValue, getValueFromFactory, getValueWithSameAnnotations, initialStore, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, setFixedInitialStore, splitAssignments, usesSequentialSemantics, visitArrayAccess, 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, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThisLiteral, visitInstanceOf, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLessThan, visitLessThanOrEqual, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitNumericalSubtraction, 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, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThisLiteral, visitInstanceOf, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLessThan, visitLessThanOrEqual, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitNumericalSubtraction, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, visitUnsignedRightShift

Constructor Detail

SameLenTransfer

public SameLenTransfer(CFAnalysis analysis)

Method Detail

visitAssignment

public TransferResult<CFValue,CFStore> visitAssignment(AssignmentNode node,
                                                       TransferInput<CFValue,CFStore> in)

Handles case 1

Specified by:

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

Overrides:

visitAssignment in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

strengthenAnnotationOfEqualTo

protected TransferResult<CFValue,CFStore> strengthenAnnotationOfEqualTo(TransferResult<CFValue,CFStore> result,
                                                                        Node firstNode,
                                                                        Node secondNode,
                                                                        CFValue firstValue,
                                                                        CFValue secondValue,
                                                                        boolean notEqualTo)

Implements the transfer rules for both equal nodes and not-equals nodes.

Overrides:

strengthenAnnotationOfEqualTo in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

Parameters:

result - the previous result

notEqualTo - 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.

Returns:

the conditional transfer result (if information has been added), or null.