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 java.lang.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.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	UBQualifier.LessThanLengthOf	The less-than-length-of qualifier (@LTLengthOf).
static class	UBQualifier.UpperBoundLiteralQualifier	Represents an integer value that is known at compile time.
static class	UBQualifier.UpperBoundUnknownQualifier	The top type qualifier.

Constructor Summary

Constructors

Constructor	Description
UBQualifier()

Method Summary

Modifier and Type	Method	Description
static UBQualifier	createUBQualifier(java.lang.String sequence, java.lang.String offset)
static UBQualifier	createUBQualifier(java.util.List<java.lang.String> sequences, java.util.List<java.lang.String> offsets)	Creates an UBQualifier from the given sequences and offsets.
static UBQualifier	createUBQualifier(java.util.List<java.lang.String> sequences, java.util.List<java.lang.String> offsets, @Nullable java.lang.String extraOffset)	Creates an UBQualifier from the given sequences and offsets, with the given additional offset.
static UBQualifier	createUBQualifier(javax.lang.model.element.AnnotationMirror am, @Nullable java.lang.String offset, UpperBoundChecker ubChecker)	Create a UBQualifier from the given annotation, with an extra offset.
static UBQualifier	createUBQualifier(javax.lang.model.element.AnnotationMirror am, UpperBoundChecker ubChecker)	Create a UBQualifier from the given annotation.
static UBQualifier	createUBQualifier(AnnotatedTypeMirror type, javax.lang.model.element.AnnotationMirror top, UpperBoundChecker ubChecker)	Create an upper bound qualifier.
abstract UBQualifier	glb(UBQualifier other)
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	isBottom()	Returns true if this UBQualifier is the bottom type.
boolean	isLessThanLengthOf(java.lang.String sequence)	Is the value with this qualifier less than the length of sequence?
boolean	isLessThanLengthOfAny(java.util.List<java.lang.String> sequences)	Is the value with this qualifier less than the length of any of the sequences?
boolean	isLessThanLengthQualifier()
boolean	isLessThanOrEqualTo(java.lang.String sequence)	Is the value with this qualifier less than or equal to the length of sequence?
boolean	isLiteral()	Returns true if this UBQualifier represents a literal integer.
boolean	isPoly()	Return true if this is UBQualifier.PolyQualifier.
abstract boolean	isSubtype(UBQualifier superType)
boolean	isUnknown()	Returns true if this UBQualifier is the top type.
abstract UBQualifier	lub(UBQualifier other)
UBQualifier	minusOffset(int value)
UBQualifier	minusOffset(Node node, UpperBoundAnnotatedTypeFactory factory)
UBQualifier	plusOffset(int value)
UBQualifier	plusOffset(Node node, UpperBoundAnnotatedTypeFactory factory)	Add the node as an offset to a copy of this qualifier.
UBQualifier	widenUpperBound(UBQualifier obj)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

UBQualifier

public UBQualifier()

Method Detail

createUBQualifier

public static UBQualifier createUBQualifier(javax.lang.model.element.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(javax.lang.model.element.AnnotationMirror am,
                                            @Nullable java.lang.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(java.lang.String sequence,
                                            java.lang.String offset)

createUBQualifier

public static UBQualifier createUBQualifier(AnnotatedTypeMirror type,
                                            javax.lang.model.element.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(java.util.List<java.lang.String> sequences,
                                            java.util.List<java.lang.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(java.util.List<java.lang.String> sequences,
                                            java.util.List<java.lang.String> offsets,
                                            @Nullable java.lang.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(java.lang.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(java.util.List<java.lang.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(java.lang.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(java.lang.String sequence,
                                     java.lang.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(java.lang.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