public class ExecutionVariableExtractor extends AbstractUpdateExtractor
IExecutionVariable
s.Modifier and Type | Class and Description |
---|---|
static class |
ExecutionVariableExtractor.ExtractedExecutionValue
The
IExecutionValue instantiated by the ExecutionVariableExtractor . |
static class |
ExecutionVariableExtractor.ExtractedExecutionVariable
The
IExecutionVariable instantiated by the ExecutionVariableExtractor . |
AbstractUpdateExtractor.ExecutionVariableValuePair, AbstractUpdateExtractor.ExtractLocationParameter, AbstractUpdateExtractor.NodeGoal
modalityPio, node
Constructor and Description |
---|
ExecutionVariableExtractor(Node node,
PosInOccurrence modalityPio,
IExecutionNode<?> executionNode,
Term condition,
boolean simplifyConditions)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
IExecutionVariable[] |
analyse()
Extracts the current state and represents it as
IExecutionVariable s. |
protected void |
analyzeTreeStructure(java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>> topVariables,
java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.ParentDefinition,java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap)
Analyzes the tree structure of the given
ExecutionVariableValuePair s. |
protected void |
createValues(IExecutionVariable variable,
java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
AbstractUpdateExtractor.ExecutionVariableValuePair firstPair,
java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.ParentDefinition,java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap,
java.util.List<IExecutionValue> valueListToFill,
ImmutableList<Term> alreadyVisitedObjects)
Creates the
IExecutionValue s of the given IExecutionVariable . |
protected IExecutionVariable |
createVariablesValueStructure(java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.ParentDefinition,java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap,
ExecutionVariableExtractor.ExtractedExecutionValue parentValue,
ImmutableList<Term> alreadyVisitedObjects)
Creates an
IExecutionVariable for the given ExecutionVariableValuePair s. |
protected Pair<java.lang.Boolean,ImmutableList<Term>> |
updateAlreadyVisitedObjects(ImmutableList<Term> alreadyVisitedObjects,
Term value)
Updates the already visited objects list if required.
|
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
public ExecutionVariableExtractor(Node node, PosInOccurrence modalityPio, IExecutionNode<?> executionNode, Term condition, boolean simplifyConditions) throws ProofInputException
node
- The Node
which provides the state.modalityPio
- The PosInOccurrence
in the Node
.executionNode
- The current IExecutionNode
.condition
- An optional additional condition.simplifyConditions
- true
simplify conditions, false
do not simplify conditions.ProofInputException
- Occurred Exceptionpublic IExecutionVariable[] analyse() throws ProofInputException
IExecutionVariable
s.IExecutionVariable
s representing the current state.ProofInputException
- Occurred Exception.protected void analyzeTreeStructure(java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs, java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>> topVariables, java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.ParentDefinition,java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap)
ExecutionVariableValuePair
s.pairs
- The ExecutionVariableValuePair
s to analyze.topVariables
- The state locations,contentMap
- The child locations.protected IExecutionVariable createVariablesValueStructure(java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs, java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.ParentDefinition,java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap, ExecutionVariableExtractor.ExtractedExecutionValue parentValue, ImmutableList<Term> alreadyVisitedObjects) throws ProofInputException
IExecutionVariable
for the given ExecutionVariableValuePair
s.pairs
- The ExecutionVariableValuePair
s to represent.contentMap
- The Map
providing child content information.parentValue
- The optional parent IExecutionValue
.alreadyVisitedObjects
- The value Term
s of already visited objects on the current path in the variable-value-hierarchy.IExecutionVariable
.ProofInputException
- Occurred Exception.protected void createValues(IExecutionVariable variable, java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs, AbstractUpdateExtractor.ExecutionVariableValuePair firstPair, java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.ParentDefinition,java.util.Map<de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor.LocationDefinition,java.util.List<AbstractUpdateExtractor.ExecutionVariableValuePair>>> contentMap, java.util.List<IExecutionValue> valueListToFill, ImmutableList<Term> alreadyVisitedObjects) throws ProofInputException
IExecutionValue
s of the given IExecutionVariable
.variable
- The IExecutionVariable
.pairs
- The ExecutionVariableValuePair
s which provides the content.firstPair
- The first entry in the ExecutionVariableValuePair
s.contentMap
- The content Map
.valueListToFill
- The result List
to fill.alreadyVisitedObjects
- The value Term
s of already visited objects on the current path in the variable-value-hierarchy.ProofInputException
- Occurred Exception.protected Pair<java.lang.Boolean,ImmutableList<Term>> updateAlreadyVisitedObjects(ImmutableList<Term> alreadyVisitedObjects, Term value)
alreadyVisitedObjects
- The value Term
s of already visited objects on the current path in the variable-value-hierarchy.value
- The current value.Copyright © 2003-2019 The KeY-Project.