Package | Description |
---|---|
de.uka.ilkd.key.gui.smt |
This package contains the graphical user interface of the SMT backend.
|
de.uka.ilkd.key.smt.model |
Modifier and Type | Method and Description |
---|---|
static java.util.List<java.lang.String> |
CETree.computeArrayFields(ObjectVal ov) |
static java.util.List<Pair<java.lang.String,java.lang.String>> |
CETree.computeFields(ObjectVal ov) |
static java.util.List<Pair<java.lang.String,java.lang.String>> |
CETree.computeFunctions(ObjectVal ov) |
static java.util.List<Pair<java.lang.String,java.lang.String>> |
CETree.computeObjectProperties(ObjectVal ov,
java.lang.String sortName) |
static java.lang.String |
CETree.computeSortName(ObjectVal ov) |
Modifier and Type | Method and Description |
---|---|
ObjectVal |
Model.findObject(java.lang.String ref)
finds the object the ref parameter is referring to
|
ObjectVal |
Model.getObject(java.lang.String name,
Heap heap)
returns the object of the given name found in the heap
|
Modifier and Type | Method and Description |
---|---|
java.util.Set<ObjectVal> |
Model.getNecessaryPrestateObjects(java.lang.String location)
returns set of necessary prestate objects
|
java.util.List<ObjectVal> |
Heap.getObjects() |
java.util.Set<ObjectVal> |
Model.getReachableObjects(java.lang.String name,
Heap heap)
returns all objects reachable from the specified one in the fiven heap
|
java.util.Set<ObjectVal> |
Model.pointsTo(java.lang.String name,
Heap heap)
set of objects the specified object points to
|
Modifier and Type | Method and Description |
---|---|
boolean |
Heap.add(ObjectVal object)
Adds an object to the heap.
|
Copyright © 2003-2019 The KeY-Project.