Package de.uzl.its.swat.symbolic.value.reference.array

Class IntArrayValue

java.lang.Object

de.uzl.its.swat.symbolic.value.Value<T,K>

de.uzl.its.swat.symbolic.value.reference.ObjectValue<org.sosy_lab.java_smt.api.ArrayFormula<TI,TE>,K>

de.uzl.its.swat.symbolic.value.reference.array.AbstractArrayValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,IntValue,IntValue,int[]>

de.uzl.its.swat.symbolic.value.reference.array.IntArrayValue

public class IntArrayValue
extends AbstractArrayValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,IntValue,IntValue,int[]>

Wrapper for Arrays that contain integer values.

Field Summary

Fields inherited from class de.uzl.its.swat.symbolic.value.reference.array.AbstractArrayValue

amgr, context, elementFormulaType, formulaType, indexFormulaType, parentRef, parentRefIdx, size

Fields inherited from class de.uzl.its.swat.symbolic.value.reference.ObjectValue

address, ADDRESS_UNKNOWN, className

Fields inherited from class de.uzl.its.swat.symbolic.value.Value

concrete, formula, inc, name, symbol

Constructor Summary

Constructors

Constructor	Description
IntArrayValue(org.sosy_lab.java_smt.api.SolverContext context, int[] concrete, int address)
IntArrayValue(org.sosy_lab.java_smt.api.SolverContext context, IntValue size, int address)
IntArrayValue(org.sosy_lab.java_smt.api.SolverContext context, IntValue size, int address, IntValue parentRefIdx, ArrayArrayValue parentRef)

Method Summary

Modifier and Type	Method	Description
AbstractArrayValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,IntValue,IntValue,int[]>	asArrayValue()
IntArrayValue	asIntArrayValue()
IntValue	getElement(IntValue idx)	Returns the formula that represents the element at the specified index.
protected void	initArray(int size)	Initializes the array with the default value.
protected void	initArray(int[] array)
void	storeElement(IntValue idx, IntValue val)	Stores the formula representing an element at the position specified by the index formula.
String	toString()	Returns the string representation of the value used to visualize the stack.

Methods inherited from class de.uzl.its.swat.symbolic.value.reference.array.AbstractArrayValue

asBooleanArrayValue, asByteArrayValue, asCharArrayValue, asDoubleArrayValue, asFloatArrayValue, asLongArrayValue, asObjectArrayValue, asShortArrayValue, checkIndex, genericToString, getContext

Methods inherited from class de.uzl.its.swat.symbolic.value.reference.ObjectValue

asFloatValue, asIntValue, asObjectValue, equals, getAddress, getConcrete, getField, getFields, getnFields, IF_ACMPEQ, IF_ACMPNE, IFNONNULL, IFNULL, invokeMethod, MAKE_SYMBOLIC, MAKE_SYMBOLIC, setAddress, setField, setFields

Methods inherited from class de.uzl.its.swat.symbolic.value.Value

asBooleanValue, asByteValue, asCharValue, asDoubleValue, asLongValue, asNumericalValue, asShortValue, asStringValue, getBounds, getConcreteEncoded, getName, getType, initSymbolic, initSymbolic, MAKE_SYMBOLIC, reset

Methods inherited from class java.lang.Object

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

Constructor Details

IntArrayValue

public IntArrayValue(org.sosy_lab.java_smt.api.SolverContext context,
 IntValue size,
 int address)

IntArrayValue

public IntArrayValue(org.sosy_lab.java_smt.api.SolverContext context,
 IntValue size,
 int address,
 IntValue parentRefIdx,
 ArrayArrayValue parentRef)

IntArrayValue

public IntArrayValue(org.sosy_lab.java_smt.api.SolverContext context,
 int[] concrete,
 int address)

Method Details

getElement

public IntValue getElement(IntValue idx)

Description copied from class: AbstractArrayValue

Returns the formula that represents the element at the specified index.

Specified by:

getElement in class AbstractArrayValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,IntValue,IntValue,int[]>

Parameters:

idx - The formula that specifies the index.

Returns:

The formula that specifies the retrieved/ retrievable element.

storeElement

public void storeElement(IntValue idx,
 IntValue val)

Description copied from class: AbstractArrayValue

Stores the formula representing an element at the position specified by the index formula.

Specified by:

storeElement in class AbstractArrayValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,IntValue,IntValue,int[]>

Parameters:

idx - The index formula.

val - The element formula.

initArray

protected void initArray(int size)

Description copied from class: AbstractArrayValue

Initializes the array with the default value.

Specified by:

initArray in class AbstractArrayValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,IntValue,IntValue,int[]>

Parameters:

size - The size of the array.

initArray

protected void initArray(int[] array)

asIntArrayValue

public IntArrayValue asIntArrayValue()

Overrides:

asIntArrayValue in class AbstractArrayValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,IntValue,IntValue,int[]>

asArrayValue

public AbstractArrayValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,IntValue,IntValue,int[]> asArrayValue()

Overrides:

asArrayValue in class AbstractArrayValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,IntValue,IntValue,int[]>

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 ObjectValue<org.sosy_lab.java_smt.api.ArrayFormula<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula>,int[]>

Returns:

the string representation of the value.