Package de.uzl.its.swat.symbolic.value.primitive.numeric.integral

Class LongValue

java.lang.Object
de.uzl.its.swat.symbolic.value.Value<T,K>
de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Long>
de.uzl.its.swat.symbolic.value.primitive.numeric.integral.LongValue
public class LongValue extends NumericalValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Long>
Wrapper for longs to represent symbolic and concrete information on the symbolic stack

  • Constructor Details

    • LongValue

      public LongValue(org.sosy_lab.java_smt.api.SolverContext context, long concrete)
      Creates a LongValue without symbolic information but a concrete value.
      Parameters:
      context - The SolverContext to create formulas in the native Solver environment.
      concrete - The concrete (long) value.

    • LongValue

      public LongValue(org.sosy_lab.java_smt.api.SolverContext context, long concrete, org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula formula)
      Creates a LongValue with prior symbolic information and a concrete value.
      Parameters:
      context - The SolverContext to create formulas in the native Solver environment.
      concrete - The concrete (long) value.
      formula - The formula representing the symbolic information.

  • Method Details

    • MAKE_SYMBOLIC

      public String MAKE_SYMBOLIC(String namePrefix)
      Turns this LongValue into a symbolic variable
      Overrides:
      MAKE_SYMBOLIC in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Long>
      Parameters:
      namePrefix -
      Returns:
      The numerical identifier of this symbolic variable

    • MAKE_SYMBOLIC

      public String MAKE_SYMBOLIC()
      Turns this LongValue into a symbolic variable
      Overrides:
      MAKE_SYMBOLIC in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Long>
      Returns:
      The numerical identifier of this symbolic variable

    • MAKE_SYMBOLIC

      public String MAKE_SYMBOLIC(long idx)
      Turns this IntValue into a symbolic variable
      Overrides:
      MAKE_SYMBOLIC in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Long>
      Parameters:
      idx -
      Returns:
      The numerical identifier of this symbolic variable

    • getBounds

      public org.sosy_lab.java_smt.api.BooleanFormula getBounds(boolean upper)
      Creates a formula that asserts that this symbolic value is withing the bounds of this type
      Overrides:
      getBounds in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Long>
      Parameters:
      upper - If the upper or lower bound should be created
      Returns:
      The BooleanFormula that represents the bounds check

    • LADD

      public LongValue LADD(LongValue l)
      Adds two longs
      Parameters:
      l - The other LongValue
      Returns:
      The resulting LongValue

    • checkZero

      public org.sosy_lab.java_smt.api.BooleanFormula checkZero()
      Creates a BooleanFormula that asserts that a value is not zero
      Returns:
      The resulting BooleanFormula

    • LAND

      public LongValue LAND(LongValue l)
      Calculates the bitwise and of two longs in binary representation
      Parameters:
      l - The other LongValue
      Returns:
      The resulting LongValue

    • LDIV

      public LongValue LDIV(LongValue l)
      Divides two longs
      Parameters:
      l - The other LongValue
      Returns:
      The resulting LongValue

    • LMUL

      public LongValue LMUL(LongValue l)
      Multiplies two longs
      Parameters:
      l - The other LongValue
      Returns:
      The resulting LongValue

    • LNEG

      public LongValue LNEG()
      Negates a long
      Returns:
      The resulting LongValue

    • LOR

      public LongValue LOR(LongValue l)
      Calculates the bitwise or of two longs
      Parameters:
      l - The other LongValue
      Returns:
      The resulting LongValue

    • LREM

      public LongValue LREM(LongValue l)
      Calculates the modulo of two longs
      Parameters:
      l - The other LongValue
      Returns:
      The resulting IntValue

    • LSHL

      public LongValue LSHL(IntValue i)
      Calculates the bitwise left shift of a long
      Parameters:
      i - The amount to shift
      Returns:
      The resulting LongValue

    • LSHR

      public LongValue LSHR(IntValue i)
      Calculates the bitwise arithmetic right shift of a long
      Parameters:
      i - The amount to shift
      Returns:
      The resulting LongValue

    • LSUB

      public LongValue LSUB(LongValue l)
      Subtracts two longs
      Parameters:
      l - The other LongValue
      Returns:
      The resulting LongValue

    • LUSHR

      public LongValue LUSHR(IntValue i)
      Calculates the bitwise logical right shift of a long
      Parameters:
      i - The amount to shift
      Returns:
      The resulting LongValue

    • LXOR

      public LongValue LXOR(LongValue l)
      Calculates the bitwise exclusive or of two longs
      Parameters:
      l - The other LongValue
      Returns:
      The resulting IntValue

    • LCMP

      public IntValue LCMP(LongValue l)
      Compares two longs and returns: 0 if both values are equal 1 if this long is greater -1 if the parameter is greater ToDo (Nils): This method is not validated
      Parameters:
      l - The other LongValueValue
      Returns:
      The resulting IntValue with the boolean conditions

    • L2D

      public DoubleValue L2D()
      Converts a long into a double
      Returns:
      The resulting DoubleValue

    • L2F

      public FloatValue L2F()
      Converts a long into a float
      Returns:
      The resulting FloatValue

    • L2I

      public IntValue L2I()
      Converts a long into an int
      Returns:
      The resulting IntValue

    • asLongValue

      public LongValue asLongValue()
      Overrides:
      asLongValue in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Long>

    • asStringValue

      public StringValue asStringValue()
      Overrides:
      asStringValue in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Long>

    • getConcreteEncoded

      public String getConcreteEncoded()
      Overrides:
      getConcreteEncoded in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Long>

    • toString

      public String toString()
      Returns the string representation of the value used to visualize the stack. The representation is not complete.
      Overrides:
      toString in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Long>
      Returns:
      the string representation of the value.