org.checkerframework.framework.flow

Class CFAbstractValue<V extends CFAbstractValue<V>>

java.lang.Object

org.checkerframework.framework.flow.CFAbstractValue<V>

All Implemented Interfaces:

AbstractValue<V>

Direct Known Subclasses:

CFValue, NullnessValue

public abstract class CFAbstractValue<V extends CFAbstractValue<V>>
extends Object
implements AbstractValue<V>

An implementation of an abstract value used by the Checker Framework org.checkerframework.dataflow analysis. Contains a set of annotations.

Author:

Stefan Heule

Field Summary

Fields

Modifier and Type	Field and Description
protected CFAbstractAnalysis<V,?,?>	analysis The analysis class this store belongs to.
protected AnnotatedTypeMirror	type The type (with annotations) corresponding to this abstract value.
protected TypeHierarchy	typeHierarchy

Constructor Summary

Constructors

Constructor and Description
CFAbstractValue(CFAbstractAnalysis<V,?,?> analysis, AnnotatedTypeMirror type)

Method Summary

Modifier and Type	Method and Description
boolean	equals(Object obj)
AnnotatedTypeMirror	getType()
int	hashCode()
boolean	isSubtypeOf(CFAbstractValue<V> other) Returns whether this value is a subtype of the argument other.
V	leastUpperBound(V other) Compute the least upper bound of two stores.
V	mostSpecific(V other, V backup) Returns the more specific version of two values this and other.
static boolean	mostSpecificTypeVariable(AnnotatedTypeFactory typeFactory, AnnotatedTypeMirror type1, AnnotatedTypeMirror type2, AnnotatedTypeMirror backup, AnnotatedTypeMirror.AnnotatedTypeVariable result) Refines the result annotated type variable with the most specific of type1 and type2.
String	toString()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

analysis

protected final CFAbstractAnalysis<V extends CFAbstractValue<V>,?,?> analysis

The analysis class this store belongs to.

typeHierarchy

protected final TypeHierarchy typeHierarchy

type

protected final AnnotatedTypeMirror type

The type (with annotations) corresponding to this abstract value.

Constructor Detail

CFAbstractValue

public CFAbstractValue(CFAbstractAnalysis<V,?,?> analysis,
                       AnnotatedTypeMirror type)

Method Detail

getType

@Pure
public AnnotatedTypeMirror getType()

leastUpperBound

public V leastUpperBound(V other)

Description copied from interface: AbstractValue

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 AbstractValue<V extends CFAbstractValue<V>>

isSubtypeOf

public boolean isSubtypeOf(CFAbstractValue<V> other)

Returns whether this value is a subtype of the argument other. The annotations are compared per hierarchy, and missing annotations are treated as 'top'.

mostSpecific

public V mostSpecific(V other,
                      V backup)

Returns the more specific version of two values this and other. If they do not contain information for all hierarchies, then it is possible that information from both this and other are taken.

If neither of the two is more specific for one of the hierarchies (i.e., if the two are incomparable as determined by TypeHierarchy.isSubtype(AnnotatedTypeMirror, AnnotatedTypeMirror) , then the respective value from backup is used.

TODO: The code in this method is rather similar to leastUpperBound(CFAbstractValue). Can code be reused?

mostSpecificTypeVariable

public static boolean mostSpecificTypeVariable(AnnotatedTypeFactory typeFactory,
                                               AnnotatedTypeMirror type1,
                                               AnnotatedTypeMirror type2,
                                               AnnotatedTypeMirror backup,
                                               AnnotatedTypeMirror.AnnotatedTypeVariable result)

Refines the result annotated type variable with the most specific of type1 and type2.

Returns:

True if the result was annotated in all hierarchy, false if the result could not be annotated in one or more annotation hierarchies

equals

public boolean equals(Object obj)

Overrides:

equals in class Object

hashCode

@Pure
public int hashCode()

Overrides:

hashCode in class Object

toString

@SideEffectFree
public String toString()

Overrides:

toString in class Object

Returns:

The string representation as a comma-separated list.