Package | Description |
---|---|
de.uka.ilkd.key.symbolic_execution |
Modifier and Type | Method and Description |
---|---|
protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> |
AbstractUpdateExtractor.extractLocationsFromSequent(Sequent sequent,
java.util.Set<Term> objectsToIgnore)
|
protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> |
AbstractUpdateExtractor.extractLocationsFromTerm(Term term,
java.util.Set<Term> objectsToIgnore)
|
protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> |
SymbolicLayoutExtractor.updateLocationsAccordingtoEquivalentClass(java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
ImmutableList<ISymbolicEquivalenceClass> equivalentClasses)
Replaces the parent of each
ExtractLocationParameter according
to the ISymbolicEquivalenceClass es, because there is no guarantee
that the strategy evaluates each aliased location to the same symbolic value. |
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractUpdateExtractor.collectLocationsFromHeapTerms(Term selectTerm,
Term variableTerm,
HeapLDT heapLDT,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> toFill,
java.util.Set<Term> objectsToIgnore)
Collects the
AbstractUpdateExtractor.ExtractLocationParameter location from the heap Term s. |
protected void |
AbstractUpdateExtractor.collectLocationsFromHeapUpdate(Term term,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locationsToFill,
java.util.Set<Term> updateCreatedObjectsToFill,
java.util.Set<Term> updateValueObjectsToFill)
|
protected void |
AbstractUpdateExtractor.collectLocationsFromTerm(java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> toFill,
Term term,
java.util.Set<Term> objectsToIgnore)
Utility method of
AbstractUpdateExtractor.extractLocationsFromTerm(Term, Set) which
recursively extracts the locations. |
protected void |
AbstractUpdateExtractor.collectLocationsFromTerm(Term updateTerm,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locationsToFill,
java.util.Set<Term> updateCreatedObjectsToFill,
java.util.Set<Term> updateValueObjectsToFill,
java.util.Set<Term> objectsToIgnore)
|
protected void |
AbstractUpdateExtractor.collectLocationsFromUpdates(Sequent sequent,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locationsToFill,
java.util.Set<Term> updateCreatedObjectsToFill,
java.util.Set<Term> updateValueObjectsToFill,
java.util.Set<Term> objectsToIgnore)
|
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.
|
protected Term |
AbstractUpdateExtractor.createLocationPredicateAndTerm(java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> valueSelectParameter)
Creates a predicate and a
Term which can be used to compute the
values defined by the given AbstractUpdateExtractor.ExtractLocationParameter s. |
protected ISymbolicLayout |
SymbolicLayoutExtractor.getLayout(java.util.Map<java.lang.Integer,ISymbolicLayout> confiurationsMap,
int layoutIndex,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
java.lang.String stateName,
boolean currentLayout)
Helper method of
SymbolicLayoutExtractor.getInitialLayout(int) and
SymbolicLayoutExtractor.getCurrentLayout(int) to lazily compute and get a memory layout. |
protected ISymbolicLayout |
SymbolicLayoutExtractor.lazyComputeLayout(ImmutableSet<Term> layout,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
java.lang.String stateName,
boolean currentLayout)
Computes a memory layout lazily when it is first time requested via
#getLayout(Map, int, Term, Set, String, boolean) . |
protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> |
SymbolicLayoutExtractor.updateLocationsAccordingtoEquivalentClass(java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
ImmutableList<ISymbolicEquivalenceClass> equivalentClasses)
Replaces the parent of each
ExtractLocationParameter according
to the ISymbolicEquivalenceClass es, because there is no guarantee
that the strategy evaluates each aliased location to the same symbolic value. |
Constructor and Description |
---|
ExtractLocationParameter(AbstractUpdateExtractor.ExtractLocationParameter original,
Term newParent)
Constructor for cloning purpose.
|
Copyright © 2003-2019 The KeY-Project.