Cleanup: Removal of the write and read settings using Properties

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

@@ -4,16 +4,17 @@
 package de.uka.ilkd.key.testgen;
 
 import java.io.File;
-import java.util.Properties;
 
 import de.uka.ilkd.key.settings.AbstractSettings;
 import de.uka.ilkd.key.settings.Configuration;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.settings.SettingsConverter;
 
 import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.NullMarked;
 import org.jspecify.annotations.Nullable;
 
+@NullMarked
 public class TestGenerationSettings extends AbstractSettings {
     // region Default Values for option fields
     private static final boolean DEFAULT_APPLYSYMBOLICEX = false;
@@ -77,6 +78,15 @@ public TestGenerationSettings(TestGenerationSettings data) {
 
     }
 
+    /**
+     * @deprecated weigl: This method seems broken. I would expect: copy() = new TGS(this)
+     */
+    @Deprecated(forRemoval = true)
+    public TestGenerationSettings copy(TestGenerationSettings data) {
+        return new TestGenerationSettings(data);
+    }
+
+    public TestGenerationSettings copy() {
     public TestGenerationSettings copy() {
         return new TestGenerationSettings(this);
     }
@@ -111,25 +121,6 @@ public boolean includePostCondition() {
         return includePostCondition;
     }
 
-    @Override
-    public void readSettings(Properties props) {
-        var prefix = "[" + CATEGORY + "]";
-        setApplySymbolicExecution(SettingsConverter.read(props,
-            prefix + PROP_APPLY_SYMBOLIC_EXECUTION, DEFAULT_APPLYSYMBOLICEX));
-        setMaxUnwinds(SettingsConverter.read(props, prefix + PROP_MAX_UWINDS, DEFAULT_MAXUNWINDS));
-        setOutputPath(SettingsConverter.read(props, prefix + PROP_OUTPUT_PATH, DEFAULT_OUTPUTPATH));
-        setRemoveDuplicates(SettingsConverter.read(props,
-            prefix + PROP_REMOVE_DUPLICATES, DEFAULT_REMOVEDUPLICATES));
-        setUseRFL(SettingsConverter.read(props, prefix + PROP_USE_RFL, DEFAULT_USERFL));
-        setConcurrentProcesses(SettingsConverter.read(props,
-            prefix + PROP_CONCURRENT_PROCESSES, DEFAULT_CONCURRENTPROCESSES));
-        setInvariantForAll(SettingsConverter.read(props,
-            prefix + PROP_INVARIANT_FOR_ALL, DEFAULT_INVARIANTFORALL));
-        setIncludePostCondition(SettingsConverter.read(props,
-            PROP_INCLUDE_POST_CONDITION, DEFAULT_INCLUDEPOSTCONDITION));
-        setOnlyTestClasses(SettingsConverter.read(props, PROP_ONLY_TEST_CLASSES, false));
-    }
-
     public boolean removeDuplicates() {
         return removeDuplicates;
     }
@@ -181,19 +172,8 @@ public boolean isUseRFL() {
         return useRFL;
     }
 
-    @Override
-    public void writeSettings(Properties props) {
-        var prefix = "[" + CATEGORY + "]";
-        SettingsConverter.store(props, prefix + PROP_APPLY_SYMBOLIC_EXECUTION,
-            applySymbolicExecution);
-        SettingsConverter.store(props, prefix + PROP_CONCURRENT_PROCESSES, concurrentProcesses);
-        SettingsConverter.store(props, prefix + PROP_INVARIANT_FOR_ALL, invariantForAll);
-        SettingsConverter.store(props, prefix + PROP_MAX_UWINDS, maxUnwinds);
-        SettingsConverter.store(props, prefix + PROP_OUTPUT_PATH, outputPath);
-        SettingsConverter.store(props, prefix + PROP_REMOVE_DUPLICATES, removeDuplicates);
-        SettingsConverter.store(props, prefix + PROP_USE_RFL, useRFL);
-        SettingsConverter.store(props, prefix + PROP_INCLUDE_POST_CONDITION, includePostCondition);
-        SettingsConverter.store(props, prefix + PROP_ONLY_TEST_CLASSES, onlyTestClasses);
+    public boolean useJunit() {
+        return useJunit;
     }
 
     @Override
@@ -229,7 +209,7 @@ public void writeSettings(Configuration props) {
     }
 
     public void set(TestGenerationSettings settings) {
-        Properties p = new Properties();
+        Configuration p = new Configuration();
         settings.writeSettings(p);
         readSettings(p);
     }

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/AbstractTestGenerator.java

@@ -154,9 +154,9 @@ public void generateTestCases(final StopRequest stopRequest, final TGReporter lo
 
         // create special smt settings for test case generation
         final ProofIndependentSMTSettings piSettings =
-            ProofIndependentSettings.DEFAULT_INSTANCE.getSMTSettings().clone();
+            ProofIndependentSettings.DEFAULT_INSTANCE.getSMTSettings().copy();
         piSettings.setMaxConcurrentProcesses(settings.getNumberOfProcesses());
-        final ProofDependentSMTSettings pdSettings = proof.getSettings().getSMTSettings().clone();
+        final ProofDependentSMTSettings pdSettings = proof.getSettings().getSMTSettings().copy();
         final NewSMTTranslationSettings newSettings =
             new NewSMTTranslationSettings(proof.getSettings().getNewSMTSettings());
         pdSettings.setInvariantForall(settings.invariantForAll());

key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java

@@ -87,9 +87,9 @@ public static class File extends KeyAst<KeYParser.FileContext> {
             ProofSettings settings = new ProofSettings(ProofSettings.DEFAULT_SETTINGS);
 
             if (ctx.preferences() != null && ctx.preferences().s != null) {
-                String text = StringUtil.trim(ctx.preferences().s.getText(), '"')
-                        .replace("\\\\:", ":");
-                settings.loadSettingsFromPropertyString(text);
+                throw new IllegalStateException(
+                    "You try to load a KeY file in an deprecated format. " +
+                        "The settings are not a string of properties anymore. Please rewrite to the JSON-like format.");
             } else if (ctx.preferences() != null && ctx.preferences().c != null) {
                 var cb = new ConfigurationBuilder();
                 var c = (Configuration) ctx.preferences().c.accept(cb);

key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java

@@ -120,17 +120,18 @@ public class Proof implements ProofObject<Goal>, Named {
      * settings valid independent of a proof
      */
     private final ProofIndependentSettings pis;
+
     /**
      * when different users load and save a proof this vector fills up with Strings containing the
      * usernames.
      */
-    public List<String> userLog;
+    public List<String> userLog = new ArrayList<>();
 
     /**
      * when load and save a proof with different versions of key this vector fills up with Strings
      * containing the GIT versions.
      */
-    public List<String> keyVersionLog;
+    public List<String> keyVersionLog = new ArrayList<>();
 
     private long autoModeTime = 0;
 
@@ -172,8 +173,8 @@ public class Proof implements ProofObject<Goal>, Named {
      */
     private Proof(Name name, InitConfig initConfig) {
         this.name = name;
-        assert initConfig != null : "Tried to create proof without valid services.";
-        this.initConfig = initConfig;
+        this.initConfig =
+            Objects.requireNonNull(initConfig, "Tried to create proof without valid services.");
 
         if (initConfig.getSettings() == null) {
             // if no settings have been assigned yet, take default settings

key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java

@@ -3,8 +3,9 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof.io;
 
+import java.io.IOException;
+import java.io.StringReader;
 import java.util.ArrayDeque;
-import java.util.ArrayList;
 import java.util.LinkedList;
 import java.util.List;
 
@@ -143,26 +144,16 @@ public void beginExpr(ProofElementID eid, String str) {
                 TacletInformation tacletInfo = (TacletInformation) ruleInfo;
                 tacletInfo.ifDirectFormulaList = tacletInfo.ifDirectFormulaList.append(str);
             }
-            case KeY_USER -> { // UserLog
-                if (proof.userLog == null) {
-                    proof.userLog = new ArrayList<>();
-                }
-                proof.userLog.add(str);
-            }
-            case KeY_VERSION -> { // Version log
-                if (proof.keyVersionLog == null) {
-                    proof.keyVersionLog = new ArrayList<>();
-                }
-                proof.keyVersionLog.add(str);
-            }
-            case KeY_SETTINGS -> // ProofSettings
-                loadPreferences(str);
-            case BUILT_IN_RULE -> { // BuiltIn rules
-                {
-                    final AppNodeIntermediate newNode = new AppNodeIntermediate();
-                    currNode.addChild(newNode);
-                    currNode = newNode;
-                }
+        case KeY_USER -> // UserLog
+            proof.userLog.add(str);
+        case KeY_VERSION -> // Version log
+            proof.keyVersionLog.add(str);
+        case KeY_SETTINGS -> // ProofSettings
+            loadPreferences(str);
+        case BUILT_IN_RULE -> { // BuiltIn rules
+            final AppNodeIntermediate newNode = new AppNodeIntermediate();
+            currNode.addChild(newNode);
+            currNode = newNode;
                 ruleInfo = new BuiltinRuleInformation(str);
             }
             case CONTRACT -> ((BuiltinRuleInformation) ruleInfo).currContract = str;
@@ -330,7 +321,11 @@ private BuiltInAppIntermediate constructBuiltInApp() {
      */
     private void loadPreferences(String preferences) {
         final ProofSettings proofSettings = new ProofSettings(ProofSettings.DEFAULT_SETTINGS);
-        proofSettings.loadSettingsFromPropertyString(preferences);
+        try {
+            proofSettings.loadSettingsFromJSONStream(new StringReader(preferences));
+        } catch (IOException e) {
+            throw new RuntimeException(e); // no I/O exception on strings.
+        }
     }
 
     /**