Class AccumulationValue
java.lang.Object
org.checkerframework.framework.flow.CFAbstractValue<AccumulationValue>
org.checkerframework.common.accumulation.AccumulationValue
- All Implemented Interfaces:
AbstractValue<AccumulationValue>
AccumulationValue holds additional information about accumulated facts ("values", not to be
confused with "Value" in the name of this class) that cannot be stored in the accumulation type,
because they are not a refinement of that type. This situation occurs for type variables and
wildcards, for which calling
AccumulationTransfer.accumulate(Node, TransferResult, String...) would otherwise have no effect (since the types are invariant: T is not a supertype
of Accumulator(a) T unless both bounds of T are supertypes of Accumulator(a)). This enables an
accumulation checker (or, typically, a client of that accumulation checker) to resolve
accumulated facts even on types that are type variables. For example, the Resource Leak Checker
uses this facility to check that calls to close() on variables whose type is a type variable have
actually occurred, such as in this example:
public static <T extends java.io.Closeable> void close(
@Owning @MustCall("close") T value) throws Exception {
value.close();
}
-
Nested Class Summary
Nested classes/interfaces inherited from class org.checkerframework.framework.flow.CFAbstractValue
CFAbstractValue.AnnotationSetCombiner, CFAbstractValue.ValueGlb, CFAbstractValue.ValueLub -
Field Summary
Fields inherited from class org.checkerframework.framework.flow.CFAbstractValue
analysis, annotations, atypeFactory, qualHierarchy, underlyingType -
Constructor Summary
ConstructorsModifierConstructorDescriptionprotectedAccumulationValue(CFAbstractAnalysis<AccumulationValue, ?, ?> analysis, AnnotationMirrorSet annotations, TypeMirror underlyingType) Creates a new CFAbstractValue. -
Method Summary
Modifier and TypeMethodDescriptionIf the underlying type is a type variable or a wildcard, then this is a set of accumulated values.mostSpecific(AccumulationValue other, AccumulationValue backup) Returns the more specific of two valuesthisandother.toString()Returns the string representation.protected AccumulationValueupperBound(@Nullable AccumulationValue other, TypeMirror upperBoundTypeMirror, boolean shouldWiden) Returns an upper bound ofthisandother.Methods inherited from class org.checkerframework.framework.flow.CFAbstractValue
canBeMissingAnnotations, equals, getAnnotations, getUnderlyingType, greatestLowerBound, hashCode, leastUpperBound, leastUpperBound, toStringFullyQualified, toStringSimple, validateSet, widenUpperBound
-
Constructor Details
-
AccumulationValue
protected AccumulationValue(CFAbstractAnalysis<AccumulationValue, ?, ?> analysis, AnnotationMirrorSet annotations, TypeMirror underlyingType) Creates a new CFAbstractValue.- Parameters:
analysis- the analysis class this value belongs toannotations- the annotations in this abstract valueunderlyingType- the underlying (Java) type in this abstract value
-
-
Method Details
-
getAccumulatedValues
If the underlying type is a type variable or a wildcard, then this is a set of accumulated values. Otherwise, it is null.- Returns:
- the set (this is not a copy of the set, but an alias)
-
upperBound
protected AccumulationValue upperBound(@Nullable AccumulationValue other, TypeMirror upperBoundTypeMirror, boolean shouldWiden) Description copied from class:CFAbstractValueReturns an upper bound ofthisandother. The underlying type of the value returned isupperBoundTypeMirror. IfshouldWidenis false, this method returns the least upper bound ofthisandother.This is the implementation of
CFAbstractValue.leastUpperBound(CFAbstractValue, TypeMirror),CFAbstractValue.leastUpperBound(CFAbstractValue),CFAbstractValue.widenUpperBound(CFAbstractValue), andCFAbstractValue.upperBound(CFAbstractValue, boolean). Subclasses may override it.- Overrides:
upperBoundin classCFAbstractValue<AccumulationValue>- Parameters:
other- an abstract valueupperBoundTypeMirror- the underlying type of the returned valueshouldWiden- true if the method should perform widening- Returns:
- an upper bound of this and
other
-
mostSpecific
Description copied from class:CFAbstractValueReturns the more specific of two valuesthisandother. If they do not contain information for all hierarchies, then it is possible that information from boththisandotherare taken.If neither of the two is more specific for one of the hierarchies (i.e., if the two are incomparable as determined by
QualifierHierarchy.isSubtypeShallow(AnnotationMirror, TypeMirror, AnnotationMirror, TypeMirror), then the respective value frombackupis used.- Overrides:
mostSpecificin classCFAbstractValue<AccumulationValue>- Parameters:
other- the other value to obtain information frombackup- the value to use ifthisandotherare incomparable- Returns:
- the more specific of two values
thisandother
-
toString
Description copied from class:CFAbstractValueReturns the string representation.- Overrides:
toStringin classCFAbstractValue<AccumulationValue>- Returns:
- the string representation
-