org.checkerframework.checker.index.upperbound

Class OffsetEquation

java.lang.Object

org.checkerframework.checker.index.upperbound.OffsetEquation

public class OffsetEquation
extends Object

An offset equation is 2 sets of Java expression strings, one set of added terms and one set of subtracted terms, and a single integer constant. The Java expression strings have been standardized and viewpoint-adapted.

Field Summary

Fields

Modifier and Type	Field and Description
static OffsetEquation	NEG_1
static OffsetEquation	ONE
static OffsetEquation	ZERO

Method Summary

Modifier and Type	Method and Description
OffsetEquation	copyAdd(char op, OffsetEquation other) Adds or subtracts the other equation to a copy of this one.
static OffsetEquation	createOffsetForInt(int value) Creates an offset equation that is only the int value specified.
static OffsetEquation	createOffsetFromJavaExpression(String expressionEquation) Creates an offset equation from the expressionEquation.
static OffsetEquation	createOffsetFromNode(Node node, AnnotationProvider factory, char op) Creates an offset equation from the Node.
static OffsetEquation	createOffsetFromNodesValue(Node node, ValueAnnotatedTypeFactory factory, char op) If node is an int value known at compile time, then the returned equation is just the int value or if op is '-', the return equation is the negation of the int value.
boolean	equals(@Nullable Object o)
String	getError()
int	getInt() Returns the int value associated with this equation.
static OffsetEquation	getIntOffsetEquation(Set<OffsetEquation> equationSet) Returns the offset equation that is an int value or null if there isn't one.
boolean	hasError()
int	hashCode()
boolean	isInt() Returns true if this equation is a single int value.
boolean	isNegativeOrZero() Returns true if this equation is negative or zero.
boolean	isNegOne() Returns true if this equation is exactly -1.
boolean	isNonNegative() Returns true if this equation non-negative.
boolean	lessThanOrEqual(OffsetEquation other) Returns whether or not this equation is known to be less than or equal to the other equation.
OffsetEquation	removeSequenceLengths(List<String> sequences) Makes a copy of this offset and removes any added terms that are accesses to the length of the listed sequences.
String	toString()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

ZERO

public static final OffsetEquation ZERO

NEG_1

public static final OffsetEquation NEG_1

ONE

public static final OffsetEquation ONE

Method Detail

hasError

public boolean hasError()

getError

public String getError()

equals

public boolean equals(@Nullable Object o)

Overrides:

equals in class Object

hashCode

public int hashCode()

Overrides:

hashCode in class Object

toString

public String toString()

Overrides:

toString in class Object

removeSequenceLengths

public OffsetEquation removeSequenceLengths(List<String> sequences)

Makes a copy of this offset and removes any added terms that are accesses to the length of the listed sequences. If any terms were removed, then the copy is returned. Otherwise, null is returned.

Parameters:

sequences - list of sequences (arrays or strings)

Returns:

a copy of this equation with array.length and string.length() removed or null if no array.lengths or string.length() could be removed

copyAdd

public OffsetEquation copyAdd(char op,
                              OffsetEquation other)

Adds or subtracts the other equation to a copy of this one.

If subtraction is specified, then every term in other is subtracted.

Parameters:

op - '-' for subtraction or '+' for addition

other - equation to add or subtract

Returns:

a copy of this equation +/- other

lessThanOrEqual

public boolean lessThanOrEqual(OffsetEquation other)

Returns whether or not this equation is known to be less than or equal to the other equation.

Parameters:

other - equation

Returns:

whether or not this equation is known to be less than or equal to the other equation

isInt

public boolean isInt()

Returns true if this equation is a single int value.

Returns:

true if this equation is a single int value

getInt

public int getInt()

Returns the int value associated with this equation.

The equation may or may not have other terms. Use isInt() to determine if the equation is only this int value.

Returns:

the int value associated with this equation

isNegOne

public boolean isNegOne()

Returns true if this equation is exactly -1.

Returns:

true if this equation is exactly -1

isNonNegative

public boolean isNonNegative()

Returns true if this equation non-negative.

Returns:

true if this equation non-negative

isNegativeOrZero

public boolean isNegativeOrZero()

Returns true if this equation is negative or zero.

Returns:

true if this equation is negative or zero

getIntOffsetEquation

public static OffsetEquation getIntOffsetEquation(Set<OffsetEquation> equationSet)

Returns the offset equation that is an int value or null if there isn't one.

Parameters:

equationSet - a set of offset equations

Returns:

the offset equation that is an int value or null if there isn't one

createOffsetForInt

public static OffsetEquation createOffsetForInt(int value)

Creates an offset equation that is only the int value specified.

Parameters:

value - int value of the equation

Returns:

an offset equation that is only the int value specified

createOffsetFromJavaExpression

public static OffsetEquation createOffsetFromJavaExpression(String expressionEquation)

Creates an offset equation from the expressionEquation. The expressionEquation may be several Java expressions added or subtracted from each other. The expressionEquation may also start with + or -. If the expressionEquation is the empty string, then the offset equation returned is zero.

Parameters:

expressionEquation - a Java expression made up of sums and differences

Returns:

an offset equation created from expressionEquation

createOffsetFromNodesValue

public static OffsetEquation createOffsetFromNodesValue(Node node,
                                                        ValueAnnotatedTypeFactory factory,
                                                        char op)

If node is an int value known at compile time, then the returned equation is just the int value or if op is '-', the return equation is the negation of the int value.

Otherwise, null is returned.

Parameters:

node - the Node from which to create an offset equation

factory - an AnnotationTypeFactory

op - '+' or '-'

Returns:

an offset equation from value of known or null if the value isn't known

createOffsetFromNode

public static OffsetEquation createOffsetFromNode(Node node,
                                                  AnnotationProvider factory,
                                                  char op)

Creates an offset equation from the Node.

If node is an addition or subtracted node, then this method is called recursively on the left and right hand nodes and the two equations are added/subtracted to each other depending on the value of op.

Otherwise the return equation is created by converting the node to a JavaExpression and then added as a term to the returned equation. If op is '-' then it is a subtracted term.

Parameters:

node - the Node from which to create an offset equation

factory - an AnnotationTypeFactory

op - '+' or '-'

Returns:

an offset equation from the Node