Package | Description |
---|---|
de.uka.ilkd.key.symbolic_execution |
Modifier and Type | Method and Description |
---|---|
protected java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair> |
AbstractUpdateExtractor.computeVariableValuePairs(Term layoutCondition,
Term layoutTerm,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
boolean currentLayout,
boolean simplifyConditions)
The method starts a side proof with the given arguments to compute
the values and objects of the requested memory layout.
|
Modifier and Type | Method and Description |
---|---|
protected void |
ExecutionVariableExtractor.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 . |
Modifier and Type | Method and Description |
---|---|
protected void |
ExecutionVariableExtractor.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 |
ExecutionVariableExtractor.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 |
ExecutionVariableExtractor.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 ISymbolicLayout |
SymbolicLayoutExtractor.createLayoutFromExecutionVariableValuePairs(ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
java.lang.String stateName)
Creates an
ISymbolicLayout which shows the objects,
values and associations defined by the given ExecutionVariableValuePair s. |
protected void |
ExecutionVariableExtractor.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 void |
ExecutionVariableExtractor.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 |
ExecutionVariableExtractor.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 IExecutionVariable |
ExecutionVariableExtractor.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. |
Copyright © 2003-2019 The KeY-Project.