de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.KeYlessLoopCondition

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

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.KeYlessLoopCondition

All Implemented Interfaces:

IExecutionBlockStartNode<JavaStatement>, IExecutionElement, IExecutionLoopCondition, IExecutionNode<JavaStatement>

Enclosing class:

ExecutionNodeReader

public static class ExecutionNodeReader.KeYlessLoopCondition
extends ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode<JavaStatement>
implements IExecutionLoopCondition

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

Author:

Martin Hentschel

Field Summary

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

Method Summary

Modifier and Type	Method and Description
java.lang.String	getElementType() Returns a human readable element type name.
Expression	getGuardExpression() Returns the loop expression which is executed.
PositionInfo	getGuardExpressionPositionInfo() Returns the code position of the executed loop expression (IExecutionLoopCondition.getGuardExpression()).

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

addBlockCompletion, getBlockCompletions, isBlockOpened

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

getBlockCompletions, isBlockOpened

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

Constructor Detail

KeYlessLoopCondition

public KeYlessLoopCondition(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

getGuardExpression

public Expression getGuardExpression()

Returns the loop expression which is executed.

Specified by:

getGuardExpression in interface IExecutionLoopCondition

Returns:

The executed loop expression.

getGuardExpressionPositionInfo

public PositionInfo getGuardExpressionPositionInfo()

Returns the code position of the executed loop expression (IExecutionLoopCondition.getGuardExpression()).

Specified by:

getGuardExpressionPositionInfo in interface IExecutionLoopCondition

Returns:

The code of the executed loop expression.

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.