It run for BinarySearch

Author: wadoon

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/Format.java

@@ -1,5 +1,8 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.testgen;
 
 public enum Format {
     Plain, JUnit4, JUnit5, TestNG,
-}
+}

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java

@@ -21,12 +21,12 @@
 import de.uka.ilkd.key.settings.ProofDependentSMTSettings;
 import de.uka.ilkd.key.settings.ProofIndependentSMTSettings;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
-import de.uka.ilkd.key.testgen.settings.TestGenerationSettings;
 import de.uka.ilkd.key.smt.*;
 import de.uka.ilkd.key.smt.lang.SMTSort;
 import de.uka.ilkd.key.smt.model.Model;
 import de.uka.ilkd.key.smt.solvertypes.SolverType;
 import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
+import de.uka.ilkd.key.testgen.settings.TestGenerationSettings;
 
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/OutputEnvironment.java

@@ -0,0 +1,42 @@
+package de.uka.ilkd.key.testgen;
+
+import java.io.IOException;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.StandardCopyOption;
+import java.util.Objects;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (02.02.24)
+ */
+public record OutputEnvironment(Path targetFolder) {
+    public Path getSourceDir() {
+        return targetFolder.resolve("src");
+    }
+
+    public Path getTestSourceDir() {
+        return targetFolder.resolve("test");
+    }
+
+    public Path getAntFile() {
+        return targetFolder.resolve("build.xml");
+    }
+
+    public Path getReadmeFile() {
+        return targetFolder.resolve("README.md");
+    }
+
+    public void init() throws IOException {
+        Files.createDirectories(getSourceDir());
+        Files.createDirectories(getTestSourceDir());
+
+        installAntFile();
+    }
+
+    private void installAntFile() throws IOException {
+        try (var buildXml = getClass().getResourceAsStream("/de/uka/ilkd/key/tcg/build.xml")) {
+            Files.copy(Objects.requireNonNull(buildXml), getAntFile(), StandardCopyOption.REPLACE_EXISTING);
+        }
+    }
+}

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java

@@ -3,10 +3,10 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.testgen;
 
-import java.util.Set;
-
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
+import de.uka.ilkd.key.java.declaration.ParameterDeclaration;
+import de.uka.ilkd.key.java.declaration.VariableSpecification;
 import de.uka.ilkd.key.logic.JavaBlock;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.TermLabelManager;
@@ -20,17 +20,22 @@
 import de.uka.ilkd.key.speclang.Contract;
 import de.uka.ilkd.key.speclang.Contract.OriginalVariables;
 import de.uka.ilkd.key.speclang.FunctionalOperationContract;
-
+import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
+import java.util.Objects;
+import java.util.Set;
+
 public record ProofInfo(Proof proof, Services services) {
     private static final Logger LOGGER = LoggerFactory.getLogger(ProofInfo.class);
 
     public ProofInfo(Proof proof) {
         this(proof, proof.getServices());
     }
 
+
+    @Nullable
     public IProgramMethod getMUT() {
         SpecificationRepository spec = services.getSpecificationRepository();
         IObserverFunction f = spec.getTargetOfProof(proof);
@@ -41,20 +46,56 @@ public IProgramMethod getMUT() {
         }
     }
 
+    @Nullable
+    public String getMUTCall() {
+        var m = getMUT();
+        if (m == null) return null;
+
+        var name = m.getFullName();
+        if (name == null) return null;
+
+        StringBuilder params = new StringBuilder();
+        for (ParameterDeclaration p : m.getParameters()) {
+            for (VariableSpecification v : p.getVariables()) {
+                IProgramVariable var = v.getProgramVariable();
+                params.append(",").append(var.name());
+            }
+        }
+        if (!params.isEmpty()) {
+            params = new StringBuilder(params.substring(1));
+        }
+
+        String caller;
+        if (m.isStatic()) {
+            caller = getTypeOfClassUnderTest().getName();
+        } else {
+            caller = "self";
+        }
+
+        if (m.getReturnType().equals(KeYJavaType.VOID_TYPE)) {
+            return caller + "." + name + "(" + params + ");";
+        } else {
+            String returnType = m.getReturnType().getFullName();
+            return returnType + " result = " + caller + "." + name + "(" + params + ");";
+        }
+    }
+
+    @Nullable
     public KeYJavaType getTypeOfClassUnderTest() {
         if (getMUT() == null) {
             return null;
         }
         return getMUT().getContainerType();
     }
 
+    @Nullable
     public KeYJavaType getReturnType() {
         return getMUT().getType();
     }
 
     public Contract getContract() {
         ContractPO po = services.getSpecificationRepository().getPOForProof(proof);
-        return po.getContract();
+        return Objects.requireNonNull(po).getContract();
     }
 
     public Term getPostCondition() {

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java

@@ -3,12 +3,13 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.testgen;
 
-import com.squareup.javapoet.*;
-import de.uka.ilkd.key.logic.sort.Sort;
-
-import javax.lang.model.element.Modifier;
 import java.util.HashMap;
 import java.util.HashSet;
+import javax.lang.model.element.Modifier;
+
+import de.uka.ilkd.key.logic.sort.Sort;
+
+import com.squareup.javapoet.*;
 
 /**
  * Creates the RFL.java file, that provides setter and getter methods using the reflection API as
@@ -28,10 +29,10 @@ public class ReflectionClassCreator {
 
     // setter and getter methods will be created for these types.
     private static final String[] PRIMITIVE_TYPES =
-            {"int", "long", "byte", "char", "boolean", "float", "double"};
+        { "int", "long", "byte", "char", "boolean", "float", "double" };
 
     // Default values for primitive types
-    private static final String[] PRIM_TYP_DEF_VAL = {"0", "0", "0", "' '", "false", "0", "0"};
+    private static final String[] PRIM_TYP_DEF_VAL = { "0", "0", "0", "' '", "false", "0", "0" };
 
     private final HashSet<Sort> usedObjectSorts;
     private final HashSet<String> usedObjectSortsStrings;
@@ -110,21 +111,23 @@ private HashSet<String> sortsToString() {
     private TypeSpec.Builder classDecl(boolean staticClass) {
         var tb = TypeSpec.classBuilder(NAME_OF_CLASS);
         tb.addModifiers(Modifier.PUBLIC);
-        if (staticClass) tb.addModifiers(Modifier.STATIC);
-        tb.addJavadoc("""
-                // This file was generated by KeY Version %s (www.key-project.org).
-                /** This class enables the test suite to read and write protected and private
-                * fields of other classes. It can also simulate ghost fields using a hashmap.
-                * Ghostfields are implicit fields that exist in the specification but not in the
-                * actual Java class. Futhermore, this class also enables to create an object of
-                * any class even if it has no default constructor. To create objects the
-                * the objenesis library is required and must be provided when compiling and
-                * executing the test suite. * @see http://docs.oracle.com/javase/tutorial/reflect/member/ctorInstance.html
-                * @see http://code.google.com/p/objenesis
-                * @see http://objenesis.org/
-                * @author gladisch").append(NEW_LINE);
-                * @author mbender").append(NEW_LINE);
-                */""");
+        if (staticClass)
+            tb.addModifiers(Modifier.STATIC);
+        tb.addJavadoc(
+            """
+                    // This file was generated by KeY Version %s (www.key-project.org).
+                    /** This class enables the test suite to read and write protected and private
+                    * fields of other classes. It can also simulate ghost fields using a hashmap.
+                    * Ghostfields are implicit fields that exist in the specification but not in the
+                    * actual Java class. Futhermore, this class also enables to create an object of
+                    * any class even if it has no default constructor. To create objects the
+                    * the objenesis library is required and must be provided when compiling and
+                    * executing the test suite. * @see http://docs.oracle.com/javase/tutorial/reflect/member/ctorInstance.html
+                    * @see http://code.google.com/p/objenesis
+                    * @see http://objenesis.org/
+                    * @author gladisch").append(NEW_LINE);
+                    * @author mbender").append(NEW_LINE);
+                    */""");
         return tb;
     }
 
@@ -137,14 +140,15 @@ private void ghostMapDecls(TypeSpec.Builder clazz) {
         clazz.addField(String.class, "NoSuchFieldExceptionText", Modifier.PUBLIC, Modifier.STATIC);
         clazz.addField(Boolean.TYPE, "ghostMapActive", Modifier.PUBLIC, Modifier.STATIC);
         clazz.addField(ParameterizedTypeName.get(HashMap.class, Integer.class, Object.class),
-                "ghostModelFields",
-                Modifier.PUBLIC, Modifier.STATIC);
+            "ghostModelFields",
+            Modifier.PUBLIC, Modifier.STATIC);
         clazz.addMethod(MethodSpec.methodBuilder("getHash")
                 .addModifiers(Modifier.PUBLIC, Modifier.STATIC)
                 .addParameter(Class.class, "c")
                 .addParameter(Object.class, "obj")
                 .addParameter(String.class, "attr")
-                .addStatement("return c.hashCode() * (obj!=null?obj.hashCode():1) * attr.hashCode();")
+                .addStatement(
+                    "return c.hashCode() * (obj!=null?obj.hashCode():1) * attr.hashCode();")
                 .build());
     }
 
@@ -158,7 +162,8 @@ private void instanceMethod(TypeSpec.Builder clazz) {
                 .returns(Object.class)
                 .addParameter(Class.class, "c")
                 .addException(Exception.class)
-                .addJavadoc("The Objenesis library can create instances of classes that have no default constructor.")
+                .addJavadoc(
+                    "The Objenesis library can create instances of classes that have no default constructor.")
                 .addStatement("Object res=objenesis.newInstance(c);")
                 .beginControlFlow("if (res==null)")
                 .addStatement("throw new Exception($S+c);", "Couldn't create instance of class: ")
@@ -169,24 +174,25 @@ private void instanceMethod(TypeSpec.Builder clazz) {
 
     private void staticInitializer(boolean ghostMapActive, TypeSpec.Builder clazz) {
         clazz.addStaticBlock(
-                CodeBlock.builder()
-                        .addStatement("objenesis = new org.objenesis.ObjenesisStd();")
-                        .add("ghostMapActive = $L;", ghostMapActive)
-                        .add("ghostModelFields = new java.util.HashMap<Integer,Object>();")
-                        .add("NoSuchFieldExceptionText =")
-                        .addStatement("/*This exception occurs when ghost fields or model fields are used in " +
-                                "the code or if mock objects are used that have different fields, than the real objects." +
-                                "The tester should extend the handling of such fields in this generated utility class RFL.java.*/;)"
-                        ).build()
-        );
+            CodeBlock.builder()
+                    .addStatement("objenesis = new org.objenesis.ObjenesisStd();")
+                    .add("ghostMapActive = $L;", ghostMapActive)
+                    .add("ghostModelFields = new java.util.HashMap<Integer,Object>();")
+                    .add("NoSuchFieldExceptionText =")
+                    .addStatement(
+                        "/*This exception occurs when ghost fields or model fields are used in " +
+                            "the code or if mock objects are used that have different fields, than the real objects."
+                            +
+                            "The tester should extend the handling of such fields in this generated utility class RFL.java.*/;)")
+                    .build());
     }
 
     /**
      * All calls to create objects for the given sorts
      */
     private void instances(final HashSet<String> sorts, TypeSpec.Builder clazz) {
-        //r.append(NEW_LINE).append("  // ---The methods for object creation---").append(NEW_LINE)
-        //        .append(NEW_LINE);
+        // r.append(NEW_LINE).append(" // ---The methods for object creation---").append(NEW_LINE)
+        // .append(NEW_LINE);
         for (final String sort : sorts) {
             clazz.addMethod(newRef(sort));
         }
@@ -236,8 +242,8 @@ private MethodSpec newInstance(final String sort) {
                 .returns(returnType)
                 .addException(RuntimeException.class)
                 .addStatement("try{ return ($N) newInstance($N.class); } " +
-                                "catch (java.lang.Throwable e) { throw new java.lang.RuntimeException(e); }",
-                        returnType)
+                    "catch (java.lang.Throwable e) { throw new java.lang.RuntimeException(e); }",
+                    returnType)
                 .build();
     }
 
@@ -287,15 +293,16 @@ private MethodSpec declareSetter(final String sort, final boolean prim) {
 
         if (prim)
             ms.addStatement("f.set" + Character.toUpperCase(sort.charAt(0)) + sort.substring(1)
-                    + "(obj, val);");
+                + "(obj, val);");
         else
             ms.addStatement("f.set(obj, val);");
 
         ms.nextControlFlow("catch(NoSuchFieldException e)")
                 .beginControlFlow("if(ghostMapActive)")
                 .addStatement("ghostModelFields.put(getHash(c,obj,attr), val);")
                 .nextControlFlow("else")
-                .addStatement("throw new RuntimeException(e.toString() + NoSuchFieldExceptionText);")
+                .addStatement(
+                    "throw new RuntimeException(e.toString() + NoSuchFieldExceptionText);")
                 .endControlFlow()
                 .nextControlFlow("catch(Exception e)")
                 .addStatement("throw new RuntimeException(e);")
@@ -327,7 +334,7 @@ private MethodSpec declareGetter(final String sort, final String def, final bool
 
         if (prim)
             ms.addStatement("return f.get" + Character.toUpperCase(sort.charAt(0))
-                    + sort.substring(1) + "(obj);");
+                + sort.substring(1) + "(obj);");
         else
             ms.addStatement("return ($N) f.get(obj);", retType);