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 java.lang.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
static class	UBQualifier.UpperBoundUnknownQualifier

Constructor Summary

Constructors

Constructor and Description
UBQualifier()

Method Summary

Modifier and Type	Method and Description
static UBQualifier	createUBQualifier(AnnotatedTypeMirror type, javax.lang.model.element.AnnotationMirror top)
static UBQualifier	createUBQualifier(javax.lang.model.element.AnnotationMirror am)
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.lang.String sequence, java.lang.String offset)
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	isBottom()
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	isPoly()
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(javax.lang.model.element.AnnotationMirror am)

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)

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

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

public boolean isPoly()

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

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