Modifier and Type | Class and Description |
---|---|
static class |
ExecutionNodeReader.AbstractKeYlessBaseExecutionNode<S extends SourceElement>
An implementation of
IExecutionBaseMethodReturn which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode<S extends SourceElement>
An abstract implementation of
IExecutionBlockStartNode which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.AbstractKeYlessExecutionNode<S extends SourceElement>
An abstract implementation of
IExecutionNode which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessBlockContract
An implementation of
IExecutionAuxiliaryContract which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessBranchCondition
An implementation of
IExecutionLoopCondition which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessBranchStatement
An implementation of
IExecutionBranchStatement which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessExceptionalMethodReturn
An implementation of
IExecutionExceptionalMethodReturn which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessJoin
An implementation of
IExecutionJoin which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessLoopCondition
An implementation of
IExecutionLoopCondition which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessLoopInvariant
An implementation of
IExecutionLoopInvariant which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessLoopStatement
An implementation of
IExecutionLoopStatement which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessMethodCall
An implementation of
IExecutionMethodCall which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessMethodReturn
An implementation of
IExecutionMethodReturn which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessOperationContract
An implementation of
IExecutionOperationContract which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessStart
An implementation of
IExecutionStart which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessStatement
An implementation of
IExecutionStatement which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessTermination
An implementation of
IExecutionTermination which is independent
from KeY and provides such only children and default attributes. |
Modifier and Type | Method and Description |
---|---|
protected IExecutionNode<?>[] |
SymbolicExecutionTreeBuilder.createCallStack(Node node)
Computes the method call stack of the given
Node . |
protected IExecutionNode<?> |
ExecutionNodeReader.findNode(IExecutionNode<?> root,
java.lang.String path)
Searches the
IExecutionNode starting at the given root
which is defined by the path. |
IExecutionNode<?> |
SymbolicExecutionTreeBuilder.getBestExecutionNode(Node proofNode)
Returns the best matching
IExecutionNode for the given proof Node
in the parent hierarchy. |
IExecutionNode<?>[] |
SymbolicExecutionTreeBuilder.SymbolicExecutionCompletions.getBlockCompletions()
Returns the newly block completion.
|
IExecutionNode<?>[] |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getCallStack()
Returns the method call stack.
|
IExecutionNode<?>[] |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getChildren()
Returns the available children.
|
IExecutionNode<?> |
SymbolicExecutionTreeBuilder.getExecutionNode(Node proofNode)
Searches the
IExecutionNode which represents the given Node of KeY's proof tree. |
protected IExecutionNode<?> |
ExecutionNodePreorderIterator.getNextOnParent(IExecutionNode<?> node)
Returns the next element to select if all children of the given
IExecutionNode are visited. |
IExecutionNode<?> |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getParent()
Returns the parent
IExecutionNode or null if the
current node is the root. |
IExecutionNode<?> |
ExecutionNodeReader.KeYLessLink.getSource()
Returns the source.
|
IExecutionNode<?> |
ExecutionNodeReader.KeYLessLink.getTarget()
Returns the target.
|
IExecutionNode<?> |
ExecutionNodePreorderIterator.next()
Returns the next
IExecutionNode in the containment hierarchy. |
IExecutionNode<?> |
ExecutionNodeReader.read(java.io.File file)
Reads the given
File . |
IExecutionNode<?> |
ExecutionNodeReader.read(java.io.InputStream in)
Reads from the given
InputStream and closes it. |
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>> |
SymbolicExecutionTreeBuilder.findAfterBlockMap(java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> afterBlockMaps,
Node node)
Searches the relevant after block
Map in the given once for the given Node . |
protected java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> |
SymbolicExecutionTreeBuilder.getAfterBlockMaps(int id)
Returns the after block map used for the given ID.
|
protected java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> |
SymbolicExecutionTreeBuilder.getAfterBlockMaps(SymbolicExecutionTermLabel label)
Returns the after block map.
|
ImmutableList<IExecutionNode<?>> |
ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode.getBlockCompletions()
Returns the up to now discovered
IExecutionNode s. |
protected java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>> |
SymbolicExecutionTreeBuilder.updateAfterBlockMap(Node node,
RuleApp ruleApp)
Updates the after block maps when a symbolic execution tree node is detected.
|
Modifier and Type | Method and Description |
---|---|
void |
ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode.addBlockCompletion(IExecutionNode<?> blockCompletion)
Adds the given block completion.
|
void |
ExecutionNodeReader.AbstractKeYlessExecutionNode.addCallStackEntry(IExecutionNode<?> entry)
Adds the given entry to the call stack.
|
void |
ExecutionNodeReader.AbstractKeYlessExecutionNode.addChild(IExecutionNode<?> child)
Adds the given child.
|
protected void |
ExecutionNodeWriter.appendCallStack(int level,
IExecutionNode<?> node,
boolean saveCallStack,
java.lang.StringBuffer sb)
Appends the call stack entries if required to the given
StringBuffer . |
protected void |
ExecutionNodeWriter.appendChildren(int childLevel,
IExecutionNode<?> parent,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Appends the child nodes to the given
StringBuffer . |
protected void |
ExecutionNodeWriter.appendCompletedBlocks(int level,
IExecutionNode<?> node,
java.lang.StringBuffer sb)
Appends the completed block entries to the given
StringBuffer . |
protected void |
ExecutionNodeWriter.appendConstraints(int level,
IExecutionNode<?> node,
boolean saveConstraints,
java.lang.StringBuffer sb)
Appends the contained
IExecutionConstraint s to the given StringBuffer . |
protected void |
ExecutionNodeWriter.appendExecutionNode(int level,
IExecutionNode<?> node,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints,
java.lang.StringBuffer sb)
Converts the given
IExecutionNode into XML and appends it to the StringBuffer . |
protected void |
ExecutionNodeWriter.appendOutgoingLinks(int level,
IExecutionNode<?> node,
java.lang.StringBuffer sb) |
protected void |
ExecutionNodeWriter.appendVariables(int level,
IExecutionNode<?> node,
boolean saveVariables,
boolean saveConstraints,
java.lang.StringBuffer sb)
Appends the contained
IExecutionVariable s to the given StringBuffer . |
protected java.lang.String |
ExecutionNodeWriter.computePath(IExecutionNode<?> node)
Computes the path from the root of the symbolic execution tree to the given
IExecutionNode . |
protected ExecutionNodeReader.AbstractKeYlessExecutionNode<?> |
ExecutionNodeReader.createExecutionNode(IExecutionNode<?> parent,
java.lang.String uri,
java.lang.String localName,
java.lang.String qName,
org.xml.sax.Attributes attributes)
Creates a new
IExecutionNode with the given content. |
protected IExecutionNode<?> |
ExecutionNodeReader.findNode(IExecutionNode<?> root,
java.lang.String path)
Searches the
IExecutionNode starting at the given root
which is defined by the path. |
IExecutionLink |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getIncomingLink(IExecutionNode<?> source)
Returns the incoming
IExecutionLink . |
protected IExecutionNode<?> |
ExecutionNodePreorderIterator.getNextOnParent(IExecutionNode<?> node)
Returns the next element to select if all children of the given
IExecutionNode are visited. |
IExecutionLink |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getOutgoingLink(IExecutionNode<?> target)
Returns the outgoing
IExecutionLink . |
protected IExecutionBranchCondition |
SymbolicExecutionTreeBuilder.searchDirectParentBodyPreservesInvariantBranchCondition(IExecutionNode<?> current)
Searches the direct parent
IExecutionBranchCondition representing
the 'Body Preserves Invariant' branch. |
void |
ExecutionNodeReader.KeYLessLink.setSource(IExecutionNode<?> source)
Sets the source.
|
void |
ExecutionNodeReader.KeYLessLink.setTarget(IExecutionNode<?> target)
Sets the target.
|
java.lang.String |
ExecutionNodeWriter.toXML(IExecutionNode<?> node,
java.lang.String encoding,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints)
Converts the given
IExecutionNode into XML. |
void |
ExecutionNodeWriter.write(IExecutionNode<?> node,
java.lang.String encoding,
java.io.File file,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints)
Writes the given
IExecutionNode as XML file. |
void |
ExecutionNodeWriter.write(IExecutionNode<?> node,
java.lang.String encoding,
java.io.OutputStream out,
boolean saveVariables,
boolean saveCallStack,
boolean saveReturnValues,
boolean saveConstraints)
Writes the given
IExecutionNode into the OutputStream . |
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>> |
SymbolicExecutionTreeBuilder.findAfterBlockMap(java.util.Map<Node,java.util.Map<SymbolicExecutionTreeBuilder.JavaPair,ImmutableList<IExecutionNode<?>>>> afterBlockMaps,
Node node)
Searches the relevant after block
Map in the given once for the given Node . |
protected boolean |
SymbolicExecutionTreeBuilder.isContained(ImmutableList<IExecutionNode<?>> list,
Node node)
Checks if one of the give
IExecutionNode s represents the given Node . |
Constructor and Description |
---|
AbstractKeYlessBaseExecutionNode(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
java.lang.String signature,
java.lang.String formatedMethodReturn)
Constructor.
|
AbstractKeYlessExecutionBlockStartNode(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
boolean blockOpened)
Constructor.
|
AbstractKeYlessExecutionNode(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged)
Constructor.
|
ExecutionNodePreorderIterator(IExecutionNode<?> start)
Constructor.
|
ExecutionNodeSymbolicLayoutExtractor(IExecutionNode<?> executionNode)
Constructor.
|
ExecutionVariableExtractor(Node node,
PosInOccurrence modalityPio,
IExecutionNode<?> executionNode,
Term condition,
boolean simplifyConditions)
Constructor.
|
ExtractedExecutionValue(IExecutionNode<?> parentNode,
Node proofNode,
IExecutionVariable variable,
Term condition,
Term value)
Constructor.
|
ExtractedExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
IProgramVariable programVariable,
Term arrayIndex,
Term arrayStartIndex,
Term arrayEndIndex,
Term additionalCondition,
ExecutionVariableExtractor.ExtractedExecutionValue parentValue)
Constructor.
|
KeYlessBlockContract(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
boolean preconditionComplied)
Constructor.
|
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.
|
KeYlessBranchStatement(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
boolean blockOpened)
Constructor.
|
KeYlessExceptionalMethodReturn(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
java.lang.String signature,
java.lang.String formatedMethodReturn)
Constructor.
|
KeYlessJoin(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
boolean weakeningVerified)
Constructor.
|
KeYlessLoopCondition(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
boolean blockOpened)
Constructor.
|
KeYlessLoopInvariant(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
boolean initiallyValid)
Constructor.
|
KeYlessLoopStatement(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
boolean blockOpened)
Constructor.
|
KeYlessMethodCall(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged)
Constructor.
|
KeYlessMethodReturn(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
java.lang.String nameIncludingReturnValue,
java.lang.String signature,
java.lang.String signatureIncludingReturnValue,
boolean returnValueComputed,
java.lang.String formatedMethodReturn)
Constructor.
|
KeYlessOperationContract(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
boolean preconditionComplied,
boolean hasNotNullCheck,
boolean notNullCheckComplied,
java.lang.String formatedResultTerm,
java.lang.String formatedExceptionTerm,
java.lang.String formatedSelfTerm,
java.lang.String formatedContractParams)
Constructor.
|
KeYlessStatement(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged)
Constructor.
|
KeYlessTermination(IExecutionNode<?> parent,
java.lang.String name,
java.lang.String formatedPathCondition,
boolean pathConditionChanged,
IExecutionTermination.TerminationKind terminationKind,
boolean branchVerified)
Constructor.
|
Modifier and Type | Interface and Description |
---|---|
interface |
IExecutionAuxiliaryContract
A node in the symbolic execution tree which represents a use block/loop contract application.
|
interface |
IExecutionBaseMethodReturn<S extends SourceElement>
Defines the common interface of
IExecutionMethodReturn
and IExecutionExceptionalMethodReturn . |
interface |
IExecutionBlockStartNode<S extends SourceElement>
An extended
IExecutionNode which groups several child nodes. |
interface |
IExecutionBranchCondition
A node in the symbolic execution tree which represents a branch condition,
e.g.
|
interface |
IExecutionBranchStatement
A node in the symbolic execution tree which represents a node which
creates multiple child branches defined by branch conditions (
ISEDBranchCondition ),
e.g. |
interface |
IExecutionExceptionalMethodReturn
A node in the symbolic execution tree which represents a exceptional method return.
|
interface |
IExecutionJoin
A node in the symbolic execution tree which represents a join.
|
interface |
IExecutionLoopCondition
A node in the symbolic execution tree which represents a loop condition,
e.g.
|
interface |
IExecutionLoopInvariant
A node in the symbolic execution tree which represents a loop invariant application.
|
interface |
IExecutionLoopStatement
A node in the symbolic execution tree which represents a loop.
|
interface |
IExecutionMethodCall
A node in the symbolic execution tree which represents a method call,
e.g.
|
interface |
IExecutionMethodReturn
A node in the symbolic execution tree which represents a method return,
e.g.
|
interface |
IExecutionOperationContract
A node in the symbolic execution tree which represents a use operation contract application.
|
interface |
IExecutionStart
The start node of a symbolic execution tree.
|
interface |
IExecutionStatement
A node in the symbolic execution tree which represents a single statement,
e.g.
|
interface |
IExecutionTermination
A node in the symbolic execution tree which represents the normal termination of a branch,
e.g.
|
Modifier and Type | Method and Description |
---|---|
IExecutionNode<?>[] |
IExecutionNode.getCallStack()
Returns the method call stack.
|
IExecutionNode<?>[] |
IExecutionNode.getChildren()
Returns the available children.
|
IExecutionNode<?> |
IExecutionNode.getParent()
Returns the parent
IExecutionNode or null if the
current node is the root. |
IExecutionNode<?> |
IExecutionLink.getSource()
Returns the source.
|
IExecutionNode<?> |
IExecutionLink.getTarget()
Returns the target.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<IExecutionNode<?>> |
IExecutionBlockStartNode.getBlockCompletions()
Returns the up to now discovered
IExecutionNode s. |
Modifier and Type | Method and Description |
---|---|
IExecutionLink |
IExecutionNode.getIncomingLink(IExecutionNode<?> source)
Returns the incoming
IExecutionLink . |
IExecutionLink |
IExecutionNode.getOutgoingLink(IExecutionNode<?> target)
Returns the outgoing
IExecutionLink . |
Modifier and Type | Method and Description |
---|---|
IExecutionNode<?>[] |
AbstractExecutionNode.getCallStack()
Returns the method call stack.
|
IExecutionNode<?> |
ExecutionVariable.getParentNode()
Returns the parent
IExecutionNode which provides this ExecutionVariable . |
IExecutionNode<?> |
ExecutionLink.getSource()
Returns the source.
|
IExecutionNode<?> |
ExecutionLink.getTarget()
Returns the target.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<IExecutionNode<?>> |
AbstractExecutionBlockStartNode.getBlockCompletions()
Returns the up to now discovered
IExecutionNode s. |
Modifier and Type | Method and Description |
---|---|
void |
AbstractExecutionBlockStartNode.addBlockCompletion(IExecutionNode<?> blockCompletion)
Registers the given
IExecutionNode . |
IExecutionLink |
AbstractExecutionNode.getIncomingLink(IExecutionNode<?> source)
Returns the incoming
IExecutionLink . |
IExecutionLink |
AbstractExecutionNode.getOutgoingLink(IExecutionNode<?> target)
Returns the outgoing
IExecutionLink . |
void |
AbstractExecutionBlockStartNode.removeBlockCompletion(IExecutionNode<?> completion)
Removes the given block completion.
|
void |
AbstractExecutionNode.removeChild(IExecutionNode<?> child)
Removes the given child.
|
void |
AbstractExecutionNode.setCallStack(IExecutionNode<?>[] callStack)
Sets the call stack.
|
Constructor and Description |
---|
ExecutionAllArrayIndicesVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
IProgramVariable arrayProgramVariable,
Term additionalCondition)
Constructor.
|
ExecutionLink(IExecutionNode<?> source,
IExecutionNode<?> target)
Constructor.
|
ExecutionLink(IExecutionNode<?> source,
IExecutionNode<?> target)
Constructor.
|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
IProgramVariable programVariable,
Term additionalCondition)
Constructor for a "normal" child value.
|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
ExecutionValue parentValue,
Term arrayIndex,
ExecutionValue lengthValue,
Term additionalCondition)
Constructor for an array cell value.
|
ExecutionVariable(IExecutionNode<?> parentNode,
Node proofNode,
PosInOccurrence modalityPIO,
IProgramVariable programVariable,
Term additionalCondition)
Constructor for a "normal" value.
|
Modifier and Type | Method and Description |
---|---|
static IExecutionNode<?> |
SymbolicExecutionUtil.getRoot(IExecutionNode<?> executionNode)
Returns the root of the given
IExecutionNode . |
Modifier and Type | Method and Description |
---|---|
static boolean |
SymbolicExecutionUtil.canComputeVariables(IExecutionNode<?> node,
Services services)
Checks if it is right now possible to compute the variables of the given
IExecutionNode
via getVariables() . |
static IExecutionVariable[] |
SymbolicExecutionUtil.createAllExecutionVariables(IExecutionNode<?> node,
Node proofNode,
PosInOccurrence modalityPIO,
Term condition)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static IExecutionConstraint[] |
SymbolicExecutionUtil.createExecutionConstraints(IExecutionNode<?> node)
Creates for the given
IExecutionNode the contained
IExecutionConstraint s. |
static IExecutionVariable[] |
SymbolicExecutionUtil.createExecutionVariables(IExecutionNode<?> node)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static IExecutionVariable[] |
SymbolicExecutionUtil.createExecutionVariables(IExecutionNode<?> node,
Node proofNode,
PosInOccurrence modalityPIO,
Term condition)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static IExecutionVariable[] |
SymbolicExecutionUtil.createExecutionVariables(IExecutionNode<?> node,
Term condition)
Creates for the given
IExecutionNode the contained
root IExecutionVariable s. |
static IExecutionNode<?> |
SymbolicExecutionUtil.getRoot(IExecutionNode<?> executionNode)
Returns the root of the given
IExecutionNode . |
Copyright © 2003-2019 The KeY-Project.