Package org.checkerframework.common.accumulation

Class AccumulationValue

  • All Implemented Interfaces:
    AbstractValue<AccumulationValue>
    public class AccumulationValue
extends CFAbstractValue<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();
   }

    • Constructor Detail

      • AccumulationValue

        protected AccumulationValue​(CFAbstractAnalysis<AccumulationValue,​?,​?> analysis,
                            AnnotationMirrorSet annotations,
                            javax.lang.model.type.TypeMirror underlyingType)
        Creates a new CFAbstractValue.
        Parameters:
        analysis - the analysis class this value belongs to
        annotations - the annotations in this abstract value
        underlyingType - the underlying (Java) type in this abstract value