public abstract class AbstractBackwardSlicer extends AbstractSlicer
AbstractSlicer.SequentInfo
Constructor and Description |
---|
AbstractBackwardSlicer() |
Modifier and Type | Method and Description |
---|---|
protected abstract boolean |
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. |
ImmutableArray<Node> |
doSlicing(Node seedNode,
Location seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Performs the slicing.
|
protected java.util.Set<Location> |
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 |
updateRelevantLocations(ProgramElement read,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info,
Services services)
Updates the relevant locations.
|
analyzeEquality, analyzeEquivalenceClasses, analyzeHeapUpdate, analyzeSequent, analyzeSequent, analyzeUpdate, analyzeUpdates, computeFirstCommonPrefixLength, computeRepresentativeAlias, createSortedSet, findNewAlternative, listModifiedHeapLocations, listModifiedLocations, normalizeAlias, normalizeAlias, normalizeArrayIndex, performRemoveRelevant, removeRelevant, removeRelevant, slice, slice, slice, startsWith, toLocation, toLocation, toLocationRecursive, toReferencePrefix, toTerm, toTerm, updateAliases
public ImmutableArray<Node> doSlicing(Node seedNode, Location seedLocation, ImmutableList<ISymbolicEquivalenceClass> sec) throws ProofInputException
doSlicing
in class AbstractSlicer
seedNode
- The seed Node
to start slicing at.seedLocation
- The seed Location
.sec
- The optional ISymbolicEquivalenceClass
es to consider.ProofInputException
protected abstract boolean accept(Node node, Node previousChild, Services services, java.util.Set<Location> relevantLocations, AbstractSlicer.SequentInfo info, SourceElement activeStatement) throws ProofInputException
Node
is part of the slice or not.node
- The Node
to check.previousChild
- The previously visited child Node
or null
the first time.services
- The Services
to use.relevantLocations
- The relevant locations.info
- The SequentInfo
with the aliases and so on.activeStatement
- The currently active statement.true
Node
should be part of slice, false
Node
should not be part of slice.ProofInputException
protected void updateRelevantLocations(ProgramElement read, java.util.Set<Location> relevantLocations, AbstractSlicer.SequentInfo info, Services services)
read
- The Expression
which provides new relevant locations.relevantLocations
- The relevant locations to update.info
- The SequentInfo
with the aliases and so on.services
- The Services
to use.protected java.util.Set<Location> 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)
services
- The Services
to use.oldLocationsToUpdate
- The locations to update.newAliases
- The new aliases.oldAliases
- The old aliases.outdatedPrefix
- The prefix of outdated locations.thisReference
- The ReferencePrefix
which is represented by this
(ThisReference
).