Package org.checkerframework.checker.index

Class Subsequence

java.lang.Object

org.checkerframework.checker.index.Subsequence

public class Subsequence
extends Object

Holds information from HasSubsequence annotations.

Field Summary

Fields

Modifier and Type	Field	Description
final String	array	Name of the Subsequence.
final String	from	First index of the subsequence in the backing sequence.
final String	to	Last index of the subsequence in the backing sequence.

Method Summary

Modifier and Type	Method	Description
static @Nullable Subsequence	getSubsequenceFromReceiver(JavaExpression expr, BaseAnnotatedTypeFactoryForIndexChecker factory)	Returns a Subsequence representing the HasSubsequence annotation on the declaration of rec or null if there is not such annotation.
static @Nullable Subsequence	getSubsequenceFromTree(Tree varTree, BaseAnnotatedTypeFactoryForIndexChecker factory)	Returns a Subsequence representing the HasSubsequence annotation on the declaration of varTree or null if there is not such annotation.
static String	negateString(String s)	Returns the additive inverse of the given String.
String	toString()

Methods inherited from class java.lang.Object

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

Field Details

array

public final String array

Name of the Subsequence.

from

public final String from

First index of the subsequence in the backing sequence.

to

public final String to

Last index of the subsequence in the backing sequence.

Method Details

getSubsequenceFromTree

public static @Nullable Subsequence getSubsequenceFromTree(Tree varTree,
 BaseAnnotatedTypeFactoryForIndexChecker factory)

Returns a Subsequence representing the HasSubsequence annotation on the declaration of varTree or null if there is not such annotation.

Note that this method does not standardize or viewpoint adapt the arguments to the annotation, unlike getSubsequenceFromReceiver.

Parameters:

varTree - some tree

factory - an AnnotatedTypeFactory

Returns:

null or a new Subsequence from the declaration of varTree

getSubsequenceFromReceiver

public static @Nullable Subsequence getSubsequenceFromReceiver(JavaExpression expr,
 BaseAnnotatedTypeFactoryForIndexChecker factory)

Returns a Subsequence representing the HasSubsequence annotation on the declaration of rec or null if there is not such annotation.

Parameters:

expr - some tree

factory - an AnnotatedTypeFactory

Returns:

null or a new Subsequence from the declaration of varTree

negateString

public static String negateString(String s)

Returns the additive inverse of the given String. That is, if the result of this method is some String s', then s + s' == 0 will evaluate to true. Note that this relies on the fact that the JavaExpression parser cannot parse multiplication, so it naively just changes '-' to '+' and vice-versa.

Parameters:

s - a Java expression string

Returns:

the negated string

toString

public String toString()

Overrides:

toString in class Object