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 and Description
String	array Name of the Subsequence.
String	from First index of the subsequence in the backing sequence.
String	to Last index of the subsequence in the backing sequence.

Method Summary

Modifier and Type	Method and Description
static 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 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 Detail

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 Detail

getSubsequenceFromTree

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