org.checkerframework.checker.lock

Class LockStore

java.lang.Object

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

org.checkerframework.checker.lock.LockStore

All Implemented Interfaces:

Store<LockStore>

public class LockStore
extends CFAbstractStore<CFValue,LockStore>

Nested Class Summary

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

Store.FlowRule, Store.Kind

Field Summary

Fields

Modifier and Type	Field and Description
protected boolean	inConstructorOrInitializer
protected AnnotationMirror	LOCKHELD

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

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

Constructor Summary

Constructors

Constructor and Description
LockStore(CFAbstractAnalysis<CFValue,LockStore,?> analysis, boolean sequentialSemantics)
LockStore(CFAbstractAnalysis<CFValue,LockStore,?> analysis, CFAbstractStore<CFValue,LockStore> other) Copy constructor.

Method Summary

Modifier and Type	Method and Description
@Nullable CFValue	getValue(FlowExpressions.Receiver expr)
void	insertExactValue(FlowExpressions.Receiver r, AnnotationMirror a)
void	insertExactValue(FlowExpressions.Receiver r, CFValue value)
protected void	internalDotOutput(StringBuilder result) Adds a DOT representation of the internal information of this store to result.
LockStore	leastUpperBound(LockStore other) Compute the least upper bound of two stores.
void	setInConstructorOrInitializer()

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

canAlias, canInsertReceiver, clearValue, copy, equals, escapeDoubleQuotes, getValue, getValue, getValue, getValue, getValue, hasDOToutput, initializeMethodParameter, initializeThisValue, insertThisValue, insertValue, insertValue, isSideEffectFree, removeConflicting, removeConflicting, removeConflicting, replaceValue, supersetOf, toDOToutput, toString, toStringEscapeDoubleQuotes, updateForArrayAssignment, updateForAssignment, updateForFieldAccessAssignment, updateForLocalVariableAssignment, updateForMethodCall

Methods inherited from class java.lang.Object

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

Field Detail

inConstructorOrInitializer

protected boolean inConstructorOrInitializer

LOCKHELD

protected final AnnotationMirror LOCKHELD

Constructor Detail

LockStore

public LockStore(CFAbstractAnalysis<CFValue,LockStore,?> analysis,
                 boolean sequentialSemantics)

LockStore

public LockStore(CFAbstractAnalysis<CFValue,LockStore,?> analysis,
                 CFAbstractStore<CFValue,LockStore> other)

Copy constructor.

Method Detail

leastUpperBound

public LockStore leastUpperBound(LockStore other)

Description copied from interface: Store

Compute the least upper bound of two stores.

Important: This method must fulfill the following contract:

• Does not change this.
• Does not change other.
• Returns a fresh object which is not aliased yet.
• Returns an object of the same (dynamic) type as this, even if the signature is more permissive.
• Is commutative.

Specified by:

leastUpperBound in interface Store<LockStore>

Overrides:

leastUpperBound in class CFAbstractStore<CFValue,LockStore>

insertExactValue

public void insertExactValue(FlowExpressions.Receiver r,
                             AnnotationMirror a)

insertExactValue

public void insertExactValue(FlowExpressions.Receiver r,
                             CFValue value)

setInConstructorOrInitializer

public void setInConstructorOrInitializer()

getValue

public @Nullable CFValue getValue(FlowExpressions.Receiver expr)

Overrides:

getValue in class CFAbstractStore<CFValue,LockStore>

Returns:

Current abstract value of a flow expression, or null if no information is available.

internalDotOutput

protected void internalDotOutput(StringBuilder result)

Adds a DOT representation of the internal information of this store to result.

Overrides:

internalDotOutput in class CFAbstractStore<CFValue,LockStore>