de.uka.ilkd.key.symbolic_execution.model

Interface IExecutionBranchCondition

All Superinterfaces:

IExecutionElement, IExecutionNode<SourceElement>

All Known Implementing Classes:

ExecutionBranchCondition, ExecutionNodeReader.KeYlessBranchCondition

public interface IExecutionBranchCondition
extends IExecutionNode<SourceElement>

A node in the symbolic execution tree which represents a branch condition, e.g. x < 0.

The default implementation is ExecutionBranchCondition which is instantiated via a SymbolicExecutionTreeBuilder instance.

Author:

Martin Hentschel

See Also:

SymbolicExecutionTreeBuilder, ExecutionBranchCondition

Field Summary

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

INTERNAL_NODE_NAME_END, INTERNAL_NODE_NAME_START

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	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 getBranchCondition() is already computed.
boolean	isMergedBranchCondition() Checks if this branch condition is a merged one.

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

Method Detail

getAdditionalBranchLabel

java.lang.String getAdditionalBranchLabel()

Returns the optional additional branch label.

Returns:

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

isBranchConditionComputed

boolean isBranchConditionComputed()

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

Returns:

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

getBranchCondition

Term getBranchCondition()
                 throws ProofInputException

Returns the branch condition as Term.

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

Returns:

The branch condition as Term.

Throws:

ProofInputException

getFormatedBranchCondition

java.lang.String getFormatedBranchCondition()
                                     throws ProofInputException

Returns the human readable branch condition as string.

Returns:

The human readable branch condition.

Throws:

ProofInputException

isMergedBranchCondition

boolean isMergedBranchCondition()

Checks if this branch condition is a merged one.

Returns:

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

getMergedProofNodes

Node[] getMergedProofNodes()

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

It includes also IExecutionElement.getProofNode().

Returns:

The merged proof nodes.

getMergedBranchCondtions

Term[] getMergedBranchCondtions()
                         throws ProofInputException

Returns the branch condition Terms.

Returns:

The branch condition Terms.

Throws:

ProofInputException