Package 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:

ForwardTransferFunction<CFValue,CFStore>, 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	Description
SameLenTransfer(CFAnalysis analysis)	Create a new SameLenTransfer.

Method Summary

Modifier and Type	Method	Description
protected void	addInformationFromPreconditions(CFStore info, AnnotatedTypeFactory factory, UnderlyingAST.CFGMethod method, MethodTree methodTree, 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

createTransferResult, finishValue, finishValue, getNarrowedValue, getValueFromFactory, getWidenedValue, initialStore, insertIntoStores, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, recreateTransferResult, setFixedInitialStore, splitAssignments, usesSequentialSemantics, visitArrayAccess, visitCase, visitClassName, visitConditionalNot, visitEqualTo, visitExpressionStatement, visitFieldAccess, visitInstanceOf, visitLambdaResultExpression, visitLocalVariable, visitMethodInvocation, visitNarrowingConversion, visitNode, visitNotEqual, visitObjectCreation, visitReturn, visitStringConversion, visitSwitchExpressionNode, visitTernaryExpression, visitThis, visitVariableDeclaration, visitWideningConversion

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

visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitClassDeclaration, visitConditionalAnd, visitConditionalOr, visitDeconstructorPattern, visitDoubleLiteral, visitExplicitThis, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThis, 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, visitDeconstructorPattern, visitDoubleLiteral, visitExplicitThis, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThis, 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 Details

SameLenTransfer

public SameLenTransfer(CFAnalysis analysis)

Create a new SameLenTransfer.

Parameters:

analysis - the CFAnalysis

Method Details

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

firstNode - the node that might be more precise

secondNode - the node whose type to possibly refine

firstValue - the abstract value that might be more precise

secondValue - the abstract value that might be less precise

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 res

addInformationFromPreconditions

protected void addInformationFromPreconditions(CFStore info,
 AnnotatedTypeFactory factory,
 UnderlyingAST.CFGMethod method,
 MethodTree methodTree,
 ExecutableElement methodElement)

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

Overrides:

addInformationFromPreconditions in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

Parameters:

info - the initial store for the method body

factory - the type factory

method - the AST for a method declaration

methodTree - the declaration of the method; is a field of methodAst

methodElement - the element for the method