public class InitializationStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>> extends CFAbstractStore<V,S>
CFAbstractStore and additionally tracks which fields of the 'self'
reference have been initialized.InitializationTransferStore.FlowRule, Store.Kind| Modifier and Type | Field and Description |
|---|---|
protected Set<VariableElement> |
initializedFields
The set of fields that are initialized.
|
protected Map<FieldAccess,V> |
invariantFields
The set of fields that have the 'invariant' annotation, and their value.
|
analysis, arrayValues, classValues, fieldValues, localVariableValues, methodValues, sequentialSemantics, thisValue| Constructor and Description |
|---|
InitializationStore(CFAbstractAnalysis<V,S,?> analysis,
boolean sequentialSemantics) |
InitializationStore(S other)
A copy constructor.
|
| Modifier and Type | Method and Description |
|---|---|
void |
addInitializedField(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(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). |
CFAbstractAnalysis<V,S,?> |
getAnalysis()
Returns the analysis associated with this store.
|
void |
insertValue(JavaExpression je,
V value,
boolean permitNondeterministic)
|
protected String |
internalVisualize(CFGVisualizer<V,S,?> viz)
Adds a representation of the internal information of this Store to visualizer
viz. |
boolean |
isFieldInitialized(Element f)
Is the field identified by the element
f initialized? |
S |
leastUpperBound(S other)
Compute the least upper bound of two stores.
|
protected boolean |
supersetOf(CFAbstractStore<V,S> o)
Returns true iff this
CFAbstractStore contains a superset of the map entries of the
argument CFAbstractStore. |
void |
updateForMethodCall(MethodInvocationNode n,
AnnotatedTypeFactory atypeFactory,
V val)
Remove any information that might not be valid any more after a method call, and add
information guaranteed by the method.
|
canAlias, canInsertJavaExpression, clearValue, copy, equals, getFieldValue, getFieldValues, getUid, getValue, getValue, getValue, getValue, getValue, getValue, hashCode, initializeMethodParameter, initializeThisValue, insertOrRefine, insertOrRefine, insertOrRefinePermitNondeterministic, insertThisValue, insertValue, insertValue, insertValuePermitNondeterministic, insertValuePermitNondeterministic, isMonotonicUpdate, isSideEffectFree, removeConflicting, removeConflicting, removeConflicting, replaceValue, shouldInsert, toString, updateForArrayAssignment, updateForAssignment, updateForFieldAccessAssignment, updateForLocalVariableAssignment, visualize, widenedUpperBoundprotected final Set<VariableElement> initializedFields
protected final Map<FieldAccess,V extends CFAbstractValue<V>> invariantFields
public InitializationStore(CFAbstractAnalysis<V,S,?> analysis, boolean sequentialSemantics)
public InitializationStore(S other)
public void insertValue(JavaExpression je, V value, boolean permitNondeterministic)
CFAbstractStore.insertValue(JavaExpression, CFAbstractValue) and CFAbstractStore.insertValuePermitNondeterministic(org.checkerframework.dataflow.expression.JavaExpression, javax.lang.model.element.AnnotationMirror).
Every overriding implementation should start with
if (!shouldInsert) {
return;
}
If the receiver is a field, and has an invariant annotation, then it can be considered initialized.
insertValue in class CFAbstractStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>je - the expression to insert in the storevalue - the value of the expressionpermitNondeterministic - if false, does nothing if expr is nondeterministic; if
true, permits nondeterministic expressions to be placed in the storepublic void updateForMethodCall(MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, V val)
SideEffectFree or Pure), then no information needs to be removed.
a.f needs to be removed, except
if the method n cannot modify a.f (e.g., if a is a local
variable or this, and f is final).
val in the store.
Additionally, the InitializationStore keeps all field values for fields that have
the 'invariant' annotation.
updateForMethodCall in class CFAbstractStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>public void addInitializedField(FieldAccess field)
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).public void addInitializedField(VariableElement f)
f as initialized (the caller needs to ensure
that the field belongs to the current class, or is a static field).public boolean isFieldInitialized(Element f)
f initialized?protected boolean supersetOf(CFAbstractStore<V,S> o)
CFAbstractStoreCFAbstractStore 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.supersetOf in class CFAbstractStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>public S leastUpperBound(S other)
StoreImportant: This method must fulfill the following contract:
this.
other.
this, even if the signature is
more permissive.
leastUpperBound in interface Store<S extends InitializationStore<V,S>>leastUpperBound in class CFAbstractStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>protected String internalVisualize(CFGVisualizer<V,S,?> viz)
CFAbstractStoreviz.internalVisualize in class CFAbstractStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>viz - the visualizerStorepublic CFAbstractAnalysis<V,S,?> getAnalysis()