de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.AbstractKeYlessExecutionElement

java.lang.Object

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionElement

All Implemented Interfaces:

IExecutionElement

Direct Known Subclasses:

ExecutionNodeReader.AbstractKeYlessExecutionNode, ExecutionNodeReader.KeYlessConstraint, ExecutionNodeReader.KeYlessMethodReturnValue, ExecutionNodeReader.KeYlessValue, ExecutionNodeReader.KeYlessVariable

Enclosing class:

ExecutionNodeReader

public abstract static class ExecutionNodeReader.AbstractKeYlessExecutionElement
extends java.lang.Object
implements IExecutionElement

An abstract implementation of IExecutionElement 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
AbstractKeYlessExecutionElement(java.lang.String name) Constructor.

Method Summary

Modifier and Type	Method and Description
RuleApp	getAppliedRuleApp() Returns the applied RuleApp.
InitConfig	getInitConfig() Returns the InitConfig used by IExecutionElement.getProof().
java.lang.String	getName() Returns a human readable name which describes this element.
Proof	getProof() Returns the Proof from which the symbolic execution tree was extracted.
Node	getProofNode() Returns the Node in KeY's proof tree which is represented by this execution tree node.
NodeInfo	getProofNodeInfo() Returns the NodeInfo of IExecutionElement.getProofNode().
Services	getServices() Returns the Services used by IExecutionElement.getProof().
ITreeSettings	getSettings() Returns the ITreeSettings to use.
boolean	isDisposed() Checks if the proof is disposed.
java.lang.String	toString()

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

getElementType, getModalityPIO

Field Detail

name

private final java.lang.String name

The name.

Constructor Detail

AbstractKeYlessExecutionElement

public AbstractKeYlessExecutionElement(java.lang.String name)

Constructor.

Parameters:

name - The name of this node.

Method Detail

getServices

public Services getServices()

Returns the Services used by IExecutionElement.getProof().

Specified by:

getServices in interface IExecutionElement

Returns:

The Services used by IExecutionElement.getProof().

getInitConfig

public InitConfig getInitConfig()

Returns the InitConfig used by IExecutionElement.getProof().

Specified by:

getInitConfig in interface IExecutionElement

Returns:

The InitConfig used by IExecutionElement.getProof().

getProof

public Proof getProof()

Returns the Proof from which the symbolic execution tree was extracted.

Specified by:

getProof in interface IExecutionElement

Returns:

The Proof from which the symbolic execution tree was extracted.

getAppliedRuleApp

public RuleApp getAppliedRuleApp()

Returns the applied RuleApp.

Specified by:

getAppliedRuleApp in interface IExecutionElement

Returns:

The applied RuleApp.

getProofNode

public Node getProofNode()

Returns the Node in KeY's proof tree which is represented by this execution tree node.

Specified by:

getProofNode in interface IExecutionElement

Returns:

The Node in KeY's proof tree which is represented by this execution tree node.

getProofNodeInfo

public NodeInfo getProofNodeInfo()

Returns the NodeInfo of IExecutionElement.getProofNode().

Specified by:

getProofNodeInfo in interface IExecutionElement

Returns:

The NodeInfo of IExecutionElement.getProofNode().

getName

public java.lang.String getName()

Returns a human readable name which describes this element.

Specified by:

getName in interface IExecutionElement

Returns:

The human readable name which describes this element.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

isDisposed

public boolean isDisposed()

Checks if the proof is disposed.

Specified by:

isDisposed in interface IExecutionElement

Returns:

true proof is disposed, false proof is not disposed and still valid.

getSettings

public ITreeSettings getSettings()

Returns the ITreeSettings to use.

Specified by:

getSettings in interface IExecutionElement

Returns:

The ITreeSettings to use.