Class OffsetEquation
java.lang.Object
org.checkerframework.checker.index.upperbound.OffsetEquation
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 viewpointadapted.
An OffsetEquation is mutable.

Field Summary
Modifier and TypeFieldDescriptionstatic final OffsetEquation
The equation for 1.static final OffsetEquation
The equation for 1.static final OffsetEquation
The equation for 0 (zero). 
Constructor Summary
ModifierConstructorDescriptionprotected
OffsetEquation
(OffsetEquation other) Create a new OffsetEquation that is a copy of the given one. 
Method Summary
Modifier and TypeMethodDescriptioncopyAdd
(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 @Nullable 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
getError()
int
getInt()
Returns the int value associated with this equation.static @Nullable 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
Returns true if this equation is negative or zero.boolean
isNegOne()
Returns true if this equation is exactly 1.boolean
Returns true if this equation nonnegative.boolean
lessThanOrEqual
(OffsetEquation other) Returns whether or not this equation is known to be less than or equal to the other equation.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.toString()

Field Details

ZERO
The equation for 0 (zero). 
NEG_1
The equation for 1. 
ONE
The equation for 1.


Constructor Details

OffsetEquation
Create a new OffsetEquation that is a copy of the given one. Parameters:
other
 the OffsetEquation to copy


Method Details

hasError
public boolean hasError() 
getError

equals

hashCode
public int hashCode() 
toString

removeSequenceLengths
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
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 additionother
 equation to add or subtract Returns:
 a copy of this equation +/ other

lessThanOrEqual
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 nonnegative. Returns:
 true if this equation nonnegative

isNegativeOrZero
public boolean isNegativeOrZero()Returns true if this equation is negative or zero. Returns:
 true if this equation is negative or zero

getIntOffsetEquation
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
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
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 @Nullable 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 equationfactory
 an AnnotationTypeFactoryop
 '+' or '' Returns:
 an offset equation from value of known or null if the value isn't known

createOffsetFromNode
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 equationfactory
 an AnnotationTypeFactoryop
 '+' or '' Returns:
 an offset equation from the Node
