Package org.checkerframework.dataflow.analysis

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

java.lang.Object

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

org.checkerframework.dataflow.analysis.RegularTransferResult<V,S>

Type Parameters:

V - type of the abstract value that is tracked

S - the store type used in the analysis

public class RegularTransferResult<V extends AbstractValue<V>,S extends Store<S>>
extends TransferResult<V,S>

Implementation of a TransferResult with just one non-exceptional store. The result of getThenStore and getElseStore is equal to the only underlying store.

Field Summary

Fields

Modifier and Type	Field	Description
protected final S	store	The regular result store.

Fields inherited from class org.checkerframework.dataflow.analysis.TransferResult

exceptionalStores, resultValue

Constructor Summary

Constructors

Constructor	Description
RegularTransferResult(@Nullable V value, S resultStore)	Create a new RegularTransferResult(AbstractValue, Store, Map, boolean), using null for TransferResult.exceptionalStores and false for TransferResult.storeChanged().
RegularTransferResult(@Nullable V value, S resultStore, boolean storeChanged)	Create a new RegularTransferResult(AbstractValue, Store, Map, boolean), using null for TransferResult.exceptionalStores.
RegularTransferResult(@Nullable V value, S resultStore, @Nullable Map<TypeMirror,S> exceptionalStores)	Create a new RegularTransferResult(AbstractValue, Store, Map, boolean), using false for TransferResult.storeChanged().
RegularTransferResult(@Nullable V value, S resultStore, @Nullable Map<TypeMirror,S> exceptionalStores, boolean storeChanged)	Create a TransferResult with resultStore as the resulting store.

Method Summary

Modifier and Type	Method	Description
boolean	containsTwoStores()	Returns true if and only if this transfer result contains two stores that are potentially not equal.
S	getElseStore()	Returns the result store produced if the Node this result belongs to evaluates to false.
S	getRegularStore()	The regular result store.
S	getThenStore()	Returns the result store produced if the Node this result belongs to evaluates to true.
boolean	storeChanged()	See TransferResult.storeChanged().
String	toString()

Methods inherited from class org.checkerframework.dataflow.analysis.TransferResult

getExceptionalStore, getExceptionalStores, getResultValue, setResultValue

Methods inherited from class java.lang.Object

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

Field Details

store

protected final S extends Store<S> store

The regular result store.

Constructor Details

RegularTransferResult

public RegularTransferResult(@Nullable V value,
 S resultStore,
 boolean storeChanged)

Create a new RegularTransferResult(AbstractValue, Store, Map, boolean), using null for TransferResult.exceptionalStores.

Exceptions: If the corresponding Node throws an exception, then it is assumed that no special handling is necessary and the store before the corresponding Node will be passed along any exceptional edge.

Aliasing: resultStore is not allowed to be used anywhere outside of this class (including use through aliases). Complete control over the object is transferred to this class.

Parameters:

value - the abstract value produced by the transfer function

resultStore - regular result store

storeChanged - whether the store changed; see TransferResult.storeChanged()

See Also:

• RegularTransferResult(AbstractValue, Store, Map, boolean)

RegularTransferResult

public RegularTransferResult(@Nullable V value,
 S resultStore)

Create a new RegularTransferResult(AbstractValue, Store, Map, boolean), using null for TransferResult.exceptionalStores and false for TransferResult.storeChanged().

Parameters:

value - the abstract value produced by the transfer function

resultStore - regular result store

See Also:

• RegularTransferResult(AbstractValue, Store, Map, boolean)

RegularTransferResult

public RegularTransferResult(@Nullable V value,
 S resultStore,
 @Nullable Map<TypeMirror,S> exceptionalStores)

Create a new RegularTransferResult(AbstractValue, Store, Map, boolean), using false for TransferResult.storeChanged().

Parameters:

value - the abstract value produced by the transfer function

resultStore - the regular result store

exceptionalStores - the stores in case the basic block throws an exception, or null if the basic block does not throw any exceptions

See Also:

• RegularTransferResult(AbstractValue, Store, Map, boolean)

RegularTransferResult

public RegularTransferResult(@Nullable V value,
 S resultStore,
 @Nullable Map<TypeMirror,S> exceptionalStores,
 boolean storeChanged)

Create a TransferResult with resultStore as the resulting store. If the corresponding Node is a boolean node, then resultStore is used for both the 'then' and 'else' edge.

Exceptions: If the corresponding Node throws an exception, then the corresponding store in exceptionalStores is used. If no exception is found in exceptionalStores, then it is assumed that no special handling is necessary and the store before the corresponding Node will be passed along any exceptional edge.

Aliasing: resultStore and any store in exceptionalStores are not allowed to be used anywhere outside of this class (including use through aliases). Complete control over the objects is transferred to this class.

Parameters:

value - the abstract value produced by the transfer function

resultStore - the regular result store

exceptionalStores - the stores in case the basic block throws an exception, or null if the basic block does not throw any exceptions

storeChanged - see TransferResult.storeChanged()

Method Details

getRegularStore

public S getRegularStore()

The regular result store.

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

See TransferResult.storeChanged().

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

See Also:

• TransferResult.storeChanged()