org.checkerframework.checker.nullness

Class NullnessStore

java.lang.Object

org.checkerframework.framework.flow.CFAbstractStore<V,S>

org.checkerframework.checker.initialization.InitializationStore<NullnessValue,NullnessStore>

org.checkerframework.checker.nullness.NullnessStore

All Implemented Interfaces:

Store<NullnessStore>, org.plumelib.util.UniqueId

public class NullnessStore
extends InitializationStore<NullnessValue,NullnessStore>
implements org.plumelib.util.UniqueId

Behaves like InitializationStore, but additionally tracks whether PolyNull is known to be Nullable.

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	isPolyNullNull True if, at this point, PolyNull is known to be Nullable.

Fields inherited from class org.checkerframework.checker.initialization.InitializationStore

initializedFields, invariantFields

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

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

Constructor Summary

Constructors

Constructor and Description
NullnessStore(CFAbstractAnalysis<NullnessValue,NullnessStore,?> analysis, boolean sequentialSemantics) Create a NullnessStore.
NullnessStore(NullnessStore s)

Method Summary

Modifier and Type	Method and Description
long	getUid() Returns the unique ID of this object.
protected String	internalVisualize(CFGVisualizer<NullnessValue,NullnessStore,?> viz) Adds a representation of the internal information of this Store to visualizer viz.
boolean	isPolyNullNull()
NullnessStore	leastUpperBound(NullnessStore other) Compute the least upper bound of two stores.
void	setPolyNullNull(boolean isPolyNullNull)
protected boolean	supersetOf(CFAbstractStore<NullnessValue,NullnessStore> o) Returns true iff this CFAbstractStore contains a superset of the map entries of the argument CFAbstractStore.

Methods inherited from class org.checkerframework.checker.initialization.InitializationStore

addInitializedField, addInitializedField, getAnalysis, getFieldValues, insertValue, isFieldInitialized, updateForMethodCall

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

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

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.plumelib.util.UniqueId

getClassAndUid

Field Detail

isPolyNullNull

protected boolean isPolyNullNull

True if, at this point, PolyNull is known to be Nullable.

Constructor Detail

NullnessStore

public NullnessStore(CFAbstractAnalysis<NullnessValue,NullnessStore,?> analysis,
                     boolean sequentialSemantics)

Create a NullnessStore.

Parameters:

analysis - the analysis class this store belongs to

sequentialSemantics - should the analysis use sequential Java semantics (i.e., assume that only one thread is running at all times)?

NullnessStore

public NullnessStore(NullnessStore s)

Method Detail

getUid

public long getUid()

Returns the unique ID of this object.

Specified by:

getUid in interface org.plumelib.util.UniqueId

Overrides:

getUid in class CFAbstractStore<NullnessValue,NullnessStore>

Returns:

the unique ID of this object.

leastUpperBound

public NullnessStore leastUpperBound(NullnessStore 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<NullnessStore>

Overrides:

leastUpperBound in class InitializationStore<NullnessValue,NullnessStore>

supersetOf

protected boolean supersetOf(CFAbstractStore<NullnessValue,NullnessStore> o)

Description copied from class: CFAbstractStore

Returns true iff this CFAbstractStore contains a superset of the map entries of the argument CFAbstractStore. Note that we test the entry keys and values by Java equality, not by any subtype relationship. This method is used primarily to simplify the equals predicate.

Overrides:

supersetOf in class InitializationStore<NullnessValue,NullnessStore>

internalVisualize

protected String internalVisualize(CFGVisualizer<NullnessValue,NullnessStore,?> viz)

Description copied from class: CFAbstractStore

Adds a representation of the internal information of this Store to visualizer viz.

Overrides:

internalVisualize in class InitializationStore<NullnessValue,NullnessStore>

Parameters:

viz - the visualizer

Returns:

a representation of the internal information of this Store

isPolyNullNull

public boolean isPolyNullNull()

setPolyNullNull

public void setPolyNullNull(boolean isPolyNullNull)