de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode<S extends SourceElement>

java.lang.Object

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

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

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode<S>

All Implemented Interfaces:

IExecutionBlockStartNode<S>, IExecutionElement, IExecutionNode<S>

Direct Known Subclasses:

ExecutionNodeReader.KeYlessBranchStatement, ExecutionNodeReader.KeYlessLoopCondition, ExecutionNodeReader.KeYlessLoopStatement

Enclosing class:

ExecutionNodeReader

public abstract static class ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode<S extends SourceElement>
extends ExecutionNodeReader.AbstractKeYlessExecutionNode<S>
implements IExecutionBlockStartNode<S>

An abstract implementation of IExecutionBlockStartNode 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<IExecutionNode<?>>	blockCompletions The block completions.
private boolean	blockOpened Is a block opened?

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
AbstractKeYlessExecutionBlockStartNode(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged, boolean blockOpened) Constructor.

Method Summary

Modifier and Type	Method and Description
void	addBlockCompletion(IExecutionNode<?> blockCompletion) Adds the given block completion.
ImmutableList<IExecutionNode<?>>	getBlockCompletions() Returns the up to now discovered IExecutionNodes.
boolean	isBlockOpened() Checks if a block might be opened.

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, getElementType, getInitConfig, getModalityPIO, getName, getProof, getProofNode, getProofNodeInfo, getServices, getSettings, isDisposed

Field Detail

blockCompletions

private ImmutableList<IExecutionNode<?>> blockCompletions

The block completions.

blockOpened

private final boolean blockOpened

Is a block opened?

Constructor Detail

AbstractKeYlessExecutionBlockStartNode

public AbstractKeYlessExecutionBlockStartNode(IExecutionNode<?> parent,
                                              java.lang.String name,
                                              java.lang.String formatedPathCondition,
                                              boolean pathConditionChanged,
                                              boolean blockOpened)

Constructor.

Parameters:

parent - The parent IExecutionNode.

name - The name of this node.

formatedPathCondition - The formated path condition.

pathConditionChanged - Is the path condition changed compared to parent?

blockOpened - false block is definitively not opened, true block is or might be opened.

Method Detail

getBlockCompletions

public ImmutableList<IExecutionNode<?>> getBlockCompletions()

Returns the up to now discovered IExecutionNodes.

Specified by:

getBlockCompletions in interface IExecutionBlockStartNode<S extends SourceElement>

Returns:

The up to now discovered IExecutionNodes.

addBlockCompletion

public void addBlockCompletion(IExecutionNode<?> blockCompletion)

Adds the given block completion.

Parameters:

blockCompletion - The block completion to add.

isBlockOpened

public boolean isBlockOpened()

Checks if a block might be opened.

Specified by:

isBlockOpened in interface IExecutionBlockStartNode<S extends SourceElement>

Returns:

false block is definitively not opened, true block is or might be opened.