CFAbstractStore (checker-framework 3.11.0 API)

java.lang.Object
- org.checkerframework.framework.flow.CFAbstractStore<V,S>

All Implemented Interfaces:

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

Direct Known Subclasses:

CFStore, InitializationStore, KeyForStore, LockStore
```
public abstract class CFAbstractStore<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>
extends Object
implements Store<S>, org.plumelib.util.UniqueId
```
A store for the Checker Framework analysis. It tracks the annotations of memory locations such as local variables and fields.
When adding a new field to track values for a code construct (similar to localVariableValues and thisValue), it is important to review all constructors and methods in this class for locations where the new field must be handled (such as the copy constructor and clearValue), as well as all constructors/methods in subclasses of {code CFAbstractStore}. Note that this includes not only overridden methods in the subclasses, but new methods in the subclasses as well. Also check if BaseTypeVisitor#getJavaExpressionContextFromNode(Node) needs to be updated. Failing to do so may result in silent failures that are time consuming to debug.

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 CFAbstractAnalysis<V,S,?>`	`analysis` The analysis class this store belongs to.
`protected Map<ArrayAccess,V>`	`arrayValues` Information collected about arrays, using the internal representation `ArrayAccess`.
`protected Map<ClassName,V>`	`classValues` Information collected about classname.class values, using the internal representation `ClassName`.
`protected Map<FieldAccess,V>`	`fieldValues` Information collected about fields, using the internal representation `FieldAccess`.
`protected Map<LocalVariable,V>`	`localVariableValues` Information collected about local variables (including method arguments).
`protected Map<MethodCall,V>`	`methodValues` Information collected about method calls, using the internal representation `MethodCall`.
`protected boolean`	`sequentialSemantics` Should the analysis use sequential Java semantics (i.e., assume that only one thread is running at all times)?
`protected V`	`thisValue` Information collected about the current object.

Constructor Summary

Constructors
Modifier	Constructor and Description
`protected`	`CFAbstractStore(CFAbstractAnalysis<V,S,?> analysis, boolean sequentialSemantics)`
`protected`	`CFAbstractStore(CFAbstractStore<V,S> other)` Copy constructor.

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`boolean`	`canAlias(JavaExpression a, JavaExpression b)` Can the objects `a` and `b` be aliases? Returns a conservative answer (i.e., returns `true` if not enough information is available to determine aliasing).
`static boolean`	`canInsertJavaExpression(JavaExpression expr)` Returns true if `expr` can be stored in this store.
`void`	`clearValue(JavaExpression expr)` Remove any knowledge about the expression `expr` (correctly deciding where to remove the information depending on the type of the expression `expr`).
`S`	`copy()` Returns an exact copy of this store.
`boolean`	`equals(@Nullable Object o)`
`V`	`getFieldValue(FieldAccess fieldAccess)` Returns the current abstract value of a field access, or `null` if no information is available.
`Map<FieldAccess,V>`	`getFieldValues()` Returns information about fields.
`long`	`getUid()`
`V`	`getValue(ArrayAccessNode n)` Returns the current abstract value of a field access, or `null` if no information is available.
`V`	`getValue(FieldAccessNode n)` Returns the current abstract value of a field access, or `null` if no information is available.
`V`	`getValue(JavaExpression expr)` Returns the current abstract value of a Java expression, or `null` if no information is available.
`V`	`getValue(LocalVariableNode n)` Returns the current abstract value of a local variable, or `null` if no information is available.
`V`	`getValue(MethodInvocationNode n)` Returns the current abstract value of a method call, or `null` if no information is available.
`V`	`getValue(ThisNode n)` Returns the current abstract value of the current object, or `null` if no information is available.
`int`	`hashCode()`
`void`	`initializeMethodParameter(LocalVariableNode p, V value)` Set the abstract value of a method parameter (only adds the information to the store, does not remove any other knowledge).
`void`	`initializeThisValue(AnnotationMirror a, TypeMirror underlyingType)` Set the value of the current object.
`void`	`insertOrRefine(JavaExpression expr, AnnotationMirror newAnno)` Add the annotation `newAnno` for the expression `expr` (correctly deciding where to store the information depending on the type of the expression `expr`).
`protected void`	`insertOrRefine(JavaExpression expr, AnnotationMirror newAnno, boolean permitNondeterministic)` Helper function for `insertOrRefine(JavaExpression, AnnotationMirror)` and `insertOrRefinePermitNondeterministic(org.checkerframework.dataflow.expression.JavaExpression, javax.lang.model.element.AnnotationMirror)`.
`void`	`insertOrRefinePermitNondeterministic(JavaExpression expr, AnnotationMirror newAnno)` Like `insertOrRefine(JavaExpression, AnnotationMirror)`, but permits nondeterministic expressions to be inserted.
`void`	`insertThisValue(AnnotationMirror a, TypeMirror underlyingType)`
`void`	`insertValue(JavaExpression expr, AnnotationMirror a)` Add the annotation `a` for the expression `expr` (correctly deciding where to store the information depending on the type of the expression `expr`).
`void`	`insertValue(JavaExpression expr, V value)` Add the abstract value `value` for the expression `expr` (correctly deciding where to store the information depending on the type of the expression `expr`).
`protected void`	`insertValue(JavaExpression expr, V value, boolean permitNondeterministic)` Helper method for `insertValue(JavaExpression, CFAbstractValue)` and `insertValuePermitNondeterministic(org.checkerframework.dataflow.expression.JavaExpression, javax.lang.model.element.AnnotationMirror)`.
`void`	`insertValuePermitNondeterministic(JavaExpression expr, AnnotationMirror a)` Like `insertValue(JavaExpression, AnnotationMirror)`, but permits nondeterministic expressions to be stored.
`void`	`insertValuePermitNondeterministic(JavaExpression expr, V value)` Like `insertValue(JavaExpression, CFAbstractValue)`, but updates the store even if `expr` is nondeterministic.
`protected String`	`internalVisualize(CFGVisualizer<V,S,?> viz)` Adds a representation of the internal information of this Store to visualizer `viz`.
`protected boolean`	`isMonotonicUpdate(FieldAccess fieldAcc, V value)` Return true if fieldAcc is an update of a monotonic qualifier to its target qualifier.
`protected boolean`	`isSideEffectFree(AnnotatedTypeFactory atypeFactory, ExecutableElement method)` Indicates whether the given method is side-effect-free as far as the current store is concerned.
`S`	`leastUpperBound(S other)` Compute the least upper bound of two stores.
`protected void`	`removeConflicting(ArrayAccess arrayAccess, V val)` Remove any information in the store that might not be true any more after `arrayAccess` has been assigned a new value (with the abstract value `val`).
`protected void`	`removeConflicting(FieldAccess fieldAccess, V val)` Remove any information in this store that might not be true any more after `fieldAccess` has been assigned a new value (with the abstract value `val`).
`protected void`	`removeConflicting(LocalVariable var)` Remove any information in this store that might not be true any more after `localVar` has been assigned a new value.
`void`	`replaceValue(JavaExpression expr, V value)` Completely replaces the abstract value `value` for the expression `expr` (correctly deciding where to store the information depending on the type of the expression `expr`).
`protected boolean`	`shouldInsert(JavaExpression expr, V value, boolean permitNondeterministic)` Returns true if the given (expression, value) pair can be inserted in the store, namely if the value is non-null and the expression does not contain unknown or a nondeterministic expression.
`protected boolean`	`supersetOf(CFAbstractStore<V,S> other)` Returns true iff this `CFAbstractStore` contains a superset of the map entries of the argument `CFAbstractStore`.
`String`	`toString()`
`protected void`	`updateForArrayAssignment(ArrayAccess arrayAccess, V val)` Update the information in the store by considering an assignment with target `n`, where the target is an array access.
`void`	`updateForAssignment(Node n, V val)` Update the information in the store by considering an assignment with target `n`.
`protected void`	`updateForFieldAccessAssignment(FieldAccess fieldAccess, V val)` Update the information in the store by considering a field assignment with target `n`, where the right hand side has the abstract value `val`.
`protected void`	`updateForLocalVariableAssignment(LocalVariable receiver, V val)` Set the abstract value of a local variable in the store.
`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.
`String`	`visualize(CFGVisualizer<?,S,?> viz)` Delegate visualization responsibility to a visualizer.
`S`	`widenedUpperBound(S previous)` Compute an upper bound of two stores that is wider than the least upper bound of the two stores.

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
  - analysis
```
protected final CFAbstractAnalysis<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,?> analysis
```
    The analysis class this store belongs to.
  - localVariableValues
```
protected final Map<LocalVariable,V extends CFAbstractValue<V>> localVariableValues
```
    Information collected about local variables (including method arguments).
  - thisValue
```
protected V extends CFAbstractValue<V> thisValue
```
    Information collected about the current object.
  - fieldValues
```
protected Map<FieldAccess,V extends CFAbstractValue<V>> fieldValues
```
    Information collected about fields, using the internal representation FieldAccess.
  - arrayValues
```
protected Map<ArrayAccess,V extends CFAbstractValue<V>> arrayValues
```
    Information collected about arrays, using the internal representation ArrayAccess.
  - methodValues
```
protected Map<MethodCall,V extends CFAbstractValue<V>> methodValues
```
    Information collected about method calls, using the internal representation MethodCall.
  - classValues
```
protected Map<ClassName,V extends CFAbstractValue<V>> classValues
```
    Information collected about classname.class values, using the internal representation ClassName.
  - sequentialSemantics
```
protected final boolean sequentialSemantics
```
    Should the analysis use sequential Java semantics (i.e., assume that only one thread is running at all times)?
- Constructor Detail
  - CFAbstractStore
```
protected CFAbstractStore(CFAbstractAnalysis<V,S,?> analysis,
                          boolean sequentialSemantics)
```
  - CFAbstractStore
```
protected CFAbstractStore(CFAbstractStore<V,S> other)
```
    Copy constructor.
- Method Detail
  - getFieldValues
```
public Map<FieldAccess,V> getFieldValues()
```
    Returns information about fields. Clients should not side-effect the returned value, which is aliased to internal state.
    
    Returns:
    
    information about fields
  - getUid
```
public long getUid()
```
    Specified by:
    
    getUid in interface org.plumelib.util.UniqueId
  - initializeMethodParameter
```
public void initializeMethodParameter(LocalVariableNode p,
                                      V value)
```
    Set the abstract value of a method parameter (only adds the information to the store, does not remove any other knowledge). Any previous information is erased; this method should only be used to initialize the abstract value.
  - initializeThisValue
```
public void initializeThisValue(AnnotationMirror a,
                                TypeMirror underlyingType)
```
    Set the value of the current object. Any previous information is erased; this method should only be used to initialize the value.
  - isSideEffectFree
```
protected boolean isSideEffectFree(AnnotatedTypeFactory atypeFactory,
                                   ExecutableElement method)
```
    Indicates whether the given method is side-effect-free as far as the current store is concerned. In some cases, a store for a checker allows for other mechanisms to specify whether a method is side-effect-free. For example, unannotated methods may be considered side-effect-free by default.
    
    Parameters:
    
    atypeFactory - the type factory used to retrieve annotations on the method element
    
    method - the method element
    
    Returns:
    
    whether the method is side-effect-free
  - updateForMethodCall
```
public 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.
    1. If the method is side-effect-free (as indicated by SideEffectFree or Pure), then no information needs to be removed.
    2. Otherwise, all information about field accesses 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).
    3. Furthermore, if the field has a monotonic annotation, then its information can also be kept.
    Furthermore, if the method is deterministic, we store its result val in the store.
  - insertValue
```
public void insertValue(JavaExpression expr,
                        AnnotationMirror a)
```
    Add the annotation a for the expression expr (correctly deciding where to store the information depending on the type of the expression expr).
    This method does not take care of removing other information that might be influenced by changes to certain parts of the state.
    If there is already a value v present for expr, then the stronger of the new and old value are taken (according to the lattice). Note that this happens per hierarchy, and if the store already contains information about a hierarchy other than as hierarchy, that information is preserved.
    If expr is nondeterministic, this method does not insert value into the store.
    
    Parameters:
    
    expr - an expression
    
    a - an annotation for the expression
  - insertValuePermitNondeterministic
```
public void insertValuePermitNondeterministic(JavaExpression expr,
                                              AnnotationMirror a)
```
    Like insertValue(JavaExpression, AnnotationMirror), but permits nondeterministic expressions to be stored.
    For an explanation of when to permit nondeterministic expressions, see insertValuePermitNondeterministic(JavaExpression, CFAbstractValue).
    
    Parameters:
    
    expr - an expression
    
    a - an annotation for the expression
  - insertOrRefine
```
public final void insertOrRefine(JavaExpression expr,
                                 AnnotationMirror newAnno)
```
    Add the annotation newAnno for the expression expr (correctly deciding where to store the information depending on the type of the expression expr).
    This method does not take care of removing other information that might be influenced by changes to certain parts of the state.
    If there is already a value v present for expr, then the greatest lower bound of the new and old value is inserted into the store unless it's bottom. Some checkers do not override QualifierHierarchy.greatestLowerBound(AnnotationMirror, AnnotationMirror) and the default implementation will return the bottom qualifier incorrectly. So this method conservatively does not insert the glb if it is bottom.
    Note that this happens per hierarchy, and if the store already contains information about a hierarchy other than newAnno's hierarchy, that information is preserved.
    If expr is nondeterministic, this method does not insert value into the store.
    
    Parameters:
    
    expr - an expression
    
    newAnno - the expression's annotation
  - insertOrRefinePermitNondeterministic
```
public final void insertOrRefinePermitNondeterministic(JavaExpression expr,
                                                       AnnotationMirror newAnno)
```
    Like insertOrRefine(JavaExpression, AnnotationMirror), but permits nondeterministic expressions to be inserted.
    For an explanation of when to permit nondeterministic expressions, see insertValuePermitNondeterministic(JavaExpression, CFAbstractValue).
    
    Parameters:
    
    expr - an expression
    
    newAnno - the expression's annotation
  - insertOrRefine
```
protected void insertOrRefine(JavaExpression expr,
                              AnnotationMirror newAnno,
                              boolean permitNondeterministic)
```
    Helper function for insertOrRefine(JavaExpression, AnnotationMirror) and insertOrRefinePermitNondeterministic(org.checkerframework.dataflow.expression.JavaExpression, javax.lang.model.element.AnnotationMirror).
    
    Parameters:
    
    expr - an expression
    
    newAnno - the expression's annotation
    
    permitNondeterministic - whether nondeterministic expressions may be inserted into the store
  - canInsertJavaExpression
```
public static boolean canInsertJavaExpression(JavaExpression expr)
```
    Returns true if expr can be stored in this store.
  - insertValue
```
public final void insertValue(JavaExpression expr,
                              V value)
```
    Add the abstract value value for the expression expr (correctly deciding where to store the information depending on the type of the expression expr).
    This method does not take care of removing other information that might be influenced by changes to certain parts of the state.
    If there is already a value v present for expr, then the stronger of the new and old value are taken (according to the lattice). Note that this happens per hierarchy, and if the store already contains information about a hierarchy for which value does not contain information, then that information is preserved.
    If expr is nondeterministic, this method does not insert value into the store.
    
    Parameters:
    
    expr - the expression to insert in the store
    
    value - the value of the expression
  - insertValuePermitNondeterministic
```
public final void insertValuePermitNondeterministic(JavaExpression expr,
                                                    V value)
```
    Like insertValue(JavaExpression, CFAbstractValue), but updates the store even if expr is nondeterministic.
    Usually, nondeterministic JavaExpressions should not be stored in a Store. For example, in the body of if (nondet() == 3) {...}, the store should not record that the value of nondet() is 3, because it might not be 3 the next time nondet() is executed.
    However, contracts can mention a nondeterministic JavaExpression. For example, a contract might have a postcondition thatnondet() is odd. This means that the next call tonondet() will return odd. Such a postcondition may be evicted from the store by calling a side-effecting method.
    
    Parameters:
    
    expr - the expression to insert in the store
    
    value - the value of the expression
  - shouldInsert
```
protected boolean shouldInsert(JavaExpression expr,
                               V value,
                               boolean permitNondeterministic)
```
    Returns true if the given (expression, value) pair can be inserted in the store, namely if the value is non-null and the expression does not contain unknown or a nondeterministic expression.
    This method returning true does not guarantee that the value will be inserted; the implementation of insertValue( JavaExpression, CFAbstractValue, boolean) might still not insert it.
    
    Parameters:
    
    expr - the expression to insert in the store
    
    value - the value of the expression
    
    permitNondeterministic - if false, returns false if expr is nondeterministic; if true, permits nondeterministic expressions to be placed in the store
    
    Returns:
    
    true if the given (expression, value) pair can be inserted in the store
  - insertValue
```
protected void insertValue(JavaExpression expr,
                           V value,
                           boolean permitNondeterministic)
```
    Helper method for insertValue(JavaExpression, CFAbstractValue) and insertValuePermitNondeterministic(org.checkerframework.dataflow.expression.JavaExpression, javax.lang.model.element.AnnotationMirror).
    Every overriding implementation should start with
```
 if (!shouldInsert) {
   return;
 }
 
```
    Parameters:
    
    expr - the expression to insert in the store
    
    value - the value of the expression
    
    permitNondeterministic - if false, does nothing if expr is nondeterministic; if true, permits nondeterministic expressions to be placed in the store
  - isMonotonicUpdate
```
protected boolean isMonotonicUpdate(FieldAccess fieldAcc,
                                    V value)
```
    Return true if fieldAcc is an update of a monotonic qualifier to its target qualifier. (e.g. @MonotonicNonNull to @NonNull). Always returns false if sequentialSemantics is true.
    
    Returns:
    
    true if fieldAcc is an update of a monotonic qualifier to its target qualifier (e.g. @MonotonicNonNull to @NonNull)
  - insertThisValue
```
public void insertThisValue(AnnotationMirror a,
                            TypeMirror underlyingType)
```
  - replaceValue
```
public void replaceValue(JavaExpression expr,
                         V value)
```
    Completely replaces the abstract value value for the expression expr (correctly deciding where to store the information depending on the type of the expression expr). Any previous information is discarded.
    This method does not take care of removing other information that might be influenced by changes to certain parts of the state.
  - clearValue
```
public void clearValue(JavaExpression expr)
```
    Remove any knowledge about the expression expr (correctly deciding where to remove the information depending on the type of the expression expr).
  - getValue
```
public V getValue(JavaExpression expr)
```
    Returns the current abstract value of a Java expression, or null if no information is available.
    
    Returns:
    
    the current abstract value of a Java expression, or null if no information is available
  - getValue
```
public V getValue(FieldAccessNode n)
```
    Returns the current abstract value of a field access, or null if no information is available.
    
    Parameters:
    
    n - the node whose abstract value to return
    
    Returns:
    
    the current abstract value of a field access, or null if no information is available
  - getFieldValue
```
public V getFieldValue(FieldAccess fieldAccess)
```
    Returns the current abstract value of a field access, or null if no information is available.
    
    Parameters:
    
    fieldAccess - the field access to look up in this store
    
    Returns:
    
    current abstract value of a field access, or null if no information is available
  - getValue
```
public V getValue(MethodInvocationNode n)
```
    Returns the current abstract value of a method call, or null if no information is available.
    
    Parameters:
    
    n - a method call
    
    Returns:
    
    the current abstract value of a method call, or null if no information is available
  - getValue
```
public V getValue(ArrayAccessNode n)
```
    Returns the current abstract value of a field access, or null if no information is available.
    
    Parameters:
    
    n - the node whose abstract value to return
    
    Returns:
    
    the current abstract value of a field access, or null if no information is available
  - updateForAssignment
```
public void updateForAssignment(Node n,
                                V val)
```
    Update the information in the store by considering an assignment with target n.
    
    Parameters:
    
    n - the left-hand side of an assignment
    
    val - the right-hand value of an assignment
  - updateForFieldAccessAssignment
```
protected void updateForFieldAccessAssignment(FieldAccess fieldAccess,
                                              V val)
```
    Update the information in the store by considering a field assignment with target n, where the right hand side has the abstract value val.
    
    Parameters:
    
    val - the abstract value of the value assigned to n (or null if the abstract value is not known).
  - updateForArrayAssignment
```
protected void updateForArrayAssignment(ArrayAccess arrayAccess,
                                        V val)
```
    Update the information in the store by considering an assignment with target n, where the target is an array access.
    See removeConflicting(ArrayAccess,CFAbstractValue), as it is called first by this method.
  - updateForLocalVariableAssignment
```
protected void updateForLocalVariableAssignment(LocalVariable receiver,
                                                V val)
```
    Set the abstract value of a local variable in the store. Overwrites any value that might have been available previously.
    
    Parameters:
    
    val - the abstract value of the value assigned to n (or null if the abstract value is not known).
  - removeConflicting
```
protected void removeConflicting(FieldAccess fieldAccess,
                                 V val)
```
    Remove any information in this store that might not be true any more after fieldAccess has been assigned a new value (with the abstract value val). This includes the following steps (assume that fieldAccess is of the form a.f for some a.
    1. Update the abstract value of other field accesses b.g where the field is equal (that is, f=g), and the receiver b might alias the receiver of fieldAccess, a. This update will raise the abstract value for such field accesses to at least val (or the old value, if that was less precise). However, this is only necessary if the field g is not final.
    2. Remove any abstract values for field accesses b.g where fieldAccess might alias any expression in the receiver b.
    3. Remove any information about method calls.
    4. Remove any abstract values an array access b[i] where fieldAccess might alias any expression in the receiver a or index i.
    Parameters:
    
    val - the abstract value of the value assigned to n (or null if the abstract value is not known).
  - removeConflicting
```
protected void removeConflicting(ArrayAccess arrayAccess,
                                 V val)
```
    Remove any information in the store that might not be true any more after arrayAccess has been assigned a new value (with the abstract value val). This includes the following steps (assume that arrayAccess is of the form a[i] for some a.
    1. Remove any abstract value for other array access b[j] where a and b can be aliases, or where either b or j contains a modifiable alias of a[i].
    2. Remove any abstract values for field accesses b.g where a[i] might alias any expression in the receiver b and there is an array expression somewhere in the receiver.
    3. Remove any information about method calls.
    Parameters:
    
    val - the abstract value of the value assigned to n (or null if the abstract value is not known).
  - removeConflicting
```
protected void removeConflicting(LocalVariable var)
```
    Remove any information in this store that might not be true any more after localVar has been assigned a new value. This includes the following steps:
    1. Remove any abstract values for field accesses b.g where localVar might alias any expression in the receiver b.
    2. Remove any abstract values for array accesses a[i] where localVar might alias the receiver a.
    3. Remove any information about method calls where the receiver or any of the parameters contains localVar.
  - canAlias
```
public boolean canAlias(JavaExpression a,
                        JavaExpression b)
```
    Can the objects a and b be aliases? Returns a conservative answer (i.e., returns true if not enough information is available to determine aliasing).
    
    Specified by:
    
    canAlias in interface Store<S extends CFAbstractStore<V,S>>
  - getValue
```
public V getValue(LocalVariableNode n)
```
    Returns the current abstract value of a local variable, or null if no information is available.
    
    Returns:
    
    the current abstract value of a local variable, or null if no information is available
  - getValue
```
public V getValue(ThisNode n)
```
    Returns the current abstract value of the current object, or null if no information is available.
    
    Parameters:
    
    n - a reference to "this"
    
    Returns:
    
    the current abstract value of the current object, or null if no information is available
  - copy
```
public S copy()
```
    Description copied from interface: Store
    
    Returns an exact copy of this store.
    
    Specified by:
    
    copy in interface Store<S extends CFAbstractStore<V,S>>
    
    Returns:
    
    an exact copy of this store
  - leastUpperBound
```
public S leastUpperBound(S 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<S extends CFAbstractStore<V,S>>
  - widenedUpperBound
```
public S widenedUpperBound(S previous)
```
    Description copied from interface: Store
    Compute an upper bound of two stores that is wider than the least upper bound of the two stores. Used to jump to a higher abstraction to allow faster termination of the fixed point computations in Analysis. previous must be the previous store.
    A particular analysis might not require widening and should implement this method by calling leastUpperBound.
    Important: This method must fulfill the following contract:
    - Does not change this.
    - Does not change previous.
    - 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:
    
    widenedUpperBound in interface Store<S extends CFAbstractStore<V,S>>
    
    Parameters:
    
    previous - must be the previous store
  - supersetOf
```
protected boolean supersetOf(CFAbstractStore<V,S> other)
```
    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.
  - equals
```
public boolean equals(@Nullable Object o)
```
    Overrides:
    
    equals in class Object
  - hashCode
```
public int hashCode()
```
    Overrides:
    
    hashCode in class Object
  - toString
```
@SideEffectFree
public String toString()
```
    Overrides:
    
    toString in class Object
  - visualize
```
public String visualize(CFGVisualizer<?,S,?> viz)
```
    Description copied from interface: Store
    
    Delegate visualization responsibility to a visualizer.
    
    Specified by:
    
    visualize in interface Store<S extends CFAbstractStore<V,S>>
    
    Parameters:
    
    viz - the visualizer to visualize this store
    
    Returns:
    
    the String representation of this store
  - internalVisualize
```
protected String internalVisualize(CFGVisualizer<V,S,?> viz)
```
    Adds a representation of the internal information of this Store to visualizer viz.
    
    Parameters:
    
    viz - the visualizer
    
    Returns:
    
    a representation of the internal information of this Store

Class CFAbstractStore<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>

Nested Class Summary

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

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Methods inherited from interface org.plumelib.util.UniqueId

Field Detail

analysis

localVariableValues

thisValue

fieldValues

arrayValues

methodValues

classValues

sequentialSemantics

Constructor Detail

CFAbstractStore

CFAbstractStore

Method Detail

getFieldValues

getUid

initializeMethodParameter

initializeThisValue

isSideEffectFree

updateForMethodCall

insertValue

insertValuePermitNondeterministic

insertOrRefine

insertOrRefinePermitNondeterministic

insertOrRefine

canInsertJavaExpression

insertValue

insertValuePermitNondeterministic

shouldInsert

insertValue

isMonotonicUpdate

insertThisValue

replaceValue

clearValue

getValue

getValue

getFieldValue

getValue

getValue

updateForAssignment

updateForFieldAccessAssignment

updateForArrayAssignment

updateForLocalVariableAssignment

removeConflicting

removeConflicting

removeConflicting

canAlias

getValue

getValue

copy

leastUpperBound

widenedUpperBound

supersetOf

equals

hashCode

toString

visualize

internalVisualize