de.uka.ilkd.key.symbolic_execution

Class SymbolicLayoutReader.KeYlessState

java.lang.Object

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

de.uka.ilkd.key.symbolic_execution.SymbolicLayoutReader.AbstractKeYlessAssociationValueContainer

de.uka.ilkd.key.symbolic_execution.SymbolicLayoutReader.KeYlessState

All Implemented Interfaces:

ISymbolicAssociationValueContainer, ISymbolicElement, ISymbolicState

Enclosing class:

SymbolicLayoutReader

public static class SymbolicLayoutReader.KeYlessState
extends SymbolicLayoutReader.AbstractKeYlessAssociationValueContainer
implements ISymbolicState

An implementation of ISymbolicState 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	name The name.

Constructor Summary

Constructors

Constructor and Description
KeYlessState(java.lang.String name) Constructor.

Method Summary

Modifier and Type	Method and Description
ISymbolicAssociation	getAssociation(IProgramVariable programVariable, boolean isArrayIndex, Term arrayIndex, Term condition) Returns the ISymbolicAssociation with the given IProgramVariable.
java.lang.String	getName() Returns the name of this state.
ISymbolicValue	getValue(IProgramVariable programVariable, boolean isArrayIndex, Term arrayIndex, Term condition) Returns the ISymbolicValue with the given IProgramVariable.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.SymbolicLayoutReader.AbstractKeYlessAssociationValueContainer

addAssociation, addValue, getAssociations, getValues

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

getAssociations, getValues

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

getSettings

Field Detail

name

private java.lang.String name

The name.

Constructor Detail

KeYlessState

public KeYlessState(java.lang.String name)

Constructor.

Parameters:

name - The name.

Method Detail

getName

public java.lang.String getName()

Returns the name of this state.

Specified by:

getName in interface ISymbolicState

Returns:

The name of this state.

getAssociation

public ISymbolicAssociation getAssociation(IProgramVariable programVariable,
                                           boolean isArrayIndex,
                                           Term arrayIndex,
                                           Term condition)

Returns the ISymbolicAssociation with the given IProgramVariable.

Specified by:

getAssociation in interface ISymbolicAssociationValueContainer

Parameters:

programVariable - The IProgramVariable for which the ISymbolicAssociation is requested.

isArrayIndex - Is array index?

arrayIndex - The array index.

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

Returns:

The found ISymbolicAssociation or null if no ISymbolicAssociation is available with the given IProgramVariable.

getValue

public ISymbolicValue getValue(IProgramVariable programVariable,
                               boolean isArrayIndex,
                               Term arrayIndex,
                               Term condition)

Returns the ISymbolicValue with the given IProgramVariable.

Specified by:

getValue in interface ISymbolicAssociationValueContainer

Parameters:

programVariable - The IProgramVariable for which the ISymbolicValue is requested.

isArrayIndex - Is array index?

arrayIndex - The array index.

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

Returns:

The found ISymbolicValue or null if no ISymbolicValue is available with the given IProgramVariable.