org.checkerframework.dataflow.analysis

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

java.lang.Object

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

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

Type Parameters:

S - the Store used to keep track of intermediate results

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

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

Author:

Stefan Heule

Field Summary

Fields

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

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

exceptionalStores, resultValue

Constructor Summary

Constructors

Constructor and Description
RegularTransferResult(A value, S resultStore)
RegularTransferResult(A value, S resultStore, boolean storeChanged) Create a TransferResult with resultStore as the resulting store.
RegularTransferResult(A value, S resultStore, java.util.Map<javax.lang.model.type.TypeMirror,S> exceptionalStores)
RegularTransferResult(A value, S resultStore, java.util.Map<javax.lang.model.type.TypeMirror,S> exceptionalStores, boolean storeChanged) Create a TransferResult with resultStore as the resulting store.

Method Summary

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

store

protected S extends Store<S> store

The regular result store.

Constructor Detail

RegularTransferResult

public RegularTransferResult(A value,
                             S resultStore,
                             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 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 transfered to this class.

RegularTransferResult

public RegularTransferResult(A value,
                             S resultStore)

RegularTransferResult

public RegularTransferResult(A value,
                             S resultStore,
                             java.util.Map<javax.lang.model.type.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.

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

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

RegularTransferResult

public RegularTransferResult(A value,
                             S resultStore,
                             java.util.Map<javax.lang.model.type.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 java.lang.String toString()

Overrides:

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