| java.lang.Object de.uka.ilkd.key.unittest.ModelGenerator
ModelGenerator | public class ModelGenerator (Code) | | |
COGENT | final public static int COGENT(Code) | | |
SIMPLIFY | final public static int SIMPLIFY(Code) | | |
cached | public static int cached(Code) | | |
decProdForTestGen | public static int decProdForTestGen(Code) | | |
checkIndices | public static boolean checkIndices(Term t, Services serv)(Code) | | Returns true iff no negative array indices are contained in t.
|
collectProgramVariables | public void collectProgramVariables()(Code) | | Collects the program variables occuring in node.
|
containsImplicitAttr | public static boolean containsImplicitAttr(Term t)(Code) | | |
createModels | public Model[] createModels()(Code) | | Trys to create a model and returns the equivalence classes contained in
the partial model.
|
getExecutionTrace | public String getExecutionTrace()(Code) | | Returns the associated ExecutionTrace as a String.
|
getLocations | public SetOfTerm getLocations()(Code) | | Returns the set of locations occuring in node.
|
getNonPrimitiveLocationEqvClasses | public EquivalenceClass[] getNonPrimitiveLocationEqvClasses()(Code) | | Returns the EquivalenceClasses that contain locations of nonprimitive
types.
|
getOriginalNode | public Node getOriginalNode()(Code) | | |
getPrimitiveLocationEqvClasses | public EquivalenceClass[] getPrimitiveLocationEqvClasses()(Code) | | Returns the EquivalenceClasses that contain locations of type int or
boolean
|
getProgramVariables | public SetOfProgramVariable getProgramVariables()(Code) | | |
|
|