V - type of the abstract value that is trackedS - the store type used in the analysispublic 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).
| Modifier and Type | Field and Description |
|---|---|
protected @Nullable Map<TypeMirror,S> |
exceptionalStores
The stores in case the basic block throws an exception (or
null if the corresponding
Node does not throw any exceptions). |
protected V |
resultValue
The abstract value of the
Node associated with
this TransferResult, or null if no value has been produced. |
| Modifier | Constructor and Description |
|---|---|
protected |
TransferResult(V resultValue,
@Nullable Map<TypeMirror,S> exceptionalStores)
Create a new TransferResult, given
resultValue and exceptionalStores. |
| Modifier and Type | Method and Description |
|---|---|
abstract boolean |
containsTwoStores()
Returns
true if and only if this transfer result contains two stores that are
potentially not equal. |
abstract S |
getElseStore()
Returns the result store produced if the
Node
this result belongs to evaluates to false. |
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). |
@Nullable Map<TypeMirror,S> |
getExceptionalStores()
|
abstract S |
getRegularStore()
Returns the regular result store produced if no exception is thrown by the
Node corresponding to this transfer function result. |
V |
getResultValue()
Returns the abstract value produced by the transfer function,
null otherwise. |
abstract S |
getThenStore()
Returns the result store produced if the
Node
this result belongs to evaluates to true. |
void |
setResultValue(V resultValue)
Set the value of
resultValue. |
abstract boolean |
storeChanged()
Returns
true if and only if the transfer function returning this transfer result
changed the regularStore, elseStore, or thenStore. |
protected V extends AbstractValue<V> resultValue
Node associated with
this TransferResult, or null if no value has been produced.protected final @Nullable Map<TypeMirror,S extends Store<S>> exceptionalStores
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.protected TransferResult(V resultValue, @Nullable Map<TypeMirror,S> exceptionalStores)
resultValue and exceptionalStores.resultValue - the abstract value of the Node associated with this TransferResultexceptionalStores - the stores in case the basic block throws an exception (or null if the corresponding Node does not
throw any exceptions)public V getResultValue()
null otherwise.null otherwisepublic void setResultValue(V resultValue)
resultValue.resultValue - the abstract value of the Node associated with this TransferResultpublic abstract S getRegularStore()
Node corresponding to this transfer function result.Node corresponding to this transfer function resultpublic abstract S getThenStore()
Node
this result belongs to evaluates to true.Node
this result belongs to evaluates to truepublic abstract S getElseStore()
Node
this result belongs to evaluates to false.Node
this result belongs to evaluates to falsepublic S getExceptionalStore(TypeMirror exception)
exception
(or null if no special handling is required for exceptional edges).exception - an exception typeexception
(or null if no special handling is required for exceptional edges)public @Nullable Map<TypeMirror,S> getExceptionalStores()
TypeMirror to Store, null otherwisegetExceptionalStore(TypeMirror)public abstract boolean containsTwoStores()
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.true if and only if this transfer result contains two stores that are
potentially not equalpublic abstract boolean storeChanged()
true if and only if the transfer function returning this transfer result
changed the regularStore, elseStore, or thenStore.true if and only if the transfer function returning this transfer result
changed the regularStore, elseStore, or thenStore