Package org.checkerframework.checker.index.upperbound

Class UBQualifier.LessThanLengthOf

  • Enclosing class:
    UBQualifier
    public static class UBQualifier.LessThanLengthOf
extends UBQualifier
    The less-than-length-of qualifier (@LTLengthOf).

    • Method Detail

      • hasSequenceWithOffset

        public boolean hasSequenceWithOffset​(java.lang.String sequence,
                                     int offset)
        Description copied from class: UBQualifier
        Returns whether or not this qualifier has sequence with the specified offset.
        Overrides:
        hasSequenceWithOffset in class UBQualifier
        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​(java.lang.String sequence,
                                     java.lang.String offset)
        Description copied from class: UBQualifier
        Returns whether or not this qualifier has sequence with the specified offset.
        Overrides:
        hasSequenceWithOffset in class UBQualifier
        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​(java.lang.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​(java.util.List<java.lang.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​(java.lang.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 javax.lang.model.element.AnnotationMirror convertToAnnotation​(javax.annotation.processing.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 javax.lang.model.element.AnnotationMirror convertToSubstringIndexAnnotation​(javax.annotation.processing.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 java.lang.Object o)
        Overrides:
        equals in class java.lang.Object

      • hashCode

        public int hashCode()
        Overrides:
        hashCode in class java.lang.Object

      • 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:
        whether 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

      • 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​(java.util.List<java.lang.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​(java.util.List<java.lang.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​(java.lang.String sequence,
                                               long value,
                                               int minlen)

      • isValidReplacement

        public boolean isValidReplacement​(java.lang.String sequence,
                                  java.lang.String replacementSequence,
                                  UBQualifier.LessThanLengthOf other)
        Checks whether replacing sequence with replacementSequence in this qualifier creates replacementSequence entry in other.

      • toString

        public java.lang.String toString()
        Overrides:
        toString in class java.lang.Object

      • getSequences

        public java.lang.Iterable<? extends java.lang.String> getSequences()

      • removeOffset

        public UBQualifier removeOffset​(java.lang.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