de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.KeYlessStart

java.lang.Object

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

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionNode<SourceElement>

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.KeYlessStart

All Implemented Interfaces:

IExecutionElement, IExecutionNode<SourceElement>, IExecutionStart

Enclosing class:

ExecutionNodeReader

public static class ExecutionNodeReader.KeYlessStart
extends ExecutionNodeReader.AbstractKeYlessExecutionNode<SourceElement>
implements IExecutionStart

An implementation of IExecutionStart 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 ImmutableList<IExecutionTermination>	terminations The up to now discovered IExecutionTerminations.

Fields inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionStart

DEFAULT_START_NODE_NAME

Fields inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionNode

INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START

Constructor Summary

Constructors

Constructor and Description
KeYlessStart(java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged) Constructor.

Method Summary

Modifier and Type	Method and Description
void	addTermination(IExecutionTermination termination) Adds the given IExecutionTermination.
java.lang.String	getElementType() Returns a human readable element type name.
ImmutableList<IExecutionTermination>	getTerminations() Returns the up to now discovered IExecutionTerminations.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionNode

addCallStackEntry, addChild, addCompletedBlock, addConstraint, addIncomingLink, addOutgoingLink, addVariable, getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getModalityPIO, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged

Methods inherited from class de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionElement

getAppliedRuleApp, getInitConfig, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed, 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.IExecutionNode

getActivePositionInfo, getActiveStatement, getBlockCompletionCondition, getCallStack, getChildren, getCompletedBlocks, getConstraints, getCurrentLayout, getFormatedBlockCompletionCondition, getFormatedPathCondition, getIncomingLink, getIncomingLinks, getInitialLayout, getLayoutsCount, getLayoutsEquivalenceClasses, getOutgoingLink, getOutgoingLinks, getParent, getPathCondition, getVariables, getVariables, isPathConditionChanged

Methods inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionElement

getAppliedRuleApp, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

Field Detail

terminations

private ImmutableList<IExecutionTermination> terminations

The up to now discovered IExecutionTerminations.

Constructor Detail

KeYlessStart

public KeYlessStart(java.lang.String name,
                    java.lang.String formatedPathCondition,
                    boolean pathConditionChanged)

Constructor.

Parameters:

name - The name of this node.

formatedPathCondition - The formated path condition.

pathConditionChanged - Is the path condition changed compared to parent?

Method Detail

getElementType

public java.lang.String getElementType()

Returns a human readable element type name.

Specified by:

getElementType in interface IExecutionElement

Returns:

The human readable element type.

addTermination

public void addTermination(IExecutionTermination termination)

Adds the given IExecutionTermination.

Parameters:

termination - The IExecutionTermination to add.

getTerminations

public ImmutableList<IExecutionTermination> getTerminations()

Returns the up to now discovered IExecutionTerminations.

Specified by:

getTerminations in interface IExecutionStart

Returns:

The up to now discovered IExecutionTerminations.