org.checkerframework.checker.initialization

Class InitializationStore<V extends org.checkerframework.framework.flow.CFAbstractValue<V>,S extends InitializationStore<V,S>>

java.lang.Object

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

org.checkerframework.checker.initialization.InitializationStore<V,S>

All Implemented Interfaces:

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

Direct Known Subclasses:

NullnessStore

public class InitializationStore<V extends org.checkerframework.framework.flow.CFAbstractValue<V>,S extends InitializationStore<V,S>>
extends org.checkerframework.framework.flow.CFAbstractStore<V,S>

A store that extends CFAbstractStore and additionally tracks which fields of the 'self' reference have been initialized.

See Also:

InitializationTransfer

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 java.util.Set<javax.lang.model.element.VariableElement>	initializedFields The set of fields that are initialized.
protected java.util.Map<org.checkerframework.dataflow.analysis.FlowExpressions.FieldAccess,V>	invariantFields The set of fields that have 'invariant' annotation.

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

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

Constructor Summary

Constructors

Constructor and Description
InitializationStore(org.checkerframework.framework.flow.CFAbstractAnalysis<V,S,?> analysis, boolean sequentialSemantics)
InitializationStore(S other) A copy constructor.

Method Summary

Modifier and Type	Method and Description
void	addInitializedField(org.checkerframework.dataflow.analysis.FlowExpressions.FieldAccess field) Mark the field identified by the element field as initialized (if it belongs to the current class, or is static (in which case there is no aliasing issue and we can just add all static fields).
void	addInitializedField(javax.lang.model.element.VariableElement f) Mark the field identified by the element f as initialized (the caller needs to ensure that the field belongs to the current class, or is a static field).
org.checkerframework.framework.flow.CFAbstractAnalysis<V,S,?>	getAnalysis()
java.util.Map<org.checkerframework.dataflow.analysis.FlowExpressions.FieldAccess,V>	getFieldValues()
void	insertValue(org.checkerframework.dataflow.analysis.FlowExpressions.Receiver r, V value)
protected void	internalVisualize(org.checkerframework.dataflow.cfg.CFGVisualizer<V,S,?> viz)
boolean	isFieldInitialized(javax.lang.model.element.Element f) Is the field identified by the element f initialized?
S	leastUpperBound(S other)
protected boolean	supersetOf(org.checkerframework.framework.flow.CFAbstractStore<V,S> o)
void	updateForMethodCall(org.checkerframework.dataflow.cfg.node.MethodInvocationNode n, org.checkerframework.framework.type.AnnotatedTypeFactory atypeFactory, V val)

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

canAlias, canInsertReceiver, clearValue, copy, equals, getValue, getValue, getValue, getValue, getValue, getValue, hashCode, initializeMethodParameter, initializeThisValue, 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

Field Detail

initializedFields

protected final java.util.Set<javax.lang.model.element.VariableElement> initializedFields

The set of fields that are initialized.

invariantFields

protected final java.util.Map<org.checkerframework.dataflow.analysis.FlowExpressions.FieldAccess,V extends org.checkerframework.framework.flow.CFAbstractValue<V>> invariantFields

The set of fields that have 'invariant' annotation.

Constructor Detail

InitializationStore

public InitializationStore(org.checkerframework.framework.flow.CFAbstractAnalysis<V,S,?> analysis,
                           boolean sequentialSemantics)

InitializationStore

public InitializationStore(S other)

A copy constructor.

Method Detail

insertValue

public void insertValue(org.checkerframework.dataflow.analysis.FlowExpressions.Receiver r,
                        V value)

If the receiver is a field, and has an invariant annotation, then it can be considered initialized.

Overrides:

insertValue in class org.checkerframework.framework.flow.CFAbstractStore<V extends org.checkerframework.framework.flow.CFAbstractValue<V>,S extends InitializationStore<V,S>>

updateForMethodCall

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

Additionally, the InitializationStore keeps all field values for fields that have the 'invariant' annotation.

Overrides:

updateForMethodCall in class org.checkerframework.framework.flow.CFAbstractStore<V extends org.checkerframework.framework.flow.CFAbstractValue<V>,S extends InitializationStore<V,S>>

addInitializedField

public void addInitializedField(org.checkerframework.dataflow.analysis.FlowExpressions.FieldAccess field)

Mark the field identified by the element field as initialized (if it belongs to the current class, or is static (in which case there is no aliasing issue and we can just add all static fields).

addInitializedField

public void addInitializedField(javax.lang.model.element.VariableElement f)

Mark the field identified by the element f as initialized (the caller needs to ensure that the field belongs to the current class, or is a static field).

isFieldInitialized

public boolean isFieldInitialized(javax.lang.model.element.Element f)

Is the field identified by the element f initialized?

supersetOf

protected boolean supersetOf(org.checkerframework.framework.flow.CFAbstractStore<V,S> o)

Overrides:

supersetOf in class org.checkerframework.framework.flow.CFAbstractStore<V extends org.checkerframework.framework.flow.CFAbstractValue<V>,S extends InitializationStore<V,S>>

leastUpperBound

public S leastUpperBound(S other)

Specified by:

leastUpperBound in interface org.checkerframework.dataflow.analysis.Store<S extends InitializationStore<V,S>>

Overrides:

leastUpperBound in class org.checkerframework.framework.flow.CFAbstractStore<V extends org.checkerframework.framework.flow.CFAbstractValue<V>,S extends InitializationStore<V,S>>

internalVisualize

protected void internalVisualize(org.checkerframework.dataflow.cfg.CFGVisualizer<V,S,?> viz)

Overrides:

internalVisualize in class org.checkerframework.framework.flow.CFAbstractStore<V extends org.checkerframework.framework.flow.CFAbstractValue<V>,S extends InitializationStore<V,S>>

getFieldValues

public java.util.Map<org.checkerframework.dataflow.analysis.FlowExpressions.FieldAccess,V> getFieldValues()

getAnalysis

public org.checkerframework.framework.flow.CFAbstractAnalysis<V,S,?> getAnalysis()