org.checkerframework.checker.lock

Class LockStore

java.lang.Object

org.checkerframework.framework.flow.CFAbstractStore<org.checkerframework.framework.flow.CFValue,LockStore>

org.checkerframework.checker.lock.LockStore

All Implemented Interfaces:

org.checkerframework.dataflow.analysis.Store<LockStore>

public class LockStore
extends org.checkerframework.framework.flow.CFAbstractStore<org.checkerframework.framework.flow.CFValue,LockStore>

Nested Class Summary

Nested classes/interfaces inherited from interface org.checkerframework.dataflow.analysis.Store

org.checkerframework.dataflow.analysis.Store.FlowRule, org.checkerframework.dataflow.analysis.Store.Kind

Field Summary

Fields

Modifier and Type	Field and Description
protected boolean	inConstructorOrInitializer If true, indicates that the store refers to a point in the code inside a constructor or initializer.

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

analysis, arrayValues, classValues, fieldValues, localVariableValues, methodValues, sequentialSemantics, thisValue

Constructor Summary

Constructors

Constructor and Description
LockStore(LockAnalysis analysis, boolean sequentialSemantics)
LockStore(LockAnalysis analysis, org.checkerframework.framework.flow.CFAbstractStore<org.checkerframework.framework.flow.CFValue,LockStore> other) Copy constructor.

Method Summary

Modifier and Type	Method and Description
@Nullable org.checkerframework.framework.flow.CFValue	getValue(org.checkerframework.dataflow.analysis.FlowExpressions.Receiver expr)
void	insertLockPossiblyHeld(org.checkerframework.dataflow.analysis.FlowExpressions.Receiver r)
void	insertValue(org.checkerframework.dataflow.analysis.FlowExpressions.Receiver r, @Nullable org.checkerframework.framework.flow.CFValue value)
protected void	internalVisualize(org.checkerframework.dataflow.cfg.CFGVisualizer<org.checkerframework.framework.flow.CFValue,LockStore,?> viz)
protected boolean	isSideEffectFree(org.checkerframework.framework.type.AnnotatedTypeFactory atypeFactory, javax.lang.model.element.ExecutableElement method)
LockStore	leastUpperBound(LockStore other)
void	setInConstructorOrInitializer()
void	updateForMethodCall(org.checkerframework.dataflow.cfg.node.MethodInvocationNode n, org.checkerframework.framework.type.AnnotatedTypeFactory atypeFactory, org.checkerframework.framework.flow.CFValue val)

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

canAlias, canInsertReceiver, clearValue, copy, equals, getValue, getValue, getValue, getValue, getValue, hashCode, initializeMethodParameter, initializeThisValue, insertThisValue, insertValue, isMonotonicUpdate, removeConflicting, removeConflicting, removeConflicting, replaceValue, supersetOf, toString, updateForArrayAssignment, updateForAssignment, updateForFieldAccessAssignment, updateForLocalVariableAssignment, visualize, widenedUpperBound

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

inConstructorOrInitializer

protected boolean inConstructorOrInitializer

If true, indicates that the store refers to a point in the code inside a constructor or initializer. This is useful because constructors and initializers are special with regard to the set of locks that is considered to be held. For example, 'this' is considered to be held inside a constructor.

Constructor Detail

LockStore

public LockStore(LockAnalysis analysis,
                 boolean sequentialSemantics)

LockStore

public LockStore(LockAnalysis analysis,
                 org.checkerframework.framework.flow.CFAbstractStore<org.checkerframework.framework.flow.CFValue,LockStore> other)

Copy constructor.

Method Detail

leastUpperBound

public LockStore leastUpperBound(LockStore other)

Specified by:

leastUpperBound in interface org.checkerframework.dataflow.analysis.Store<LockStore>

Overrides:

leastUpperBound in class org.checkerframework.framework.flow.CFAbstractStore<org.checkerframework.framework.flow.CFValue,LockStore>

insertLockPossiblyHeld

public void insertLockPossiblyHeld(org.checkerframework.dataflow.analysis.FlowExpressions.Receiver r)

setInConstructorOrInitializer

public void setInConstructorOrInitializer()

getValue

public @Nullable org.checkerframework.framework.flow.CFValue getValue(org.checkerframework.dataflow.analysis.FlowExpressions.Receiver expr)

Overrides:

getValue in class org.checkerframework.framework.flow.CFAbstractStore<org.checkerframework.framework.flow.CFValue,LockStore>

internalVisualize

protected void internalVisualize(org.checkerframework.dataflow.cfg.CFGVisualizer<org.checkerframework.framework.flow.CFValue,LockStore,?> viz)

Overrides:

internalVisualize in class org.checkerframework.framework.flow.CFAbstractStore<org.checkerframework.framework.flow.CFValue,LockStore>

isSideEffectFree

protected boolean isSideEffectFree(org.checkerframework.framework.type.AnnotatedTypeFactory atypeFactory,
                                   javax.lang.model.element.ExecutableElement method)

Overrides:

isSideEffectFree in class org.checkerframework.framework.flow.CFAbstractStore<org.checkerframework.framework.flow.CFValue,LockStore>

updateForMethodCall

public void updateForMethodCall(org.checkerframework.dataflow.cfg.node.MethodInvocationNode n,
                                org.checkerframework.framework.type.AnnotatedTypeFactory atypeFactory,
                                org.checkerframework.framework.flow.CFValue val)

Overrides:

updateForMethodCall in class org.checkerframework.framework.flow.CFAbstractStore<org.checkerframework.framework.flow.CFValue,LockStore>

insertValue

public void insertValue(org.checkerframework.dataflow.analysis.FlowExpressions.Receiver r,
                        @Nullable org.checkerframework.framework.flow.CFValue value)

Overrides:

insertValue in class org.checkerframework.framework.flow.CFAbstractStore<org.checkerframework.framework.flow.CFValue,LockStore>