Merge remote-tracking branch 'origin/main' into weigl/config

* origin/main: (62 commits)
  Fix comment author and nicer message
  fix typo in filename
  Fail gracefully
  Fix conversion to number of empty string
  Unused files
  Fix bsumSplitInvalid being notprovable
  Move file again
  Move file
  Remove duplicate group
  Spotless
  Fix option being ignored by not being formatted
  Fix proof settings not being used
  Sort output of DefaultChoices
  Cleanup
  Fix input
  Fix input
  Fix writing of the pr number
  Fix type of `Long.MIN_VALUE` and `Long.MAX_VALUE`
  Reword message
  Fix script syntax errors
  ...

.github/workflows/artiweb.yml

@@ -1,3 +1,5 @@
+name: Artiweb Comment
+
 on:
   workflow_run:
     workflows: [Tests]
@@ -6,61 +8,81 @@ on:
 
 # taken from https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#using-data-from-the-triggering-workflow
 jobs:
-  download:
+  comment:
     runs-on: ubuntu-latest
     steps:
       - name: 'Download artifact'
+        id: da
         uses: actions/github-script@v6
         with:
           script: |
-            let allArtifacts = await github.rest.actions.listWorkflowRunArtifacts({
+            if (context.payload.workflow_run === undefined) {
+                core.setFailed("No workflow run found");
+            }
+            const allArtifacts = await github.rest.actions.listWorkflowRunArtifacts({
                owner: context.repo.owner,
                repo: context.repo.repo,
                run_id: context.payload.workflow_run.id,
             });
-            let matchArtifact = allArtifacts.data.artifacts.filter((artifact) => {
-              return artifact.name == "pr-number"
-            })[0];
-            let download = await github.rest.actions.downloadArtifact({
-               owner: context.repo.owner,
-               repo: context.repo.repo,
-               artifact_id: matchArtifact.id,
-               archive_format: 'zip',
+            
+            const testArtifact = allArtifacts.data.artifacts.find((artifact) => {
+               return artifact.name == "test-results"
             });
-            let fs = require('fs');
-            fs.writeFileSync(`${process.env.GITHUB_WORKSPACE}/pr_number.zip`, Buffer.from(download.data));
-            let testArtifact = allArtifacts.data.artifacts.filter((artifact) => {
-              return artifact.name == "test-results"
-            })[0];
-            echo "TEST_ARTIFACT_NUMBER={testArtifact.id}" >> $GITHUB_ENV
+            if (testArtifact !== undefined) {
+               core.info("Found test-results artifact id: " + testArtifact.id);
+               core.setOutput("test-artifact-id", testArtifact.id);
+            } else {
+               core.info("Artifact test-results was not found");
+            }
+            
+            const numberArtifact = allArtifacts.data.artifacts.find((artifact) => {
+               return artifact.name == "pr-number"
+            });
+            if (numberArtifact !== undefined) {
+               core.info("Found pr-number artifact id: " + numberArtifact.id); 
+               let download = await github.rest.actions.downloadArtifact({
+                  owner: context.repo.owner,
+                  repo: context.repo.repo,
+                  artifact_id: numberArtifact.id,
+                  archive_format: 'zip',
+               });
+               let fs = require('fs');
+               fs.writeFileSync(`${process.env.GITHUB_WORKSPACE}/pr_number.zip`, Buffer.from(download.data));
+            } else {
+               core.setFailed("Artifact pr-number was not found");
+            }
 
       - name: 'Unzip artifact'
         run: unzip pr_number.zip
 
       - name: 'Read pr number'
+        id: rpn
         uses: actions/github-script@v6
         with:
           github-token: ${{ secrets.GITHUB_TOKEN }}
           script: |
             let fs = require('fs');
-            let issue_number = Number(fs.readFileSync('./pr_number'));
-            echo "PR_NUMBER={issue_number}" >> $GITHUB_ENV
-
+            let issue_number_text = fs.readFileSync('./pr_number');
+            core.info("Found pr number \"" + issue_number_text + "\"");
+            core.setOutput("pr-number", issue_number_text === "" ? "" : Number(issue_number_text));
       - name: Find Comment
+        if: ${{ steps.rpn.outputs.pr-number != '' }}
         uses: peter-evans/find-comment@v2
         id: fc
         with:
-          issue-number: ${{ env.PR_NUMBER }}
-          comment-author: 'KiKi'
+          issue-number: ${{ steps.rpn.outputs.pr-number }}
+          comment-author: 'github-actions'
           body-includes: Artiweb
 
       - name: Create or update comment
+        if: ${{ steps.rpn.outputs.pr-number != '' }}
         uses: peter-evans/create-or-update-comment@v2
         with:
           comment-id: ${{ steps.fc.outputs.comment-id }}
-          issue-number: ${{ env.PR_NUMBER }}
+          issue-number: ${{ steps.rpn.outputs.pr-number }}
           body: |
-            Test artifacts will be available on [Artiweb](https://keyproject.github.io/artiweb/${env.PR_NUMBER}/).
+            Thank you for your contribution.
             
-            The newest artifact is [here](https://keyproject.github.io/artiweb/${env.PR_NUMBER}/${env.TEST_ARTIFACT_NUMBER}/).
+            The test artifacts are available on [Artiweb](https://keyproject.github.io/artiweb/${{steps.rpn.outputs.pr-number}}/).
+            The newest artifact is [here](https://keyproject.github.io/artiweb/${{steps.rpn.outputs.pr-number}}/${{steps.da.outputs.test-artifact-id}}/).
           edit-mode: replace

.github/workflows/tests.yml

@@ -28,11 +28,17 @@ jobs:
       GH_TOKEN: ${{ github.token }}
     steps:
       - name: Save PR number
-        env:
-          PR_NUMBER: ${{ github.event.number }}
-        run: |
-          mkdir -p ./pr
-          echo $PR_NUMBER > ./pr/pr_number
+        uses: actions/github-script@v6
+        with:
+          script: |
+            const fs = require('fs');
+            const util = require('util');
+            fs.mkdirSync("./pr", { recursive: true });
+            const payload = context.payload;
+            const number = (payload.issue || payload.pull_request || payload).number;
+            const text = number === undefined ? "" : String(number);
+            core.info("Pr number is " + number + ", writing \"" + text + "\"");
+            fs.writeFileSync("./pr/pr_number", text);
       - uses: actions/upload-artifact@v3
         with:
           name: pr-number

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/ProofReferenceUtil.java

@@ -114,7 +114,7 @@ private static class ReferenceAnalaystProofVisitor implements ProofVisitor {
          * The result.
          */
         private final LinkedHashSet<IProofReference<?>> result =
-            new LinkedHashSet<IProofReference<?>>();
+            new LinkedHashSet<>();
 
         /**
          * Constructor.
@@ -168,7 +168,7 @@ public static LinkedHashSet<IProofReference<?>> computeProofReferences(Node node
      */
     public static LinkedHashSet<IProofReference<?>> computeProofReferences(Node node,
             Services services, ImmutableList<IProofReferencesAnalyst> analysts) {
-        LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<IProofReference<?>>();
+        LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();
         if (node != null && analysts != null) {
             for (IProofReferencesAnalyst analyst : analysts) {
                 LinkedHashSet<IProofReference<?>> analystResult =

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ClassAxiomAndInvariantProofReferencesAnalyst.java

@@ -66,19 +66,19 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
                     // Invariant was applied
                     PartialInvAxiom axiom = (PartialInvAxiom) found;
                     DefaultProofReference<ClassInvariant> reference =
-                        new DefaultProofReference<ClassInvariant>(IProofReference.USE_INVARIANT,
+                        new DefaultProofReference<>(IProofReference.USE_INVARIANT,
                             node, axiom.getInv());
                     LinkedHashSet<IProofReference<?>> result =
-                        new LinkedHashSet<IProofReference<?>>();
+                        new LinkedHashSet<>();
                     result.add(reference);
                     return result;
                 } else if (found != null) {
                     // ClassAxiom was applied
                     DefaultProofReference<ClassAxiom> reference =
-                        new DefaultProofReference<ClassAxiom>(IProofReference.USE_AXIOM, node,
+                        new DefaultProofReference<>(IProofReference.USE_AXIOM, node,
                             found);
                     LinkedHashSet<IProofReference<?>> result =
-                        new LinkedHashSet<IProofReference<?>>();
+                        new LinkedHashSet<>();
                     result.add(reference);
                     return result;
                 } else {

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ContractProofReferencesAnalyst.java

@@ -23,9 +23,9 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
         if (node.getAppliedRuleApp() instanceof AbstractContractRuleApp) {
             AbstractContractRuleApp contractRuleApp =
                 (AbstractContractRuleApp) node.getAppliedRuleApp();
-            DefaultProofReference<Contract> reference = new DefaultProofReference<Contract>(
+            DefaultProofReference<Contract> reference = new DefaultProofReference<>(
                 IProofReference.USE_CONTRACT, node, contractRuleApp.getInstantiation());
-            LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<IProofReference<?>>();
+            LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();
             result.add(reference);
             return result;
         } else {

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/IProofReferencesAnalyst.java

@@ -31,5 +31,5 @@ public interface IProofReferencesAnalyst {
      * @return The found {@link IProofReference} or {@code null}/empty set if the applied rule is
      *         not supported.
      */
-    public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services);
+    LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services);
 }

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodBodyExpandProofReferencesAnalyst.java

@@ -27,9 +27,9 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
                 MethodBodyStatement mbs = (MethodBodyStatement) info.getActiveStatement();
                 IProgramMethod pm = mbs.getProgramMethod(services);
                 DefaultProofReference<IProgramMethod> reference =
-                    new DefaultProofReference<IProgramMethod>(IProofReference.INLINE_METHOD, node,
+                    new DefaultProofReference<>(IProofReference.INLINE_METHOD, node,
                         pm);
-                LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<IProofReference<?>>();
+                LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();
                 result.add(reference);
                 return result;
             } else {

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodCallProofReferencesAnalyst.java

@@ -6,7 +6,6 @@
 import de.uka.ilkd.key.java.ProgramElement;
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
-import de.uka.ilkd.key.java.abstraction.Type;
 import de.uka.ilkd.key.java.expression.Assignment;
 import de.uka.ilkd.key.java.reference.ExecutionContext;
 import de.uka.ilkd.key.java.reference.MethodReference;
@@ -50,14 +49,14 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
                     IProofReference<IProgramMethod> reference = createReference(node, services,
                         context, (MethodReference) info.getActiveStatement());
                     LinkedHashSet<IProofReference<?>> result =
-                        new LinkedHashSet<IProofReference<?>>();
+                        new LinkedHashSet<>();
                     result.add(reference);
                     return result;
                 } else if (info.getActiveStatement() instanceof Assignment) {
                     Assignment assignment = (Assignment) info.getActiveStatement();
                     ExecutionContext context = extractContext(node, services);
                     LinkedHashSet<IProofReference<?>> result =
-                        new LinkedHashSet<IProofReference<?>>();
+                        new LinkedHashSet<>();
                     for (int i = 0; i < assignment.getChildCount(); i++) {
                         ProgramElement child = assignment.getChildAt(i);
                         if (child instanceof MethodReference) {
@@ -106,7 +105,7 @@ protected IProofReference<IProgramMethod> createReference(Node node, Services se
         if (context != null) {
             KeYJavaType refPrefixType = mr.determineStaticPrefixType(services, context);
             IProgramMethod pm = mr.method(services, refPrefixType, context);
-            return new DefaultProofReference<IProgramMethod>(IProofReference.CALL_METHOD, node, pm);
+            return new DefaultProofReference<>(IProofReference.CALL_METHOD, node, pm);
         } else {
             if (!(node.getAppliedRuleApp() instanceof PosTacletApp)) {
                 throw new IllegalArgumentException("PosTacletApp expected.");
@@ -131,8 +130,8 @@ protected IProofReference<IProgramMethod> createReference(Node node, Services se
                 throw new IllegalArgumentException("Empty argument list expected.");
             }
             IProgramMethod pm = services.getJavaInfo().getProgramMethod(type.getKeYJavaType(),
-                method.toString(), ImmutableSLList.<Type>nil(), type.getKeYJavaType());
-            return new DefaultProofReference<IProgramMethod>(IProofReference.CALL_METHOD, node, pm);
+                method.toString(), ImmutableSLList.nil(), type.getKeYJavaType());
+            return new DefaultProofReference<>(IProofReference.CALL_METHOD, node, pm);
         }
     }
 }

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java

@@ -31,12 +31,12 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
         if (node.getAppliedRuleApp() != null && node.getNodeInfo() != null) {
             SourceElement statement = node.getNodeInfo().getActiveStatement();
             if (statement instanceof CopyAssignment) {
-                LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<IProofReference<?>>();
+                LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();
                 listReferences(node, (CopyAssignment) statement,
                     services.getJavaInfo().getArrayLength(), result, true);
                 return result;
             } else if (statement instanceof If) {
-                LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<IProofReference<?>>();
+                LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();
                 listReferences(node, ((If) statement).getExpression(),
                     services.getJavaInfo().getArrayLength(), result, false);
                 return result;
@@ -63,7 +63,7 @@ protected void listReferences(Node node, ProgramElement pe, ProgramVariable arra
             ProgramVariable pv = (ProgramVariable) pe;
             if (pv.isMember()) {
                 DefaultProofReference<ProgramVariable> reference =
-                    new DefaultProofReference<ProgramVariable>(IProofReference.ACCESS, node,
+                    new DefaultProofReference<>(IProofReference.ACCESS, node,
                         (ProgramVariable) pe);
                 ProofReferenceUtil.merge(toFill, reference);
             }
@@ -76,7 +76,7 @@ protected void listReferences(Node node, ProgramElement pe, ProgramVariable arra
             ProgramVariable pv = fr.getProgramVariable();
             if (pv != arrayLength) {
                 DefaultProofReference<ProgramVariable> reference =
-                    new DefaultProofReference<ProgramVariable>(IProofReference.ACCESS, node, pv);
+                    new DefaultProofReference<>(IProofReference.ACCESS, node, pv);
                 ProofReferenceUtil.merge(toFill, reference);
             }
         } else if (includeExpressionContainer && pe instanceof ExpressionContainer) {

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/DefaultProofReference.java

@@ -16,22 +16,22 @@ public class DefaultProofReference<T> implements IProofReference<T> {
     /**
      * The reference kind as human readable {@link String}.
      */
-    private String kind;
+    private final String kind;
 
     /**
      * The source {@link Proof}.
      */
-    private Proof source;
+    private final Proof source;
 
     /**
      * The target source member.
      */
-    private T target;
+    private final T target;
 
     /**
      * The {@link Node} in which the reference was found.
      */
-    private LinkedHashSet<Node> nodes = new LinkedHashSet<Node>();
+    private final LinkedHashSet<Node> nodes = new LinkedHashSet<>();
 
     /**
      * Constructor