de.uka.ilkd.key.symbolic_execution.slicing

Class ThinBackwardSlicer

java.lang.Object

de.uka.ilkd.key.symbolic_execution.slicing.AbstractSlicer

de.uka.ilkd.key.symbolic_execution.slicing.AbstractBackwardSlicer

de.uka.ilkd.key.symbolic_execution.slicing.ThinBackwardSlicer

public class ThinBackwardSlicer
extends AbstractBackwardSlicer

Implementation of thin backward slicing.

Author:

Martin Hentschel

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.symbolic_execution.slicing.AbstractSlicer

AbstractSlicer.SequentInfo

Constructor Summary

Constructors

Constructor and Description
ThinBackwardSlicer()

Method Summary

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.

Methods inherited from class de.uka.ilkd.key.symbolic_execution.slicing.AbstractBackwardSlicer

doSlicing, updateOutdatedLocations, updateRelevantLocations

Methods inherited from class de.uka.ilkd.key.symbolic_execution.slicing.AbstractSlicer

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

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ThinBackwardSlicer

public ThinBackwardSlicer()

Method Detail

accept

protected boolean accept(Node node,
                         Node previousChild,
                         Services services,
                         java.util.Set<Location> relevantLocations,
                         AbstractSlicer.SequentInfo info,
                         SourceElement activeStatement)
                  throws ProofInputException

Decides if the given Node is part of the slice or not.

Specified by:

accept in class AbstractBackwardSlicer

Parameters:

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.

Returns:

true Node should be part of slice, false Node should not be part of slice.

Throws:

ProofInputException