org.checkerframework.qualframework.base.dataflow

Class QualStore<Q>

java.lang.Object

org.checkerframework.qualframework.base.dataflow.QualStore<Q>

All Implemented Interfaces:

Store<QualStore<Q>>

public class QualStore<Q>
extends Object
implements Store<QualStore<Q>>

QualStore is a Store for quals. It proxies a CFStore adapter.

Nested Class Summary

Nested classes/interfaces inherited from interface org.checkerframework.dataflow.analysis.Store

Store.FlowRule, Store.Kind

Constructor Summary

Constructors

Constructor and Description
QualStore(QualAnalysis<Q> analysis, CFStore adapter)

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).
QualStore<Q>	copy()
CFStore	getUnderlyingStore()
boolean	hasDOToutput()
void	insertValue(FlowExpressions.Receiver r, Q regexAnnotation)
QualStore<Q>	leastUpperBound(QualStore<Q> other) Compute the least upper bound of two stores.
String	toDOToutput()

Methods inherited from class java.lang.Object

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

Constructor Detail

QualStore

public QualStore(QualAnalysis<Q> analysis,
                 CFStore adapter)

Method Detail

copy

public QualStore<Q> copy()

Specified by:

copy in interface Store<QualStore<Q>>

Returns:

An exact copy of this store.

leastUpperBound

public QualStore<Q> leastUpperBound(QualStore<Q> other)

Description copied from interface: Store

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.

Specified by:

leastUpperBound in interface Store<QualStore<Q>>

canAlias

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

Description copied from interface: Store

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

Specified by:

canAlias in interface Store<QualStore<Q>>

hasDOToutput

public boolean hasDOToutput()

Specified by:

hasDOToutput in interface Store<QualStore<Q>>

Returns:

Whether the Store supports DOT graph output.

toDOToutput

public String toDOToutput()

Specified by:

toDOToutput in interface Store<QualStore<Q>>

Returns:

The store encoded as a DOT graph for visualization.

getUnderlyingStore

public CFStore getUnderlyingStore()

insertValue

public void insertValue(FlowExpressions.Receiver r,
                        Q regexAnnotation)