org.checkerframework.dataflow.analysis

Interface Store<S extends Store<S>>

Type Parameters:

S - The type of the store returned by copy and that is used in leastUpperBound. Usually it is the implementing class itself, e.g. in T extends Store<T>.

All Known Implementing Classes:

CFAbstractStore, CFStore, ConstantPropagationStore, InitializationStore, LockStore, NullnessStore, QualStore

public interface Store<S extends Store<S>>

A store is used to keep track of the information that the org.checkerframework.dataflow analysis has accumulated at any given point in time.

Author:

Stefan Heule

Nested Class Summary

Nested Classes

Modifier and Type	Interface and Description
static class	Store.FlowRule
static class	Store.Kind

Method Summary

Modifier and Type	Method and Description
boolean	canAlias(FlowExpressions.Receiver a, FlowExpressions.Receiver b) Can the objects a and b be aliases? Returns a conservative answer (i.e., returns true if not enough information is available to determine aliasing).
S	copy()
boolean	hasDOToutput()
S	leastUpperBound(S other) Compute the least upper bound of two stores.
String	toDOToutput()

Method Detail

copy

S copy()

Returns:

An exact copy of this store.

leastUpperBound

S leastUpperBound(S other)

Compute the least upper bound of two stores.

Important: This method must fulfill the following contract:

• Does not change this.
• Does not change other.
• Returns a fresh object which is not aliased yet.
• Returns an object of the same (dynamic) type as this, even if the signature is more permissive.
• Is commutative.

canAlias

boolean canAlias(FlowExpressions.Receiver a,
                 FlowExpressions.Receiver b)

Can the objects a and b be aliases? Returns a conservative answer (i.e., returns true if not enough information is available to determine aliasing).

hasDOToutput

boolean hasDOToutput()

Returns:

Whether the Store supports DOT graph output.

toDOToutput

String toDOToutput()

Returns:

The store encoded as a DOT graph for visualization.