org.checkerframework.checker.index.samelen

Class SameLenTransfer

java.lang.Object

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

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

org.checkerframework.framework.flow.CFTransfer

org.checkerframework.checker.index.samelen.SameLenTransfer

All Implemented Interfaces:

org.checkerframework.dataflow.analysis.TransferFunction<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore>, org.checkerframework.dataflow.cfg.node.NodeVisitor<org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore>,org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore>>

public class SameLenTransfer
extends org.checkerframework.framework.flow.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(org.checkerframework.framework.flow.CFAnalysis analysis)

Method Summary

Modifier and Type	Method and Description
protected org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore>	strengthenAnnotationOfEqualTo(org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> result, org.checkerframework.dataflow.cfg.node.Node firstNode, org.checkerframework.dataflow.cfg.node.Node secondNode, org.checkerframework.framework.flow.CFValue firstValue, org.checkerframework.framework.flow.CFValue secondValue, boolean notEqualTo) Implements the transfer rules for both equal nodes and not-equals nodes.
org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore>	visitAssignment(org.checkerframework.dataflow.cfg.node.AssignmentNode node, org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.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(org.checkerframework.framework.flow.CFAnalysis analysis)

Method Detail

visitAssignment

public org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> visitAssignment(org.checkerframework.dataflow.cfg.node.AssignmentNode node,
                                                                                                                                                                      org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> in)

Handles case 1

Specified by:

visitAssignment in interface org.checkerframework.dataflow.cfg.node.NodeVisitor<org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore>,org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore>>

Overrides:

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

strengthenAnnotationOfEqualTo

protected org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> strengthenAnnotationOfEqualTo(org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> result,
                                                                                                                                                                                       org.checkerframework.dataflow.cfg.node.Node firstNode,
                                                                                                                                                                                       org.checkerframework.dataflow.cfg.node.Node secondNode,
                                                                                                                                                                                       org.checkerframework.framework.flow.CFValue firstValue,
                                                                                                                                                                                       org.checkerframework.framework.flow.CFValue secondValue,
                                                                                                                                                                                       boolean notEqualTo)

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

Overrides:

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