public class ExecutionNodeSymbolicLayoutExtractor extends SymbolicLayoutExtractor
SymbolicLayoutExtractor
for IExecutionNode
s.AbstractUpdateExtractor.ExecutionVariableValuePair, AbstractUpdateExtractor.ExtractLocationParameter, AbstractUpdateExtractor.NodeGoal
Modifier and Type | Field and Description |
---|---|
private IExecutionNode<?> |
executionNode
The
IExecutionNode to extract memory layouts from. |
modalityPio, node
Constructor and Description |
---|
ExecutionNodeSymbolicLayoutExtractor(IExecutionNode<?> executionNode)
Constructor.
|
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.
|
analyse, applyCut, applyCutRules, collectObjectsFromSequent, collectSymbolicObjectsFromTerm, createLayoutFromExecutionVariableValuePairs, createObjectForTerm, createSequentForEquivalenceClassComputation, extractAppliedCutsFromGoals, extractAppliedCutsSet, extractInitialUpdates, filterOutObjectsToIgnore, findEquivalentClass, getCurrentLayout, getEquivalenceClasses, getInitialLayout, getLayout, getLayoutsCount, isAnalysed, lazyComputeEquivalenzClasses, lazyComputeLayout, sortTerms, updateLocationsAccordingtoEquivalentClass
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
private final IExecutionNode<?> executionNode
IExecutionNode
to extract memory layouts from.public ExecutionNodeSymbolicLayoutExtractor(IExecutionNode<?> executionNode)
executionNode
- The IExecutionNode
to extract memory layouts from.protected java.lang.String computeInitialStateName()
computeInitialStateName
in class SymbolicLayoutExtractor
protected java.lang.String computeCurrentStateName()
computeCurrentStateName
in class SymbolicLayoutExtractor