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.InitializationTransfer
Store.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)
Creates a new InitializationStore.
|
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, computeNewValueAndInsert, 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, widenedUpperBound
protected final Set<VariableElement> initializedFields
protected final Map<FieldAccess,V extends CFAbstractValue<V>> invariantFields
public InitializationStore(CFAbstractAnalysis<V,S,?> analysis, boolean sequentialSemantics)
analysis
- the analysis class this store belongs tosequentialSemantics
- should the analysis use sequential Java semantics?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).field
- a field that is initializedpublic 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).f
- a field that is initializedpublic boolean isFieldInitialized(Element f)
f
initialized?protected boolean supersetOf(CFAbstractStore<V,S> o)
CFAbstractStore
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.supersetOf
in class CFAbstractStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>
public S leastUpperBound(S other)
Store
Important: 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)
CFAbstractStore
viz
.internalVisualize
in class CFAbstractStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>
viz
- the visualizerStore
public CFAbstractAnalysis<V,S,?> getAnalysis()