Package org.checkerframework.common.value

Class ValueAnalysis

java.lang.Object
org.checkerframework.dataflow.analysis.AbstractAnalysis<CFValue,CFStore,CFTransfer>
org.checkerframework.dataflow.analysis.ForwardAnalysisImpl<CFValue,CFStore,CFTransfer>
org.checkerframework.framework.flow.CFAbstractAnalysis<CFValue,CFStore,CFTransfer>
org.checkerframework.framework.flow.CFAnalysis
org.checkerframework.common.value.ValueAnalysis
All Implemented Interfaces:
Analysis<CFValue,CFStore,CFTransfer>, ForwardAnalysis<CFValue,CFStore,CFTransfer>
public class ValueAnalysis extends CFAnalysis
The dataflow analysis for the Value Checker.

It differs from the default analysis only in that it converts the IntRangeFrom* annotations, which are aliases that the Index Checker introduces, into the IntRange annotations that the rest of the Value Checker reasons about. Without this conversion, whether an abstract value holds an alias or an IntRange would depend on whether the value happens to have been merged at a control-flow join point.

  • Constructor Details

  • Method Details

    • createAbstractValue

      public @Nullable CFValue createAbstractValue(AnnotationMirrorSet annotations, TypeMirror underlyingType)
      Returns an abstract value containing the given annotations and underlyingType. Returns null if the annotation set has missing annotations.

      This conversion bounds an IntRangeFrom* alias by the maximum value of underlyingType, whereas ValueQualifierHierarchy.leastUpperBoundQualifiers bounds it by Long.MAX_VALUE. The bound here is the more precise of the two.

      Overrides:
      createAbstractValue in class CFAnalysis
      Parameters:
      annotations - the annotations for the result annotated type
      underlyingType - the unannotated type for the result annotated type
      Returns:
      an abstract value containing the given annotations and underlyingType or null if annotations is missing annotations