Package org.checkerframework.checker.index.upperbound

Class UBQualifier

java.lang.Object
org.checkerframework.checker.index.upperbound.UBQualifier
Direct Known Subclasses:
UBQualifier.LessThanLengthOf, UBQualifier.UpperBoundLiteralQualifier, UBQualifier.UpperBoundUnknownQualifier
public abstract class UBQualifier extends Object
Abstraction for Upper Bound annotations. This abstract class has 4 subclasses, each of which is a nested class: UBQualifier.LessThanLengthOf, UBQualifier.UpperBoundUnknownQualifier, UpperBoundBottomQualifier, and PolyQualifier.

LTLengthOf is modeled by UBQualifier.LessThanLengthOf. LTEqLengthOf is equivalent to @UBQualifier.LessThanLengthOf with an offset of -1. LTOMLengthOf is equivalent to @UBQualifier.LessThanLengthOf with an offset of 1.

  • Constructor Details

    • UBQualifier

      public UBQualifier()

  • Method Details

    • createUBQualifier

      public static UBQualifier createUBQualifier(AnnotationMirror am, UpperBoundChecker ubChecker)
      Create a UBQualifier from the given annotation.
      Parameters:
      am - the annotation to turn into a UBQualifier
      ubChecker - used to obtain the fields of am
      Returns:
      a UBQualifier that represents the same information as the given annotation

    • createUBQualifier

      public static UBQualifier createUBQualifier(AnnotationMirror am, @Nullable String offset, UpperBoundChecker ubChecker)
      Create a UBQualifier from the given annotation, with an extra offset.
      Parameters:
      am - the annotation to turn into a UBQualifier
      offset - the extra offset; may be null
      ubChecker - used to obtain the fields of am
      Returns:
      a UBQualifier that represents the same information as the given annotation (plus an optional offset)

    • createUBQualifier

      public static UBQualifier createUBQualifier(String sequence, String offset)

    • createUBQualifier

      public static UBQualifier createUBQualifier(AnnotatedTypeMirror type, AnnotationMirror top, UpperBoundChecker ubChecker)
      Create an upper bound qualifier.
      Parameters:
      type - the type from which to obtain an annotation
      top - the top annotation in a hierarchy; the annotation in this hierarchy will be used
      ubChecker - used to obtain the fields of am
      Returns:
      a new upper bound qualifier

    • createUBQualifier

      public static UBQualifier createUBQualifier(List<String> sequences, List<String> offsets)
      Creates an UBQualifier from the given sequences and offsets. The list of sequences may not be empty. If the offsets list is empty, then an offset of 0 is used for each sequence. If the offsets list is not empty, then it must be the same size as sequence.
      Parameters:
      sequences - non-empty list of sequences
      offsets - list of offset, if empty, an offset of 0 is used
      Returns:
      an UBQualifier for the sequences with the given offsets

    • createUBQualifier

      public static UBQualifier createUBQualifier(List<String> sequences, List<String> offsets, @Nullable String extraOffset)
      Creates an UBQualifier from the given sequences and offsets, with the given additional offset. The list of sequences may not be empty. If the offsets list is empty, then an offset of 0 is used for each sequence. If the offsets list is not empty, then it must be the same size as sequence.
      Parameters:
      sequences - non-empty list of sequences
      offsets - list of offset, if empty, an offset of 0 is used
      extraOffset - offset to add to each element of offsets; may be null
      Returns:
      an UBQualifier for the sequences with the given offsets

    • plusOffset

      public UBQualifier plusOffset(Node node, UpperBoundAnnotatedTypeFactory factory)
      Add the node as an offset to a copy of this qualifier. If this qualifier is UNKNOWN or BOTTOM, then UNKNOWN is returned. Otherwise, see UBQualifier.LessThanLengthOf.plusOffset(int) for an explanation of how node is added as an offset.
      Parameters:
      node - a Node
      factory - an AnnotatedTypeFactory
      Returns:
      a copy of this qualifier with node added as an offset

    • plusOffset

      public UBQualifier plusOffset(int value)

    • minusOffset

      public UBQualifier minusOffset(Node node, UpperBoundAnnotatedTypeFactory factory)

    • minusOffset

      public UBQualifier minusOffset(int value)

    • isLessThanLengthQualifier

      public boolean isLessThanLengthQualifier()

    • isLiteral

      public boolean isLiteral()
      Returns true if this UBQualifier represents a literal integer.
      Returns:
      true if this UBQualifier represents a literal integer

    • isUnknown

      public boolean isUnknown()
      Returns true if this UBQualifier is the top type.
      Returns:
      true if this UBQualifier is the top type

    • isBottom

      public boolean isBottom()
      Returns true if this UBQualifier is the bottom type.
      Returns:
      true if this UBQualifier is the bottom type

    • isPoly

      @Pure public boolean isPoly()
      Return true if this is UBQualifier.PolyQualifier.
      Returns:
      true if this is UBQualifier.PolyQualifier

    • isSubtype

      public abstract boolean isSubtype(UBQualifier superType)

    • lub

      public abstract UBQualifier lub(UBQualifier other)

    • widenUpperBound

      public UBQualifier widenUpperBound(UBQualifier obj)

    • glb

      public abstract UBQualifier glb(UBQualifier other)

    • isLessThanLengthOf

      public boolean isLessThanLengthOf(String sequence)
      Is the value with this qualifier less than the length of sequence?
      Parameters:
      sequence - a String sequence
      Returns:
      whether or not the value with this qualifier is less than the length of sequence

    • isLessThanLengthOfAny

      public boolean isLessThanLengthOfAny(List<String> sequences)
      Is the value with this qualifier less than the length of any of the sequences?
      Parameters:
      sequences - list of sequences
      Returns:
      whether or not the value with this qualifier is less than the length of any of the sequences

    • hasSequenceWithOffset

      public boolean hasSequenceWithOffset(String sequence, int offset)
      Returns whether or not this qualifier has sequence with the specified offset.
      Parameters:
      sequence - sequence expression
      offset - the offset being looked for
      Returns:
      whether or not this qualifier has sequence with the specified offset

    • hasSequenceWithOffset

      public boolean hasSequenceWithOffset(String sequence, String offset)
      Returns whether or not this qualifier has sequence with the specified offset.
      Parameters:
      sequence - sequence expression
      offset - the offset being looked for
      Returns:
      whether or not this qualifier has sequence with the specified offset

    • isLessThanOrEqualTo

      public boolean isLessThanOrEqualTo(String sequence)
      Is the value with this qualifier less than or equal to the length of sequence?
      Parameters:
      sequence - a String sequence
      Returns:
      whether or not the value with this qualifier is less than or equal to the length of sequence