de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.KeYlessTermination

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

All Implemented Interfaces:

IExecutionElement, IExecutionNode<SourceElement>, IExecutionTermination

Enclosing class:

ExecutionNodeReader

public static class ExecutionNodeReader.KeYlessTermination
extends ExecutionNodeReader.AbstractKeYlessExecutionNode<SourceElement>
implements IExecutionTermination

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

Author:

Martin Hentschel

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.symbolic_execution.model.IExecutionTermination

IExecutionTermination.TerminationKind

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	branchVerified The branch verified flag.
private IExecutionTermination.TerminationKind	terminationKind The IExecutionTermination.TerminationKind.

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

LOOP_BODY_TERMINATION_NODE_NAME, NORMAL_TERMINATION_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
KeYlessTermination(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged, IExecutionTermination.TerminationKind terminationKind, boolean branchVerified) Constructor.

Method Summary

Modifier and Type	Method and Description
java.lang.String	getElementType() Returns a human readable element type name.
Sort	getExceptionSort() Returns the Sort of the caught exception.
IProgramVariable	getExceptionVariable() Returns the IProgramVariable which is used in the Sequent of Proof.root() to check if a normal or exceptional termination occurred.
IExecutionTermination.TerminationKind	getTerminationKind() Returns the IExecutionTermination.TerminationKind.
boolean	isBranchVerified() Checks if this branch would be closed without the uninterpreted predicate and thus be treated as valid/closed in a regular proof.

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

terminationKind

private final IExecutionTermination.TerminationKind terminationKind

The IExecutionTermination.TerminationKind.

branchVerified

private final boolean branchVerified

The branch verified flag.

Constructor Detail

KeYlessTermination

public KeYlessTermination(IExecutionNode<?> parent,
                          java.lang.String name,
                          java.lang.String formatedPathCondition,
                          boolean pathConditionChanged,
                          IExecutionTermination.TerminationKind terminationKind,
                          boolean branchVerified)

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?

exceptionalTermination - Exceptional termination?

branchVerified - The branch verified flag.

Method Detail

getExceptionVariable

public IProgramVariable getExceptionVariable()

Returns the IProgramVariable which is used in the Sequent of Proof.root() to check if a normal or exceptional termination occurred.

Specified by:

getExceptionVariable in interface IExecutionTermination

Returns:

The IProgramVariable which is used to caught global exceptions.

getExceptionSort

public Sort getExceptionSort()

Returns the Sort of the caught exception.

Specified by:

getExceptionSort in interface IExecutionTermination

Returns:

The Sort of the caught exception.

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.

getTerminationKind

public IExecutionTermination.TerminationKind getTerminationKind()

Returns the IExecutionTermination.TerminationKind.

Specified by:

getTerminationKind in interface IExecutionTermination

Returns:

The IExecutionTermination.TerminationKind.

isBranchVerified

public boolean isBranchVerified()

Checks if this branch would be closed without the uninterpreted predicate and thus be treated as valid/closed in a regular proof.

Specified by:

isBranchVerified in interface IExecutionTermination

Returns:

true verified/closed, false not verified/still open