Modifier and Type | Class and Description |
---|---|
static class |
SymbolicLayoutReader.KeYlessEquivalenceClass
An implementation of
ISymbolicEquivalenceClass which is independent
from KeY and provides such only children and default attributes. |
Modifier and Type | Method and Description |
---|---|
protected ISymbolicEquivalenceClass |
SymbolicLayoutExtractor.findEquivalentClass(ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
Term term)
Searches the
ISymbolicEquivalenceClass from the given one
which contains the given Term . |
Modifier and Type | Method and Description |
---|---|
ImmutableList<ISymbolicEquivalenceClass> |
SymbolicLayoutReader.KeYlessLayout.getEquivalenceClasses()
Returns the equivalence classes.
|
ImmutableList<ISymbolicEquivalenceClass> |
SymbolicLayoutExtractor.getEquivalenceClasses(int layoutIndex)
Returns the equivalence class of the memory layout defined by the index.
|
ImmutableList<ISymbolicEquivalenceClass> |
ExecutionNodeReader.AbstractKeYlessExecutionNode.getLayoutsEquivalenceClasses(int configurationIndex)
Returns the equivalence classes of the memory layout with the given index.
|
protected ImmutableList<ISymbolicEquivalenceClass> |
SymbolicLayoutExtractor.lazyComputeEquivalenceClasses(ImmutableSet<Term> appliedCuts)
Computes the equivalence classes from the given applied cut rules
lazily when
SymbolicLayoutExtractor.getEquivalenceClasses(int) is called the first time. |
Modifier and Type | Method and Description |
---|---|
void |
SymbolicLayoutReader.KeYlessLayout.addEquivalenceClass(ISymbolicEquivalenceClass ec)
Add a new child
ISymbolicEquivalenceClass . |
protected void |
SymbolicLayoutWriter.appendEquivalenceClass(int level,
ISymbolicEquivalenceClass ec,
java.lang.StringBuffer sb)
Appends the given
ISymbolicEquivalenceClass with its children to the given StringBuffer . |
Modifier and Type | Method and Description |
---|---|
protected ISymbolicLayout |
SymbolicLayoutExtractor.createLayoutFromExecutionVariableValuePairs(ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
java.util.Set<AbstractUpdateExtractor.ExecutionVariableValuePair> pairs,
java.lang.String stateName)
Creates an
ISymbolicLayout which shows the objects,
values and associations defined by the given ExecutionVariableValuePair s. |
protected void |
SymbolicLayoutExtractor.createObjectForTerm(java.util.Map<Term,SymbolicObject> objects,
ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
SymbolicLayout result,
Term objectTerm)
Creates for the object defined by the given
Term an SymbolicObject instance if not already available. |
protected ISymbolicEquivalenceClass |
SymbolicLayoutExtractor.findEquivalentClass(ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
Term term)
Searches the
ISymbolicEquivalenceClass from the given one
which contains the given Term . |
protected ISymbolicLayout |
SymbolicLayoutExtractor.lazyComputeLayout(ImmutableSet<Term> layout,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
ImmutableList<ISymbolicEquivalenceClass> equivalentClasses,
java.lang.String stateName,
boolean currentLayout)
Computes a memory layout lazily when it is first time requested via
#getLayout(Map, int, Term, Set, String, boolean) . |
protected java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> |
SymbolicLayoutExtractor.updateLocationsAccordingtoEquivalentClass(java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> locations,
ImmutableList<ISymbolicEquivalenceClass> equivalentClasses)
Replaces the parent of each
ExtractLocationParameter according
to the ISymbolicEquivalenceClass es, because there is no guarantee
that the strategy evaluates each aliased location to the same symbolic value. |
Modifier and Type | Method and Description |
---|---|
ImmutableList<ISymbolicEquivalenceClass> |
IExecutionNode.getLayoutsEquivalenceClasses(int layoutIndex)
Returns the equivalence classes of the memory layout with the given index.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<ISymbolicEquivalenceClass> |
AbstractExecutionNode.getLayoutsEquivalenceClasses(int layoutIndex)
Returns the equivalence classes of the memory layout with the given index.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<ISymbolicEquivalenceClass> |
ISymbolicLayout.getEquivalenceClasses()
Returns the equivalence classes.
|
Modifier and Type | Class and Description |
---|---|
class |
SymbolicEquivalenceClass
Default implementation of
ISymbolicEquivalenceClass . |
Modifier and Type | Method and Description |
---|---|
ImmutableList<ISymbolicEquivalenceClass> |
SymbolicLayout.getEquivalenceClasses()
Returns the equivalence classes.
|
Constructor and Description |
---|
SymbolicLayout(IModelSettings settings,
ImmutableList<ISymbolicEquivalenceClass> equivalenceClasses)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
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 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. |
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.
|
ImmutableArray<Node> |
AbstractSlicer.slice(Node seedNode,
Location seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the slice.
|
ImmutableArray<Node> |
AbstractSlicer.slice(Node seedNode,
ReferencePrefix seedLocation,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the slice.
|
ImmutableArray<Node> |
AbstractSlicer.slice(Node seedNode,
Term term,
ImmutableList<ISymbolicEquivalenceClass> sec)
Computes the slice.
|
Copyright © 2003-2019 The KeY-Project.