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

Class AbstractArrayValue<TI extends org.sosy_lab.java_smt.api.Formula,TE extends org.sosy_lab.java_smt.api.Formula,VI extends Value<?,?>,VE extends Value<?,?>,K>

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<TI,TE,VI,VE,K>

Direct Known Subclasses:

ArrayArrayValue, BooleanArrayValue, ByteArrayValue, CharArrayValue, DoubleArrayValue, FloatArrayValue, IntArrayValue, LongArrayValue, ShortArrayValue, StringArrayValue

public abstract class AbstractArrayValue<TI extends org.sosy_lab.java_smt.api.Formula,TE extends org.sosy_lab.java_smt.api.Formula,VI extends Value<?,?>,VE extends Value<?,?>,K>
extends ObjectValue<org.sosy_lab.java_smt.api.ArrayFormula<TI,TE>,K>

Abstract class for symbolic arrays.

Field Summary

Fields

Modifier and Type	Field	Description
protected org.sosy_lab.java_smt.api.ArrayFormulaManager	amgr	Java-smt formula manager for array theory
protected org.sosy_lab.java_smt.api.SolverContext	context	Solver context to interact with the native solver (used for creating formulas)
protected org.sosy_lab.java_smt.api.FormulaType<TE>	elementFormulaType	Formula type used for the elements of the symbolic array
protected org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType<TI,TE>	formulaType	Formula type representing the index - element pair
protected org.sosy_lab.java_smt.api.FormulaType<TI>	indexFormulaType	Formula type used for the indices of the symbolic array
protected ArrayArrayValue	parentRef
protected IntValue	parentRefIdx
IntValue	size	Integer wrapper that represents the size of the array

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
AbstractArrayValue(org.sosy_lab.java_smt.api.SolverContext context, org.sosy_lab.java_smt.api.FormulaType<TI> indexFormulaType, org.sosy_lab.java_smt.api.FormulaType<TE> elementFormulaType, IntValue size, int address)
AbstractArrayValue(org.sosy_lab.java_smt.api.SolverContext context, org.sosy_lab.java_smt.api.FormulaType<TI> indexFormulaType, org.sosy_lab.java_smt.api.FormulaType<TE> elementFormulaType, org.sosy_lab.java_smt.api.ArrayFormula<TI,TE> formula, IntValue size, int address)

Method Summary

Modifier and Type	Method	Description
AbstractArrayValue<TI,TE,VI,VE,K>	asArrayValue()
BooleanArrayValue	asBooleanArrayValue()
ByteArrayValue	asByteArrayValue()
CharArrayValue	asCharArrayValue()
DoubleArrayValue	asDoubleArrayValue()
FloatArrayValue	asFloatArrayValue()
IntArrayValue	asIntArrayValue()
LongArrayValue	asLongArrayValue()
ObjectArrayValue	asObjectArrayValue()
ShortArrayValue	asShortArrayValue()
org.sosy_lab.java_smt.api.BooleanFormula	checkIndex(IntValue idx)
String	genericToString(String type)
org.sosy_lab.java_smt.api.SolverContext	getContext()
abstract VE	getElement(IntValue idx)	Returns the formula that represents the element at the specified index.
protected abstract void	initArray(int size)	Initializes the array with the default value.
abstract void	storeElement(IntValue idx, VE val)	Stores the formula representing an element at the position specified by the index formula.

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, toString

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

amgr

protected org.sosy_lab.java_smt.api.ArrayFormulaManager amgr

Java-smt formula manager for array theory

context

protected org.sosy_lab.java_smt.api.SolverContext context

Solver context to interact with the native solver (used for creating formulas)

indexFormulaType

protected org.sosy_lab.java_smt.api.FormulaType<TI extends org.sosy_lab.java_smt.api.Formula> indexFormulaType

Formula type used for the indices of the symbolic array

elementFormulaType

protected org.sosy_lab.java_smt.api.FormulaType<TE extends org.sosy_lab.java_smt.api.Formula> elementFormulaType

Formula type used for the elements of the symbolic array

formulaType

protected org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType<TI extends org.sosy_lab.java_smt.api.Formula,TE extends org.sosy_lab.java_smt.api.Formula> formulaType

Formula type representing the index - element pair

size

public IntValue size

Integer wrapper that represents the size of the array

parentRefIdx

@Nullable
protected IntValue parentRefIdx

parentRef

@Nullable
protected ArrayArrayValue parentRef

Constructor Details

AbstractArrayValue

public AbstractArrayValue(org.sosy_lab.java_smt.api.SolverContext context,
 org.sosy_lab.java_smt.api.FormulaType<TI> indexFormulaType,
 org.sosy_lab.java_smt.api.FormulaType<TE> elementFormulaType,
 IntValue size,
 int address)

AbstractArrayValue

public AbstractArrayValue(org.sosy_lab.java_smt.api.SolverContext context,
 org.sosy_lab.java_smt.api.FormulaType<TI> indexFormulaType,
 org.sosy_lab.java_smt.api.FormulaType<TE> elementFormulaType,
 org.sosy_lab.java_smt.api.ArrayFormula<TI,TE> formula,
 IntValue size,
 int address)

Method Details

getElement

public abstract VE getElement(IntValue idx)

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

Parameters:

idx - The formula that specifies the index.

Returns:

The formula that specifies the retrieved/ retrievable element.

storeElement

public abstract void storeElement(IntValue idx,
 VE val)

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

Parameters:

idx - The index formula.

val - The element formula.

checkIndex

public org.sosy_lab.java_smt.api.BooleanFormula checkIndex(IntValue idx)

initArray

protected abstract void initArray(int size)

Initializes the array with the default value.

Parameters:

size - The size of the array.

asArrayValue

public AbstractArrayValue<TI,TE,VI,VE,K> asArrayValue()

Overrides:

asArrayValue in class ObjectValue<org.sosy_lab.java_smt.api.ArrayFormula<TI extends org.sosy_lab.java_smt.api.Formula,TE extends org.sosy_lab.java_smt.api.Formula>,K>

asIntArrayValue

public IntArrayValue asIntArrayValue()

asBooleanArrayValue

public BooleanArrayValue asBooleanArrayValue()

asLongArrayValue

public LongArrayValue asLongArrayValue()

asFloatArrayValue

public FloatArrayValue asFloatArrayValue()

asObjectArrayValue

public ObjectArrayValue asObjectArrayValue()

Overrides:

asObjectArrayValue in class ObjectValue<org.sosy_lab.java_smt.api.ArrayFormula<TI extends org.sosy_lab.java_smt.api.Formula,TE extends org.sosy_lab.java_smt.api.Formula>,K>

asByteArrayValue

public ByteArrayValue asByteArrayValue()

asCharArrayValue

public CharArrayValue asCharArrayValue()

asDoubleArrayValue

public DoubleArrayValue asDoubleArrayValue()

asShortArrayValue

public ShortArrayValue asShortArrayValue()

getContext

public org.sosy_lab.java_smt.api.SolverContext getContext()

genericToString

public String genericToString(String type)