Package org.checkerframework.dataflow.analysis

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

java.lang.Object

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

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

Type Parameters:

V - type of the abstract value that is tracked

S - the store type used in the analysis

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

Implementation of a TransferResult with two non-exceptional stores. The 'then' store contains information valid when the previous boolean-valued expression was true, and the 'else' store contains information valid when the expression was false.

getRegularStore() returns the least upper bound of the two underlying stores.

Field Summary

Fields

Modifier and Type	Field	Description
protected S	elseStore	The 'else' result store.
protected S	thenStore	The 'then' result store.

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

exceptionalStores, resultValue

Constructor Summary

Constructors

Constructor	Description
ConditionalTransferResult(@Nullable V value, S thenStore, S elseStore)	Create a new ConditionalTransferResult(AbstractValue, Store, Store, Map, boolean), using false for whether the store changed and null for TransferResult.exceptionalStores.
ConditionalTransferResult(@Nullable V value, S thenStore, S elseStore, boolean storeChanged)	Create a new ConditionalTransferResult(AbstractValue, Store, Store, Map, boolean), using null for TransferResult.exceptionalStores.
ConditionalTransferResult(@Nullable V value, S thenStore, S elseStore, @Nullable java.util.Map<javax.lang.model.type.TypeMirror,S> exceptionalStores, boolean storeChanged)	Create a ConditionalTransferResult with thenStore as the resulting store if the corresponding Node evaluates to true and elseStore otherwise.
ConditionalTransferResult(V value, S thenStore, S elseStore, @Nullable java.util.Map<javax.lang.model.type.TypeMirror,S> exceptionalStores)	Create a new ConditionalTransferResult(AbstractValue, Store, Store, Map, boolean), using false for the storeChanged formal parameter.

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()	Returns true if and only if the transfer function returning this transfer result changed the regularStore, elseStore, or thenStore.
java.lang.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 Detail

thenStore

protected final S extends Store<S> thenStore

The 'then' result store.

elseStore

protected final S extends Store<S> elseStore

The 'else' result store.

Constructor Detail

ConditionalTransferResult

public ConditionalTransferResult(@Nullable V value,
                                 S thenStore,
                                 S elseStore,
                                 boolean storeChanged)

Create a new ConditionalTransferResult(AbstractValue, Store, 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: thenStore and elseStore 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

thenStore - 'then' result store

elseStore - 'else' result store

storeChanged - whether the store changed

See Also:

ConditionalTransferResult(AbstractValue, Store, Store, Map, boolean)

ConditionalTransferResult

public ConditionalTransferResult(@Nullable V value,
                                 S thenStore,
                                 S elseStore)

Create a new ConditionalTransferResult(AbstractValue, Store, Store, Map, boolean), using false for whether the store changed and null for TransferResult.exceptionalStores.

Parameters:

value - the abstract value produced by the transfer function

thenStore - thenStore

elseStore - elseStore

See Also:

ConditionalTransferResult(AbstractValue, Store, Store, Map, boolean)

ConditionalTransferResult

public ConditionalTransferResult(V value,
                                 S thenStore,
                                 S elseStore,
                                 @Nullable java.util.Map<javax.lang.model.type.TypeMirror,S> exceptionalStores)

Create a new ConditionalTransferResult(AbstractValue, Store, Store, Map, boolean), using false for the storeChanged formal parameter.

Parameters:

value - the abstract value produced by the transfer function

thenStore - thenStore

elseStore - elseStore

exceptionalStores - TransferResult.exceptionalStores

See Also:

ConditionalTransferResult(AbstractValue, Store, Store, Map, boolean)

ConditionalTransferResult

public ConditionalTransferResult(@Nullable V value,
                                 S thenStore,
                                 S elseStore,
                                 @Nullable java.util.Map<javax.lang.model.type.TypeMirror,S> exceptionalStores,
                                 boolean storeChanged)

Create a ConditionalTransferResult with thenStore as the resulting store if the corresponding Node evaluates to true and elseStore otherwise.

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: thenStore, elseStore, 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

thenStore - thenStore

elseStore - elseStore

exceptionalStores - TransferResult.exceptionalStores

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

Method Detail

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 java.lang.String toString()

Overrides:

toString in class java.lang.Object

storeChanged

public boolean storeChanged()

Description copied from class: TransferResult

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

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