Package org.checkerframework.checker.index

Class Subsequence

java.lang.Object

org.checkerframework.checker.index.Subsequence

public class Subsequence
extends java.lang.Object

Holds information from HasSubsequence annotations.

Field Summary

Fields

Modifier and Type	Field	Description
java.lang.String	array	Name of the Subsequence.
java.lang.String	from	First index of the subsequence in the backing sequence.
java.lang.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(com.sun.source.tree.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 java.lang.String	negateString(java.lang.String s)	Returns the additive inverse of the given String.
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

array

public final java.lang.String array

Name of the Subsequence.

from

public final java.lang.String from

First index of the subsequence in the backing sequence.

to

public final java.lang.String to

Last index of the subsequence in the backing sequence.

Method Detail

getSubsequenceFromTree

public static @Nullable Subsequence getSubsequenceFromTree(com.sun.source.tree.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 java.lang.String negateString(java.lang.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 java.lang.String toString()

Overrides:

toString in class java.lang.Object