Package org.checkerframework.dataflow.analysis

Interface Store<S extends Store<S>>

Type Parameters:
S - the type of the store returned by copy and that is used in leastUpperBound. Usually it is the implementing class itself, e.g. in T extends Store<T>.
All Known Implementing Classes:
AccumulationStore, BusyExprStore, CFAbstractStore, CFStore, ConstantPropagationStore, InitializationStore, KeyForStore, LiveVarStore, LockStore, NullnessNoInitStore, ReachingDefinitionStore
public interface Store<S extends Store<S>>
A store is used to keep track of the information that the org.checkerframework.dataflow analysis has accumulated at any given point in time.

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Interface
    Description
    static enum 
    Store.FlowRule
    A flow rule describes how stores flow along one edge between basic blocks.
    static enum 
    Store.Kind
     

  • Method Summary

    Modifier and Type
    Method
    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).
    S
    copy()
    Returns an exact copy of this store.
    boolean
    equals(@Nullable Object o)
    Returns true if this is equal to the given argument.
    S
    leastUpperBound(S other)
    Compute the least upper bound of two stores.
    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.

  • Method Details

    • copy

      S copy()
      Returns an exact copy of this store.
      Returns:
      an exact copy of this store

    • leastUpperBound

      S leastUpperBound(S other)
      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.

    • widenedUpperBound

      S widenedUpperBound(S previous)
      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.
      Parameters:
      previous - must be the previous store

    • canAlias

      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).

    • visualize

      String visualize(CFGVisualizer<?,S,?> viz)
      Delegate visualization responsibility to a visualizer.
      Parameters:
      viz - the visualizer to visualize this store
      Returns:
      the String representation of this store

    • equals

      boolean equals(@Nullable Object o)
      Returns true if this is equal to the given argument.
      Overrides:
      equals in class Object
      Parameters:
      o - the object to compare against this
      Returns:
      true if this is equal to the given argument