wip picocli

Author: wadoon

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

@@ -5,28 +5,26 @@
 
 import org.key_project.util.java.StringUtil;
 
-public interface Constants {
-
+public class Constants {
     /**
      * Constant for the line break which is used by the operating system.
      * <p>
      * <b>Do not use {@code \n}!</b>
      */
-    String NEW_LINE = StringUtil.NEW_LINE;
-    String NULLABLE = "/*@ nullable */";
-    String ALL_OBJECTS = "allObjects";
-    String ALL_INTS = "allInts";
-    String ALL_BOOLS = "allBools";
-    String ALL_HEAPS = "allHeaps";
-    String ALL_FIELDS = "allFields";
-    String ALL_SEQ = "allSeq";
-    String ALL_LOCSETS = "allLocSets";
-
-    String OBJENESIS_NAME = "objenesis-2.2.jar";
-
-    String OLDMap = "old";
-
-    String TAB = "   ";
+    public static final String NEW_LINE = StringUtil.NEW_LINE;
+    public static final String NULLABLE = "/*@ nullable */";
+    public static final String ALL_OBJECTS = "allObjects";
+    public static final String ALL_INTS = "allInts";
+    public static final String ALL_BOOLS = "allBools";
+    public static final String ALL_HEAPS = "allHeaps";
+    public static final String ALL_FIELDS = "allFields";
+    public static final String ALL_SEQ = "allSeq";
+    public static final String ALL_LOCSETS = "allLocSets";
+    public static final String OBJENESIS_NAME = "objenesis-2.2.jar";
+    public static final String OLD_MAP = "old";
+    public static final String TAB = "   ";
+    public static final String DUMMY_POSTFIX = "DummyImpl";
 
-    String DUMMY_POSTFIX = "DummyImpl";
+    private Constants() {
+    }
 }

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

@@ -1,3 +1,6 @@
+/* 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;
 
 import java.io.IOException;
@@ -7,30 +10,38 @@
 import java.util.Objects;
 
 /**
+ * This class manages the different paths in the output folder.
  * @author Alexander Weigl
  * @version 1 (02.02.24)
  */
 public record OutputEnvironment(Path targetFolder) {
+    /** Returns the source code folder */
     public Path getSourceDir() {
         return targetFolder.resolve("src");
     }
 
+    /** Returns the test code folder */
     public Path getTestSourceDir() {
         return targetFolder.resolve("test");
     }
 
+    /** Returns the path to the ANT build.xml file */
     public Path getAntFile() {
         return targetFolder.resolve("build.xml");
     }
 
+    /** Returns the path to the README.md file */
     public Path getReadmeFile() {
         return targetFolder.resolve("README.md");
     }
 
+    /**
+     * Initialize/create the necessary directories.
+     * @throws IOException if the output folder is not write or the folders can not be created.
+     */
     public void init() throws IOException {
         Files.createDirectories(getSourceDir());
         Files.createDirectories(getTestSourceDir());
-
         installAntFile();
     }
 

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

@@ -25,11 +25,6 @@
 
 import org.key_project.logic.sort.Sort;
 
-import org.jspecify.annotations.Nullable;
-
-import org.key_project.logic.sort.Sort;
-
-import org.jspecify.annotations.Nullable;
 import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
@@ -46,8 +41,8 @@ public ProofInfo(Proof proof) {
     public IProgramMethod getMUT() {
         SpecificationRepository spec = services.getSpecificationRepository();
         IObserverFunction f = spec.getTargetOfProof(proof);
-        if (f instanceof IProgramMethod) {
-            return (IProgramMethod) f;
+        if (f instanceof IProgramMethod pm) {
+            return pm;
         } else {
             return null;
         }
@@ -64,8 +59,8 @@ public String getMUTCall() {
         StringBuilder params = new StringBuilder();
         for (ParameterDeclaration p : m.getParameters()) {
             for (VariableSpecification v : p.getVariables()) {
-                IProgramVariable var = v.getProgramVariable();
-                params.append(",").append(var.name());
+                IProgramVariable pvar = v.getProgramVariable();
+                params.append(",").append(pvar.name());
             }
         }
         if (!params.isEmpty()) {
@@ -122,9 +117,8 @@ public Term getPreConTerm() {
         Contract c = getContract();
         if (c instanceof FunctionalOperationContract t) {
             OriginalVariables orig = t.getOrigVars();
-            Term post = t.getPre(services.getTypeConverter().getHeapLDT().getHeap(), orig.self,
+            return t.getPre(services.getTypeConverter().getHeapLDT().getHeap(), orig.self,
                     orig.params, orig.atPres, services);
-            return post;
         }
         // no pre <==> false
         return services.getTermBuilder().ff();

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

@@ -7,7 +7,7 @@
 import java.util.HashSet;
 import javax.lang.model.element.Modifier;
 
-import de.uka.ilkd.key.logic.sort.Sort;
+import org.key_project.logic.sort.Sort;
 
 import com.squareup.javapoet.*;
 
@@ -77,8 +77,8 @@ public void addSort(String s) {
      */
     private HashSet<String> sortsToString() {
         final HashSet<String> result = new HashSet<>();
-        for (final Sort var : usedObjectSorts) {
-            String sort = var.toString();
+        for (final Sort s : usedObjectSorts) {
+            String sort = s.toString();
             // We only want Object-Types
             if (!" jbyte jint jlong jfloat jdouble jboolean jchar ".contains(" " + sort + " ")) {
                 if (" jbyte[] jint[] jlong[] jfloat[] jdouble[] jboolean[] jchar[] "
@@ -191,8 +191,6 @@ private void staticInitializer(boolean ghostMapActive, TypeSpec.Builder clazz) {
      * 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);
         for (final String sort : sorts) {
             clazz.addMethod(newRef(sort));
         }