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).

Nested Class Summary

Nested classes/interfaces inherited from class org.checkerframework.checker.index.upperbound.UBQualifier

UBQualifier.LessThanLengthOf, UBQualifier.UpperBoundUnknownQualifier

Method Summary

Modifier and Type	Method and Description
javax.lang.model.element.AnnotationMirror	convertToAnnotation(javax.annotation.processing.ProcessingEnvironment env) Returns the AnnotationMirror that represents this qualifier.
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.
UBQualifier	divide(int divisor) If divisor == 1, return this object.
boolean	equals(java.lang.Object o)
java.lang.Iterable<? extends java.lang.String>	getSequences()
UBQualifier	glb(UBQualifier other)
int	hashCode()
boolean	hasSequenceWithOffset(java.lang.String sequence, int offset) Returns whether or not this qualifier has sequence with the specified offset.
boolean	hasSequenceWithOffset(java.lang.String sequence, java.lang.String offset) Returns whether or not this qualifier has sequence with the specified offset.
boolean	isLessThanLengthOf(java.lang.String sequence) Is a value with this type less than the length of the sequence?
boolean	isLessThanLengthOfAny(java.util.List<java.lang.String> sequences) Is a value with this type less than the length of any of the sequences?
boolean	isLessThanLengthQualifier()
boolean	isLessThanOrEqualTo(java.lang.String sequence) Is a value with this type less than or equal to the length of sequence?
boolean	isSubtype(UBQualifier superType) If superType is Unknown, return true.
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.
boolean	isValuePlusOffsetLessThanMinLen(java.lang.String sequence, long value, int minlen)
UBQualifier	lub(UBQualifier other) If other is Unknown, return Unknown.
UBQualifier	minusOffset(int value) Adds the negation of value as an offset to a copy of this qualifier.
UBQualifier	minusOffset(Node node, UpperBoundAnnotatedTypeFactory factory) Adds node as a negative offset to a copy of this qualifier.
UBQualifier	plusOffset(int value) Adds value as an offset to a copy of this qualifier.
UBQualifier	plusOffset(Node node, UpperBoundAnnotatedTypeFactory factory) Adds node as an offset to a copy of this qualifier.
UBQualifier	removeOffset(java.lang.String sequence, int offset) Generates a new UBQualifer without the given sequence and offset.
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.
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.
java.lang.String	toString()
UBQualifier	widenUpperBound(UBQualifier obj)

Methods inherited from class org.checkerframework.checker.index.upperbound.UBQualifier

createUBQualifier, createUBQualifier, createUBQualifier, createUBQualifier, createUBQualifier, createUBQualifier, isBottom, isPoly, isUnknown

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

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(java.lang.Object o)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.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, this qualifier must contain all the sequences in superType. For each the offsets for each sequence in superType, there must be 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

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 - 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 - 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 and offset.