Class ConditionalTransferResult<V extends AbstractValue<V>,S extends Store<S>>

java.lang.Object
org.checkerframework.dataflow.analysis.TransferResult<V,S>
org.checkerframework.dataflow.analysis.ConditionalTransferResult<V,S>
Type Parameters:
V - type of the abstract value that is tracked
S - the store type used in the analysis

public class ConditionalTransferResult<V extends AbstractValue<V>,S extends Store<S>> extends TransferResult<V,S>
Implementation of a TransferResult with two non-exceptional stores. The 'then' store contains information valid when the previous boolean-valued expression was true, and the 'else' store contains information valid when the expression was false.

getRegularStore() returns the least upper bound of the two underlying stores.

  • Field Details

    • thenStore

      protected final S extends Store<S> thenStore
      The 'then' result store.
    • elseStore

      protected final S extends Store<S> elseStore
      The 'else' result store.
  • Constructor Details

  • Method Details

    • getRegularStore

      public S getRegularStore()
      Description copied from class: TransferResult
      Returns the regular result store produced if no exception is thrown by the Node corresponding to this transfer function result.
      Specified by:
      getRegularStore in class TransferResult<V extends AbstractValue<V>,S extends Store<S>>
      Returns:
      the regular result store produced if no exception is thrown by the Node corresponding to this transfer function result
    • getThenStore

      public S getThenStore()
      Description copied from class: TransferResult
      Returns the result store produced if the Node this result belongs to evaluates to true.
      Specified by:
      getThenStore in class TransferResult<V extends AbstractValue<V>,S extends Store<S>>
      Returns:
      the result store produced if the Node this result belongs to evaluates to true
    • getElseStore

      public S getElseStore()
      Description copied from class: TransferResult
      Returns the result store produced if the Node this result belongs to evaluates to false.
      Specified by:
      getElseStore in class TransferResult<V extends AbstractValue<V>,S extends Store<S>>
      Returns:
      the result store produced if the Node this result belongs to evaluates to false
    • containsTwoStores

      public boolean containsTwoStores()
      Description copied from class: TransferResult
      Returns true if and only if this transfer result contains two stores that are potentially not equal. Note that the result true does not imply that getRegularStore cannot be called (or vice versa for false). Rather, it indicates that getThenStore or getElseStore can be used to give more precise results. Otherwise, if the result is false, then all three methods getRegularStore, getThenStore, and getElseStore return equivalent stores.
      Specified by:
      containsTwoStores in class TransferResult<V extends AbstractValue<V>,S extends Store<S>>
      Returns:
      true if and only if this transfer result contains two stores that are potentially not equal
    • toString

      public String toString()
      Overrides:
      toString in class Object
    • storeChanged

      public boolean storeChanged()
      Description copied from class: TransferResult
      Returns true if and only if the transfer function returning this transfer result changed the regularStore, elseStore, or thenStore.
      Specified by:
      storeChanged in class TransferResult<V extends AbstractValue<V>,S extends Store<S>>
      Returns:
      true if and only if the transfer function returning this transfer result changed the regularStore, elseStore, or thenStore