Package org.checkerframework.checker.lock

Class LockTransfer

java.lang.Object

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

org.checkerframework.framework.flow.CFAbstractTransfer<CFValue,LockStore,LockTransfer>

org.checkerframework.checker.lock.LockTransfer

All Implemented Interfaces:

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

public class LockTransfer
extends CFAbstractTransfer<CFValue,LockStore,LockTransfer>

LockTransfer handles constructors, initializers, synchronized methods, and synchronized blocks.

Field Summary

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

analysis, sequentialSemantics

Constructor Summary

Constructors

Constructor	Description
LockTransfer(LockAnalysis analysis, LockChecker checker)	Create a transfer function for the Lock Checker.

Method Summary

Modifier and Type	Method	Description
LockStore	initialStore(UnderlyingAST underlyingAST, java.util.List<LocalVariableNode> parameters)	The initial store maps method formal parameters to their currently most refined type.
protected void	makeLockHeld(LockStore store, Node node)	Sets a given Node to @LockHeld in the given store.
protected void	makeLockHeld(TransferResult<CFValue,LockStore> result, Node node)	Sets a given Node node to LockHeld in the given TransferResult.
protected void	makeLockPossiblyHeld(LockStore store, Node node)	Sets a given Node to @LockPossiblyHeld in the given store.
protected void	makeLockPossiblyHeld(TransferResult<CFValue,LockStore> result, Node node)	Sets a given Node node to LockPossiblyHeld in the given TransferResult.
TransferResult<CFValue,LockStore>	visitSynchronized(SynchronizedNode n, TransferInput<CFValue,LockStore> p)

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

addInformationFromPreconditions, createTransferResult, finishValue, finishValue, getNarrowedValue, getValueFromFactory, getWidenedValue, insertIntoStores, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, recreateTransferResult, setFixedInitialStore, splitAssignments, strengthenAnnotationOfEqualTo, usesSequentialSemantics, visitArrayAccess, visitAssignment, visitCase, visitClassName, visitConditionalNot, visitDeconstructorPattern, 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, 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, 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, visitThrow, visitTypeCast, visitUnsignedRightShift

Constructor Detail

LockTransfer

public LockTransfer(LockAnalysis analysis,
                    LockChecker checker)

Create a transfer function for the Lock Checker.

Parameters:

analysis - the analysis this transfer function belongs to

checker - the type-checker this transfer function belongs to

Method Detail

makeLockHeld

protected void makeLockHeld(LockStore store,
                            Node node)

Sets a given Node to @LockHeld in the given store.

Parameters:

store - the store to update

node - the node that should be @LockHeld

makeLockPossiblyHeld

protected void makeLockPossiblyHeld(LockStore store,
                                    Node node)

Sets a given Node to @LockPossiblyHeld in the given store.

Parameters:

store - the store to update

node - the node that should be @LockPossiblyHeld

makeLockHeld

protected void makeLockHeld(TransferResult<CFValue,LockStore> result,
                            Node node)

Sets a given Node node to LockHeld in the given TransferResult.

makeLockPossiblyHeld

protected void makeLockPossiblyHeld(TransferResult<CFValue,LockStore> result,
                                    Node node)

Sets a given Node node to LockPossiblyHeld in the given TransferResult.

initialStore

public LockStore initialStore(UnderlyingAST underlyingAST,
                              java.util.List<LocalVariableNode> parameters)

Description copied from class: CFAbstractTransfer

The initial store maps method formal parameters to their currently most refined type.

Specified by:

initialStore in interface ForwardTransferFunction<CFValue,LockStore>

Overrides:

initialStore in class CFAbstractTransfer<CFValue,LockStore,LockTransfer>

Parameters:

underlyingAST - an abstract syntax tree

parameters - a list of local variable nodes representing formal parameters (if any)

Returns:

the initial store

visitSynchronized

public TransferResult<CFValue,LockStore> visitSynchronized(SynchronizedNode n,
                                                                 TransferInput<CFValue,LockStore> p)

Specified by:

visitSynchronized in interface NodeVisitor<TransferResult<CFValue,LockStore>,TransferInput<CFValue,LockStore>>

Overrides:

visitSynchronized in class AbstractNodeVisitor<TransferResult<CFValue,LockStore>,TransferInput<CFValue,LockStore>>