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:

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

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

Field Summary

Fields

Modifier and Type	Field and Description
protected LockAnalysis	analysis Type-specific version of super.analysis.
protected LockChecker	checker
protected AnnotationMirror	LOCKHELD Annotations of the lock type system.
protected AnnotationMirror	LOCKPOSSIBLYHELD Annotations of the lock type system.

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

sequentialSemantics

Constructor Summary

Constructors

Constructor and Description
LockTransfer(LockAnalysis analysis, LockChecker checker)

Method Summary

Modifier and Type	Method and Description
LockStore	initialStore(UnderlyingAST underlyingAST, 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, finishValue, finishValue, getTypeFactoryOfSubchecker, getValueFromFactory, getValueWithSameAnnotations, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, setFixedInitialStore, splitAssignments, strengthenAnnotationOfEqualTo, visitArrayAccess, visitAssignment, visitCase, visitClassName, visitConditionalNot, visitEqualTo, visitFieldAccess, visitInstanceOf, visitLocalVariable, visitMethodInvocation, visitNarrowingConversion, visitNode, visitNotEqual, 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, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLessThan, visitLessThanOrEqual, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitNumericalSubtraction, visitObjectCreation, visitPackageName, visitParameterizedType, visitPrimitiveType, visitReturn, 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, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThisLiteral, visitIntegerDivision, visitIntegerLiteral, visitIntegerRemainder, visitLeftShift, visitLessThan, visitLessThanOrEqual, visitLongLiteral, visitMarker, visitMemberReference, visitMethodAccess, visitNullChk, visitNullLiteral, visitNumericalAddition, visitNumericalMinus, visitNumericalMultiplication, visitNumericalPlus, visitNumericalSubtraction, visitObjectCreation, visitPackageName, visitParameterizedType, visitPrimitiveType, visitReturn, visitShortLiteral, visitSignedRightShift, visitStringConcatenate, visitStringLiteral, visitSuper, visitThrow, visitTypeCast, visitUnsignedRightShift

Field Detail

analysis

protected LockAnalysis analysis

Type-specific version of super.analysis.

checker

protected LockChecker checker

LOCKHELD

protected final AnnotationMirror LOCKHELD

Annotations of the lock type system.

LOCKPOSSIBLYHELD

protected final AnnotationMirror LOCKPOSSIBLYHELD

Annotations of the lock type system.

Constructor Detail

LockTransfer

public LockTransfer(LockAnalysis analysis,
                    LockChecker checker)

Method Detail

makeLockHeld

protected void makeLockHeld(LockStore store,
                            Node node)

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

makeLockPossiblyHeld

protected void makeLockPossiblyHeld(LockStore store,
                                    Node node)

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

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,
                              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 TransferFunction<CFValue,LockStore>

Overrides:

initialStore in class CFAbstractTransfer<CFValue,LockStore,LockTransfer>

Returns:

The initial store to be used by the org.checkerframework.dataflow analysis. parameters is only set if the underlying AST is a method.

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