org.checkerframework.dataflow.analysis

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

java.lang.Object

org.checkerframework.dataflow.analysis.TransferResult<A,S>

Type Parameters:

S - The Store used to keep track of intermediate results.

Direct Known Subclasses:

ConditionalTransferResult, RegularTransferResult

public abstract class TransferResult<A extends AbstractValue<A>,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).

Author:

Stefan Heule

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 A	resultValue The abstract value of the Node associated with this TransferResult, or null if no value has been produced.

Constructor Summary

Constructors

Constructor and Description
TransferResult(A resultValue)

Method Summary

Modifier and Type	Method and Description
abstract boolean	containsTwoStores()
abstract S	getElseStore()
S	getExceptionalStore(TypeMirror exception)
Map<TypeMirror,S>	getExceptionalStores()
abstract S	getRegularStore()
A	getResultValue()
abstract S	getThenStore()
void	setResultValue(A resultValue)
abstract boolean	storeChanged()

Methods inherited from class java.lang.Object

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

Field Detail

exceptionalStores

protected @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.

resultValue

protected A extends AbstractValue<A> resultValue

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

Constructor Detail

TransferResult

public TransferResult(A resultValue)

Method Detail

getResultValue

public A getResultValue()

Returns:

The abstract value produced by the transfer function.

setResultValue

public void setResultValue(A resultValue)

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.

getThenStore

public abstract S getThenStore()

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.

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).

getExceptionalStores

public Map<TypeMirror,S> getExceptionalStores()

Returns:

Returns a Map of TypeMirror to Store.

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.

storeChanged

public abstract boolean storeChanged()

Returns:

true if and only if the transfer function returning this transfer result changed the regularStore, elseStore, or thenStore.