public class ExecutionNodeReader
extends java.lang.Object
ExecutionNodeWriter
.ExecutionNodeWriter
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.AbstractKeYlessExecutionElement
An abstract implementation of
IExecutionElement 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.KeYlessConstraint
An implementation of
IExecutionConstraint 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.KeYLessLink
An implementation of
IExecutionLink 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.KeYlessMethodReturnValue
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. |
static class |
ExecutionNodeReader.KeYlessValue
An implementation of
IExecutionValue which is independent
from KeY and provides such only children and default attributes. |
static class |
ExecutionNodeReader.KeYlessVariable
An implementation of
IExecutionVariable which is independent
from KeY and provides such only children and default attributes. |
private class |
ExecutionNodeReader.SEDSAXHandler
DefaultHandler implementation used in read(InputStream) . |
Constructor and Description |
---|
ExecutionNodeReader() |
Modifier and Type | Method and Description |
---|---|
protected ExecutionNodeReader.AbstractKeYlessExecutionNode<?> |
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. |
ExecutionNodeReader.KeYlessMethodReturnValue |
createMethodReturnValue(java.lang.String uri,
java.lang.String localName,
java.lang.String qName,
org.xml.sax.Attributes attributes)
Creates a new
IExecutionMethodReturnValue with the given content. |
protected ExecutionNodeReader.KeYlessValue |
createValue(IExecutionVariable parentVariable,
java.lang.String uri,
java.lang.String localName,
java.lang.String qName,
org.xml.sax.Attributes attributes)
Creates a new
IExecutionValue with the given content. |
protected ExecutionNodeReader.KeYlessVariable |
createVariable(IExecutionValue parentValue,
java.lang.String uri,
java.lang.String localName,
java.lang.String qName,
org.xml.sax.Attributes attributes)
Creates a new
IExecutionVariable with the given content. |
protected IExecutionNode<?> |
findNode(IExecutionNode<?> root,
java.lang.String path)
Searches the
IExecutionNode starting at the given root
which is defined by the path. |
protected java.lang.String |
getAdditionalBranchLabel(org.xml.sax.Attributes attributes)
Returns the additional branch label value.
|
protected java.lang.String |
getArrayIndexString(org.xml.sax.Attributes attributes)
Returns the array index value.
|
protected java.lang.String |
getBranchCondition(org.xml.sax.Attributes attributes)
Returns the branch condition value.
|
protected boolean |
getBranchVerified(org.xml.sax.Attributes attributes)
Returns the is branch verified value.
|
protected java.lang.String |
getConditionString(org.xml.sax.Attributes attributes)
Returns the value condition string value.
|
protected java.lang.String |
getContractParameters(org.xml.sax.Attributes attributes)
Returns the contract parameters value.
|
protected java.lang.String |
getExceptionTerm(org.xml.sax.Attributes attributes)
Returns the exception term value.
|
protected boolean |
getHasCondition(org.xml.sax.Attributes attributes)
Returns the is has condition value.
|
protected java.lang.String |
getMethodReturnCondition(org.xml.sax.Attributes attributes)
Returns the method return condition value.
|
protected java.lang.String |
getName(org.xml.sax.Attributes attributes)
Returns the name value.
|
protected java.lang.String |
getNameIncludingReturnValue(org.xml.sax.Attributes attributes)
Returns the name value including return value.
|
protected java.lang.String |
getPathCondition(org.xml.sax.Attributes attributes)
Returns the path condition value.
|
protected java.lang.String |
getPathInTree(org.xml.sax.Attributes attributes)
Returns the path in tree value.
|
protected java.lang.String |
getResultTerm(org.xml.sax.Attributes attributes)
Returns the result term value.
|
protected java.lang.String |
getReturnValueString(org.xml.sax.Attributes attributes)
Returns the return value string value.
|
protected java.lang.String |
getSelfTerm(org.xml.sax.Attributes attributes)
Returns the self term value.
|
protected java.lang.String |
getSignature(org.xml.sax.Attributes attributes)
Returns the signature value.
|
protected java.lang.String |
getSignatureIncludingReturnValue(org.xml.sax.Attributes attributes)
Returns the signature value including return value.
|
protected IExecutionTermination.TerminationKind |
getTerminationKind(org.xml.sax.Attributes attributes)
Returns the termination kind value.
|
protected java.lang.String |
getTypeString(org.xml.sax.Attributes attributes)
Returns the type string value.
|
protected java.lang.String |
getValueString(org.xml.sax.Attributes attributes)
Returns the value string value.
|
protected boolean |
isArrayIndex(org.xml.sax.Attributes attributes)
Returns the is array index value.
|
protected boolean |
isBlockCompletionEntry(java.lang.String uri,
java.lang.String localName,
java.lang.String qName)
Checks if the currently parsed tag represents an entry of
IExecutionBlockStartNode.getBlockCompletions() . |
protected boolean |
isBlockOpened(org.xml.sax.Attributes attributes)
Returns the block opened value.
|
protected boolean |
isBranchConditionComputed(org.xml.sax.Attributes attributes)
Returns the is branch condition computed value.
|
protected boolean |
isCallStackEntry(java.lang.String uri,
java.lang.String localName,
java.lang.String qName)
Checks if the currently parsed tag represents an entry of
IExecutionNode.getCallStack() . |
protected boolean |
isCallStateVariable(java.lang.String uri,
java.lang.String localName,
java.lang.String qName)
Checks if the currently parsed tag represents an
IExecutionVariable . |
protected boolean |
isCompletedBlockEntry(java.lang.String uri,
java.lang.String localName,
java.lang.String qName)
Checks if the currently parsed tag represents an entry of
IExecutionNode.getCompletedBlocks() . |
protected boolean |
isConstraint(java.lang.String uri,
java.lang.String localName,
java.lang.String qName)
Checks if the currently parsed tag represents an
IExecutionConstraint . |
protected boolean |
isHasNotNullCheck(org.xml.sax.Attributes attributes)
Returns the has not null check value.
|
protected boolean |
isInitiallyValid(org.xml.sax.Attributes attributes)
Returns the initially valid value.
|
protected boolean |
isMergedBranchCondition(org.xml.sax.Attributes attributes)
Returns the merged branch condition value.
|
protected boolean |
isMethodReturnEntry(java.lang.String uri,
java.lang.String localName,
java.lang.String qName)
Checks if the currently parsed tag represents an entry of
IExecutionMethodCall.getMethodReturns() . |
protected boolean |
isMethodReturnValue(java.lang.String uri,
java.lang.String localName,
java.lang.String qName)
Checks if the currently parsed tag represents an
IExecutionMethodReturnValue . |
protected boolean |
isNotNullCheckComplied(org.xml.sax.Attributes attributes)
Returns the not null check complied value.
|
protected boolean |
isOutgoingLink(java.lang.String uri,
java.lang.String localName,
java.lang.String qName)
Checks if the currently parsed tag represents an entry of
IExecutionNode.getOutgoingLinks() . |
protected boolean |
isPathConditionChanged(org.xml.sax.Attributes attributes)
Returns the path condition changed value.
|
protected boolean |
isPreconditionComplied(org.xml.sax.Attributes attributes)
Returns the precondition complied value.
|
protected boolean |
isReturnValueComputed(org.xml.sax.Attributes attributes)
Returns the is return value computed value.
|
protected boolean |
isTerminationEntry(java.lang.String uri,
java.lang.String localName,
java.lang.String qName)
Checks if the currently parsed tag represents an entry of
IExecutionStart.getTerminations() . |
protected boolean |
isValue(java.lang.String uri,
java.lang.String localName,
java.lang.String qName)
Checks if the currently parsed tag represents an
IExecutionValue . |
protected boolean |
isValueAnObject(org.xml.sax.Attributes attributes)
Returns the is value an object value.
|
protected boolean |
isValueUnknown(org.xml.sax.Attributes attributes)
Returns the is value unknown value.
|
protected boolean |
isVariable(java.lang.String uri,
java.lang.String localName,
java.lang.String qName)
Checks if the currently parsed tag represents an
IExecutionVariable . |
protected boolean |
isWeakeningVerified(org.xml.sax.Attributes attributes)
Returns if the weakening is verified.
|
IExecutionNode<?> |
read(java.io.File file)
Reads the given
File . |
IExecutionNode<?> |
read(java.io.InputStream in)
Reads from the given
InputStream and closes it. |
public IExecutionNode<?> read(java.io.File file) throws javax.xml.parsers.ParserConfigurationException, org.xml.sax.SAXException, java.io.IOException
File
.file
- The File
to read.javax.xml.parsers.ParserConfigurationException
- Occurred Exception.org.xml.sax.SAXException
- Occurred Exception.java.io.IOException
- Occurred Exception.public IExecutionNode<?> read(java.io.InputStream in) throws javax.xml.parsers.ParserConfigurationException, org.xml.sax.SAXException, java.io.IOException
InputStream
and closes it.in
- The InputStream
to read from.javax.xml.parsers.ParserConfigurationException
- Occurred Exception.org.xml.sax.SAXException
- Occurred Exception.java.io.IOException
- Occurred Exception.protected IExecutionNode<?> findNode(IExecutionNode<?> root, java.lang.String path) throws org.xml.sax.SAXException
IExecutionNode
starting at the given root
which is defined by the path.root
- The IExecutionNode
to start search.path
- The path.IExecutionNode
.org.xml.sax.SAXException
- If it was not possible to find the node.protected boolean isConstraint(java.lang.String uri, java.lang.String localName, java.lang.String qName)
IExecutionConstraint
.uri
- The URI.localName
- THe local name.qName
- The qName.true
represents an IExecutionConstraint
, false
is something else.protected boolean isVariable(java.lang.String uri, java.lang.String localName, java.lang.String qName)
IExecutionVariable
.uri
- The URI.localName
- THe local name.qName
- The qName.true
represents an IExecutionVariable
, false
is something else.protected boolean isCallStateVariable(java.lang.String uri, java.lang.String localName, java.lang.String qName)
IExecutionVariable
.uri
- The URI.localName
- THe local name.qName
- The qName.true
represents an IExecutionVariable
, false
is something else.protected boolean isMethodReturnValue(java.lang.String uri, java.lang.String localName, java.lang.String qName)
IExecutionMethodReturnValue
.uri
- The URI.localName
- THe local name.qName
- The qName.true
represents an IExecutionMethodReturnValue
, false
is something else.protected boolean isValue(java.lang.String uri, java.lang.String localName, java.lang.String qName)
IExecutionValue
.uri
- The URI.localName
- THe local name.qName
- The qName.true
represents an IExecutionValue
, false
is something else.protected boolean isCallStackEntry(java.lang.String uri, java.lang.String localName, java.lang.String qName)
IExecutionNode.getCallStack()
.uri
- The URI.localName
- THe local name.qName
- The qName.true
represents call stack entry, false
is something else.protected boolean isMethodReturnEntry(java.lang.String uri, java.lang.String localName, java.lang.String qName)
IExecutionMethodCall.getMethodReturns()
.uri
- The URI.localName
- THe local name.qName
- The qName.true
represents method return entry, false
is something else.protected boolean isCompletedBlockEntry(java.lang.String uri, java.lang.String localName, java.lang.String qName)
IExecutionNode.getCompletedBlocks()
.uri
- The URI.localName
- THe local name.qName
- The qName.true
represents completed block entry, false
is something else.protected boolean isOutgoingLink(java.lang.String uri, java.lang.String localName, java.lang.String qName)
IExecutionNode.getOutgoingLinks()
.uri
- The URI.localName
- THe local name.qName
- The qName.true
represents block completion entry, false
is something else.protected boolean isBlockCompletionEntry(java.lang.String uri, java.lang.String localName, java.lang.String qName)
IExecutionBlockStartNode.getBlockCompletions()
.uri
- The URI.localName
- THe local name.qName
- The qName.true
represents block completion entry, false
is something else.protected boolean isTerminationEntry(java.lang.String uri, java.lang.String localName, java.lang.String qName)
IExecutionStart.getTerminations()
.uri
- The URI.localName
- THe local name.qName
- The qName.true
represents termination entry, false
is something else.protected ExecutionNodeReader.KeYlessVariable createVariable(IExecutionValue parentValue, java.lang.String uri, java.lang.String localName, java.lang.String qName, org.xml.sax.Attributes attributes)
IExecutionVariable
with the given content.parentValue
- The parent IExecutionValue
.uri
- The URI.localName
- THe local name.qName
- The qName.attributes
- The attributes.IExecutionVariable
.public ExecutionNodeReader.KeYlessMethodReturnValue createMethodReturnValue(java.lang.String uri, java.lang.String localName, java.lang.String qName, org.xml.sax.Attributes attributes)
IExecutionMethodReturnValue
with the given content.uri
- The URI.localName
- THe local name.qName
- The qName.attributes
- The attributes.IExecutionMethodReturnValue
.protected ExecutionNodeReader.KeYlessValue createValue(IExecutionVariable parentVariable, java.lang.String uri, java.lang.String localName, java.lang.String qName, org.xml.sax.Attributes attributes)
IExecutionValue
with the given content.parentVariable
- The parent IExecutionVariable
.uri
- The URI.localName
- THe local name.qName
- The qName.attributes
- The attributes.IExecutionValue
.protected ExecutionNodeReader.AbstractKeYlessExecutionNode<?> createExecutionNode(IExecutionNode<?> parent, java.lang.String uri, java.lang.String localName, java.lang.String qName, org.xml.sax.Attributes attributes) throws org.xml.sax.SAXException
IExecutionNode
with the given content.parent
- The parent IExecutionNode
.uri
- The URI.localName
- THe local name.qName
- The qName.attributes
- The attributes.IExecutionNode
.org.xml.sax.SAXException
- Occurred Exception.protected java.lang.String getAdditionalBranchLabel(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getPathInTree(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getName(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getNameIncludingReturnValue(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getSignature(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getSignatureIncludingReturnValue(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected IExecutionTermination.TerminationKind getTerminationKind(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected boolean isPreconditionComplied(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected boolean isHasNotNullCheck(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected boolean isBlockOpened(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected boolean isReturnValueComputed(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected boolean isBranchConditionComputed(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected boolean isNotNullCheckComplied(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected boolean isInitiallyValid(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected boolean isValueAnObject(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected boolean isWeakeningVerified(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected boolean isValueUnknown(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getValueString(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getConditionString(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected boolean getHasCondition(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected boolean getBranchVerified(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getReturnValueString(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getTypeString(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getExceptionTerm(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getResultTerm(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getSelfTerm(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getContractParameters(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getArrayIndexString(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected boolean isArrayIndex(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getBranchCondition(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getPathCondition(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected java.lang.String getMethodReturnCondition(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected boolean isPathConditionChanged(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.protected boolean isMergedBranchCondition(org.xml.sax.Attributes attributes)
attributes
- The Attributes
which provides the content.