Package org.checkerframework.checker.index.upperbound

Class UBQualifier.LessThanLengthOf

java.lang.Object
org.checkerframework.checker.index.upperbound.UBQualifier
org.checkerframework.checker.index.upperbound.UBQualifier.LessThanLengthOf
Enclosing class:
UBQualifier
public static class UBQualifier.LessThanLengthOf extends UBQualifier
The less-than-length-of qualifier (@LTLengthOf).

  • Method Details

    • hasSequenceWithOffset

      public boolean hasSequenceWithOffset(String sequence, int offset)
      Description copied from class: UBQualifier
      Returns true if this qualifier has sequence with the specified offset.
      Overrides:
      hasSequenceWithOffset in class UBQualifier
      Parameters:
      sequence - sequence expression
      offset - the offset being looked for
      Returns:
      true if this qualifier has sequence with the specified offset

    • hasSequenceWithOffset

      public boolean hasSequenceWithOffset(String sequence, String offset)
      Description copied from class: UBQualifier
      Returns true if this qualifier has sequence with the specified offset.
      Overrides:
      hasSequenceWithOffset in class UBQualifier
      Parameters:
      sequence - sequence expression
      offset - the offset being looked for
      Returns:
      true if this qualifier has sequence with the specified offset

    • isLessThanOrEqualTo

      public boolean isLessThanOrEqualTo(String sequence)
      Is a value with this type less than or equal to the length of sequence?
      Overrides:
      isLessThanOrEqualTo in class UBQualifier
      Parameters:
      sequence - a String sequence
      Returns:
      true if a value with this type is less than or equal to the length of sequence

    • isLessThanLengthOfAny

      public boolean isLessThanLengthOfAny(List<String> sequences)
      Is a value with this type less than the length of any of the sequences?
      Overrides:
      isLessThanLengthOfAny in class UBQualifier
      Parameters:
      sequences - list of sequences
      Returns:
      true if a value with this type is less than the length of any of the sequences

    • isLessThanLengthOf

      public boolean isLessThanLengthOf(String sequence)
      Is a value with this type less than the length of the sequence?
      Overrides:
      isLessThanLengthOf in class UBQualifier
      Parameters:
      sequence - a String sequence
      Returns:
      true if a value with this type is less than the length of the sequence

    • convertToAnnotation

      public AnnotationMirror convertToAnnotation(ProcessingEnvironment env)
      Returns the AnnotationMirror that represents this qualifier. If possible, AnnotationMirrors using @LTEqLengthOf or @LTOMLengthOf are returned. Otherwise, @LTLengthOf is used.

      The returned annotation is canonicalized by sorting its arguments by sequence and then offset. This is so that AnnotationUtils.areSame(AnnotationMirror, AnnotationMirror) returns true for equivalent annotations.

      Parameters:
      env - a processing environment used to build the returned annotation
      Returns:
      the AnnotationMirror that represents this qualifier

    • convertToSubstringIndexAnnotation

      public AnnotationMirror convertToSubstringIndexAnnotation(ProcessingEnvironment env)
      Returns the @SubstringIndexFor AnnotationMirror from the Substring Index hierarchy that imposes the same upper bounds on the annotated expression as this qualifier. However, the upper bounds represented by this qualifier do not apply to the value -1 which is always allowed by the returned annotation.
      Parameters:
      env - a processing environment used to build the returned annotation
      Returns:
      the AnnotationMirror from the Substring Index hierarchy that represents the same upper bounds as this qualifier

    • equals

      public boolean equals(@Nullable Object o)
      Overrides:
      equals in class Object

    • hashCode

      public int hashCode()
      Overrides:
      hashCode in class Object

    • isLessThanLengthQualifier

      public boolean isLessThanLengthQualifier()
      Overrides:
      isLessThanLengthQualifier in class UBQualifier

    • isSubtype

      public boolean isSubtype(UBQualifier superType)
      If superType is Unknown, return true. If superType is Bottom, return false.

      Otherwise, return true if this qualifier contains all the sequences in superType, AND for each of the offsets for each sequence in superType, there is an offset in this qualifier for the sequence that is greater than or equal to the super offset.

      Specified by:
      isSubtype in class UBQualifier
      Parameters:
      superType - other qualifier
      Returns:
      true if this qualifier is a subtype of superType

    • lub

      public UBQualifier lub(UBQualifier other)
      If other is Unknown, return Unknown. If other is Bottom, return this.

      Otherwise lub is computed as follows:

      1. Create the intersection of the sets of arrays for this and other.

      2. For each sequence in the intersection, get the offsets for this and other. If any offset in this is a less than or equal to an offset in other, then that offset is an offset for the sequence in lub. If any offset in other is a less than or equal to an offset in this, then that offset is an offset for the sequence in lub.

      Specified by:
      lub in class UBQualifier
      Parameters:
      other - to lub with this
      Returns:
      the lub

    • widenUpperBound

      public UBQualifier widenUpperBound(UBQualifier obj)
      Overrides:
      widenUpperBound in class UBQualifier

    • glb

      public UBQualifier glb(UBQualifier other)
      Specified by:
      glb in class UBQualifier

    • plusOffset

      public UBQualifier plusOffset(Node node, UpperBoundAnnotatedTypeFactory factory)
      Adds node as an offset to a copy of this qualifier. This is done by creating an offset equation for node and then adding that equation to every offset equation in a copy of this object.
      Overrides:
      plusOffset in class UBQualifier
      Parameters:
      node - a Node
      factory - an AnnotatedTypeFactory
      Returns:
      a copy of this qualifier with node add as an offset

    • minusOffset

      public UBQualifier minusOffset(Node node, UpperBoundAnnotatedTypeFactory factory)
      Adds node as a negative offset to a copy of this qualifier. This is done by creating a negative offset equation for node and then adding that equation to every offset equation in a copy of this object.
      Overrides:
      minusOffset in class UBQualifier
      Parameters:
      node - a Node
      factory - an AnnotatedTypeFactory
      Returns:
      a copy of this qualifier with node add as an offset

    • plusOffset

      public UBQualifier plusOffset(int value)
      Adds value as an offset to a copy of this qualifier. This is done by adding value to every offset equation in a copy of this object.
      Overrides:
      plusOffset in class UBQualifier
      Parameters:
      value - int value to add
      Returns:
      a copy of this qualifier with value add as an offset

    • minusOffset

      public UBQualifier minusOffset(int value)
      Adds the negation of value as an offset to a copy of this qualifier. This is done by adding the negation of value to every offset equation in a copy of this object.
      Overrides:
      minusOffset in class UBQualifier
      Parameters:
      value - int value to add
      Returns:
      a copy of this qualifier with value add as an offset

    • removeSequenceLengthAccess

      public UBQualifier removeSequenceLengthAccess(List<String> sequences)
      Returns a copy of this qualifier with sequence-offset pairs where in the original the offset contains an access of an sequence length in sequences. The sequence length access has been removed from the offset. If the original qualifier has no sequence length offsets, then UNKNOWN is returned.
      Parameters:
      sequences - access of the length of these sequences are removed
      Returns:
      a copy of this qualifier with some offsets removed

    • removeSequenceLengthAccessAndNeg1

      public UBQualifier removeSequenceLengthAccessAndNeg1(List<String> sequences)
      Returns a copy of this qualifier with sequence-offset pairs where in the original the offset contains an access of an sequence length in sequences. The sequence length access has been removed from the offset. If the offset also has -1 then -1 is also removed.
      Parameters:
      sequences - access of the length of these sequences are removed
      Returns:
      a copy of this qualifier with some offsets removed

    • divide

      public UBQualifier divide(int divisor)
      If divisor == 1, return this object.

      If divisor greater than 1, then return a copy of this object keeping only sequences and offsets where the offset is less than or equal to zero.

      Otherwise, return UNKNOWN.

      Parameters:
      divisor - number to divide by
      Returns:
      the result of dividing a value with this qualifier by divisor

    • isValuePlusOffsetLessThanMinLen

      public boolean isValuePlusOffsetLessThanMinLen(String sequence, long value, int minlen)

    • isValidReplacement

      public boolean isValidReplacement(String sequence, String replacementSequence, UBQualifier.LessThanLengthOf other)
      Returns true if replacing sequence with replacementSequence in this qualifier creates replacementSequence entry in other.

    • toString

      public String toString()
      Overrides:
      toString in class Object

    • getSequences

      public Iterable<? extends String> getSequences()

    • removeOffset

      public UBQualifier removeOffset(String sequence, int offset)
      Generates a new UBQualifer without the given (sequence, offset) pair. Other occurrences of the sequence and the offset may remain in the result, but not together.
      Parameters:
      sequence - a Java expression representing a string
      offset - an integral offset
      Returns:
      a new UBQualifer without the given sequence and offset