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

Class IntValue

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,Integer>
de.uzl.its.swat.symbolic.value.primitive.numeric.integral.IntValue
public class IntValue extends NumericalValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Integer>
IntValue contains a pair of concrete value and a path constraint. Note that the path constraint flip the boolean signs according to the evaluated concrete value.

  • Constructor Details

    • IntValue

      public IntValue(org.sosy_lab.java_smt.api.SolverContext context, int concrete)
      Instantiates a new Int value.
      Parameters:
      context - the context
      concrete - the concrete

    • IntValue

      public IntValue(org.sosy_lab.java_smt.api.SolverContext context, int concrete, org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula formula)
      Instantiates a new Int value.
      Parameters:
      context - the context
      concrete - the concrete
      formula - the formula

  • Method Details

    • MAKE_SYMBOLIC

      public String MAKE_SYMBOLIC(String namePrefix)
      Turns this IntValue into a symbolic variable
      Overrides:
      MAKE_SYMBOLIC in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Integer>
      Parameters:
      namePrefix -
      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,Integer>
      Parameters:
      idx -
      Returns:
      The numerical identifier of this symbolic variable

    • MAKE_SYMBOLIC

      public String MAKE_SYMBOLIC()
      Turns this IntValue into a symbolic variable
      Overrides:
      MAKE_SYMBOLIC in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Integer>
      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,Integer>
      Parameters:
      upper - If the upper or lower bound should be created
      Returns:
      The BooleanFormula that represents the bounds check

    • checkPositive

      public org.sosy_lab.java_smt.api.BooleanFormula checkPositive()
      Creates a formula that asserts that a value is positive
      Returns:
      The BooleanFormula that represents the check

    • IADD

      public IntValue IADD(IntValue i)
      Adds two integers
      Parameters:
      i - The other IntValue
      Returns:
      The resulting IntValue

    • ISUB

      public IntValue ISUB(IntValue i)
      Subtracts two integers
      Parameters:
      i - The other IntValue
      Returns:
      The resulting IntValue

    • IMUL

      public IntValue IMUL(IntValue i)
      Multiplies two integers
      Parameters:
      i - The other IntValue
      Returns:
      The resulting IntValue

    • IDIV

      public IntValue IDIV(IntValue i)
      Divides two integers
      Parameters:
      i - The other IntValue
      Returns:
      The resulting IntValue

    • IREM

      public IntValue IREM(IntValue i)
      Calculates the modulo of two integers
      Parameters:
      i - The other IntValue
      Returns:
      The resulting IntValue

    • INEG

      public IntValue INEG()
      Negates an integer
      Returns:
      The resulting IntValue

    • IINC

      public IntValue IINC(int increment)
      Increments an integer
      Parameters:
      increment - The amount to increment
      Returns:
      The incremented IntValue

    • IAND

      public IntValue IAND(IntValue i)
      Calculates the bitwise and of two integers in binary representation
      Parameters:
      i - The other IntValue
      Returns:
      The resulting IntValue

    • ISHL

      public IntValue ISHL(IntValue i)
      Calculates the bitwise left shift of an integer
      Parameters:
      i - The amount to shift
      Returns:
      The resulting IntValue

    • ISHR

      public IntValue ISHR(IntValue i)
      Calculates the bitwise arithmetic right shift of an integer
      Parameters:
      i - The amount to shift
      Returns:
      The resulting IntValue

    • IUSHR

      public IntValue IUSHR(IntValue i)
      Calculates the bitwise logical right shift of an integer
      Parameters:
      i - The amount to shift
      Returns:
      The resulting IntValue

    • IOR

      public IntValue IOR(IntValue i)
      Calculates the bitwise or of two integers
      Parameters:
      i - The other IntValue
      Returns:
      The resulting IntValue

    • IXOR

      public IntValue IXOR(IntValue i)
      Calculates the bitwise exclusive or of two integers
      Parameters:
      i - The other IntValue
      Returns:
      The resulting IntValue

    • IFEQ

      public org.sosy_lab.java_smt.api.BooleanFormula IFEQ()
      Checks if the current Value is 0
      Returns:
      A BooleanFormula that represents this check

    • IFGE

      public org.sosy_lab.java_smt.api.BooleanFormula IFGE()
      Checks if the current Value is greater or equal to 0
      Returns:
      A BooleanFormula that represents this check

    • IFGT

      public org.sosy_lab.java_smt.api.BooleanFormula IFGT()
      Checks if the current Value is greater then 0
      Returns:
      A BooleanFormula that represents this check

    • IFLE

      public org.sosy_lab.java_smt.api.BooleanFormula IFLE()
      Checks if the current Value is less or equal to 0
      Returns:
      A BooleanFormula that represents this check

    • IFLT

      public org.sosy_lab.java_smt.api.BooleanFormula IFLT()
      Checks if the current Value is greater then 0
      Returns:
      A BooleanFormula that represents this check

    • IFNE

      public org.sosy_lab.java_smt.api.BooleanFormula IFNE()
      Checks if the current Value is not equal to 0
      Returns:
      A BooleanFormula that represents this check

    • IF_ICMPEQ

      public org.sosy_lab.java_smt.api.BooleanFormula IF_ICMPEQ(IntValue i)
      Checks if the two integers are equal
      Parameters:
      i - The other IntValue
      Returns:
      A BooleanFormula that represents this check

    • IF_ICMPGE

      public org.sosy_lab.java_smt.api.BooleanFormula IF_ICMPGE(IntValue i)
      Checks if the integer is greater or equal to the second integer
      Parameters:
      i - The other IntValue
      Returns:
      A BooleanFormula that represents this check

    • IF_ICMPGT

      public org.sosy_lab.java_smt.api.BooleanFormula IF_ICMPGT(IntValue i)
      Checks if the integer is greater than the second integer
      Parameters:
      i - The other IntValue
      Returns:
      A BooleanFormula that represents this check

    • IF_ICMPLE

      public org.sosy_lab.java_smt.api.BooleanFormula IF_ICMPLE(IntValue i)
      Checks if the integer is less or equal to the second integer
      Parameters:
      i - The other IntValue
      Returns:
      A BooleanFormula that represents this check

    • IF_ICMPLT

      public org.sosy_lab.java_smt.api.BooleanFormula IF_ICMPLT(IntValue i)
      Checks if the integer is less than the second integer
      Parameters:
      i - The other IntValue
      Returns:
      A BooleanFormula that represents this check

    • IF_ICMPNE

      public org.sosy_lab.java_smt.api.BooleanFormula IF_ICMPNE(IntValue i)
      Checks if the two integers are not equal
      Parameters:
      i - The other IntValue
      Returns:
      A BooleanFormula that represents this check

    • I2D

      public DoubleValue I2D()
      Converts an IntValue into a DoubleValue
      Returns:
      The resulting DoubleValue

    • I2F

      public FloatValue I2F()
      Converts an IntValue into a FloatValue
      Returns:
      The resulting FloatValue

    • I2L

      public LongValue I2L()
      Converts an IntValue into a LongValue
      Returns:
      The resulting LongValue

    • I2B

      public ByteValue I2B()
      Converts an IntValue into a ByteValue
      Returns:
      The resulting ByteValue

    • I2C

      public CharValue I2C()
      Converts an IntValue into a CharValue ToDo (Nils): Symbolic information is lost! See: Issue 60
      Returns:
      The resulting CharValue

    • I2S

      public ShortValue I2S()
      Converts an IntValue into a ShortValue
      Returns:
      The resulting ShortValue

    • checkZero

      public org.sosy_lab.java_smt.api.BooleanFormula checkZero()

    • asIntValue

      public IntValue asIntValue()
      Overrides:
      asIntValue in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Integer>

    • asCharValue

      public CharValue asCharValue()
      Overrides:
      asCharValue in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Integer>

    • asBooleanValue

      public BooleanValue asBooleanValue()
      Overrides:
      asBooleanValue in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Integer>

    • asLongValue

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

    • asShortValue

      public ShortValue asShortValue()
      Overrides:
      asShortValue in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Integer>

    • asByteValue

      public ByteValue asByteValue()
      Overrides:
      asByteValue in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Integer>

    • asStringValue

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

    • asNumericalValue

      public NumericalValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Integer> asNumericalValue()
      Overrides:
      asNumericalValue in class Value<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,Integer>

    • getConcreteEncoded

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

    • 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,Integer>
      Returns:
      the string representation of the value.