de.uka.ilkd.key.symbolic_execution

Class ExecutionNodeSymbolicLayoutExtractor

java.lang.Object

de.uka.ilkd.key.symbolic_execution.AbstractUpdateExtractor

de.uka.ilkd.key.symbolic_execution.SymbolicLayoutExtractor

de.uka.ilkd.key.symbolic_execution.ExecutionNodeSymbolicLayoutExtractor

public class ExecutionNodeSymbolicLayoutExtractor
extends SymbolicLayoutExtractor

Special SymbolicLayoutExtractor for IExecutionNodes.

Author:

Martin Hentschel

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.symbolic_execution.AbstractUpdateExtractor

AbstractUpdateExtractor.ExecutionVariableValuePair, AbstractUpdateExtractor.ExtractLocationParameter, AbstractUpdateExtractor.NodeGoal

Field Summary

Fields

Modifier and Type	Field and Description
private IExecutionNode<?>	executionNode The IExecutionNode to extract memory layouts from.

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

modalityPio, node

Constructor Summary

Constructors

Constructor and Description
ExecutionNodeSymbolicLayoutExtractor(IExecutionNode<?> executionNode) Constructor.

Method Summary

Modifier and Type	Method and Description
protected java.lang.String	computeCurrentStateName() Computes the state name of a current memory layout.
protected java.lang.String	computeInitialStateName() Computes the state name of an initial memory layout.

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

analyse, applyCut, applyCutRules, collectObjectsFromSequent, collectSymbolicObjectsFromTerm, createLayoutFromExecutionVariableValuePairs, createObjectForTerm, createSequentForEquivalenceClassComputation, extractAppliedCutsFromGoals, extractAppliedCutsSet, extractInitialUpdates, filterOutObjectsToIgnore, findEquivalentClass, getCurrentLayout, getEquivalenceClasses, getInitialLayout, getLayout, getLayoutsCount, isAnalysed, lazyComputeEquivalenzClasses, lazyComputeLayout, sortTerms, updateLocationsAccordingtoEquivalentClass

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

collectAdditionalUpdates, collectLocationsFromHeapTerms, collectLocationsFromHeapUpdate, collectLocationsFromTerm, collectLocationsFromTerm, collectLocationsFromUpdates, computeBranchCondition, computeInitialObjectsToIgnore, computeOriginalUpdates, computeValueConditions, computeVariableValuePairs, containsImplicitProgramVariable, countOpenChildren, createLocationPredicateAndTerm, extractLocationsFromSequent, extractLocationsFromTerm, fillInitialObjectsToIgnoreRecursively, getProof, getRoot, getServices, hasFreeVariables, isImplicitProgramVariable, isParentReachedOnAllChildGoals, iterateBackOnParents, removeImplicitSubTermsFromPathCondition

Methods inherited from class java.lang.Object

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

Field Detail

executionNode

private final IExecutionNode<?> executionNode

The IExecutionNode to extract memory layouts from.

Constructor Detail

ExecutionNodeSymbolicLayoutExtractor

public ExecutionNodeSymbolicLayoutExtractor(IExecutionNode<?> executionNode)

Constructor.

Parameters:

executionNode - The IExecutionNode to extract memory layouts from.

Method Detail

computeInitialStateName

protected java.lang.String computeInitialStateName()

Computes the state name of an initial memory layout.

Overrides:

computeInitialStateName in class SymbolicLayoutExtractor

Returns:

The state name of an initial memory layout.

computeCurrentStateName

protected java.lang.String computeCurrentStateName()

Computes the state name of a current memory layout.

Overrides:

computeCurrentStateName in class SymbolicLayoutExtractor

Returns:

The state name of a current memory layout.