Package org.checkerframework.dataflow.reachingdef

Class ReachingDefinitionStore

java.lang.Object
org.checkerframework.dataflow.reachingdef.ReachingDefinitionStore
All Implemented Interfaces:
Store<ReachingDefinitionStore>
public class ReachingDefinitionStore extends Object implements Store<ReachingDefinitionStore>
A reaching definition store contains a set of reaching definitions represented by ReachingDefinitionNode

  • Constructor Details

    • ReachingDefinitionStore

      public ReachingDefinitionStore()
      Create a new ReachDefinitionStore.

    • ReachingDefinitionStore

      public ReachingDefinitionStore(Set<ReachingDefinitionNode> reachingDefSet)
      Create a new ReachDefinitionStore.
      Parameters:
      reachingDefSet - a set of reaching definition nodes. The parameter is captured and the caller should not retain an alias.

  • Method Details

    • killDef

      public void killDef(Node defTarget)
      Remove the information of a reaching definition from the reaching definition set.
      Parameters:
      defTarget - target of a reaching definition

    • putDef

      public void putDef(ReachingDefinitionNode def)
      Add a reaching definition to the reaching definition set.
      Parameters:
      def - a reaching definition

    • equals

      public boolean equals(@Nullable Object obj)
      Description copied from interface: Store
      Returns true if this is equal to the given argument.
      Specified by:
      equals in interface Store<ReachingDefinitionStore>
      Overrides:
      equals in class Object
      Parameters:
      obj - the object to compare against this
      Returns:
      true if this is equal to the given argument

    • hashCode

      public int hashCode()
      Overrides:
      hashCode in class Object

    • copy

      public ReachingDefinitionStore copy()
      Description copied from interface: Store
      Returns an exact copy of this store.
      Specified by:
      copy in interface Store<ReachingDefinitionStore>
      Returns:
      an exact copy of this store

    • leastUpperBound

      public ReachingDefinitionStore leastUpperBound(ReachingDefinitionStore 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<ReachingDefinitionStore>

    • widenedUpperBound

      public ReachingDefinitionStore widenedUpperBound(ReachingDefinitionStore 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<ReachingDefinitionStore>
      Parameters:
      previous - must be the previous store

    • canAlias

      public boolean canAlias(JavaExpression a, JavaExpression b)
      Description copied from interface: Store
      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<ReachingDefinitionStore>

    • visualize

      public String visualize(CFGVisualizer<?,ReachingDefinitionStore,?> viz)
      Description copied from interface: Store
      Delegate visualization responsibility to a visualizer.
      Specified by:
      visualize in interface Store<ReachingDefinitionStore>
      Parameters:
      viz - the visualizer to visualize this store
      Returns:
      the String representation of this store

    • toString

      public String toString()
      Overrides:
      toString in class Object