de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeReader.SEDSAXHandler

java.lang.Object

org.xml.sax.helpers.DefaultHandler

de.uka.ilkd.key.symbolic_execution.ExecutionNodeReader.SEDSAXHandler

All Implemented Interfaces:

org.xml.sax.ContentHandler, org.xml.sax.DTDHandler, org.xml.sax.EntityResolver, org.xml.sax.ErrorHandler

Enclosing class:

ExecutionNodeReader

private class ExecutionNodeReader.SEDSAXHandler
extends org.xml.sax.helpers.DefaultHandler

DefaultHandler implementation used in ExecutionNodeReader.read(InputStream).

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode<?>,java.util.List<java.lang.String>>	blockCompletionEntries Maps an ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode to the path entries of its block completions.
private java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionNode<?>,java.util.List<java.lang.String>>	callStackPathEntries Maps an ExecutionNodeReader.AbstractKeYlessExecutionNode to the path entries of its call stack.
private java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionNode<?>,java.util.List<Pair<java.lang.String,java.lang.String>>>	completedBlockEntries Maps an ExecutionNodeReader.AbstractKeYlessExecutionNode to its completed block entries
private java.util.Map<ExecutionNodeReader.KeYlessMethodCall,java.util.List<java.lang.String>>	methodReturnPathEntries Maps an ExecutionNodeReader.KeYlessMethodCall to the path entries of its method returns.
private java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionNode<?>,java.util.List<java.lang.String>>	outgoingLinks Maps an ExecutionNodeReader.AbstractKeYlessExecutionNode to the path entries of its outgoing links.
private java.util.Deque<ExecutionNodeReader.AbstractKeYlessExecutionNode<?>>	parentNodeStack The parent hierarchy filled by startElement(String, String, String, Attributes) and emptied by endElement(String, String, String).
private java.util.Deque<java.lang.Object>	parentVariableValueStack The parent hierarchy of IExecutionVariable and IExecutionValue filled by startElement(String, String, String, Attributes) and emptied by endElement(String, String, String).
private IExecutionNode<?>	root The root of the read symbolic execution tree.
private java.util.Map<ExecutionNodeReader.KeYlessStart,java.util.List<java.lang.String>>	terminationPathEntries Maps an ExecutionNodeReader.KeYlessStart to the path entries of its terminations.

Constructor Summary

Constructors

Modifier	Constructor and Description
private	SEDSAXHandler()

Method Summary

Modifier and Type	Method and Description
void	endElement(java.lang.String uri, java.lang.String localName, java.lang.String qName)
java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode<?>,java.util.List<java.lang.String>>	getBlockCompletionEntries() Returns the mapping of an ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode to its block completion entries.
java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionNode<?>,java.util.List<java.lang.String>>	getCallStackPathEntries() Returns the mapping of an ExecutionNodeReader.AbstractKeYlessExecutionNode to its call stack entries.
java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionNode<?>,java.util.List<Pair<java.lang.String,java.lang.String>>>	getCompletedBlockEntries() Returns the mapping of ExecutionNodeReader.AbstractKeYlessExecutionNode to its completed block entries.
java.util.Map<ExecutionNodeReader.KeYlessMethodCall,java.util.List<java.lang.String>>	getMethodReturnPathEntries() Returns the mapping of a ExecutionNodeReader.KeYlessMethodCall to its method return entries.
java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionNode<?>,java.util.List<java.lang.String>>	getOutgoingLinks() Returns the mapping of an ExecutionNodeReader.AbstractKeYlessExecutionNode to its outgoing links.
IExecutionNode<?>	getRoot() Returns the root of the read symbolic execution tree.
java.util.Map<ExecutionNodeReader.KeYlessStart,java.util.List<java.lang.String>>	getTerminationPathEntries() Returns the mapping of a ExecutionNodeReader.KeYlessStart to its termination entries.
void	startElement(java.lang.String uri, java.lang.String localName, java.lang.String qName, org.xml.sax.Attributes attributes)

Methods inherited from class org.xml.sax.helpers.DefaultHandler

characters, endDocument, endPrefixMapping, error, fatalError, ignorableWhitespace, notationDecl, processingInstruction, resolveEntity, setDocumentLocator, skippedEntity, startDocument, startPrefixMapping, unparsedEntityDecl, warning

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

root

private IExecutionNode<?> root

The root of the read symbolic execution tree.

parentNodeStack

private final java.util.Deque<ExecutionNodeReader.AbstractKeYlessExecutionNode<?>> parentNodeStack

The parent hierarchy filled by startElement(String, String, String, Attributes) and emptied by endElement(String, String, String).

parentVariableValueStack

private final java.util.Deque<java.lang.Object> parentVariableValueStack

The parent hierarchy of IExecutionVariable and IExecutionValue filled by startElement(String, String, String, Attributes) and emptied by endElement(String, String, String).

callStackPathEntries

private final java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionNode<?>,java.util.List<java.lang.String>> callStackPathEntries

Maps an ExecutionNodeReader.AbstractKeYlessExecutionNode to the path entries of its call stack.

methodReturnPathEntries

private final java.util.Map<ExecutionNodeReader.KeYlessMethodCall,java.util.List<java.lang.String>> methodReturnPathEntries

Maps an ExecutionNodeReader.KeYlessMethodCall to the path entries of its method returns.

completedBlockEntries

private final java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionNode<?>,java.util.List<Pair<java.lang.String,java.lang.String>>> completedBlockEntries

Maps an ExecutionNodeReader.AbstractKeYlessExecutionNode to its completed block entries

blockCompletionEntries

private final java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode<?>,java.util.List<java.lang.String>> blockCompletionEntries

Maps an ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode to the path entries of its block completions.

outgoingLinks

private final java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionNode<?>,java.util.List<java.lang.String>> outgoingLinks

Maps an ExecutionNodeReader.AbstractKeYlessExecutionNode to the path entries of its outgoing links.

terminationPathEntries

private final java.util.Map<ExecutionNodeReader.KeYlessStart,java.util.List<java.lang.String>> terminationPathEntries

Maps an ExecutionNodeReader.KeYlessStart to the path entries of its terminations.

Constructor Detail

SEDSAXHandler

private SEDSAXHandler()

Method Detail

startElement

public void startElement(java.lang.String uri,
                         java.lang.String localName,
                         java.lang.String qName,
                         org.xml.sax.Attributes attributes)
                  throws org.xml.sax.SAXException

Specified by:

startElement in interface org.xml.sax.ContentHandler

Overrides:

startElement in class org.xml.sax.helpers.DefaultHandler

Throws:

org.xml.sax.SAXException

endElement

public void endElement(java.lang.String uri,
                       java.lang.String localName,
                       java.lang.String qName)
                throws org.xml.sax.SAXException

Specified by:

endElement in interface org.xml.sax.ContentHandler

Overrides:

endElement in class org.xml.sax.helpers.DefaultHandler

Throws:

org.xml.sax.SAXException

getRoot

public IExecutionNode<?> getRoot()

Returns the root of the read symbolic execution tree.

Returns:

The root of the read symbolic execution tree.

getCallStackPathEntries

public java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionNode<?>,java.util.List<java.lang.String>> getCallStackPathEntries()

Returns the mapping of an ExecutionNodeReader.AbstractKeYlessExecutionNode to its call stack entries.

Returns:

The mapping of an ExecutionNodeReader.AbstractKeYlessExecutionNode to its call stack entries.

getMethodReturnPathEntries

public java.util.Map<ExecutionNodeReader.KeYlessMethodCall,java.util.List<java.lang.String>> getMethodReturnPathEntries()

Returns the mapping of a ExecutionNodeReader.KeYlessMethodCall to its method return entries.

Returns:

The mapping of a ExecutionNodeReader.KeYlessMethodCall to its method return entries.

getCompletedBlockEntries

public java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionNode<?>,java.util.List<Pair<java.lang.String,java.lang.String>>> getCompletedBlockEntries()

Returns the mapping of ExecutionNodeReader.AbstractKeYlessExecutionNode to its completed block entries.

Returns:

The mapping of ExecutionNodeReader.AbstractKeYlessExecutionNode to its completed block entries.

getBlockCompletionEntries

public java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode<?>,java.util.List<java.lang.String>> getBlockCompletionEntries()

Returns the mapping of an ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode to its block completion entries.

Returns:

The mapping of an ExecutionNodeReader.AbstractKeYlessExecutionBlockStartNode to its block completion entries.

getTerminationPathEntries

public java.util.Map<ExecutionNodeReader.KeYlessStart,java.util.List<java.lang.String>> getTerminationPathEntries()

Returns the mapping of a ExecutionNodeReader.KeYlessStart to its termination entries.

Returns:

The mapping of a ExecutionNodeReader.KeYlessStart to its termination entries.

getOutgoingLinks

public java.util.Map<ExecutionNodeReader.AbstractKeYlessExecutionNode<?>,java.util.List<java.lang.String>> getOutgoingLinks()

Returns the mapping of an ExecutionNodeReader.AbstractKeYlessExecutionNode to its outgoing links.

Returns:

The mapping of an ExecutionNodeReader.AbstractKeYlessExecutionNode to its outgoing links.