Ncore taclets

.gitignore

@@ -70,3 +70,6 @@ key.core/src/main/antlr4/gen/
 
 scripts/tools/checkstyle/key_checks_incremental.xml
 checkstyle-diff.txt
+/key.ncore/src/main/gen/
+/key.ncore/src/main/antlr/KeYLexer.tokens
+/keyext.rusty/src/main/gen/

build.gradle

@@ -21,7 +21,7 @@ plugins {
     // id "com.github.ben-manes.versions" version "0.39.0"
 
     // Code formatting
-    id "com.diffplug.spotless" version "6.25.0"
+    id "com.diffplug.spotless" version "7.0.0.BETA2"
 
     // EISOP Checker Framework
     id "org.checkerframework" version "0.6.45"

gradle/wrapper/gradle-wrapper.properties

@@ -1,5 +1,7 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
 distributionUrl=https\://services.gradle.org/distributions/gradle-8.7-bin.zip
+networkTimeout=10000
+validateDistributionUrl=true
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

gradlew

@@ -145,15 +145,15 @@ if ! "$cygwin" && ! "$darwin" && ! "$nonstop" ; then
     case $MAX_FD in #(
       max*)
         # In POSIX sh, ulimit -H is undefined. That's why the result is checked to see if it worked.
-        # shellcheck disable=SC3045
+        # shellcheck disable=SC2039,SC3045
         MAX_FD=$( ulimit -H -n ) ||
             warn "Could not query maximum file descriptor limit"
     esac
     case $MAX_FD in  #(
       '' | soft) :;; #(
       *)
         # In POSIX sh, ulimit -n is undefined. That's why the result is checked to see if it worked.
-        # shellcheck disable=SC3045
+        # shellcheck disable=SC2039,SC3045
         ulimit -n "$MAX_FD" ||
             warn "Could not set maximum file descriptor limit to $MAX_FD"
     esac
@@ -202,11 +202,11 @@ fi
 # Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
 DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"'
 
-# Collect all arguments for the java command;
-#   * $DEFAULT_JVM_OPTS, $JAVA_OPTS, and $GRADLE_OPTS can contain fragments of
-#     shell script including quotes and variable substitutions, so put them in
-#     double quotes to make sure that they get re-expanded; and
-#   * put everything else in single quotes, so that it's not re-expanded.
+# Collect all arguments for the java command:
+#   * DEFAULT_JVM_OPTS, JAVA_OPTS, JAVA_OPTS, and optsEnvironmentVar are not allowed to contain shell fragments,
+#     and any embedded shellness will be escaped.
+#   * For example: A user cannot expect ${Hostname} to be expanded, as it is an environment variable and will be
+#     treated as '${Hostname}' itself on the command line.
 
 set -- \
         "-Dorg.gradle.appname=$APP_BASE_NAME" \

gradlew.bat

@@ -43,11 +43,11 @@ set JAVA_EXE=java.exe
 %JAVA_EXE% -version >NUL 2>&1
 if %ERRORLEVEL% equ 0 goto execute
 
-echo.
-echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
-echo.
-echo Please set the JAVA_HOME variable in your environment to match the
-echo location of your Java installation.
+echo. 1>&2
+echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. 1>&2
+echo. 1>&2
+echo Please set the JAVA_HOME variable in your environment to match the 1>&2
+echo location of your Java installation. 1>&2
 
 goto fail
 
@@ -57,11 +57,11 @@ set JAVA_EXE=%JAVA_HOME%/bin/java.exe
 
 if exist "%JAVA_EXE%" goto execute
 
-echo.
-echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME%
-echo.
-echo Please set the JAVA_HOME variable in your environment to match the
-echo location of your Java installation.
+echo. 1>&2
+echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME% 1>&2
+echo. 1>&2
+echo Please set the JAVA_HOME variable in your environment to match the 1>&2
+echo location of your Java installation. 1>&2
 
 goto fail
 

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

@@ -14,21 +14,21 @@
 import de.uka.ilkd.key.java.reference.MethodReference;
 import de.uka.ilkd.key.java.reference.TypeRef;
 import de.uka.ilkd.key.logic.JavaBlock;
-import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.op.IProgramMethod;
-import de.uka.ilkd.key.logic.op.SchemaVariable;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.NodeInfo;
 import de.uka.ilkd.key.proof_references.ProofReferenceUtil;
 import de.uka.ilkd.key.proof_references.reference.DefaultProofReference;
 import de.uka.ilkd.key.proof_references.reference.IProofReference;
 import de.uka.ilkd.key.rule.PosTacletApp;
-import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.util.MiscTools;
 
 import org.key_project.logic.Name;
+import org.key_project.logic.op.sv.SchemaVariable;
+import org.key_project.prover.rules.RuleApp;
+import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableSLList;
 

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

@@ -62,8 +62,7 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
      */
     protected void listReferences(Node node, ProgramElement pe, ProgramVariable arrayLength,
             LinkedHashSet<IProofReference<?>> toFill, boolean includeExpressionContainer) {
-        if (pe instanceof ProgramVariable) {
-            ProgramVariable pv = (ProgramVariable) pe;
+        if (pe instanceof ProgramVariable pv) {
             if (pv.isMember()) {
                 DefaultProofReference<ProgramVariable> reference =
                     new DefaultProofReference<>(IProofReference.ACCESS, node,

key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/TestKeYTypeUtil.java

@@ -10,7 +10,6 @@
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
 import de.uka.ilkd.key.util.KeYTypeUtil;
 
-import org.junit.jupiter.api.Assertions;
 import org.junit.jupiter.api.Test;
 
 import static org.junit.jupiter.api.Assertions.*;
@@ -54,9 +53,9 @@ public void testIsInnerType() throws Exception {
             // Test class with package
             assertFalse(KeYTypeUtil.isInnerType(services, typeWithPackage));
             // Test inner class without package
-            Assertions.assertTrue(KeYTypeUtil.isInnerType(services, innerTypeWithoutPackage));
+            assertTrue(KeYTypeUtil.isInnerType(services, innerTypeWithoutPackage));
             // Test inner class with package
-            Assertions.assertTrue(KeYTypeUtil.isInnerType(services, innerTypeWithPackage));
+            assertTrue(KeYTypeUtil.isInnerType(services, innerTypeWithPackage));
         } finally {
             environment.dispose();
         }
@@ -87,11 +86,11 @@ public void testGetParentName() throws Exception {
                 KeYTypeUtil.getType(services, "model.InnerAndAnonymousTypeTest.IGetter");
             assertNotNull(innerTypeWithPackage);
             // Test null
-            Assertions.assertNull(KeYTypeUtil.getParentName(services, null));
-            Assertions.assertNull(KeYTypeUtil.getParentName(null, typeWithoutPackage));
-            Assertions.assertNull(KeYTypeUtil.getParentName(null, null));
+            assertNull(KeYTypeUtil.getParentName(services, null));
+            assertNull(KeYTypeUtil.getParentName(null, typeWithoutPackage));
+            assertNull(KeYTypeUtil.getParentName(null, null));
             // Test class without package
-            Assertions.assertNull(KeYTypeUtil.getParentName(services, typeWithoutPackage));
+            assertNull(KeYTypeUtil.getParentName(services, typeWithoutPackage));
             // Test class with package
             assertEquals("model", KeYTypeUtil.getParentName(services, typeWithPackage));
             // Test inner class without package
@@ -127,14 +126,13 @@ public void testIsType() throws Exception {
             assertFalse(KeYTypeUtil.isType(services, "InnerAndAnonymousTypeTest.Invalid"));
             assertFalse(KeYTypeUtil.isType(services, "model.InnerAndAnonymousTypeTest.Invalid"));
             // Test class without package
-            Assertions.assertTrue(KeYTypeUtil.isType(services, "InnerAndAnonymousTypeTest"));
+            assertTrue(KeYTypeUtil.isType(services, "InnerAndAnonymousTypeTest"));
             // Test class with package
-            Assertions.assertTrue(KeYTypeUtil.isType(services, "model.InnerAndAnonymousTypeTest"));
+            assertTrue(KeYTypeUtil.isType(services, "model.InnerAndAnonymousTypeTest"));
             // Test inner class without package
-            Assertions
-                    .assertTrue(KeYTypeUtil.isType(services, "InnerAndAnonymousTypeTest.IGetter"));
+            assertTrue(KeYTypeUtil.isType(services, "InnerAndAnonymousTypeTest.IGetter"));
             // Test inner class with package
-            Assertions.assertTrue(
+            assertTrue(
                 KeYTypeUtil.isType(services, "model.InnerAndAnonymousTypeTest.IGetter"));
         } finally {
             environment.dispose();
@@ -153,16 +151,15 @@ public void testGetType() throws Exception {
             Services services = environment.getServices();
             assertNotNull(services);
             // Test null
-            Assertions.assertNull(KeYTypeUtil.getType(services, null));
-            Assertions.assertNull(KeYTypeUtil.getType(null, "InnerAndAnonymousTypeTest"));
-            Assertions.assertNull(KeYTypeUtil.getType(null, null));
+            assertNull(KeYTypeUtil.getType(services, null));
+            assertNull(KeYTypeUtil.getType(null, "InnerAndAnonymousTypeTest"));
+            assertNull(KeYTypeUtil.getType(null, null));
             // Test invalid names
-            Assertions.assertNull(KeYTypeUtil.getType(services, "Invalid"));
-            Assertions.assertNull(KeYTypeUtil.getType(services, "model.Invalid"));
-            Assertions.assertNull(KeYTypeUtil.getType(services, "invalid.Invalid"));
-            Assertions
-                    .assertNull(KeYTypeUtil.getType(services, "InnerAndAnonymousTypeTest.Invalid"));
-            Assertions.assertNull(
+            assertNull(KeYTypeUtil.getType(services, "Invalid"));
+            assertNull(KeYTypeUtil.getType(services, "model.Invalid"));
+            assertNull(KeYTypeUtil.getType(services, "invalid.Invalid"));
+            assertNull(KeYTypeUtil.getType(services, "InnerAndAnonymousTypeTest.Invalid"));
+            assertNull(
                 KeYTypeUtil.getType(services, "model.InnerAndAnonymousTypeTest.Invalid"));
             // Test class without package
             KeYJavaType kjt = KeYTypeUtil.getType(services, "InnerAndAnonymousTypeTest");

key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/TestProofReferenceUtil.java

@@ -39,7 +39,7 @@ public void testReferenceComputation_ExpandAndContract() throws Exception {
             new ExpectedProofReferences(IProofReference.INLINE_METHOD,
                 "UseOperationContractTest::main"),
             new ExpectedProofReferences(IProofReference.USE_CONTRACT,
-                "pre: {heap=java.lang.Object::<inv>(heap,self)<<impl>>}; mby: null; post: {heap=and(and(equals(result_magic42,Z(2(4(#))))<<origin(ensures @ file UseOperationContractTest.java @ line 12) ([])>>,java.lang.Object::<inv>(heap,self)<<impl>>)<<SC>>,equals(exc<<origin(ensures (implicit)) ([])>>,null)<<impl, origin(ensures (implicit)) ([])>>)}; mods: {heap=allLocs, savedHeap=null}; hasMod: {heap=true, savedHeap=true}; termination: diamond; transaction: false"));
+                "pre: {heap=java.lang.Object::<inv>(heap,self)<<impl>>}; mby: null; post: {heap=and(and(equals(result_magic42,Z(2(4(#))))<<origin(ensures @ file UseOperationContractTest.java @ line 12) ([])>>,java.lang.Object::<inv>(heap,self)<<impl>>)<<SC>>,equals(exc<<origin(ensures (implicit)) ([])>>,null)<<impl, origin(ensures (implicit)) ([])>>)}free post: {heap=true, savedHeap=null}; modifiable: {heap=allLocs, savedHeap=null}; hasModifiable: {heap=true, savedHeap=true}; termination: diamond; transaction: false"));
     }
 
     /**

key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/analyst/TestContractProofReferencesAnalyst.java

@@ -24,6 +24,6 @@ public void testUseOperationContracts() throws Exception {
             "/proofReferences/UseOperationContractTest/UseOperationContractTest.java",
             "UseOperationContractTest", "main", true, new ContractProofReferencesAnalyst(),
             new ExpectedProofReferences(IProofReference.USE_CONTRACT,
-                "pre: {heap=java.lang.Object::<inv>(heap,self)<<impl>>}; mby: null; post: {heap=and(and(equals(result_magic42,Z(2(4(#))))<<origin(ensures @ file UseOperationContractTest.java @ line 12) ([])>>,java.lang.Object::<inv>(heap,self)<<impl>>)<<SC>>,equals(exc<<origin(ensures (implicit)) ([])>>,null)<<impl, origin(ensures (implicit)) ([])>>)}; mods: {heap=allLocs, savedHeap=null}; hasMod: {heap=true, savedHeap=true}; termination: diamond; transaction: false"));
+                "pre: {heap=java.lang.Object::<inv>(heap,self)<<impl>>}; mby: null; post: {heap=and(and(equals(result_magic42,Z(2(4(#))))<<origin(ensures @ file UseOperationContractTest.java @ line 12) ([])>>,java.lang.Object::<inv>(heap,self)<<impl>>)<<SC>>,equals(exc<<origin(ensures (implicit)) ([])>>,null)<<impl, origin(ensures (implicit)) ([])>>)}free post: {heap=true, savedHeap=null}; modifiable: {heap=allLocs, savedHeap=null}; hasModifiable: {heap=true, savedHeap=true}; termination: diamond; transaction: false"));
     }
 }

key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLTransformer.java

@@ -65,7 +65,7 @@ public static void main(String[] args) {
         } else {
             final File riflFilename = new File(args[0]);
             final File javaFilename = new File(args[1]);
-            RIFLTransformer.transform(riflFilename, javaFilename);
+            transform(riflFilename, javaFilename);
         }
     }
 

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/BlockContractValidityTermLabelUpdate.java

@@ -6,18 +6,18 @@
 import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.BlockContractValidityTermLabel;
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.label.TermLabelState;
 import de.uka.ilkd.key.rule.BlockContractInternalRule;
 import de.uka.ilkd.key.rule.LoopContractInternalRule;
-import de.uka.ilkd.key.rule.Rule;
-import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
 import org.key_project.logic.Name;
+import org.key_project.prover.rules.Rule;
+import org.key_project.prover.rules.RuleApp;
+import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.java.CollectionUtil;
@@ -34,7 +34,7 @@ public class BlockContractValidityTermLabelUpdate implements TermLabelUpdate {
      */
     @Override
     public ImmutableList<Name> getSupportedRuleNames() {
-        return ImmutableSLList.<Name>nil().append(BlockContractInternalRule.INSTANCE.name());
+        return ImmutableSLList.singleton(BlockContractInternalRule.INSTANCE.name());
     }
 
     /**

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelMerger.java

@@ -7,11 +7,12 @@
 import java.util.Arrays;
 import java.util.List;
 
-import de.uka.ilkd.key.logic.SequentFormula;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.FormulaTermLabel;
 import de.uka.ilkd.key.logic.label.TermLabel;
 
+import org.key_project.prover.sequent.SequentFormula;
+
 /**
  * The {@link TermLabelMerger} used to merge {@link FormulaTermLabel}s.
  *
@@ -22,7 +23,8 @@ public class FormulaTermLabelMerger implements TermLabelMerger {
      * {@inheritDoc}
      */
     @Override
-    public boolean mergeLabels(SequentFormula existingSF, Term existingTerm,
+    public boolean mergeLabels(SequentFormula existingSF,
+            Term existingTerm,
             TermLabel existingLabel, SequentFormula rejectedSF, Term rejectedTerm,
             TermLabel rejectedLabel, List<TermLabel> mergedLabels) {
         if (existingLabel != null) {