de.uka.ilkd.key.symbolic_execution.model

Interface IExecutionJoin

All Superinterfaces:

IExecutionElement, IExecutionNode<SourceElement>

All Known Implementing Classes:

ExecutionJoin, ExecutionNodeReader.KeYlessJoin

public interface IExecutionJoin
extends IExecutionNode<SourceElement>

A node in the symbolic execution tree which represents a join.

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

Author:

Martin Hentschel

See Also:

SymbolicExecutionTreeBuilder, ExecutionJoin

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
boolean	isWeakeningVerificationSupported() Checks if the weakening verification is supported.
boolean	isWeakeningVerified() Checks if the weakening is verified.

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

isWeakeningVerified

boolean isWeakeningVerified()

Checks if the weakening is verified.

Returns:

true is verified, false is not verified.

isWeakeningVerificationSupported

boolean isWeakeningVerificationSupported()

Checks if the weakening verification is supported.

Returns:

true supported, false not supported.