Package | Description |
---|---|
de.uka.ilkd.key.symbolic_execution.slicing |
Modifier and Type | Method and Description |
---|---|
Location |
Location.append(Access sub)
Creates a new
Location in which the sub is appended. |
Location |
Location.append(Location sub)
Creates a new
Location in which the sub is appended. |
protected Location |
AbstractSlicer.computeRepresentativeAlias(Location location,
java.util.Map<Location,java.util.SortedSet<Location>> aliases)
Computes the representative alias of the given
Location . |
protected Location |
AbstractSlicer.findNewAlternative(java.util.SortedSet<Location> oldAlternatives,
java.util.SortedSet<Location> newAlternatives)
Returns the first found alternative which is still valid.
|
protected Location |
AbstractSlicer.normalizeAlias(Services services,
Location location,
AbstractSlicer.SequentInfo info)
Returns the representative alias for the given
Location . |
protected Location |
AbstractSlicer.normalizeAlias(Services services,
ReferencePrefix referencePrefix,
AbstractSlicer.SequentInfo info)
Returns the representative alias for the given
ReferencePrefix . |
protected Location |
AbstractSlicer.toLocation(Services services,
ReferencePrefix prefix,
ExecutionContext ec,
ReferencePrefix thisReference)
Converts the given
ReferencePrefix into a Location . |
static Location |
AbstractSlicer.toLocation(Services services,
Term term)
|
Modifier and Type | Method and Description |
---|---|
protected java.util.SortedSet<Location> |
AbstractSlicer.createSortedSet()
Creates a
SortedSet which ensures that the elements are sorted. |
java.util.Map<Location,java.util.SortedSet<Location>> |
AbstractSlicer.SequentInfo.getAliases()
Returns the found aliases.
|
java.util.Map<Location,java.util.SortedSet<Location>> |
AbstractSlicer.SequentInfo.getAliases()
Returns the found aliases.
|
protected java.util.Set<Location> |
AbstractBackwardSlicer.updateOutdatedLocations(Services services,
java.util.Set<Location> oldLocationsToUpdate,
java.util.Map<Location,java.util.SortedSet<Location>> newAliases,
java.util.Map<Location,java.util.SortedSet<Location>> oldAliases,
Location outdatedPrefix,
ReferencePrefix thisReference)
Updates the outdated locations.
|
Modifier and Type | Method and Description |
---|---|
Location |
Location.append(Location sub)
Creates a new
Location in which the sub is appended. |
protected Location |
AbstractSlicer.computeRepresentativeAlias(Location location,
java.util.Map<Location,java.util.SortedSet<Location>> aliases)
Computes the representative alias of the given
Location . |
protected abstract ImmutableArray<Node> |
AbstractSlicer.doSlicing(Node seedNode,
Location seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Performs the slicing.
|
ImmutableArray<Node> |
AbstractBackwardSlicer.doSlicing(Node seedNode,
Location seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Performs the slicing.
|
protected Location |
AbstractSlicer.normalizeAlias(Services services,
Location location,
AbstractSlicer.SequentInfo info)
Returns the representative alias for the given
Location . |
protected boolean |
AbstractSlicer.performRemoveRelevant(Services services,
Location normalized,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info)
Checks if the given
Location is directly or indirectly
contained (aliased) in the Set of relevant locations. |
protected boolean |
AbstractSlicer.removeRelevant(Services services,
Location location,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info)
Checks if the given
Location is directly or indirectly
contained (aliased) in the Set of relevant locations. |
ImmutableArray<Node> |
AbstractSlicer.slice(Node seedNode,
Location seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the slice.
|
protected void |
AbstractSlicer.updateAliases(Services services,
Location first,
Location second,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Adds the found alias consisting of first and second
ReferencePrefix to the alias Map . |
protected java.util.Set<Location> |
AbstractBackwardSlicer.updateOutdatedLocations(Services services,
java.util.Set<Location> oldLocationsToUpdate,
java.util.Map<Location,java.util.SortedSet<Location>> newAliases,
java.util.Map<Location,java.util.SortedSet<Location>> oldAliases,
Location outdatedPrefix,
ReferencePrefix thisReference)
Updates the outdated locations.
|
Modifier and Type | Method and Description |
---|---|
protected boolean |
ThinBackwardSlicer.accept(Node node,
Node previousChild,
Services services,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info,
SourceElement activeStatement)
Decides if the given
Node is part of the slice or not. |
protected abstract boolean |
AbstractBackwardSlicer.accept(Node node,
Node previousChild,
Services services,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info,
SourceElement activeStatement)
Decides if the given
Node is part of the slice or not. |
protected void |
AbstractSlicer.analyzeEquality(Services services,
Term equality,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Analyzes the given equality
Term for aliased locations. |
protected void |
AbstractSlicer.analyzeEquality(Services services,
Term equality,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Analyzes the given equality
Term for aliased locations. |
protected void |
AbstractSlicer.analyzeEquivalenceClasses(Services services,
ImmutableList<ISymbolicEquivalenceClass> sec,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Analyzes the gievn
ISymbolicEquivalenceClass es. |
protected void |
AbstractSlicer.analyzeEquivalenceClasses(Services services,
ImmutableList<ISymbolicEquivalenceClass> sec,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Analyzes the gievn
ISymbolicEquivalenceClass es. |
protected void |
AbstractSlicer.analyzeHeapUpdate(Term term,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Recursive utility method used by
#analyzeUpdate(Term, Services, HeapLDT, Map) to analyze a given update. |
protected void |
AbstractSlicer.analyzeHeapUpdate(Term term,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Recursive utility method used by
#analyzeUpdate(Term, Services, HeapLDT, Map) to analyze a given update. |
protected void |
AbstractSlicer.analyzeSequent(Services services,
Sequent sequent,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Analyzes the given
Sequent for equalities specified by top level formulas. |
protected void |
AbstractSlicer.analyzeSequent(Services services,
Sequent sequent,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Analyzes the given
Sequent for equalities specified by top level formulas. |
protected void |
AbstractSlicer.analyzeUpdate(Term term,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext ec,
ReferencePrefix thisReference)
Recursive utility method used by
#analyzeUpdates(ImmutableList, Services, HeapLDT, Map) to analyze a given update. |
protected void |
AbstractSlicer.analyzeUpdate(Term term,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext ec,
ReferencePrefix thisReference)
Recursive utility method used by
#analyzeUpdates(ImmutableList, Services, HeapLDT, Map) to analyze a given update. |
protected void |
AbstractSlicer.analyzeUpdates(ImmutableList<Term> updates,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext ec,
ReferencePrefix thisReference)
Utility method used by
#analyzeSequent(Node) to analyze the given updates. |
protected void |
AbstractSlicer.analyzeUpdates(ImmutableList<Term> updates,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext ec,
ReferencePrefix thisReference)
Utility method used by
#analyzeSequent(Node) to analyze the given updates. |
protected Location |
AbstractSlicer.computeRepresentativeAlias(Location location,
java.util.Map<Location,java.util.SortedSet<Location>> aliases)
Computes the representative alias of the given
Location . |
protected Location |
AbstractSlicer.computeRepresentativeAlias(Location location,
java.util.Map<Location,java.util.SortedSet<Location>> aliases)
Computes the representative alias of the given
Location . |
protected Location |
AbstractSlicer.findNewAlternative(java.util.SortedSet<Location> oldAlternatives,
java.util.SortedSet<Location> newAlternatives)
Returns the first found alternative which is still valid.
|
protected Location |
AbstractSlicer.findNewAlternative(java.util.SortedSet<Location> oldAlternatives,
java.util.SortedSet<Location> newAlternatives)
Returns the first found alternative which is still valid.
|
protected void |
AbstractSlicer.listModifiedHeapLocations(Term term,
Services services,
HeapLDT heapLDT,
java.util.List<Location> listToFill,
ReferencePrefix thisReference,
java.util.Set<Location> relevantLocations,
Node node)
Recursive utility method used by
#listModifiedLocations(Term, Services, HeapLDT, List, ReferencePrefix) to analyze a given update. |
protected void |
AbstractSlicer.listModifiedHeapLocations(Term term,
Services services,
HeapLDT heapLDT,
java.util.List<Location> listToFill,
ReferencePrefix thisReference,
java.util.Set<Location> relevantLocations,
Node node)
Recursive utility method used by
#listModifiedLocations(Term, Services, HeapLDT, List, ReferencePrefix) to analyze a given update. |
protected void |
AbstractSlicer.listModifiedLocations(Term term,
Services services,
HeapLDT heapLDT,
java.util.List<Location> listToFill,
ExecutionContext ec,
ReferencePrefix thisReference,
java.util.Set<Location> relevantLocations,
Node node)
|
protected void |
AbstractSlicer.listModifiedLocations(Term term,
Services services,
HeapLDT heapLDT,
java.util.List<Location> listToFill,
ExecutionContext ec,
ReferencePrefix thisReference,
java.util.Set<Location> relevantLocations,
Node node)
|
protected boolean |
AbstractSlicer.performRemoveRelevant(Services services,
Location normalized,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info)
Checks if the given
Location is directly or indirectly
contained (aliased) in the Set of relevant locations. |
protected boolean |
AbstractSlicer.removeRelevant(Services services,
Location location,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info)
Checks if the given
Location is directly or indirectly
contained (aliased) in the Set of relevant locations. |
protected boolean |
AbstractSlicer.removeRelevant(Services services,
ReferencePrefix sourceElement,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info)
Checks if the given
SourceElement is directly or indirectly
contained (aliased) in the Set of relevant locations. |
protected void |
AbstractSlicer.updateAliases(Services services,
Location first,
Location second,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Adds the found alias consisting of first and second
ReferencePrefix to the alias Map . |
protected void |
AbstractSlicer.updateAliases(Services services,
Location first,
Location second,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Adds the found alias consisting of first and second
ReferencePrefix to the alias Map . |
protected java.util.Set<Location> |
AbstractBackwardSlicer.updateOutdatedLocations(Services services,
java.util.Set<Location> oldLocationsToUpdate,
java.util.Map<Location,java.util.SortedSet<Location>> newAliases,
java.util.Map<Location,java.util.SortedSet<Location>> oldAliases,
Location outdatedPrefix,
ReferencePrefix thisReference)
Updates the outdated locations.
|
protected java.util.Set<Location> |
AbstractBackwardSlicer.updateOutdatedLocations(Services services,
java.util.Set<Location> oldLocationsToUpdate,
java.util.Map<Location,java.util.SortedSet<Location>> newAliases,
java.util.Map<Location,java.util.SortedSet<Location>> oldAliases,
Location outdatedPrefix,
ReferencePrefix thisReference)
Updates the outdated locations.
|
protected java.util.Set<Location> |
AbstractBackwardSlicer.updateOutdatedLocations(Services services,
java.util.Set<Location> oldLocationsToUpdate,
java.util.Map<Location,java.util.SortedSet<Location>> newAliases,
java.util.Map<Location,java.util.SortedSet<Location>> oldAliases,
Location outdatedPrefix,
ReferencePrefix thisReference)
Updates the outdated locations.
|
protected java.util.Set<Location> |
AbstractBackwardSlicer.updateOutdatedLocations(Services services,
java.util.Set<Location> oldLocationsToUpdate,
java.util.Map<Location,java.util.SortedSet<Location>> newAliases,
java.util.Map<Location,java.util.SortedSet<Location>> oldAliases,
Location outdatedPrefix,
ReferencePrefix thisReference)
Updates the outdated locations.
|
protected java.util.Set<Location> |
AbstractBackwardSlicer.updateOutdatedLocations(Services services,
java.util.Set<Location> oldLocationsToUpdate,
java.util.Map<Location,java.util.SortedSet<Location>> newAliases,
java.util.Map<Location,java.util.SortedSet<Location>> oldAliases,
Location outdatedPrefix,
ReferencePrefix thisReference)
Updates the outdated locations.
|
protected void |
AbstractBackwardSlicer.updateRelevantLocations(ProgramElement read,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info,
Services services)
Updates the relevant locations.
|
Constructor and Description |
---|
SequentInfo(java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext executionContext,
ReferencePrefix thisReference)
Constructor.
|
SequentInfo(java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext executionContext,
ReferencePrefix thisReference)
Constructor.
|
Copyright © 2003-2019 The KeY-Project.