Package 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.

An OffsetEquation is mutable.

  • Field Details

    • ZERO

      public static final OffsetEquation ZERO
      The equation for 0 (zero).

    • NEG_1

      public static final OffsetEquation NEG_1
      The equation for -1.

    • ONE

      public static final OffsetEquation ONE
      The equation for 1.

  • Constructor Details

    • OffsetEquation

      protected OffsetEquation(OffsetEquation other)
      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

      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