org.checkerframework.checker.index.lowerbound

Class LowerBoundTransfer

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

org.checkerframework.checker.index.lowerbound.LowerBoundTransfer

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 LowerBoundTransfer
extends IndexAbstractTransfer

Implements dataflow refinement rules based on tests: <, >, ==, and their derivatives.

Also implements the logic for binary operations: +, -, *, /, and %.

>, <, ≥, ≤, ==, and != nodes are represented as combinations of > and ≥ (e.g. == is ≥ in both directions in the then branch), and implement refinements based on these decompositions.

 Refinement/transfer rules for conditionals:

 There are two "primitives":

 x > y, which implies things about x based on y's type:

 y has type:    implies x has type:
  gte-1                nn
  nn                   pos
  pos                  pos

 and x ≥ y:

 y has type:    implies x has type:
  gte-1                gte-1
  nn                   nn
  pos                  pos

 These two "building blocks" can be combined to make all
 other conditional expressions:

 EXPR             THEN          ELSE
 x > y            x > y         y ≥ x
 x ≥ y           x ≥ y        y > x
 x < y            y > x         x ≥ y
 x ≤ y           y ≥ x        x > y

 Or, more formally:

 EXPR        THEN                                        ELSE
 x > y       x_refined = GLB(x_orig, promote(y))         y_refined = GLB(y_orig, x)
 x ≥ y      x_refined = GLB(x_orig, y)                  y_refined = GLB(y_orig, promote(x))
 x < y       y_refined = GLB(y_orig, promote(x))         x_refined = GLB(x_orig, y)
 x ≤ y      y_refined = GLB(y_orig, x)                  x_refined = GLB(x_orig, promote(y))

 where GLB is the greatest lower bound and promote is the increment
 function on types (or, equivalently, the function specified by the "x
 > y" information above).

 There's also ==, which is a special case. Only the THEN
 branch is refined:

 EXPR             THEN                   ELSE
 x == y           x ≥ y && y ≥ x       nothing known

 or, more formally:

 EXPR            THEN                                    ELSE
 x == y          x_refined = GLB(x_orig, y_orig)         nothing known
                y_refined = GLB(x_orig, y_orig)

 finally, not equal:

 EXPR             THEN                   ELSE
 x != y           nothing known          x ≥ y && y ≥ x

 more formally:

 EXPR            THEN               ELSE
 x != y          nothing known      x_refined = GLB(x_orig, y_orig)
                                   y_refined = GLB(x_orig, y_orig)

 

Dividing these rules up by cases, this class implements:

• 1. The rule described above for >
• 2. The rule described above for ≥
• 3. The rule described above for <
• 4. The rule described above for ≤
• 5. The rule described above for ==
• 6. The rule described above for !=
• 7. A special refinement for != when the value being compared to is a compile-time constant with a value exactly equal to -1 or 0 (i.e. x != -1 and x is GTEN1 implies x is non-negative). Maybe two rules?
• 8. When a compile-time constant -2 is added to a positive, the result is GTEN1
• 9. When a compile-time constant 2 is added to a GTEN1, the result is positive
• 10. When a positive is added to a positive, the result is positive
• 11. When a non-negative is added to any other type, the result is that other type
• 12. When a GTEN1 is added to a positive, the result is non-negative
• 13. When the left side of a subtraction expression is > the right side according to the LessThanChecker, the result of the subtraction expression is positive
• 14. When the left side of a subtraction expression is ≥ the right side according to the LessThanChecker, the result of the subtraction expression is non-negative
• 15. special handling for when the left side is the length of an array or String that's stored as a field, and the right side is a compile time constant. Do we need this?
• 16. Multiplying any value by a compile time constant of 1 preserves its type
• 17. Multiplying two positives produces a positive
• 18. Multiplying a positive and a non-negative produces a non-negative
• 19. Multiplying two non-negatives produces a non-negative
• 20. When the result of Math.random is multiplied by an array length, the result is NonNegative.
• 21. literal 0 divided by anything is non-negative
• 22. anything divided by literal zero is bottom
• 23. literal 1 divided by a positive or non-negative is non-negative
• 24. literal 1 divided by anything else is GTEN1
• 25. anything divided by literal 1 is itself
• 26. a positive or non-negative divided by a positive or non-negative is non-negative
• 27. anything modded by literal 1 or -1 is non-negative
• 28. a positive or non-negative modded by anything is non-negative
• 29. a GTEN1 modded by anything is GTEN1
• 30. anything right-shifted by a non-negative is non-negative
• 31. anything bitwise-anded by a non-negative is non-negative
• 32. If a and b are non-negative and a <= b and a != b, then b is pos.

Field Summary

Fields

Modifier and Type	Field and Description
javax.lang.model.element.AnnotationMirror	GTEN1 The canonical GTENegativeOne annotation.
javax.lang.model.element.AnnotationMirror	NN The canonical NonNegative annotation.
javax.lang.model.element.AnnotationMirror	POS The canonical Positive annotation.
javax.lang.model.element.AnnotationMirror	UNKNOWN The canonical LowerBoundUnknown annotation.

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

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor and Description
LowerBoundTransfer(org.checkerframework.framework.flow.CFAnalysis analysis)

Method Summary

Modifier and Type	Method and Description
javax.lang.model.element.AnnotationMirror	getAnnotationForRemainder(org.checkerframework.dataflow.cfg.node.IntegerRemainderNode node, org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p) getAnnotationForRemainder handles these cases:
protected void	refineGT(org.checkerframework.dataflow.cfg.node.Node left, javax.lang.model.element.AnnotationMirror leftAnno, org.checkerframework.dataflow.cfg.node.Node right, javax.lang.model.element.AnnotationMirror rightAnno, org.checkerframework.framework.flow.CFStore store, org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> in) The implementation of the algorithm for refining a > test.
protected void	refineGTE(org.checkerframework.dataflow.cfg.node.Node left, javax.lang.model.element.AnnotationMirror leftAnno, org.checkerframework.dataflow.cfg.node.Node right, javax.lang.model.element.AnnotationMirror rightAnno, org.checkerframework.framework.flow.CFStore store, org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> in) Refines left to exactly the level of right, since in the worst case they're equal.
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 (i.e.
org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore>	visitBitwiseAnd(org.checkerframework.dataflow.cfg.node.BitwiseAndNode n, org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)
org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore>	visitIntegerDivision(org.checkerframework.dataflow.cfg.node.IntegerDivisionNode n, org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)
org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore>	visitIntegerRemainder(org.checkerframework.dataflow.cfg.node.IntegerRemainderNode n, org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)
org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore>	visitNumericalAddition(org.checkerframework.dataflow.cfg.node.NumericalAdditionNode n, org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)
org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore>	visitNumericalMultiplication(org.checkerframework.dataflow.cfg.node.NumericalMultiplicationNode n, org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)
org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore>	visitNumericalSubtraction(org.checkerframework.dataflow.cfg.node.NumericalSubtractionNode n, org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)
org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore>	visitSignedRightShift(org.checkerframework.dataflow.cfg.node.SignedRightShiftNode n, org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)
org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore>	visitUnsignedRightShift(org.checkerframework.dataflow.cfg.node.UnsignedRightShiftNode n, org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)

Methods inherited from class org.checkerframework.checker.index.IndexAbstractTransfer

visitGreaterThan, visitGreaterThanOrEqual, visitLessThan, visitLessThanOrEqual

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

addInformationFromPreconditions, finishValue, finishValue, getValueFromFactory, getValueWithSameAnnotations, initialStore, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, setFixedInitialStore, splitAssignments, usesSequentialSemantics, visitArrayAccess, visitAssignment, 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, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThisLiteral, visitInstanceOf, visitIntegerLiteral, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalMinus, visitNumericalPlus, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, 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, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThisLiteral, visitInstanceOf, visitIntegerLiteral, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalMinus, visitNumericalPlus, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast

Field Detail

GTEN1

public final javax.lang.model.element.AnnotationMirror GTEN1

The canonical GTENegativeOne annotation.

NN

public final javax.lang.model.element.AnnotationMirror NN

The canonical NonNegative annotation.

POS

public final javax.lang.model.element.AnnotationMirror POS

The canonical Positive annotation.

UNKNOWN

public final javax.lang.model.element.AnnotationMirror UNKNOWN

The canonical LowerBoundUnknown annotation.

Constructor Detail

LowerBoundTransfer

public LowerBoundTransfer(org.checkerframework.framework.flow.CFAnalysis analysis)

Method Detail

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 (i.e. cases 5, 6, 32).

Overrides:

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

refineGT

protected void refineGT(org.checkerframework.dataflow.cfg.node.Node left,
                        javax.lang.model.element.AnnotationMirror leftAnno,
                        org.checkerframework.dataflow.cfg.node.Node right,
                        javax.lang.model.element.AnnotationMirror rightAnno,
                        org.checkerframework.framework.flow.CFStore store,
                        org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> in)

The implementation of the algorithm for refining a > test. Changes the type of left (the greater one) to one closer to bottom than the type of right. Can't call the promote function from the ATF directly because a new expression isn't introduced here - the modifications have to be made to an existing one.

This implements parts of cases 1, 2, 3, and 4 using the decomposition strategy described in the Javadoc of this class.

Specified by:

refineGT in class IndexAbstractTransfer

refineGTE

protected void refineGTE(org.checkerframework.dataflow.cfg.node.Node left,
                         javax.lang.model.element.AnnotationMirror leftAnno,
                         org.checkerframework.dataflow.cfg.node.Node right,
                         javax.lang.model.element.AnnotationMirror rightAnno,
                         org.checkerframework.framework.flow.CFStore store,
                         org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> in)

Refines left to exactly the level of right, since in the worst case they're equal. Modifies an existing type in the store, but has to be careful not to overwrite a more precise existing type.

This implements parts of cases 1, 2, 3, and 4 using the decomposition strategy described in this class's Javadoc.

Specified by:

refineGTE in class IndexAbstractTransfer

getAnnotationForRemainder

public javax.lang.model.element.AnnotationMirror getAnnotationForRemainder(org.checkerframework.dataflow.cfg.node.IntegerRemainderNode node,
                                                                           org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)

getAnnotationForRemainder handles these cases:

      27. * % 1/-1 → nn
      28. pos/nn % * → nn
      29. gten1 % * → gten1
      * % * → lbu
 

visitNumericalAddition

public org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> visitNumericalAddition(org.checkerframework.dataflow.cfg.node.NumericalAdditionNode n,
                                                                                                                                                                             org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)

Specified by:

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

visitNumericalAddition in class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<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>>

visitNumericalSubtraction

public org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> visitNumericalSubtraction(org.checkerframework.dataflow.cfg.node.NumericalSubtractionNode n,
                                                                                                                                                                                org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)

Specified by:

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

visitNumericalSubtraction in class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<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>>

visitNumericalMultiplication

public org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> visitNumericalMultiplication(org.checkerframework.dataflow.cfg.node.NumericalMultiplicationNode n,
                                                                                                                                                                                   org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)

Specified by:

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

visitNumericalMultiplication in class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<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>>

visitIntegerDivision

public org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> visitIntegerDivision(org.checkerframework.dataflow.cfg.node.IntegerDivisionNode n,
                                                                                                                                                                           org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)

Specified by:

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

visitIntegerDivision in class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<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>>

visitIntegerRemainder

public org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> visitIntegerRemainder(org.checkerframework.dataflow.cfg.node.IntegerRemainderNode n,
                                                                                                                                                                            org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)

Specified by:

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

visitIntegerRemainder in class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<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>>

visitSignedRightShift

public org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> visitSignedRightShift(org.checkerframework.dataflow.cfg.node.SignedRightShiftNode n,
                                                                                                                                                                            org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)

Specified by:

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

visitSignedRightShift in class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<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>>

visitUnsignedRightShift

public org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> visitUnsignedRightShift(org.checkerframework.dataflow.cfg.node.UnsignedRightShiftNode n,
                                                                                                                                                                              org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)

Specified by:

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

visitUnsignedRightShift in class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<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>>

visitBitwiseAnd

public org.checkerframework.dataflow.analysis.TransferResult<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> visitBitwiseAnd(org.checkerframework.dataflow.cfg.node.BitwiseAndNode n,
                                                                                                                                                                      org.checkerframework.dataflow.analysis.TransferInput<org.checkerframework.framework.flow.CFValue,org.checkerframework.framework.flow.CFStore> p)

Specified by:

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

visitBitwiseAnd in class org.checkerframework.dataflow.cfg.node.AbstractNodeVisitor<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>>