de.uka.ilkd.key.symbolic_execution.object_model.impl

Class SymbolicValue

java.lang.Object

de.uka.ilkd.key.symbolic_execution.object_model.impl.AbstractElement

de.uka.ilkd.key.symbolic_execution.object_model.impl.SymbolicValue

All Implemented Interfaces:

ISymbolicElement, ISymbolicValue

public class SymbolicValue
extends AbstractElement
implements ISymbolicValue

Default implementation of ISymbolicValue.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private Term	arrayEndIndex The array end index or null if not used.
private Term	arrayIndex The array index.
private Term	arrayStartIndex The array start index or null if not used.
private Term	condition The optional condition under which this value is valid.
private IProgramVariable	programVariable The IProgramVariable.
private Services	services The Services to use.
private Term	value The value Term.

Constructor Summary

Constructors

Constructor and Description
SymbolicValue(Services services, IProgramVariable programVariable, Term value, Term condition, IModelSettings settings) Constructor.
SymbolicValue(Services services, Term arrayIndex, Term value, Term condition, IModelSettings settings) Constructor.
SymbolicValue(Services services, Term arrayIndex, Term arrayStartIndex, Term arrayEndIndex, Term value, Term condition, IModelSettings settings) Constructor.

Method Summary

Modifier and Type	Method and Description
Term	getArrayEndIndex() Returns the array end index.
java.lang.String	getArrayEndIndexString() Returns the human readable array end index.
Term	getArrayIndex() Returns the represented array index or null if a program variable is represented..
java.lang.String	getArrayIndexString() Returns the human readable array index or null if a program variable is represented..
Term	getArrayStartIndex() Returns the array start index.
java.lang.String	getArrayStartIndexString() Returns the human readable array start index.
Term	getCondition() Returns the optional condition under which this value is valid.
java.lang.String	getConditionString() Returns the optional condition under which this value is valid as human readable String.
java.lang.String	getName() Returns a human readable name.
IProgramVariable	getProgramVariable() Returns the represented IProgramVariable or null if an array index is represented.
java.lang.String	getProgramVariableString() Returns the represented IProgramVariable as human readable String or null if an array index is represented.
Sort	getType() Returns the type of the value.
java.lang.String	getTypeString() Returns the type of the value as human readable string.
Term	getValue() Returns the value of the represented variable.
java.lang.String	getValueString() Returns the value of the represented variable as human readable String.
boolean	isArrayIndex() Checks if an array index is represented.
boolean	isArrayRange() Checks if an array range is represented.
java.lang.String	toString()

Methods inherited from class de.uka.ilkd.key.symbolic_execution.object_model.impl.AbstractElement

formatTerm, getSettings

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicElement

getSettings

Field Detail

services

private final Services services

The Services to use.

arrayIndex

private final Term arrayIndex

The array index.

arrayStartIndex

private final Term arrayStartIndex

The array start index or null if not used.

arrayEndIndex

private final Term arrayEndIndex

The array end index or null if not used.

programVariable

private final IProgramVariable programVariable

The IProgramVariable.

value

private final Term value

The value Term.

condition

private final Term condition

The optional condition under which this value is valid.

Constructor Detail

SymbolicValue

public SymbolicValue(Services services,
                     Term arrayIndex,
                     Term value,
                     Term condition,
                     IModelSettings settings)

Constructor.

Parameters:

services - The Services to use.

arrayIndex - The array index.

value - The value Term.

condition - The optional condition under which this value is valid.

settings - The IModelSettings to use.

SymbolicValue

public SymbolicValue(Services services,
                     Term arrayIndex,
                     Term arrayStartIndex,
                     Term arrayEndIndex,
                     Term value,
                     Term condition,
                     IModelSettings settings)

Constructor.

Parameters:

services - The Services to use.

arrayIndex - The array index.

arrayStartIndex - The array start index or null if not used.

arrayEndIndex - The array end index or null if not used.

value - The value Term.

condition - The optional condition under which this value is valid.

settings - The IModelSettings to use.

SymbolicValue

public SymbolicValue(Services services,
                     IProgramVariable programVariable,
                     Term value,
                     Term condition,
                     IModelSettings settings)

Constructor.

Parameters:

services - The Services to use.

programVariable - The IProgramVariable.

value - The value Term.

condition - The optional condition under which this value is valid.

settings - The IModelSettings to use.

Method Detail

getName

public java.lang.String getName()

Returns a human readable name.

Specified by:

getName in interface ISymbolicValue

Returns:

A human readable name.

isArrayIndex

public boolean isArrayIndex()

Checks if an array index is represented.

Specified by:

isArrayIndex in interface ISymbolicValue

Returns:

true is array index, false is something else.

isArrayRange

public boolean isArrayRange()

Checks if an array range is represented.

Returns:

true is array range, false is something else.

getArrayIndex

public Term getArrayIndex()

Returns the represented array index or null if a program variable is represented..

Specified by:

getArrayIndex in interface ISymbolicValue

Returns:

The represented array index or null if a program variable is represented..

getProgramVariable

public IProgramVariable getProgramVariable()

Returns the represented IProgramVariable or null if an array index is represented.

Specified by:

getProgramVariable in interface ISymbolicValue

Returns:

The represented IProgramVariable or null if an array index is represented.

getProgramVariableString

public java.lang.String getProgramVariableString()

Returns the represented IProgramVariable as human readable String or null if an array index is represented.

Specified by:

getProgramVariableString in interface ISymbolicValue

Returns:

The represented IProgramVariable as human readable String or null if an array index is represented.

getValue

public Term getValue()

Returns the value of the represented variable.

Specified by:

getValue in interface ISymbolicValue

Returns:

The value of the represented variable.

getValueString

public java.lang.String getValueString()

Returns the value of the represented variable as human readable String.

Specified by:

getValueString in interface ISymbolicValue

Returns:

The value of the represented variable as human readable String.

getType

public Sort getType()

Returns the type of the value.

Specified by:

getType in interface ISymbolicValue

Returns:

The type of the value.

getTypeString

public java.lang.String getTypeString()

Returns the type of the value as human readable string.

Specified by:

getTypeString in interface ISymbolicValue

Returns:

The type of the value as human readable string.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getCondition

public Term getCondition()

Returns the optional condition under which this value is valid.

The condition should be null by default. Only in rare cases, e.g. path condition is not strong enough to describe the path completely, is a condition is provided.

Specified by:

getCondition in interface ISymbolicValue

Returns:

The optional condition under which this value is valid.

getConditionString

public java.lang.String getConditionString()

Returns the optional condition under which this value is valid as human readable String.

The condition should be null by default. Only in rare cases, e.g. path condition is not strong enough to describe the path completely, is a condition is provided.

Specified by:

getConditionString in interface ISymbolicValue

Returns:

The optional condition under which this value is valid as human readable String.

getArrayIndexString

public java.lang.String getArrayIndexString()

Returns the human readable array index or null if a program variable is represented..

Specified by:

getArrayIndexString in interface ISymbolicValue

Returns:

The human readable array index or null if a program variable is represented..

getArrayStartIndex

public Term getArrayStartIndex()

Returns the array start index.

Returns:

The array start index.

getArrayStartIndexString

public java.lang.String getArrayStartIndexString()

Returns the human readable array start index.

Returns:

The human readable array start index.

getArrayEndIndex

public Term getArrayEndIndex()

Returns the array end index.

Returns:

The array end index.

getArrayEndIndexString

public java.lang.String getArrayEndIndexString()

Returns the human readable array end index.

Returns:

The human readable array end index.