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

Class ArrayArrayValue<TE extends org.sosy_lab.java_smt.api.Formula>

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,TE,IntValue,AbstractArrayValue<?,?,?,?,?>,ArrayList<AbstractArrayValue>>

de.uzl.its.swat.symbolic.value.reference.array.ArrayArrayValue<TE>

public class ArrayArrayValue<TE extends org.sosy_lab.java_smt.api.Formula>
extends AbstractArrayValue<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,TE,IntValue,AbstractArrayValue<?,?,?,?,?>,ArrayList<AbstractArrayValue>>

Field Summary

Fields

Modifier and Type	Field	Description
String	desc
IntValue	size

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

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

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
ArrayArrayValue(org.sosy_lab.java_smt.api.SolverContext context, IntValue[] dims, int address, org.sosy_lab.java_smt.api.FormulaType elementFormulaType, String desc, IntValue parentRefIdx, ArrayArrayValue parentRef)

Method Summary

Modifier and Type	Method	Description
static ArrayArrayValue	arrayMagic(org.sosy_lab.java_smt.api.SolverContext context, String desc, IntValue[] dims)
AbstractArrayValue<?,?,?,?,?>	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.
void	storeElement(IntValue idx, AbstractArrayValue val)	Stores the formula representing an element at the position specified by the index formula.
String	toString()	Returns the string representation of the value.
void	updateFormula(IntValue idx, TE val)

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

asArrayValue, asBooleanArrayValue, asByteArrayValue, asCharArrayValue, asDoubleArrayValue, asFloatArrayValue, asIntArrayValue, 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

Field Details

size

public IntValue size

desc

public String desc

Constructor Details

ArrayArrayValue

public ArrayArrayValue(org.sosy_lab.java_smt.api.SolverContext context,
 IntValue[] dims,
 int address,
 org.sosy_lab.java_smt.api.FormulaType elementFormulaType,
 String desc,
 IntValue parentRefIdx,
 ArrayArrayValue parentRef)

Method Details

arrayMagic

public static ArrayArrayValue arrayMagic(org.sosy_lab.java_smt.api.SolverContext context,
 String desc,
 IntValue[] dims)

getElement

public AbstractArrayValue<?,?,?,?,?> 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,TE extends org.sosy_lab.java_smt.api.Formula,IntValue,AbstractArrayValue<?,?,?,?,?>,ArrayList<AbstractArrayValue>>

Parameters:

idx - The formula that specifies the index.

Returns:

The formula that specifies the retrieved/ retrievable element.

updateFormula

public void updateFormula(IntValue idx,
 TE val)

storeElement

public void storeElement(IntValue idx,
 AbstractArrayValue 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,TE extends org.sosy_lab.java_smt.api.Formula,IntValue,AbstractArrayValue<?,?,?,?,?>,ArrayList<AbstractArrayValue>>

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,TE extends org.sosy_lab.java_smt.api.Formula,IntValue,AbstractArrayValue<?,?,?,?,?>,ArrayList<AbstractArrayValue>>

Parameters:

size - The size of the array.

toString

public String toString()

Description copied from class: Value

Returns the string representation of the value. Should be implemented by each inheriting class.

Overrides:

toString in class ObjectValue<org.sosy_lab.java_smt.api.ArrayFormula<org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula,TE extends org.sosy_lab.java_smt.api.Formula>,ArrayList<AbstractArrayValue>>

Returns:

the string representation of the value