de.uka.ilkd.key.symbolic_execution.object_model

Interface ISymbolicValue

All Superinterfaces:

ISymbolicElement

All Known Implementing Classes:

SymbolicLayoutReader.KeYlessValue, SymbolicValue

public interface ISymbolicValue
extends ISymbolicElement

Represents a variable of an ISymbolicState or ISymbolicObject which contains a value of a primitive type.

The default implementation is SymbolicValue.

Author:

Martin Hentschel

See Also:

SymbolicValue

Method Summary

Modifier and Type	Method and Description
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	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 or a program variable is represented.

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

getSettings

Method Detail

getName

java.lang.String getName()

Returns a human readable name.

Returns:

A human readable name.

isArrayIndex

boolean isArrayIndex()

Checks if an array index or a program variable is represented.

Returns:

true array index, false program variable.

getArrayIndex

Term getArrayIndex()

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

Returns:

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

getArrayIndexString

java.lang.String getArrayIndexString()

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

Returns:

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

getProgramVariable

IProgramVariable getProgramVariable()

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

Returns:

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

getProgramVariableString

java.lang.String getProgramVariableString()

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

Returns:

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

getValue

Term getValue()

Returns the value of the represented variable.

Returns:

The value of the represented variable.

getValueString

java.lang.String getValueString()

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

Returns:

The value of the represented variable as human readable String.

getType

Sort getType()

Returns the type of the value.

Returns:

The type of the value.

getTypeString

java.lang.String getTypeString()

Returns the type of the value as human readable string.

Returns:

The type of the value as human readable string.

getCondition

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.

Returns:

The optional condition under which this value is valid.

getConditionString

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.

Returns:

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