de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.KeYlessBranchCondition

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

All Implemented Interfaces:

IExecutionBranchCondition, IExecutionElement, IExecutionNode<SourceElement>

Enclosing class:

ExecutionNodeReader

public static class ExecutionNodeReader.KeYlessBranchCondition
extends ExecutionNodeReader.AbstractKeYlessExecutionNode<SourceElement>
implements IExecutionBranchCondition

An implementation of IExecutionLoopCondition 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	additionalBranchLabel The optional additional branch label.
private boolean	branchConditionComputed Indicates if branch condition is computed or not.
private java.lang.String	formatedBranchCondition The formated branch condition.
private boolean	mergedBranchCondition Merged branch condition?

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
KeYlessBranchCondition(IExecutionNode<?> parent, java.lang.String name, java.lang.String formatedPathCondition, boolean pathConditionChanged, java.lang.String formatedBranchCondition, boolean mergedBranchCondition, boolean branchConditionComputed, java.lang.String additionalBranchLabel) Constructor.

Method Summary

Modifier and Type	Method and Description
java.lang.String	getAdditionalBranchLabel() Returns the optional additional branch label.
Term	getBranchCondition() Returns the branch condition as Term.
java.lang.String	getElementType() Returns a human readable element type name.
java.lang.String	getFormatedBranchCondition() Returns the human readable branch condition as string.
Term[]	getMergedBranchCondtions() Returns the branch condition Terms.
Node[]	getMergedProofNodes() Returns the branch condition nodes in KeY's proof tree which are merged into this IExecutionBranchCondition.
boolean	isBranchConditionComputed() Checks if the value of IExecutionBranchCondition.getBranchCondition() is already computed.
boolean	isMergedBranchCondition() Checks if this branch condition is a merged one.

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

formatedBranchCondition

private final java.lang.String formatedBranchCondition

The formated branch condition.

mergedBranchCondition

private final boolean mergedBranchCondition

Merged branch condition?

branchConditionComputed

private final boolean branchConditionComputed

Indicates if branch condition is computed or not.

additionalBranchLabel

private final java.lang.String additionalBranchLabel

The optional additional branch label.

Constructor Detail

KeYlessBranchCondition

public KeYlessBranchCondition(IExecutionNode<?> parent,
                              java.lang.String name,
                              java.lang.String formatedPathCondition,
                              boolean pathConditionChanged,
                              java.lang.String formatedBranchCondition,
                              boolean mergedBranchCondition,
                              boolean branchConditionComputed,
                              java.lang.String additionalBranchLabel)

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?

formatedBranchCondition - The formated branch condition.

mergedBranchCondition - Merged branch condition?

branchConditionComputed - Is branch condition computed?

additionalBranchLabel - The optional additional branch label.

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.

getBranchCondition

public Term getBranchCondition()

Returns the branch condition as Term.

If this branch conditions merged proof nodes this Term is the overall branch condition.

Specified by:

getBranchCondition in interface IExecutionBranchCondition

Returns:

The branch condition as Term.

getFormatedBranchCondition

public java.lang.String getFormatedBranchCondition()

Returns the human readable branch condition as string.

Specified by:

getFormatedBranchCondition in interface IExecutionBranchCondition

Returns:

The human readable branch condition.

isMergedBranchCondition

public boolean isMergedBranchCondition()

Checks if this branch condition is a merged one.

Specified by:

isMergedBranchCondition in interface IExecutionBranchCondition

Returns:

true is merged branch condition, false is normal branch condition.

getMergedProofNodes

public Node[] getMergedProofNodes()

Returns the branch condition nodes in KeY's proof tree which are merged into this IExecutionBranchCondition.

It includes also IExecutionElement.getProofNode().

Specified by:

getMergedProofNodes in interface IExecutionBranchCondition

Returns:

The merged proof nodes.

getMergedBranchCondtions

public Term[] getMergedBranchCondtions()
                                throws ProofInputException

Returns the branch condition Terms.

Specified by:

getMergedBranchCondtions in interface IExecutionBranchCondition

Returns:

The branch condition Terms.

Throws:

ProofInputException

isBranchConditionComputed

public boolean isBranchConditionComputed()

Checks if the value of IExecutionBranchCondition.getBranchCondition() is already computed.

Specified by:

isBranchConditionComputed in interface IExecutionBranchCondition

Returns:

true value of IExecutionBranchCondition.getBranchCondition() is already computed, false value of IExecutionBranchCondition.getBranchCondition() needs to be computed.

getAdditionalBranchLabel

public java.lang.String getAdditionalBranchLabel()

Returns the optional additional branch label.

Specified by:

getAdditionalBranchLabel in interface IExecutionBranchCondition

Returns:

The additional branch label if available or null if not available.