Package | Description |
---|---|
de.uka.ilkd.key.symbolic_execution.slicing |
Modifier and Type | Method and Description |
---|---|
protected AbstractSlicer.SequentInfo |
AbstractSlicer.analyzeSequent(Node node,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the aliases specified by the updates of the current
Node
at the application PosInOccurrence and computes the current this reference. |
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 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 Access |
AbstractSlicer.normalizeArrayIndex(Access access,
AbstractSlicer.SequentInfo info)
Normalizes the given array index.
|
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 |
AbstractBackwardSlicer.updateRelevantLocations(ProgramElement read,
java.util.Set<Location> relevantLocations,
AbstractSlicer.SequentInfo info,
Services services)
Updates the relevant locations.
|
Copyright © 2003-2019 The KeY-Project.