public class ThinBackwardSlicer extends AbstractBackwardSlicer
AbstractSlicer.SequentInfo
Constructor and Description |
---|
ThinBackwardSlicer() |
Modifier and Type | Method and Description |
---|---|
protected 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. |
doSlicing, updateOutdatedLocations, updateRelevantLocations
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
protected 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.accept
in class AbstractBackwardSlicer
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