Package org.checkerframework.dataflow.analysis

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

java.lang.Object
org.checkerframework.dataflow.analysis.TransferResult<V,S>
Type Parameters:
V - type of the abstract value that is tracked
S - the store type used in the analysis
Direct Known Subclasses:
ConditionalTransferResult, RegularTransferResult
public abstract class TransferResult<V extends AbstractValue<V>,S extends Store<S>> extends Object
TransferResult is used as the result type of the individual transfer functions of a TransferFunction. It always belongs to the result of the individual transfer function for a particular Node, even though that org.checkerframework.dataflow.cfg.node.Node is not explicitly stored in TransferResult.

A TransferResult consists of a result value, plus one or more stores. It contains one or two stores (for 'then' and 'else'), and zero or more stores with a cause (TypeMirror).

  • Field Details

    • resultValue

      protected @Nullable V extends AbstractValue<V> resultValue
      The abstract value of the Node associated with this TransferResult, or null if no value has been produced.

      Is set by setResultValue(V).

    • exceptionalStores

      protected final @Nullable Map<TypeMirror,S extends Store<S>> exceptionalStores
      The stores in case the basic block throws an exception (or null if the corresponding Node does not throw any exceptions). Does not necessarily contain a store for every exception, in which case the in-store will be used.

  • Constructor Details

    • TransferResult

      protected TransferResult(@Nullable V resultValue, @Nullable Map<TypeMirror,S> exceptionalStores)
      Create a new TransferResult, given resultValue and exceptionalStores.
      Parameters:
      resultValue - the abstract value of the Node associated with this TransferResult
      exceptionalStores - the stores in case the basic block throws an exception (or null if the corresponding Node does not throw any exceptions)

  • Method Details

    • getResultValue

      public @Nullable V getResultValue()
      Returns the abstract value produced by the transfer function, null otherwise.
      Returns:
      the abstract value produced by the transfer function, null otherwise

    • setResultValue

      public void setResultValue(V resultValue)
      Set the value of resultValue.
      Parameters:
      resultValue - the abstract value of the Node associated with this TransferResult

    • getRegularStore

      public abstract S getRegularStore()
      Returns the regular result store produced if no exception is thrown by the Node corresponding to this transfer function result.
      Returns:
      the regular result store produced if no exception is thrown by the Node corresponding to this transfer function result

    • getThenStore

      public abstract S getThenStore()
      Returns the result store produced if the Node this result belongs to evaluates to true.
      Returns:
      the result store produced if the Node this result belongs to evaluates to true

    • getElseStore

      public abstract S getElseStore()
      Returns the result store produced if the Node this result belongs to evaluates to false.
      Returns:
      the result store produced if the Node this result belongs to evaluates to false

    • getExceptionalStore

      public @Nullable S getExceptionalStore(TypeMirror exception)
      Returns the store that flows along the outgoing exceptional edge labeled with exception (or null if no special handling is required for exceptional edges).
      Parameters:
      exception - an exception type
      Returns:
      the store that flows along the outgoing exceptional edge labeled with exception (or null if no special handling is required for exceptional edges)

    • getExceptionalStores

      public @Nullable Map<TypeMirror,S> getExceptionalStores()
      Returns a Map of TypeMirror to Store, null otherwise.
      Returns:
      a Map of TypeMirror to Store, null otherwise
      See Also:

    • containsTwoStores

      public abstract boolean containsTwoStores()
      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.
      Returns:
      true if and only if this transfer result contains two stores that are potentially not equal

    • storeChanged

      public abstract boolean storeChanged()
      Returns true if and only if the transfer function returning this transfer result changed the regularStore, elseStore, or thenStore.
      Returns:
      true if and only if the transfer function returning this transfer result changed the regularStore, elseStore, or thenStore