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