org.checkerframework.checker.index.upperbound

Class UBQualifier

java.lang.Object

org.checkerframework.checker.index.upperbound.UBQualifier

Direct Known Subclasses:

UBQualifier.LessThanLengthOf, UBQualifier.UpperBoundUnknownQualifier

public abstract class UBQualifier
extends Object

Abstraction for Upper Bound annotations.

UpperBoundUnknown is modeled as UBQualifier.UpperBoundUnknownQualifier and UpperBoundBottom is modeled as UBQualifier.UpperBoundBottomQualifier.

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 and Description
static class	UBQualifier.LessThanLengthOf The less-than-length-of qualifier (@LTLengthOf).
static class	UBQualifier.UpperBoundUnknownQualifier

Constructor Summary

Constructors

Constructor and Description
UBQualifier()

Method Summary

Modifier and Type	Method and Description
static UBQualifier	createUBQualifier(AnnotatedTypeMirror type, AnnotationMirror top)
static UBQualifier	createUBQualifier(AnnotationMirror am) Create a UBQualifier from the given annotation.
static UBQualifier	createUBQualifier(AnnotationMirror am, String offset) Create a UBQualifier from the given annotation, with an extra offset.
static UBQualifier	createUBQualifier(List<String> sequences, List<String> offsets) Creates an UBQualifier from the given sequences and offsets.
static UBQualifier	createUBQualifier(List<String> sequences, List<String> offsets, String extraOffset) Creates an UBQualifier from the given sequences and offsets, with the given additional offset.
static UBQualifier	createUBQualifier(String sequence, String offset)
abstract UBQualifier	glb(UBQualifier other)
boolean	hasSequenceWithOffset(String sequence, int offset) Returns whether or not this qualifier has sequence with the specified offset.
boolean	hasSequenceWithOffset(String sequence, String offset) Returns whether or not this qualifier has sequence with the specified offset.
boolean	isBottom()
boolean	isLessThanLengthOf(String sequence) Is the value with this qualifier less than the length of sequence?
boolean	isLessThanLengthOfAny(List<String> sequences) Is the value with this qualifier less than the length of any of the sequences?
boolean	isLessThanLengthQualifier()
boolean	isLessThanOrEqualTo(String sequence) Is the value with this qualifier less than or equal to the length of sequence?
boolean	isPoly() Return true if this is UBQualifier.PolyQualifier.
abstract boolean	isSubtype(UBQualifier superType)
boolean	isUnknown()
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(AnnotationMirror am)

Create a UBQualifier from the given annotation.

Parameters:

am - the annotation to turn into a UBQualifier

Returns:

a UBQualifier that represents the same information as the given annotation

createUBQualifier

public static UBQualifier createUBQualifier(AnnotationMirror am,
                                            String offset)

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

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)

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,
                                            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()

isUnknown

public boolean isUnknown()

isBottom

public boolean isBottom()

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