Package org.checkerframework.checker.nonempty

Class NonEmptyTransfer

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.nonempty.NonEmptyTransfer

All Implemented Interfaces:

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

public class NonEmptyTransfer
extends CFTransfer

This class implements type rules that cannot be expressed via pre- or post-condition annotations.

Field Summary

Fields

Modifier and Type	Field	Description
protected final NonEmptyAnnotatedTypeFactory	aTypeFactory	A NonEmptyAnnotatedTypeFactory instance.

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

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor	Description
NonEmptyTransfer(CFAnalysis analysis)	Create a new NonEmptyTransfer.

Method Summary

Modifier and Type	Method	Description
TransferResult<CFValue,CFStore>	visitCase(CaseNode n, TransferInput<CFValue,CFStore> in)	A case produces no value, but it may imply some facts about switch selector expression.
TransferResult<CFValue,CFStore>	visitEqualTo(EqualToNode n, TransferInput<CFValue,CFStore> in)
TransferResult<CFValue,CFStore>	visitGreaterThan(GreaterThanNode n, TransferInput<CFValue,CFStore> in)
TransferResult<CFValue,CFStore>	visitGreaterThanOrEqual(GreaterThanOrEqualNode n, TransferInput<CFValue,CFStore> in)
TransferResult<CFValue,CFStore>	visitLessThan(LessThanNode n, TransferInput<CFValue,CFStore> in)
TransferResult<CFValue,CFStore>	visitLessThanOrEqual(LessThanOrEqualNode n, TransferInput<CFValue,CFStore> in)
TransferResult<CFValue,CFStore>	visitNotEqual(NotEqualNode n, TransferInput<CFValue,CFStore> in)

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

addInformationFromPreconditions, createTransferResult, createTransferResult, finishValue, finishValue, getNarrowedValue, getValueFromFactory, getWidenedValue, initialStore, insertIntoStores, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, recreateTransferResult, recreateTransferResult, setFixedInitialStore, shouldPerformWholeProgramInference, shouldPerformWholeProgramInference, splitAssignments, strengthenAnnotationOfEqualTo, usesSequentialSemantics, visitArrayAccess, visitAssignment, visitClassName, visitConditionalNot, visitDeconstructorPattern, visitExpressionStatement, visitFieldAccess, visitInstanceOf, visitLambdaResultExpression, visitLocalVariable, visitMethodInvocation, visitNarrowingConversion, visitNode, 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, visitDoubleLiteral, visitExplicitThis, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThis, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, 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, visitExplicitThis, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitImplicitThis, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitNumericalSubtraction, visitPackageName, visitParameterizedType, visitPrimitiveType, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitSynchronized, visitThrow, visitTypeCast, visitUnsignedRightShift

Field Details

aTypeFactory

protected final NonEmptyAnnotatedTypeFactory aTypeFactory

A NonEmptyAnnotatedTypeFactory instance.

Constructor Details

NonEmptyTransfer

public NonEmptyTransfer(CFAnalysis analysis)

Create a new NonEmptyTransfer.

Parameters:

analysis - the analysis for this transfer function

Method Details

visitEqualTo

public TransferResult<CFValue,CFStore> visitEqualTo(EqualToNode n,
 TransferInput<CFValue,CFStore> in)

Specified by:

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

Overrides:

visitEqualTo in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

visitNotEqual

public TransferResult<CFValue,CFStore> visitNotEqual(NotEqualNode n,
 TransferInput<CFValue,CFStore> in)

Specified by:

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

Overrides:

visitNotEqual in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

visitLessThan

public TransferResult<CFValue,CFStore> visitLessThan(LessThanNode n,
 TransferInput<CFValue,CFStore> in)

Specified by:

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

Overrides:

visitLessThan in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitLessThanOrEqual

public TransferResult<CFValue,CFStore> visitLessThanOrEqual(LessThanOrEqualNode n,
 TransferInput<CFValue,CFStore> in)

Specified by:

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

Overrides:

visitLessThanOrEqual in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitGreaterThan

public TransferResult<CFValue,CFStore> visitGreaterThan(GreaterThanNode n,
 TransferInput<CFValue,CFStore> in)

Specified by:

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

Overrides:

visitGreaterThan in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitGreaterThanOrEqual

public TransferResult<CFValue,CFStore> visitGreaterThanOrEqual(GreaterThanOrEqualNode n,
 TransferInput<CFValue,CFStore> in)

Specified by:

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

Overrides:

visitGreaterThanOrEqual in class AbstractNodeVisitor<TransferResult<CFValue,CFStore>,TransferInput<CFValue,CFStore>>

visitCase

public TransferResult<CFValue,CFStore> visitCase(CaseNode n,
 TransferInput<CFValue,CFStore> in)

Description copied from class: CFAbstractTransfer

A case produces no value, but it may imply some facts about switch selector expression.

Specified by:

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

Overrides:

visitCase in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>