de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeWriter

java.lang.Object

de.uka.ilkd.key.symbolic_execution.AbstractWriter

de.uka.ilkd.key.symbolic_execution.ExecutionNodeWriter

public class ExecutionNodeWriter
extends AbstractWriter

Allows to persistent selected properties of IExecutionNodes as XML file. Such files can be read via an ExecutionNodeReader instance.

Author:

Martin Hentschel

See Also:

ExecutionNodeReader

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	ATTRIBUTE_ADDITIONAL_BRANCH_LABEL Attribute name to store IExecutionBranchCondition.getAdditionalBranchLabel().
static java.lang.String	ATTRIBUTE_ARRAY_INDEX Attribute name to store IExecutionVariable.getArrayIndexString().
static java.lang.String	ATTRIBUTE_BLOCK_OPENED Attribute name to store IExecutionBlockStartNode.isBlockOpened().
static java.lang.String	ATTRIBUTE_BRANCH_CONDITION Attribute name to store IExecutionBranchCondition.getFormatedBranchCondition().
static java.lang.String	ATTRIBUTE_BRANCH_CONDITION_COMPUTED Attribute name to store IExecutionBranchCondition.isBranchConditionComputed().
static java.lang.String	ATTRIBUTE_BRANCH_VERIFIED Attribute name to store IExecutionTermination.isBranchVerified().
static java.lang.String	ATTRIBUTE_CONDITION_STRING Attribute name to store IExecutionValue.getConditionString().
static java.lang.String	ATTRIBUTE_CONTRACT_PARAMETERS Attribute name to store IExecutionOperationContract.getFormatedContractParams().
static java.lang.String	ATTRIBUTE_EXCEPTION_TERM Attribute name to store IExecutionOperationContract.getFormatedExceptionTerm().
static java.lang.String	ATTRIBUTE_HAS_CONDITION Attribute name to store IExecutionMethodReturnValue.hasCondition().
static java.lang.String	ATTRIBUTE_HAS_NOT_NULL_CHECK Attribute name to store IExecutionOperationContract.hasNotNullCheck().
static java.lang.String	ATTRIBUTE_INITIALLY_VALID Attribute name to store IExecutionLoopInvariant.isInitiallyValid().
static java.lang.String	ATTRIBUTE_IS_ARRAY_INDEX Attribute name to store IExecutionVariable.isArrayIndex().
static java.lang.String	ATTRIBUTE_IS_VALUE_AN_OBJECT Attribute name to store IExecutionVariable#isValueAnObject().
static java.lang.String	ATTRIBUTE_IS_VALUE_UNKNOWN Attribute name to store IExecutionVariable#isValueUnknown().
static java.lang.String	ATTRIBUTE_MERGED_BRANCH_CONDITION Attribute name to store IExecutionBranchCondition.isMergedBranchCondition().
static java.lang.String	ATTRIBUTE_METHOD_RETURN_CONDITION Attribute name to store IExecutionBaseMethodReturn.getMethodReturnCondition().
static java.lang.String	ATTRIBUTE_NAME Attribute name to store IExecutionElement.getName().
static java.lang.String	ATTRIBUTE_NAME_INCLUDING_RETURN_VALUE Attribute name to store IExecutionMethodReturn.getNameIncludingReturnValue().
static java.lang.String	ATTRIBUTE_NOT_NULL_CHECK_COMPLIED Attribute name to store IExecutionOperationContract.isNotNullCheckComplied().
static java.lang.String	ATTRIBUTE_PATH_CONDITION Attribute name to store IExecutionNode.getPathCondition().
static java.lang.String	ATTRIBUTE_PATH_CONDITION_CHANGED Attribute name to store IExecutionNode.isPathConditionChanged().
static java.lang.String	ATTRIBUTE_PATH_IN_TREE A path which refers to an IExecutionNode starting from the root.
static java.lang.String	ATTRIBUTE_PRECONDITION_COMPLIED Attribute name to store IExecutionOperationContract.isPreconditionComplied().
static java.lang.String	ATTRIBUTE_RESULT_TERM Attribute name to store IExecutionOperationContract.getFormatedResultTerm().
static java.lang.String	ATTRIBUTE_RETURN_VALUE_COMPUTED Attribute name to store IExecutionMethodReturn.isReturnValuesComputed().
static java.lang.String	ATTRIBUTE_RETURN_VALUE_STRING Attribute name to store IExecutionMethodReturnValue.getReturnValueString().
static java.lang.String	ATTRIBUTE_SELF_TERM Attribute name to store IExecutionOperationContract.getFormatedSelfTerm().
static java.lang.String	ATTRIBUTE_SIGNATURE Attribute name to store IExecutionBaseMethodReturn.getSignature().
static java.lang.String	ATTRIBUTE_SIGNATURE_INCLUDING_RETURN_VALUE Attribute name to store IExecutionMethodReturn.getSignatureIncludingReturnValue().
static java.lang.String	ATTRIBUTE_TERMINATION_KIND Attribute exceptional termination to store IExecutionTermination.getTerminationKind().
static java.lang.String	ATTRIBUTE_TYPE_STRING Attribute name to store IExecutionVariable#getTypeString().
static java.lang.String	ATTRIBUTE_VALUE_STRING Attribute name to store IExecutionVariable#getValueString().
static java.lang.String	ATTRIBUTE_WEAKENING_VERIFIED Attribute name to store IExecutionJoin.isWeakeningVerified().
static char	PATH_SEPARATOR Character to separate path entries in attributes "path".
static java.lang.String	TAG_BLOCK_COMPLETION_ENTRY Tag name to store one entry of IExecutionBlockStartNode.getBlockCompletions().
static java.lang.String	TAG_BLOCK_CONTRACT Tag name to store IExecutionAuxiliaryContracts.
static java.lang.String	TAG_BRANCH_CONDITION Tag name to store IExecutionBranchConditions.
static java.lang.String	TAG_BRANCH_STATEMENT Tag name to store IExecutionBranchStatements.
static java.lang.String	TAG_CALL_STACK_ENTRY Tag name to store one entry of IExecutionNode.getCallStack().
static java.lang.String	TAG_CALL_STATE_VARIABLE Tag name to store call state IExecutionVariables.
static java.lang.String	TAG_COMPLETED_BLOCK_ENTRY Tag name to store on entry of IExecutionNode.getCompletedBlocks() together with its condition IExecutionNode#getFormatedBlockCompletionCondition(IExecutionNode).
static java.lang.String	TAG_CONSTRAINT Tag name to store IExecutionConstraints.
static java.lang.String	TAG_EXCEPTIONAL_METHOD_RETURN Tag name to store IExecutionExceptionalMethodReturns.
static java.lang.String	TAG_JOIN Tag name to store IExecutionJoins.
static java.lang.String	TAG_LOOP_CONDITION Tag name to store IExecutionLoopConditions.
static java.lang.String	TAG_LOOP_INVARIANT Tag name to store IExecutionLoopInvariants.
static java.lang.String	TAG_LOOP_STATEMENT Tag name to store IExecutionLoopStatements.
static java.lang.String	TAG_METHOD_CALL Tag name to store IExecutionMethodCalls.
static java.lang.String	TAG_METHOD_RETURN Tag name to store IExecutionMethodReturns.
static java.lang.String	TAG_METHOD_RETURN_ENTRY Tag name to store one entry of IExecutionMethodCall.getMethodReturns().
static java.lang.String	TAG_METHOD_RETURN_VALUE Tag name to store IExecutionMethodReturnValues.
static java.lang.String	TAG_OPERATION_CONTRACT Tag name to store IExecutionOperationContracts.
static java.lang.String	TAG_OUTGOING_LINK Tag name to store one entry of IExecutionNode.getOutgoingLinks().
static java.lang.String	TAG_START Tag name to store IExecutionStarts.
static java.lang.String	TAG_STATEMENT Tag name to store IExecutionStatements.
static java.lang.String	TAG_TERMINATION Tag name to store IExecutionTerminations.
static java.lang.String	TAG_TERMINATION_ENTRY Tag name to store one entry of IExecutionStart.getTerminations().
static java.lang.String	TAG_VALUE Tag name to store IExecutionValues.
static java.lang.String	TAG_VARIABLE Tag name to store IExecutionVariables.

Fields inherited from class de.uka.ilkd.key.symbolic_execution.AbstractWriter

ATTRIBUTE_ENCODING, ATTRIBUTE_XML_ID, DEFAULT_ENCODING, LEADING_WHITE_SPACE_PER_LEVEL, NEW_LINE

Constructor Summary

Constructors

Constructor and Description
ExecutionNodeWriter()

Method Summary

Modifier and Type	Method and Description
protected void	appendBlockCompletions(int level, IExecutionBlockStartNode<?> node, java.lang.StringBuffer sb) Appends the block completion entries to the given StringBuffer.
protected void	appendCallStack(int level, IExecutionNode<?> node, boolean saveCallStack, java.lang.StringBuffer sb) Appends the call stack entries if required to the given StringBuffer.
protected void	appendCallStateVariables(int level, IExecutionBaseMethodReturn<?> node, boolean saveVariables, boolean saveConstraints, java.lang.StringBuffer sb) Appends the contained IExecutionVariables to the given StringBuffer.
protected void	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	appendCompletedBlocks(int level, IExecutionNode<?> node, java.lang.StringBuffer sb) Appends the completed block entries to the given StringBuffer.
protected void	appendConstraint(int level, IExecutionConstraint constraint, java.lang.StringBuffer sb) Appends the given IExecutionConstraint with its children to the given StringBuffer.
protected void	appendConstraints(int level, IExecutionNode<?> node, boolean saveConstraints, java.lang.StringBuffer sb) Appends the contained IExecutionConstraints to the given StringBuffer.
protected void	appendConstraints(int level, IExecutionValue value, boolean saveConstraints, java.lang.StringBuffer sb) Appends the contained IExecutionConstraints to the given StringBuffer.
protected void	appendExecutionBlockContract(int level, IExecutionAuxiliaryContract node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, java.lang.StringBuffer sb) Converts the given IExecutionAuxiliaryContract into XML and appends it to the StringBuffer.
protected void	appendExecutionBranchCondition(int level, IExecutionBranchCondition node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, java.lang.StringBuffer sb) Converts the given IExecutionBranchCondition into XML and appends it to the StringBuffer.
protected void	appendExecutionBranchStatement(int level, IExecutionBranchStatement node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, java.lang.StringBuffer sb) Converts the given IExecutionLoopCondition into XML and appends it to the StringBuffer.
protected void	appendExecutionExceptionalMethodReturn(int level, IExecutionExceptionalMethodReturn node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, java.lang.StringBuffer sb) Converts the given IExecutionExceptionalMethodReturn into XML and appends it to the StringBuffer.
protected void	appendExecutionJoin(int level, IExecutionJoin node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, java.lang.StringBuffer sb) Converts the given IExecutionJoin into XML and appends it to the StringBuffer.
protected void	appendExecutionLoopCondition(int level, IExecutionLoopCondition node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, java.lang.StringBuffer sb) Converts the given IExecutionLoopCondition into XML and appends it to the StringBuffer.
protected void	appendExecutionLoopInvariant(int level, IExecutionLoopInvariant node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, java.lang.StringBuffer sb) Converts the given IExecutionLoopInvariant into XML and appends it to the StringBuffer.
protected void	appendExecutionLoopStatement(int level, IExecutionLoopStatement node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, java.lang.StringBuffer sb) Converts the given IExecutionLoopStatement into XML and appends it to the StringBuffer.
protected void	appendExecutionMethodCall(int level, IExecutionMethodCall node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, java.lang.StringBuffer sb) Converts the given IExecutionMethodCall into XML and appends it to the StringBuffer.
protected void	appendExecutionMethodReturn(int level, IExecutionMethodReturn node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, java.lang.StringBuffer sb) Converts the given IExecutionMethodReturn into XML and appends it to the StringBuffer.
protected void	appendExecutionMethodReturnValue(int level, IExecutionMethodReturnValue returnValue, java.lang.StringBuffer sb) Converts the given IExecutionMethodReturnValue into XML and appends it to the StringBuffer.
protected void	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	appendExecutionOperationContract(int level, IExecutionOperationContract node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, java.lang.StringBuffer sb) Converts the given IExecutionOperationContract into XML and appends it to the StringBuffer.
protected void	appendExecutionStart(int level, IExecutionStart node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, java.lang.StringBuffer sb) Converts the given IExecutionStart into XML and appends it to the StringBuffer.
protected void	appendExecutionStatement(int level, IExecutionStatement node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, java.lang.StringBuffer sb) Converts the given IExecutionStatement into XML and appends it to the StringBuffer.
protected void	appendExecutionTermination(int level, IExecutionTermination node, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints, java.lang.StringBuffer sb) Converts the given IExecutionTermination into XML and appends it to the StringBuffer.
protected void	appendMethodReturns(int level, IExecutionMethodCall node, java.lang.StringBuffer sb) Appends the method return entries to the given StringBuffer.
protected void	appendOutgoingLink(int level, IExecutionLink link, java.lang.StringBuffer sb)
protected void	appendOutgoingLinks(int level, IExecutionNode<?> node, java.lang.StringBuffer sb)
protected void	appendTerminations(int level, IExecutionStart node, java.lang.StringBuffer sb) Appends the termination entries to the given StringBuffer.
protected void	appendValue(int level, IExecutionValue value, boolean saveConstraints, java.lang.StringBuffer sb) Appends the given IExecutionValue with its children to the given StringBuffer.
protected void	appendValues(int level, IExecutionVariable variable, boolean saveConstraints, java.lang.StringBuffer sb) Appends the contained IExecutionValues to the given StringBuffer.
protected void	appendVariable(int level, IExecutionVariable variable, boolean saveConstraints, java.lang.String tagName, java.lang.StringBuffer sb) Appends the given IExecutionVariable with its children to the given StringBuffer.
protected void	appendVariables(int level, IExecutionNode<?> node, boolean saveVariables, boolean saveConstraints, java.lang.StringBuffer sb) Appends the contained IExecutionVariables to the given StringBuffer.
protected java.lang.String	computePath(IExecutionNode<?> node) Computes the path from the root of the symbolic execution tree to the given IExecutionNode.
java.lang.String	toXML(IExecutionNode<?> node, java.lang.String encoding, boolean saveVariables, boolean saveCallStack, boolean saveReturnValues, boolean saveConstraints) Converts the given IExecutionNode into XML.
void	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	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.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.AbstractWriter

appendAttribute, appendEmptyTag, appendEndTag, appendNewLine, appendStartTag, appendWhiteSpace, appendXmlHeader

Methods inherited from class java.lang.Object

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

Field Detail

ATTRIBUTE_NAME

public static final java.lang.String ATTRIBUTE_NAME

Attribute name to store IExecutionElement.getName().

See Also:

Constant Field Values

ATTRIBUTE_NAME_INCLUDING_RETURN_VALUE

public static final java.lang.String ATTRIBUTE_NAME_INCLUDING_RETURN_VALUE

Attribute name to store IExecutionMethodReturn.getNameIncludingReturnValue().

See Also:

Constant Field Values

ATTRIBUTE_SIGNATURE_INCLUDING_RETURN_VALUE

public static final java.lang.String ATTRIBUTE_SIGNATURE_INCLUDING_RETURN_VALUE

Attribute name to store IExecutionMethodReturn.getSignatureIncludingReturnValue().

See Also:

Constant Field Values

ATTRIBUTE_SIGNATURE

public static final java.lang.String ATTRIBUTE_SIGNATURE

Attribute name to store IExecutionBaseMethodReturn.getSignature().

See Also:

Constant Field Values

ATTRIBUTE_TERMINATION_KIND

public static final java.lang.String ATTRIBUTE_TERMINATION_KIND

Attribute exceptional termination to store IExecutionTermination.getTerminationKind().

See Also:

Constant Field Values

ATTRIBUTE_TYPE_STRING

public static final java.lang.String ATTRIBUTE_TYPE_STRING

Attribute name to store IExecutionVariable#getTypeString().

See Also:

Constant Field Values

ATTRIBUTE_VALUE_STRING

public static final java.lang.String ATTRIBUTE_VALUE_STRING

Attribute name to store IExecutionVariable#getValueString().

See Also:

Constant Field Values

ATTRIBUTE_CONDITION_STRING

public static final java.lang.String ATTRIBUTE_CONDITION_STRING

Attribute name to store IExecutionValue.getConditionString().

See Also:

Constant Field Values

ATTRIBUTE_RETURN_VALUE_STRING

public static final java.lang.String ATTRIBUTE_RETURN_VALUE_STRING

Attribute name to store IExecutionMethodReturnValue.getReturnValueString().

See Also:

Constant Field Values

ATTRIBUTE_HAS_CONDITION

public static final java.lang.String ATTRIBUTE_HAS_CONDITION

Attribute name to store IExecutionMethodReturnValue.hasCondition().

See Also:

Constant Field Values

ATTRIBUTE_BRANCH_VERIFIED

public static final java.lang.String ATTRIBUTE_BRANCH_VERIFIED

Attribute name to store IExecutionTermination.isBranchVerified().

See Also:

Constant Field Values

ATTRIBUTE_ARRAY_INDEX

public static final java.lang.String ATTRIBUTE_ARRAY_INDEX

Attribute name to store IExecutionVariable.getArrayIndexString().

See Also:

Constant Field Values

ATTRIBUTE_IS_ARRAY_INDEX

public static final java.lang.String ATTRIBUTE_IS_ARRAY_INDEX

Attribute name to store IExecutionVariable.isArrayIndex().

See Also:

Constant Field Values

ATTRIBUTE_BRANCH_CONDITION

public static final java.lang.String ATTRIBUTE_BRANCH_CONDITION

Attribute name to store IExecutionBranchCondition.getFormatedBranchCondition().

See Also:

Constant Field Values

ATTRIBUTE_PATH_CONDITION

public static final java.lang.String ATTRIBUTE_PATH_CONDITION

Attribute name to store IExecutionNode.getPathCondition().

See Also:

Constant Field Values

ATTRIBUTE_PATH_CONDITION_CHANGED

public static final java.lang.String ATTRIBUTE_PATH_CONDITION_CHANGED

Attribute name to store IExecutionNode.isPathConditionChanged().

See Also:

Constant Field Values

ATTRIBUTE_PATH_IN_TREE

public static final java.lang.String ATTRIBUTE_PATH_IN_TREE

A path which refers to an IExecutionNode starting from the root.

See Also:

Constant Field Values

ATTRIBUTE_MERGED_BRANCH_CONDITION

public static final java.lang.String ATTRIBUTE_MERGED_BRANCH_CONDITION

Attribute name to store IExecutionBranchCondition.isMergedBranchCondition().

See Also:

Constant Field Values

ATTRIBUTE_IS_VALUE_AN_OBJECT

public static final java.lang.String ATTRIBUTE_IS_VALUE_AN_OBJECT

Attribute name to store IExecutionVariable#isValueAnObject().

See Also:

Constant Field Values

ATTRIBUTE_IS_VALUE_UNKNOWN

public static final java.lang.String ATTRIBUTE_IS_VALUE_UNKNOWN

Attribute name to store IExecutionVariable#isValueUnknown().

See Also:

Constant Field Values

ATTRIBUTE_PRECONDITION_COMPLIED

public static final java.lang.String ATTRIBUTE_PRECONDITION_COMPLIED

Attribute name to store IExecutionOperationContract.isPreconditionComplied().

See Also:

Constant Field Values

ATTRIBUTE_HAS_NOT_NULL_CHECK

public static final java.lang.String ATTRIBUTE_HAS_NOT_NULL_CHECK

Attribute name to store IExecutionOperationContract.hasNotNullCheck().

See Also:

Constant Field Values

ATTRIBUTE_RETURN_VALUE_COMPUTED

public static final java.lang.String ATTRIBUTE_RETURN_VALUE_COMPUTED

Attribute name to store IExecutionMethodReturn.isReturnValuesComputed().

See Also:

Constant Field Values

ATTRIBUTE_BRANCH_CONDITION_COMPUTED

public static final java.lang.String ATTRIBUTE_BRANCH_CONDITION_COMPUTED

Attribute name to store IExecutionBranchCondition.isBranchConditionComputed().

See Also:

Constant Field Values

ATTRIBUTE_NOT_NULL_CHECK_COMPLIED

public static final java.lang.String ATTRIBUTE_NOT_NULL_CHECK_COMPLIED

Attribute name to store IExecutionOperationContract.isNotNullCheckComplied().

See Also:

Constant Field Values

ATTRIBUTE_INITIALLY_VALID

public static final java.lang.String ATTRIBUTE_INITIALLY_VALID

Attribute name to store IExecutionLoopInvariant.isInitiallyValid().

See Also:

Constant Field Values

ATTRIBUTE_ADDITIONAL_BRANCH_LABEL

public static final java.lang.String ATTRIBUTE_ADDITIONAL_BRANCH_LABEL

Attribute name to store IExecutionBranchCondition.getAdditionalBranchLabel().

See Also:

Constant Field Values

ATTRIBUTE_METHOD_RETURN_CONDITION

public static final java.lang.String ATTRIBUTE_METHOD_RETURN_CONDITION

Attribute name to store IExecutionBaseMethodReturn.getMethodReturnCondition().

See Also:

Constant Field Values

ATTRIBUTE_RESULT_TERM

public static final java.lang.String ATTRIBUTE_RESULT_TERM

Attribute name to store IExecutionOperationContract.getFormatedResultTerm().

See Also:

Constant Field Values

ATTRIBUTE_EXCEPTION_TERM

public static final java.lang.String ATTRIBUTE_EXCEPTION_TERM

Attribute name to store IExecutionOperationContract.getFormatedExceptionTerm().

See Also:

Constant Field Values

ATTRIBUTE_SELF_TERM

public static final java.lang.String ATTRIBUTE_SELF_TERM

Attribute name to store IExecutionOperationContract.getFormatedSelfTerm().

See Also:

Constant Field Values

ATTRIBUTE_CONTRACT_PARAMETERS

public static final java.lang.String ATTRIBUTE_CONTRACT_PARAMETERS

Attribute name to store IExecutionOperationContract.getFormatedContractParams().

See Also:

Constant Field Values

ATTRIBUTE_BLOCK_OPENED

public static final java.lang.String ATTRIBUTE_BLOCK_OPENED

Attribute name to store IExecutionBlockStartNode.isBlockOpened().

See Also:

Constant Field Values

ATTRIBUTE_WEAKENING_VERIFIED

public static final java.lang.String ATTRIBUTE_WEAKENING_VERIFIED

Attribute name to store IExecutionJoin.isWeakeningVerified().

See Also:

Constant Field Values

TAG_BRANCH_CONDITION

public static final java.lang.String TAG_BRANCH_CONDITION

Tag name to store IExecutionBranchConditions.

See Also:

Constant Field Values

TAG_START

public static final java.lang.String TAG_START

Tag name to store IExecutionStarts.

See Also:

Constant Field Values

TAG_BRANCH_STATEMENT

public static final java.lang.String TAG_BRANCH_STATEMENT

Tag name to store IExecutionBranchStatements.

See Also:

Constant Field Values

TAG_LOOP_CONDITION

public static final java.lang.String TAG_LOOP_CONDITION

Tag name to store IExecutionLoopConditions.

See Also:

Constant Field Values

TAG_LOOP_STATEMENT

public static final java.lang.String TAG_LOOP_STATEMENT

Tag name to store IExecutionLoopStatements.

See Also:

Constant Field Values

TAG_METHOD_CALL

public static final java.lang.String TAG_METHOD_CALL

Tag name to store IExecutionMethodCalls.

See Also:

Constant Field Values

TAG_METHOD_RETURN

public static final java.lang.String TAG_METHOD_RETURN

Tag name to store IExecutionMethodReturns.

See Also:

Constant Field Values

TAG_EXCEPTIONAL_METHOD_RETURN

public static final java.lang.String TAG_EXCEPTIONAL_METHOD_RETURN

Tag name to store IExecutionExceptionalMethodReturns.

See Also:

Constant Field Values

TAG_METHOD_RETURN_VALUE

public static final java.lang.String TAG_METHOD_RETURN_VALUE

Tag name to store IExecutionMethodReturnValues.

See Also:

Constant Field Values

TAG_STATEMENT

public static final java.lang.String TAG_STATEMENT

Tag name to store IExecutionStatements.

See Also:

Constant Field Values

TAG_TERMINATION

public static final java.lang.String TAG_TERMINATION

Tag name to store IExecutionTerminations.

See Also:

Constant Field Values

TAG_JOIN

public static final java.lang.String TAG_JOIN

Tag name to store IExecutionJoins.

See Also:

Constant Field Values

TAG_OPERATION_CONTRACT

public static final java.lang.String TAG_OPERATION_CONTRACT

Tag name to store IExecutionOperationContracts.

See Also:

Constant Field Values

TAG_BLOCK_CONTRACT

public static final java.lang.String TAG_BLOCK_CONTRACT

Tag name to store IExecutionAuxiliaryContracts.

See Also:

Constant Field Values

TAG_LOOP_INVARIANT

public static final java.lang.String TAG_LOOP_INVARIANT

Tag name to store IExecutionLoopInvariants.

See Also:

Constant Field Values

TAG_CONSTRAINT

public static final java.lang.String TAG_CONSTRAINT

Tag name to store IExecutionConstraints.

See Also:

Constant Field Values

TAG_VARIABLE

public static final java.lang.String TAG_VARIABLE

Tag name to store IExecutionVariables.

See Also:

Constant Field Values

TAG_CALL_STATE_VARIABLE

public static final java.lang.String TAG_CALL_STATE_VARIABLE

Tag name to store call state IExecutionVariables.

See Also:

Constant Field Values

TAG_VALUE

public static final java.lang.String TAG_VALUE

Tag name to store IExecutionValues.

See Also:

Constant Field Values

TAG_CALL_STACK_ENTRY

public static final java.lang.String TAG_CALL_STACK_ENTRY

Tag name to store one entry of IExecutionNode.getCallStack().

See Also:

Constant Field Values

TAG_METHOD_RETURN_ENTRY

public static final java.lang.String TAG_METHOD_RETURN_ENTRY

Tag name to store one entry of IExecutionMethodCall.getMethodReturns().

See Also:

Constant Field Values

TAG_COMPLETED_BLOCK_ENTRY

public static final java.lang.String TAG_COMPLETED_BLOCK_ENTRY

Tag name to store on entry of IExecutionNode.getCompletedBlocks() together with its condition IExecutionNode#getFormatedBlockCompletionCondition(IExecutionNode).

See Also:

Constant Field Values

TAG_BLOCK_COMPLETION_ENTRY

public static final java.lang.String TAG_BLOCK_COMPLETION_ENTRY

Tag name to store one entry of IExecutionBlockStartNode.getBlockCompletions().

See Also:

Constant Field Values

TAG_TERMINATION_ENTRY

public static final java.lang.String TAG_TERMINATION_ENTRY

Tag name to store one entry of IExecutionStart.getTerminations().

See Also:

Constant Field Values

TAG_OUTGOING_LINK

public static final java.lang.String TAG_OUTGOING_LINK

Tag name to store one entry of IExecutionNode.getOutgoingLinks().

See Also:

Constant Field Values

PATH_SEPARATOR

public static final char PATH_SEPARATOR

Character to separate path entries in attributes "path".

See Also:

Constant Field Values

Constructor Detail

ExecutionNodeWriter

public ExecutionNodeWriter()

Method Detail

write

public void write(IExecutionNode<?> node,
                  java.lang.String encoding,
                  java.io.File file,
                  boolean saveVariables,
                  boolean saveCallStack,
                  boolean saveReturnValues,
                  boolean saveConstraints)
           throws java.io.IOException,
                  ProofInputException

Writes the given IExecutionNode as XML file.

Parameters:

node - The IExecutionNode to save.

encoding - The encoding to use.

file - The File to save to.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

Throws:

java.io.IOException - Occurred Exception.

ProofInputException - Occurred Exception.

write

public void write(IExecutionNode<?> node,
                  java.lang.String encoding,
                  java.io.OutputStream out,
                  boolean saveVariables,
                  boolean saveCallStack,
                  boolean saveReturnValues,
                  boolean saveConstraints)
           throws java.io.IOException,
                  ProofInputException

Writes the given IExecutionNode into the OutputStream.

Parameters:

node - The IExecutionNode to save.

encoding - The encoding to use.

out - The OutputStream to save to. The OutputStream will be closed by this method.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

Throws:

java.io.IOException - Occurred Exception.

ProofInputException - Occurred Exception.

toXML

public java.lang.String toXML(IExecutionNode<?> node,
                              java.lang.String encoding,
                              boolean saveVariables,
                              boolean saveCallStack,
                              boolean saveReturnValues,
                              boolean saveConstraints)
                       throws ProofInputException

Converts the given IExecutionNode into XML.

Parameters:

node - The IExecutionNode to convert.

encoding - The encoding to use.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

Returns:

The created XML content.

Throws:

ProofInputException - Occurred Exception.

appendExecutionNode

protected void appendExecutionNode(int level,
                                   IExecutionNode<?> node,
                                   boolean saveVariables,
                                   boolean saveCallStack,
                                   boolean saveReturnValues,
                                   boolean saveConstraints,
                                   java.lang.StringBuffer sb)
                            throws ProofInputException

Converts the given IExecutionNode into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

node - The IExecutionNode to convert.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendExecutionBranchCondition

protected void appendExecutionBranchCondition(int level,
                                              IExecutionBranchCondition node,
                                              boolean saveVariables,
                                              boolean saveCallStack,
                                              boolean saveReturnValues,
                                              boolean saveConstraints,
                                              java.lang.StringBuffer sb)
                                       throws ProofInputException

Converts the given IExecutionBranchCondition into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

node - The IExecutionBranchCondition to convert.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendExecutionStart

protected void appendExecutionStart(int level,
                                    IExecutionStart node,
                                    boolean saveVariables,
                                    boolean saveCallStack,
                                    boolean saveReturnValues,
                                    boolean saveConstraints,
                                    java.lang.StringBuffer sb)
                             throws ProofInputException

Converts the given IExecutionStart into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

node - The IExecutionStart to convert.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendTerminations

protected void appendTerminations(int level,
                                  IExecutionStart node,
                                  java.lang.StringBuffer sb)

Appends the termination entries to the given StringBuffer.

Parameters:

level - The level of the children.

node - The IExecutionStart which provides the termination entries.

sb - The StringBuffer to append to.

appendExecutionBranchStatement

protected void appendExecutionBranchStatement(int level,
                                              IExecutionBranchStatement node,
                                              boolean saveVariables,
                                              boolean saveCallStack,
                                              boolean saveReturnValues,
                                              boolean saveConstraints,
                                              java.lang.StringBuffer sb)
                                       throws ProofInputException

Converts the given IExecutionLoopCondition into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

node - The IExecutionLoopCondition to convert.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendExecutionLoopCondition

protected void appendExecutionLoopCondition(int level,
                                            IExecutionLoopCondition node,
                                            boolean saveVariables,
                                            boolean saveCallStack,
                                            boolean saveReturnValues,
                                            boolean saveConstraints,
                                            java.lang.StringBuffer sb)
                                     throws ProofInputException

Converts the given IExecutionLoopCondition into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

node - The IExecutionLoopCondition to convert.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendExecutionLoopStatement

protected void appendExecutionLoopStatement(int level,
                                            IExecutionLoopStatement node,
                                            boolean saveVariables,
                                            boolean saveCallStack,
                                            boolean saveReturnValues,
                                            boolean saveConstraints,
                                            java.lang.StringBuffer sb)
                                     throws ProofInputException

Converts the given IExecutionLoopStatement into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

node - The IExecutionLoopStatement to convert.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendExecutionMethodCall

protected void appendExecutionMethodCall(int level,
                                         IExecutionMethodCall node,
                                         boolean saveVariables,
                                         boolean saveCallStack,
                                         boolean saveReturnValues,
                                         boolean saveConstraints,
                                         java.lang.StringBuffer sb)
                                  throws ProofInputException

Converts the given IExecutionMethodCall into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

node - The IExecutionMethodCall to convert.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendExecutionMethodReturn

protected void appendExecutionMethodReturn(int level,
                                           IExecutionMethodReturn node,
                                           boolean saveVariables,
                                           boolean saveCallStack,
                                           boolean saveReturnValues,
                                           boolean saveConstraints,
                                           java.lang.StringBuffer sb)
                                    throws ProofInputException

Converts the given IExecutionMethodReturn into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

node - The IExecutionMethodReturn to convert.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendExecutionExceptionalMethodReturn

protected void appendExecutionExceptionalMethodReturn(int level,
                                                      IExecutionExceptionalMethodReturn node,
                                                      boolean saveVariables,
                                                      boolean saveCallStack,
                                                      boolean saveReturnValues,
                                                      boolean saveConstraints,
                                                      java.lang.StringBuffer sb)
                                               throws ProofInputException

Converts the given IExecutionExceptionalMethodReturn into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

node - The IExecutionExceptionalMethodReturn to convert.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendExecutionMethodReturnValue

protected void appendExecutionMethodReturnValue(int level,
                                                IExecutionMethodReturnValue returnValue,
                                                java.lang.StringBuffer sb)
                                         throws ProofInputException

Converts the given IExecutionMethodReturnValue into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

returnValue - The IExecutionMethodReturnValue to convert.

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendExecutionStatement

protected void appendExecutionStatement(int level,
                                        IExecutionStatement node,
                                        boolean saveVariables,
                                        boolean saveCallStack,
                                        boolean saveReturnValues,
                                        boolean saveConstraints,
                                        java.lang.StringBuffer sb)
                                 throws ProofInputException

Converts the given IExecutionStatement into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

node - The IExecutionStatement to convert.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendExecutionJoin

protected void appendExecutionJoin(int level,
                                   IExecutionJoin node,
                                   boolean saveVariables,
                                   boolean saveCallStack,
                                   boolean saveReturnValues,
                                   boolean saveConstraints,
                                   java.lang.StringBuffer sb)
                            throws ProofInputException

Converts the given IExecutionJoin into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

node - The IExecutionJoin to convert.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendExecutionOperationContract

protected void appendExecutionOperationContract(int level,
                                                IExecutionOperationContract node,
                                                boolean saveVariables,
                                                boolean saveCallStack,
                                                boolean saveReturnValues,
                                                boolean saveConstraints,
                                                java.lang.StringBuffer sb)
                                         throws ProofInputException

Converts the given IExecutionOperationContract into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

node - The IExecutionOperationContract to convert.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendExecutionLoopInvariant

protected void appendExecutionLoopInvariant(int level,
                                            IExecutionLoopInvariant node,
                                            boolean saveVariables,
                                            boolean saveCallStack,
                                            boolean saveReturnValues,
                                            boolean saveConstraints,
                                            java.lang.StringBuffer sb)
                                     throws ProofInputException

Converts the given IExecutionLoopInvariant into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

node - The IExecutionLoopInvariant to convert.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendExecutionBlockContract

protected void appendExecutionBlockContract(int level,
                                            IExecutionAuxiliaryContract node,
                                            boolean saveVariables,
                                            boolean saveCallStack,
                                            boolean saveReturnValues,
                                            boolean saveConstraints,
                                            java.lang.StringBuffer sb)
                                     throws ProofInputException

Converts the given IExecutionAuxiliaryContract into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

node - The IExecutionLoopInvariant to convert.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendExecutionTermination

protected void appendExecutionTermination(int level,
                                          IExecutionTermination node,
                                          boolean saveVariables,
                                          boolean saveCallStack,
                                          boolean saveReturnValues,
                                          boolean saveConstraints,
                                          java.lang.StringBuffer sb)
                                   throws ProofInputException

Converts the given IExecutionTermination into XML and appends it to the StringBuffer.

Parameters:

level - The current child level.

node - The IExecutionTermination to convert.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendConstraints

protected void appendConstraints(int level,
                                 IExecutionValue value,
                                 boolean saveConstraints,
                                 java.lang.StringBuffer sb)
                          throws ProofInputException

Appends the contained IExecutionConstraints to the given StringBuffer.

Parameters:

level - The level to use.

value - The IExecutionValue which provides the IExecutionConstraints.

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendConstraints

protected void appendConstraints(int level,
                                 IExecutionNode<?> node,
                                 boolean saveConstraints,
                                 java.lang.StringBuffer sb)
                          throws ProofInputException

Appends the contained IExecutionConstraints to the given StringBuffer.

Parameters:

level - The level to use.

node - The IExecutionNode which provides the IExecutionConstraints.

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendConstraint

protected void appendConstraint(int level,
                                IExecutionConstraint constraint,
                                java.lang.StringBuffer sb)
                         throws ProofInputException

Appends the given IExecutionConstraint with its children to the given StringBuffer.

Parameters:

level - The level to use.

constraint - The IExecutionConstraint to append.

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendVariables

protected void appendVariables(int level,
                               IExecutionNode<?> node,
                               boolean saveVariables,
                               boolean saveConstraints,
                               java.lang.StringBuffer sb)
                        throws ProofInputException

Appends the contained IExecutionVariables to the given StringBuffer.

Parameters:

level - The level to use.

node - The IExecutionNode which provides the IExecutionVariables.

saveVariables - Save variables?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendCallStateVariables

protected void appendCallStateVariables(int level,
                                        IExecutionBaseMethodReturn<?> node,
                                        boolean saveVariables,
                                        boolean saveConstraints,
                                        java.lang.StringBuffer sb)
                                 throws ProofInputException

Appends the contained IExecutionVariables to the given StringBuffer.

Parameters:

level - The level to use.

node - The IExecutionNode which provides the IExecutionVariables.

saveVariables - Save variables?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendVariable

protected void appendVariable(int level,
                              IExecutionVariable variable,
                              boolean saveConstraints,
                              java.lang.String tagName,
                              java.lang.StringBuffer sb)
                       throws ProofInputException

Appends the given IExecutionVariable with its children to the given StringBuffer.

Parameters:

level - The level to use.

variable - The IExecutionVariable to append.

saveConstraints - Save constraints?

tagName - The tag name to store an IExecutionVariable.

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendValues

protected void appendValues(int level,
                            IExecutionVariable variable,
                            boolean saveConstraints,
                            java.lang.StringBuffer sb)
                     throws ProofInputException

Appends the contained IExecutionValues to the given StringBuffer.

Parameters:

level - The level to use.

variable - The IExecutionVariable which provides the IExecutionValues.

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendValue

protected void appendValue(int level,
                           IExecutionValue value,
                           boolean saveConstraints,
                           java.lang.StringBuffer sb)
                    throws ProofInputException

Appends the given IExecutionValue with its children to the given StringBuffer.

Parameters:

level - The level to use.

value - The IExecutionValue to append.

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendChildren

protected void appendChildren(int childLevel,
                              IExecutionNode<?> parent,
                              boolean saveVariables,
                              boolean saveCallStack,
                              boolean saveReturnValues,
                              boolean saveConstraints,
                              java.lang.StringBuffer sb)
                       throws ProofInputException

Appends the child nodes to the given StringBuffer.

Parameters:

childLevel - The level of the children.

parent - The parent IExecutionNode which provides the children.

saveVariables - Save variables?

saveCallStack - Save method call stack?

saveReturnValues - Save method return values?

saveConstraints - Save constraints?

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception.

appendOutgoingLinks

protected void appendOutgoingLinks(int level,
                                   IExecutionNode<?> node,
                                   java.lang.StringBuffer sb)

appendOutgoingLink

protected void appendOutgoingLink(int level,
                                  IExecutionLink link,
                                  java.lang.StringBuffer sb)

appendCallStack

protected void appendCallStack(int level,
                               IExecutionNode<?> node,
                               boolean saveCallStack,
                               java.lang.StringBuffer sb)

Appends the call stack entries if required to the given StringBuffer.

Parameters:

level - The level of the children.

node - The IExecutionNode which provides the call stack.

saveCallStack - Defines if the call stack should be saved or not.

sb - The StringBuffer to append to.

appendMethodReturns

protected void appendMethodReturns(int level,
                                   IExecutionMethodCall node,
                                   java.lang.StringBuffer sb)

Appends the method return entries to the given StringBuffer.

Parameters:

level - The level of the children.

node - The IExecutionMethodCall which provides the call stack.

sb - The StringBuffer to append to.

appendCompletedBlocks

protected void appendCompletedBlocks(int level,
                                     IExecutionNode<?> node,
                                     java.lang.StringBuffer sb)
                              throws ProofInputException

Appends the completed block entries to the given StringBuffer.

Parameters:

level - The level of the children.

node - The IExecutionNode which provides the block entries.

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception

appendBlockCompletions

protected void appendBlockCompletions(int level,
                                      IExecutionBlockStartNode<?> node,
                                      java.lang.StringBuffer sb)
                               throws ProofInputException

Appends the block completion entries to the given StringBuffer.

Parameters:

level - The level of the children.

node - The IExecutionBlockStartNode which provides the completed blocks.

sb - The StringBuffer to append to.

Throws:

ProofInputException - Occurred Exception

computePath

protected java.lang.String computePath(IExecutionNode<?> node)

Computes the path from the root of the symbolic execution tree to the given IExecutionNode.

Parameters:

node - The IExecutionNode to compute path to.

Returns:

The computed path.