Migrate from ST4 to Apache Freemarker in keyext.proofmanagement

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

@@ -25,7 +25,6 @@
  * nodes, or the number of interactions.
  *
  * @author bruns
- *
  */
 public class Statistics {
     public final int nodes;
@@ -447,4 +446,76 @@ private int tmpQuantificationRuleApps(final RuleApp ruleApp) {
             return res;
         }
     }
+
+    public long getAutoModeTimeInMillis() {
+        return autoModeTimeInMillis;
+    }
+
+    public int getBlockLoopContractApps() {
+        return blockLoopContractApps;
+    }
+
+    public int getBranches() {
+        return branches;
+    }
+
+    public int getCachedBranches() {
+        return cachedBranches;
+    }
+
+    public int getDependencyContractApps() {
+        return dependencyContractApps;
+    }
+
+    public int getInteractiveSteps() {
+        return interactiveSteps;
+    }
+
+    public int getLoopInvApps() {
+        return loopInvApps;
+    }
+
+    public int getMergeRuleApps() {
+        return mergeRuleApps;
+    }
+
+    public int getNodes() {
+        return nodes;
+    }
+
+    public int getOperationContractApps() {
+        return operationContractApps;
+    }
+
+    public int getOssApps() {
+        return ossApps;
+    }
+
+    public int getQuantifierInstantiations() {
+        return quantifierInstantiations;
+    }
+
+    public int getSmtSolverApps() {
+        return smtSolverApps;
+    }
+
+    public List<Pair<String, String>> getSummaryList() {
+        return summaryList;
+    }
+
+    public int getSymbExApps() {
+        return symbExApps;
+    }
+
+    public long getTimeInMillis() {
+        return timeInMillis;
+    }
+
+    public float getTimePerStepInMillis() {
+        return timePerStepInMillis;
+    }
+
+    public int getTotalRuleApps() {
+        return totalRuleApps;
+    }
 }

key.core/src/test/java/de/uka/ilkd/key/util/TestMiscTools.java

@@ -21,9 +21,9 @@
 
 import de.uka.ilkd.key.java.recoderext.URLDataLocation;
 
+import org.junit.jupiter.api.Disabled;
 import org.key_project.util.java.IOUtil;
 
-import org.junit.jupiter.api.Disabled;
 import org.junit.jupiter.api.Test;
 import recoder.io.ArchiveDataLocation;
 import recoder.io.DataFileLocation;
@@ -60,7 +60,7 @@ public void testMakeFilenameRelativeUnix() {
 
     @Test
     @Disabled("weigl: Disabled b/c failing on Windows Server (Github Action). " +
-        "Failing is not  reproducible on Windows.")
+        "Failing is not reproducible on Windows 10.")
     public void testMakeFilenameRelativeWindows() {
         // run only on Windows systems
         if (File.separatorChar != '\\') {

key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java

@@ -9,6 +9,8 @@
 
 import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager;
 
+import org.checkerframework.checker.initialization.qual.UnderInitialization;
+
 import static de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager.SHORTCUT_KEY_MASK;
 
 /**
@@ -58,6 +60,14 @@ public abstract class KeyAction extends AbstractAction {
      */
     public static final String LOCAL_ACCELERATOR = "LOCAL_ACCELERATOR";
 
+    /// {@inheritDoc}
+    @Override
+    public void putValue(
+            @UnderInitialization(KeyAction.class) KeyAction this,
+            String key, Object newValue) {
+        super.putValue(key, newValue);
+    }
+
     public String getName() {
         return (String) getValue(NAME);
     }

key.ui/src/main/java/de/uka/ilkd/key/util/CommandLine.java

@@ -10,6 +10,8 @@
 
 import de.uka.ilkd.key.core.Main;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  * A small framework to handle command lines.
  *
@@ -77,7 +79,7 @@ private class Option extends HelpElement {
         private String description;
         private String image;
         private String value;
-        private String parameter;
+        private @Nullable String parameter;
 
         @Override
         protected void print(PrintStream stream, int descriptionCol) {
@@ -257,7 +259,7 @@ public boolean subCommandUsed(String name) {
      *        this option (e.g. {@code <file>, time, path}, ...
      * @param description the description of the option
      */
-    public void addOption(String image, String parameter, String description) {
+    public void addOption(String image, @Nullable String parameter, String description) {
 
         if (!image.startsWith(MINUS)) {
             throw new IllegalArgumentException(

key.util/src/main/java/org/key_project/util/helper/FindResources.java

@@ -168,7 +168,9 @@ public final class FindResources {
     }
 
     public static @Nullable Path getTestCasesDirectory() {
-        return findFolder("TEST_CASES", "src/test/resources/testcase");
+        return findFolder("TEST_CASES",
+            "src/test/resources/testcase",
+            "../key.core/src/test/resources/testcase");
     }
 
     public static @Nullable Path getTestResourcesDirectory() {

keyext.proofmanagement/build.gradle

@@ -9,7 +9,7 @@ dependencies {
     implementation project(':key.core')
     implementation project(':key.ui')
 
-    implementation group: 'org.antlr', name: 'ST4', version: '4.3.4'
+    implementation("org.freemarker:freemarker:2.3.34")
 }
 
 application {
@@ -18,6 +18,26 @@ application {
     applicationName = "pm"
 }
 
+
+def testIntegrationReport = tasks.register('testIntegrationReport', JavaExec) {
+    group = "verification"
+    mainClass.set(application.mainClass)
+    classpath = sourceSets.main.runtimeClasspath
+
+    args('check', '--missing', '--settings', '--report', 'proofManagementReport.html', '--replay', '--dependency',
+            'proofBundle/simpleBundleGeneration')
+}
+
+def testIntegrationReport2 = tasks.register('testIntegrationReport2', JavaExec) {
+    group = "verification"
+    mainClass.set(application.mainClass)
+    classpath = sourceSets.main.runtimeClasspath
+
+    args('check', '--missing', '--settings', '--report', 'proofManagementReport.html', '--replay', '--dependency',
+            'src/test/pmexample2')
+}
+test.dependsOn(testIntegrationReport, testIntegrationReport2)
+
 run {
     // for debugging, something like this can be used:
     //args('check', '--missing', '--settings', '--report', 'proofManagementReport.html', '--replay', '--dependency', 'pmexample2')
@@ -32,3 +52,21 @@ shadowJar {
     archiveClassifier = "exe"
     archiveBaseName = "keyext.proofmanagement"
 }
+
+
+
+checkerFramework {
+    if(System.getProperty("ENABLE_NULLNESS")) {
+        checkers = [
+                "org.checkerframework.checker.nullness.NullnessChecker",
+        ]
+        extraJavacArgs = [
+                "-AonlyDefs=^org\\.key_project\\.proofmanagement",
+                "-Xmaxerrs", "10000",
+                "-Astubs=$projectDir/src/main/checkerframework:permit-nullness-assertion-exception.astub:checker.jar/junit-assertions.astub",
+                "-AstubNoWarnIfNotFound",
+                //"-Werror",
+                "-Aversion",
+        ]
+    }
+}

keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/FilterOutputStream.java

@@ -0,0 +1,7 @@
+package java.io;
+
+public class FilterOutputStream extends java.io.OutputStream {
+
+    protected java.io.OutputStream out;
+
+}

keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/IOException.java

@@ -0,0 +1,13 @@
+/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
+ * Date: Fri Mar 28 13:47:08 CET 2008
+ */
+package java.io;
+
+public class IOException extends java.lang.Exception
+{
+
+   public IOException();
+   public IOException(java.lang.String arg0);
+   public IOException(java.lang.String arg0, java.lang.Throwable arg1);
+   public IOException(java.lang.Throwable arg0);
+}

keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/InputStream.java

@@ -0,0 +1,7 @@
+package java.io;
+
+public class InputStream {
+
+    public InputStream();
+
+}

keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/OutputStream.java

@@ -0,0 +1,6 @@
+package java.io;
+
+public class OutputStream {
+
+
+}

keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/PrintStream.java

@@ -0,0 +1,27 @@
+package java.io;
+
+public class PrintStream extends java.io.FilterOutputStream {
+
+    public PrintStream(java.io.OutputStream out);
+    public PrintStream(java.io.OutputStream out, boolean autoFlush);
+
+    public void print(boolean b);
+    public void print(char c);
+    public void print(int i);
+    public void print(long l);
+    // public void print(float f);
+    // public void print(double d);
+    public void print(char[] s);
+    public void print(java.lang.String s);
+    public void print(java.lang.Object obj);
+    public void println();
+    public void println(boolean x);
+    public void println(char x);
+    public void println(int x);
+    public void println(long x);
+    // public void println(float x);
+    // public void println(double x);
+    public void println(char[] x);
+    public void println(java.lang.String x);
+    public void println(java.lang.Object x);
+}

keyext.proofmanagement/proofBundle/complexBundleGeneration/a/io/Serializable.java

@@ -0,0 +1,9 @@
+/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
+ * Date: Fri Mar 28 13:47:08 CET 2008
+ */
+package java.io;
+
+public interface Serializable
+{
+
+}

keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ArithmeticException.java

@@ -0,0 +1,11 @@
+/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
+ * Date: Fri Mar 28 13:47:08 CET 2008
+ */
+package java.lang;
+
+public class ArithmeticException extends java.lang.RuntimeException
+{
+
+   public ArithmeticException() { super(); }
+   public ArithmeticException(java.lang.String arg0) { super(arg0); }
+}

keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ArrayIndexOutOfBoundsException.java

@@ -0,0 +1,12 @@
+/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
+ * Date: Fri Mar 28 13:47:08 CET 2008
+ */
+package java.lang;
+
+public class ArrayIndexOutOfBoundsException extends java.lang.IndexOutOfBoundsException
+{
+
+   public ArrayIndexOutOfBoundsException() { super(); }
+   public ArrayIndexOutOfBoundsException(int arg0);
+   public ArrayIndexOutOfBoundsException(java.lang.String arg0) { super(arg0); }
+}

keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ArrayStoreException.java

@@ -0,0 +1,11 @@
+/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
+ * Date: Fri Mar 28 13:47:08 CET 2008
+ */
+package java.lang;
+
+public class ArrayStoreException extends java.lang.RuntimeException
+{
+
+   public ArrayStoreException() { super(); }
+   public ArrayStoreException(java.lang.String arg0) { super(arg0); }
+}

keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/AssertionError.java

@@ -0,0 +1,12 @@
+package java.lang;
+
+public class AssertionError extends java.lang.Error {
+    public AssertionError() {}
+    public AssertionError(java.lang.Object detailMessage) {}
+    public AssertionError(boolean detailMessage){}
+    public AssertionError(char detailMessage)   {}
+//    public AssertionError(double detailMessage) {}
+//    public AssertionError(float detailMessage)  {}
+    public AssertionError(int detailMessage)    {}
+    public AssertionError(long detailMessage)   {}
+}

keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Character.java

@@ -0,0 +1,9 @@
+package java.lang;
+
+/**
+ * Exists only for proving EVotingMachine
+ */
+public final class Character extends java.lang.Object implements java.io.Serializable, java.lang.Comparable
+{
+	static int digit(char ch, int radix);
+}

keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/Class.java

@@ -0,0 +1,8 @@
+
+
+package java.lang;
+
+
+public final class Class {
+
+}

keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/ClassCastException.java

@@ -0,0 +1,11 @@
+/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
+ * Date: Tue Apr 15 10:18:21 CEST 2008
+ */
+package java.lang;
+
+public class ClassCastException extends java.lang.RuntimeException
+{
+
+   public ClassCastException() { super(); }
+   public ClassCastException(java.lang.String arg0) { super(arg0); }
+}

keyext.proofmanagement/proofBundle/complexBundleGeneration/a/lang/CloneNotSupportedException.java

@@ -0,0 +1,11 @@
+/* This file has been generated by Stubmaker (de.uka.ilkd.stubmaker)
+ * Date: Fri Mar 28 13:47:08 CET 2008
+ */
+package java.lang;
+
+public class CloneNotSupportedException extends java.lang.Exception
+{
+
+   public CloneNotSupportedException() { super(); } 
+   public CloneNotSupportedException(java.lang.String arg0) { super(arg0); }
+}