public class LockTransfer extends CFAbstractTransfer<CFValue,LockStore,LockTransfer>
analysis, sequentialSemantics
Constructor and Description |
---|
LockTransfer(LockAnalysis analysis,
LockChecker checker) |
Modifier and Type | Method and 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)
|
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)
|
TransferResult<CFValue,LockStore> |
visitSynchronized(SynchronizedNode n,
TransferInput<CFValue,LockStore> p) |
addInformationFromPreconditions, finishValue, finishValue, getTypeFactoryOfSubchecker, getValueFromFactory, getValueWithSameAnnotations, isNotFullyInitializedReceiver, moreSpecificValue, processCommonAssignment, processConditionalPostconditions, processPostconditions, setFixedInitialStore, splitAssignments, strengthenAnnotationOfEqualTo, usesSequentialSemantics, visitArrayAccess, visitAssignment, visitCase, visitClassName, visitConditionalNot, visitEqualTo, visitFieldAccess, visitLambdaResultExpression, visitLocalVariable, visitMethodInvocation, visitNarrowingConversion, visitNode, visitNotEqual, visitObjectCreation, visitReturn, visitStringConcatenateAssignment, visitStringConversion, visitTernaryExpression, visitThisLiteral, visitVariableDeclaration, visitWideningConversion
visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThisLiteral, visitInstanceOf, 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
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
visitArrayCreation, visitArrayType, visitAssertionError, visitBitwiseAnd, visitBitwiseComplement, visitBitwiseOr, visitBitwiseXor, visitBooleanLiteral, visitCharacterLiteral, visitConditionalAnd, visitConditionalOr, visitDoubleLiteral, visitExplicitThisLiteral, visitFloatingDivision, visitFloatingRemainder, visitFloatLiteral, visitGreaterThan, visitGreaterThanOrEqual, visitImplicitThisLiteral, visitInstanceOf, 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
public LockTransfer(LockAnalysis analysis, LockChecker checker)
protected void makeLockHeld(LockStore store, Node node)
Node
to @LockHeld in the given store
.protected void makeLockPossiblyHeld(LockStore store, Node node)
Node
to @LockPossiblyHeld in the given store
.protected void makeLockHeld(TransferResult<CFValue,LockStore> result, Node node)
protected void makeLockPossiblyHeld(TransferResult<CFValue,LockStore> result, Node node)
public LockStore initialStore(UnderlyingAST underlyingAST, java.util.List<LocalVariableNode> parameters)
CFAbstractTransfer
initialStore
in interface TransferFunction<CFValue,LockStore>
initialStore
in class CFAbstractTransfer<CFValue,LockStore,LockTransfer>
parameters
is only set if the underlying AST is a method.public TransferResult<CFValue,LockStore> visitSynchronized(SynchronizedNode n, TransferInput<CFValue,LockStore> p)
visitSynchronized
in interface NodeVisitor<TransferResult<CFValue,LockStore>,TransferInput<CFValue,LockStore>>
visitSynchronized
in class AbstractNodeVisitor<TransferResult<CFValue,LockStore>,TransferInput<CFValue,LockStore>>