Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.strategy.termfeature | |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.slicing | |
de.uka.ilkd.key.symbolic_execution.strategy | |
de.uka.ilkd.key.symbolic_execution.util |
Modifier and Type | Method and Description |
---|---|
HeapLDT |
TypeConverter.getHeapLDT() |
Modifier and Type | Method and Description |
---|---|
protected HeapLDT |
LogicPrinter.getHeapLDT() |
Modifier and Type | Field and Description |
---|---|
protected HeapLDT |
AbstractPO.heapLDT |
Modifier and Type | Method and Description |
---|---|
static PrimitiveHeapTermFeature |
PrimitiveHeapTermFeature.create(HeapLDT heapLDT) |
static TermFeature |
SimplifiedSelectTermFeature.create(HeapLDT heapLDT) |
static IsHeapFunctionTermFeature |
IsHeapFunctionTermFeature.create(HeapLDT heapLDT) |
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractUpdateExtractor.collectLocationsFromHeapTerms(Term selectTerm,
Term variableTerm,
HeapLDT heapLDT,
java.util.Set<AbstractUpdateExtractor.ExtractLocationParameter> toFill,
java.util.Set<Term> objectsToIgnore)
Collects the
AbstractUpdateExtractor.ExtractLocationParameter location from the heap Term s. |
Modifier and Type | Method and Description |
---|---|
protected void |
AbstractSlicer.analyzeHeapUpdate(Term term,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
ReferencePrefix thisReference)
Recursive utility method used by
#analyzeUpdate(Term, Services, HeapLDT, Map) to analyze a given update. |
protected void |
AbstractSlicer.analyzeUpdate(Term term,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext ec,
ReferencePrefix thisReference)
Recursive utility method used by
#analyzeUpdates(ImmutableList, Services, HeapLDT, Map) to analyze a given update. |
protected void |
AbstractSlicer.analyzeUpdates(ImmutableList<Term> updates,
Services services,
HeapLDT heapLDT,
java.util.Map<Location,java.util.SortedSet<Location>> aliases,
java.util.Map<ProgramVariable,Term> localValues,
ExecutionContext ec,
ReferencePrefix thisReference)
Utility method used by
#analyzeSequent(Node) to analyze the given updates. |
protected void |
AbstractSlicer.listModifiedHeapLocations(Term term,
Services services,
HeapLDT heapLDT,
java.util.List<Location> listToFill,
ReferencePrefix thisReference,
java.util.Set<Location> relevantLocations,
Node node)
Recursive utility method used by
#listModifiedLocations(Term, Services, HeapLDT, List, ReferencePrefix) to analyze a given update. |
protected void |
AbstractSlicer.listModifiedLocations(Term term,
Services services,
HeapLDT heapLDT,
java.util.List<Location> listToFill,
ExecutionContext ec,
ReferencePrefix thisReference,
java.util.Set<Location> relevantLocations,
Node node)
|
Modifier and Type | Method and Description |
---|---|
protected void |
CutHeapObjectsTermGenerator.collectEqualityTerms(SequentFormula sf,
java.util.Set<Term> equalityTerms,
java.util.Set<Term> topTerms,
HeapLDT heapLDT,
Services services)
Computes all possible equality terms between objects in the given
SequentFormula . |
protected void |
CutHeapObjectsTermGenerator.collectStoreLocations(Term term,
java.util.Set<Term> storeLocations,
HeapLDT heapLDT)
Collects recursive all possible targets of store operations on a heap.
|
Modifier and Type | Method and Description |
---|---|
static Term |
SymbolicExecutionUtil.getArrayIndex(Services services,
HeapLDT heapLDT,
Term arrayIndexTerm)
Returns the array index defined by the given
Term . |
static ProgramVariable |
SymbolicExecutionUtil.getProgramVariable(Services services,
HeapLDT heapLDT,
Term locationTerm)
Returns the
ProgramVariable defined by the given Term . |
static boolean |
SymbolicExecutionUtil.isBaseHeap(Operator op,
HeapLDT heapLDT)
Checks if the given
Operator is the base heap. |
static boolean |
SymbolicExecutionUtil.isHeap(Operator op,
HeapLDT heapLDT)
Checks if the given
Operator is a heap. |
Copyright © 2003-2019 The KeY-Project.