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 store in TransferResult.

A TransferResult contains one or two stores (for 'then' and 'else'), and zero or more stores with a cause (TypeMirror).

Field Summary

Fields

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.

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	TransferResult(V resultValue, @Nullable Map<TypeMirror,S> exceptionalStores) Create a new TransferResult, given resultValue and exceptionalStores.

Method Summary

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() Returns a Map of TypeMirror to Store, null otherwise.
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.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

resultValue

protected V extends AbstractValue<V> resultValue

The abstract value of the Node associated with this TransferResult, or null if no value has been produced.

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 Detail

TransferResult

protected TransferResult(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 Detail

getResultValue

public 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 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:

getExceptionalStore(TypeMirror)

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