org.checkerframework.dataflow.analysis

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

java.lang.Object

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

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

Type Parameters:

S - the Store used to keep track of intermediate results

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

Implementation of a TransferResult with two non-exceptional store; one for the 'then' edge and one for 'else'. The result of getRegularStore will be the least upper bound of the two underlying stores.

Author:

Stefan Heule

Field Summary

Fields

Modifier and Type	Field and 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 and Description
ConditionalTransferResult(A value, S thenStore, S elseStore)
ConditionalTransferResult(A value, S thenStore, S elseStore, boolean storeChanged) Create a ConditionalTransferResult with thenStore as the resulting store if the corresponding Node evaluates to true and elseStore otherwise.
ConditionalTransferResult(A value, S thenStore, S elseStore, Map<TypeMirror,S> exceptionalStores)
ConditionalTransferResult(A value, S thenStore, S elseStore, Map<TypeMirror,S> exceptionalStores, boolean storeChanged) Create a ConditionalTransferResult with thenStore as the resulting store if the corresponding Node evaluates to true and elseStore otherwise.

Method Summary

Modifier and Type	Method and Description
boolean	containsTwoStores()
S	getElseStore()
S	getRegularStore()
S	getThenStore()
boolean	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 Detail

thenStore

protected S extends Store<S> thenStore

The 'then' result store.

elseStore

protected S extends Store<S> elseStore

The 'else' result store.

Constructor Detail

ConditionalTransferResult

public ConditionalTransferResult(A value,
                                 S thenStore,
                                 S elseStore,
                                 boolean storeChanged)

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

For the meaning of storeChanged, see TransferResult.storeChanged().

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 transfered to this class.

ConditionalTransferResult

public ConditionalTransferResult(A value,
                                 S thenStore,
                                 S elseStore)

ConditionalTransferResult

public ConditionalTransferResult(A value,
                                 S thenStore,
                                 S elseStore,
                                 Map<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 transfered to this class.

ConditionalTransferResult

public ConditionalTransferResult(A value,
                                 S thenStore,
                                 S elseStore,
                                 Map<TypeMirror,S> exceptionalStores)

Method Detail

getRegularStore

public S getRegularStore()

Specified by:

getRegularStore in class TransferResult<A extends AbstractValue<A>,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()

Specified by:

getThenStore in class TransferResult<A extends AbstractValue<A>,S extends Store<S>>

Returns:

the result store produced if the Node this result belongs to evaluates to true.

getElseStore

public S getElseStore()

Specified by:

getElseStore in class TransferResult<A extends AbstractValue<A>,S extends Store<S>>

Returns:

the result store produced if the Node this result belongs to evaluates to false.

containsTwoStores

public boolean containsTwoStores()

Specified by:

containsTwoStores in class TransferResult<A extends AbstractValue<A>,S extends Store<S>>

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.

toString

public String toString()

Overrides:

toString in class Object

storeChanged

public boolean storeChanged()

Specified by:

storeChanged in class TransferResult<A extends AbstractValue<A>,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()