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:

• new array: "b = new T[a.length]" implies that b is the same length as a.
• length equality: after "if (a.length == b.length)", a and b have the same length.
• object equality: 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 void	addInformationFromPreconditions(CFStore info, AnnotatedTypeFactory factory, UnderlyingAST.CFGMethod method, com.sun.source.tree.MethodTree methodTree, javax.lang.model.element.ExecutableElement methodElement) Overridden to ensure that SameLen annotations on method parameters are symmetric.
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)

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

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, visitClassDeclaration, 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, visitClassDeclaration, 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)

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.

addInformationFromPreconditions

protected void addInformationFromPreconditions(CFStore info,
                                               AnnotatedTypeFactory factory,
                                               UnderlyingAST.CFGMethod method,
                                               com.sun.source.tree.MethodTree methodTree,
                                               javax.lang.model.element.ExecutableElement methodElement)

Overridden to ensure that SameLen annotations on method parameters are symmetric.

Overrides:

addInformationFromPreconditions in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>