de.uka.ilkd.key.symbolic_execution

Class SymbolicLayoutReader.KeYlessValue

java.lang.Object

de.uka.ilkd.key.symbolic_execution.SymbolicLayoutReader.AbstractKeYlessElement

de.uka.ilkd.key.symbolic_execution.SymbolicLayoutReader.KeYlessValue

All Implemented Interfaces:

ISymbolicElement, ISymbolicValue

Enclosing class:

SymbolicLayoutReader

public static class SymbolicLayoutReader.KeYlessValue
extends SymbolicLayoutReader.AbstractKeYlessElement
implements ISymbolicValue

An implementation of ISymbolicValue which is independent from KeY and provides such only children and default attributes.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.String	arrayIndexString The array index.
private java.lang.String	conditionString The optional condition under which this value is valid.
private boolean	isArrayIndex The is array index flag.
private java.lang.String	name The name.
private java.lang.String	programVariableString The program variable.
private java.lang.String	typeString The type.
private java.lang.String	valueString The value.

Constructor Summary

Constructors

Constructor and Description
KeYlessValue(java.lang.String name, java.lang.String programVariableString, boolean isArrayIndex, java.lang.String arrayIndexString, java.lang.String valueString, java.lang.String typeString, java.lang.String conditionString) Constructor.

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 class de.uka.ilkd.key.symbolic_execution.SymbolicLayoutReader.AbstractKeYlessElement

getSettings

Methods inherited from class java.lang.Object

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

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

getSettings

Field Detail

programVariableString

private java.lang.String programVariableString

The program variable.

valueString

private java.lang.String valueString

The value.

typeString

private java.lang.String typeString

The type.

name

private java.lang.String name

The name.

isArrayIndex

private boolean isArrayIndex

The is array index flag.

arrayIndexString

private java.lang.String arrayIndexString

The array index.

conditionString

private java.lang.String conditionString

The optional condition under which this value is valid.

Constructor Detail

KeYlessValue

public KeYlessValue(java.lang.String name,
                    java.lang.String programVariableString,
                    boolean isArrayIndex,
                    java.lang.String arrayIndexString,
                    java.lang.String valueString,
                    java.lang.String typeString,
                    java.lang.String conditionString)

Constructor.

Parameters:

name - The name.

programVariableString - The program variable.

isArrayIndex - The is array index flag.

arrayIndexString - The array index.

valueString - The value.

typeString - The type.

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

Method Detail

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.

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 or a program variable is represented.

Specified by:

isArrayIndex in interface ISymbolicValue

Returns:

true array index, false program variable.

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..

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..

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.