org.checkerframework.checker.mustcall

Class MustCallTransfer

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.mustcall.MustCallTransfer

All Implemented Interfaces:

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

public class MustCallTransfer
extends CFTransfer

Transfer function for the must-call type system. Its primary purposes are (1) to create temporary variables for expressions (which allow those expressions to have refined information in the store, which the consistency checker can use), and (2) to reset refined information when a method annotated with @CreatesObligation is called.

Field Summary

Fields

Modifier and Type	Field and Description
protected long	uid A unique identifier counter for node names.

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

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor and Description
MustCallTransfer(CFAnalysis analysis) Create a MustCallTransfer.

Method Summary

Modifier and Type	Method and Description
protected @Nullable VariableTree	createTemporaryVar(Node node) Creates a variable declaration for the given expression node, if possible.
protected String	uniqueName(String prefix) Creates a unique, abitrary string that can be used as a name for a temporary variable, using the given prefix.
void	updateStoreWithTempVar(TransferResult<CFValue,CFStore> result, Node node) This method either creates or looks up the temp var t for node, and then updates the store to give t the same type as node.
TransferResult<CFValue,CFStore>	visitMethodInvocation(MethodInvocationNode n, TransferInput<CFValue,CFStore> in)
TransferResult<CFValue,CFStore>	visitObjectCreation(ObjectCreationNode node, TransferInput<CFValue,CFStore> input)
TransferResult<CFValue,CFStore>	visitStringConversion(StringConversionNode n, TransferInput<CFValue,CFStore> p)
TransferResult<CFValue,CFStore>	visitTernaryExpression(TernaryExpressionNode node, TransferInput<CFValue,CFStore> input)

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

addInformationFromPreconditions, createTransferResult, finishValue, finishValue, getNarrowedValue, getValueFromFactory, getValueWithSameAnnotations, getWidenedValue, initialStore, insertIntoStores, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, recreateTransferResult, setFixedInitialStore, splitAssignments, strengthenAnnotationOfEqualTo, usesSequentialSemantics, visitArrayAccess, visitAssignment, visitCase, visitClassName, visitConditionalNot, visitEqualTo, visitFieldAccess, visitInstanceOf, visitLambdaResultExpression, visitLocalVariable, visitNarrowingConversion, visitNode, visitNotEqual, visitReturn, visitStringConcatenateAssignment, 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, 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, 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

Field Detail

uid

protected long uid

A unique identifier counter for node names.

Constructor Detail

MustCallTransfer

public MustCallTransfer(CFAnalysis analysis)

Create a MustCallTransfer.

Parameters:

analysis - the analysis

Method Detail

visitStringConversion

public TransferResult<CFValue,CFStore> visitStringConversion(StringConversionNode n,
                                                             TransferInput<CFValue,CFStore> p)

Specified by:

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

Overrides:

visitStringConversion in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

visitMethodInvocation

public TransferResult<CFValue,CFStore> visitMethodInvocation(MethodInvocationNode n,
                                                             TransferInput<CFValue,CFStore> in)

Specified by:

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

Overrides:

visitMethodInvocation in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

visitObjectCreation

public TransferResult<CFValue,CFStore> visitObjectCreation(ObjectCreationNode node,
                                                           TransferInput<CFValue,CFStore> input)

Specified by:

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

Overrides:

visitObjectCreation in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

visitTernaryExpression

public TransferResult<CFValue,CFStore> visitTernaryExpression(TernaryExpressionNode node,
                                                              TransferInput<CFValue,CFStore> input)

Specified by:

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

Overrides:

visitTernaryExpression in class CFAbstractTransfer<CFValue,CFStore,CFTransfer>

updateStoreWithTempVar

public void updateStoreWithTempVar(TransferResult<CFValue,CFStore> result,
                                   Node node)

This method either creates or looks up the temp var t for node, and then updates the store to give t the same type as node.

Parameters:

node - the node to be assigned to a temporary variable

result - the transfer result containing the store to be modified

createTemporaryVar

protected @Nullable VariableTree createTemporaryVar(Node node)

Creates a variable declaration for the given expression node, if possible.

Parameters:

node - an expression node

Returns:

a variable tree for the node, or null if an appropriate containing element cannot be located

uniqueName

protected String uniqueName(String prefix)

Creates a unique, abitrary string that can be used as a name for a temporary variable, using the given prefix. Can be used up to Long.MAX_VALUE times.

Parameters:

prefix - the prefix for the name

Returns:

a unique name that starts with the prefix