Merge remote-tracking branch 'origin/main' into setStatement

# By Drodt (57) and others
# Via GitHub (26) and others
* origin/main: (158 commits)
  ColorSettings: drop old configuration file format
  Merge main into extraxt-new-core
  Bump ch.qos.logback:logback-classic from 1.5.0 to 1.5.3
  fixes #1533
  added checkbox to disable example loader directly in dialog
  address reviewer comments:
  set border + spotless + typo
  JML enabled keys indicator for the status line
  add test case for adt taclets
  Fix position info for equality expr errors
  Revert debugging code
  Spotless
  Add ADT Deconstructors
  Moved TestSMTMod to newsmt2
  spotless applied to TestSMTMod
  Added test for Modulo Translation
  Added translation from KeY mod to SMT mod. Soundness derived from translation of KeY div to SMT div
  preventing NPEs in overloaded operators
  added test cases for operator overloading
  activate the OverloadedOperatorHandler.java for LocSet datatype and repair translation
  ...

# Conflicts:
#	key.core/src/main/java/de/uka/ilkd/key/logic/op/LocationVariable.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java

Author: wadoon

README.md

@@ -14,7 +14,7 @@ For more information, refer to
   * [Verification of `java.util.IdentityHashMap`](https://doi.org/10.1007/978-3-031-07727-2_4),
   * [Google Award for analysing a bug in `LinkedList`](https://www.key-project.org/2023/07/23/cwi-researchers-win-google-award-for-finding-a-bug-in-javas-linkedlist-using-key/)
 
-The current version of KeY is 2.12.0, licensed under GPL v2.
+The current version of KeY is 2.12.2, licensed under GPL v2.
 
 
 Feel free to use the project templates to get started using KeY:
@@ -26,7 +26,7 @@ Feel free to use the project templates to get started using KeY:
 
 * Hardware: >=2 GB RAM
 * Operating System: Linux/Unix, MacOSX, Windows
-* Java SE 11 or newer
+* Java 17 or newer
 * Optionally, KeY can make use of the following binaries:
   * SMT Solvers:
     * [Z3](https://github.com/Z3Prover/z3#z3)
@@ -113,7 +113,7 @@ This is the KeY project - Integrated Deductive Software Design
 Copyright (C) 2001-2011 Universität Karlsruhe, Germany
 						Universität Koblenz-Landau, Germany
 						and Chalmers University of Technology, Sweden
-Copyright (C) 2011-2023 Karlsruhe Institute of Technology, Germany
+Copyright (C) 2011-2024 Karlsruhe Institute of Technology, Germany
 						Technical University Darmstadt, Germany
 						Chalmers University of Technology, Sweden
 

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.23.3"
+    id "com.diffplug.spotless" version "6.25.0"
 }
 
 // Configure this project for use inside IntelliJ:
@@ -70,16 +70,16 @@ subprojects {
     }
 
     dependencies {
-        implementation("org.slf4j:slf4j-api:2.0.10")
+        implementation("org.slf4j:slf4j-api:2.0.12")
 
-        testImplementation("ch.qos.logback:logback-classic:1.4.14")
-        testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.1'
-        testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.1'
+        testImplementation("ch.qos.logback:logback-classic:1.5.3")
+        testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.2'
+        testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.2'
         testImplementation project(':key.util')
 
         testCompileOnly 'junit:junit:4.13.2'
-        testRuntimeOnly 'org.junit.vintage:junit-vintage-engine:5.10.1'
-        testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.1'
+        testRuntimeOnly 'org.junit.vintage:junit-vintage-engine:5.10.2'
+        testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.2'
 
         implementation("org.jspecify:jspecify:0.3.0")
     }

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

@@ -8,9 +8,7 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
-import de.uka.ilkd.key.logic.Name;
 import de.uka.ilkd.key.logic.op.IObserverFunction;
-import de.uka.ilkd.key.logic.sort.Sort;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.init.ProofOblInput;
 import de.uka.ilkd.key.proof_references.reference.DefaultProofReference;
@@ -21,10 +19,12 @@
 import de.uka.ilkd.key.speclang.ClassInvariant;
 import de.uka.ilkd.key.speclang.PartialInvAxiom;
 import de.uka.ilkd.key.util.MiscTools;
-import de.uka.ilkd.key.util.Pair;
 
+import org.key_project.logic.Name;
+import org.key_project.logic.sort.Sort;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableSet;
+import org.key_project.util.collection.Pair;
 
 /**
  * Extracts used {@link ClassAxiom} and {@link ClassInvariant}s.

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

@@ -14,7 +14,6 @@
 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.Name;
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.logic.TermBuilder;
@@ -29,6 +28,7 @@
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.util.MiscTools;
 
+import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableSLList;
 

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

@@ -7,9 +7,9 @@
 import java.util.Map.Entry;
 
 import de.uka.ilkd.key.util.LinkedHashMap;
-import de.uka.ilkd.key.util.Pair;
 
 import org.key_project.util.collection.KeYCollections;
+import org.key_project.util.collection.Pair;
 
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;

key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/package-info.java

@@ -0,0 +1,8 @@
+/**
+ * RIFL is short for "Requirements for Information Flow Language",
+ * a tool-indepentent specification language developed in the RS3 project.
+ * The RIFL/Java dialect is documented in XXX.
+ * This package contains a transformer from input RIFL files (XML) and
+ * original Java files to JML* annotated files.
+ */
+package de.uka.ilkd.key.util.rifl;

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

@@ -6,7 +6,6 @@
 import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.logic.Name;
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.BlockContractValidityTermLabel;
@@ -18,6 +17,7 @@
 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.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.java.CollectionUtil;

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

@@ -18,6 +18,7 @@
 import de.uka.ilkd.key.rule.merge.CloseAfterMerge;
 import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil;
 
+import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.java.CollectionUtil;
 

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

@@ -23,6 +23,7 @@
 import de.uka.ilkd.key.rule.TacletApp;
 import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil;
 
+import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.java.CollectionUtil;
 

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

@@ -6,7 +6,6 @@
 import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.logic.Name;
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.TermLabel;
@@ -16,6 +15,7 @@
 import de.uka.ilkd.key.rule.WhileInvariantRule;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
+import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 

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

@@ -6,7 +6,6 @@
 import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.logic.Name;
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.TermLabel;
@@ -16,6 +15,7 @@
 import de.uka.ilkd.key.rule.WhileInvariantRule;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
+import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 

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

@@ -4,7 +4,6 @@
 package de.uka.ilkd.key.rule.label;
 
 import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.logic.Name;
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.LabelCollection;
@@ -20,6 +19,7 @@
 import de.uka.ilkd.key.rule.UseOperationContractRule;
 import de.uka.ilkd.key.rule.WhileInvariantRule;
 
+import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 

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

@@ -6,14 +6,14 @@
 import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.logic.Name;
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.SymbolicExecutionTermLabel;
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.label.TermLabelState;
 import de.uka.ilkd.key.rule.*;
 
+import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.java.CollectionUtil;

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

@@ -8,10 +8,10 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.ldt.HeapLDT;
+import de.uka.ilkd.key.ldt.JavaDLTheory;
 import de.uka.ilkd.key.logic.*;
 import de.uka.ilkd.key.logic.label.OriginTermLabel;
 import de.uka.ilkd.key.logic.op.*;
-import de.uka.ilkd.key.logic.sort.Sort;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
@@ -25,6 +25,8 @@
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
+import org.key_project.logic.Name;
+import org.key_project.logic.sort.Sort;
 import org.key_project.util.Strings;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
@@ -567,9 +569,9 @@ protected Term createLocationPredicateAndTerm(
             sorts[i] = arguments[i].sort();
         }
         // Create predicate which will be used in formulas to store the value interested in.
-        Function newPredicate =
-            new Function(new Name(getServices().getTermBuilder().newName("LayoutPredicate")),
-                Sort.FORMULA, sorts);
+        JFunction newPredicate =
+            new JFunction(new Name(getServices().getTermBuilder().newName("LayoutPredicate")),
+                JavaDLTheory.FORMULA, sorts);
         // Create formula which contains the value interested in.
         Term newTerm = getServices().getTermBuilder().func(newPredicate, arguments);
         return newTerm;
@@ -788,12 +790,13 @@ public ExtractLocationParameter(Term arrayStartIndex, Term arrayEndIndex, Term p
                 OriginTermLabel.removeOriginLabels(arrayStartIndex, getServices());
             this.arrayEndIndex = OriginTermLabel.removeOriginLabels(arrayEndIndex, getServices());
             TermBuilder tb = getServices().getTermBuilder();
-            Function constantFunction = new Function(
+            JFunction constantFunction = new JFunction(
                 new Name(tb.newName(ExecutionAllArrayIndicesVariable.ARRAY_INDEX_CONSTANT_NAME)),
                 getServices().getTypeConverter().getIntegerLDT().targetSort());
             this.arrayRangeConstant = tb.func(constantFunction);
-            Function notAValueFunction = new Function(
-                new Name(tb.newName(ExecutionAllArrayIndicesVariable.NOT_A_VALUE_NAME)), Sort.ANY);
+            JFunction notAValueFunction = new JFunction(
+                new Name(tb.newName(ExecutionAllArrayIndicesVariable.NOT_A_VALUE_NAME)),
+                JavaDLTheory.ANY);
             this.notAValue = tb.func(notAValueFunction);
         }
 
@@ -939,19 +942,19 @@ public Term createPreValueTerm() {
                 } else {
                     if (getServices().getJavaInfo().getArrayLength() == programVariable) {
                         // Special handling for length attribute of arrays
-                        Function function =
+                        JFunction function =
                             getServices().getTypeConverter().getHeapLDT().getLength();
                         return tb.func(function, createPreParentTerm());
                     } else {
-                        Function function =
+                        JFunction function =
                             getServices().getTypeConverter().getHeapLDT().getFieldSymbolForPV(
                                 (LocationVariable) programVariable, getServices());
                         return tb.dot(programVariable.sort(), createPreParentTerm(), function);
                     }
                 }
             } else {
                 if (programVariable.isStatic()) {
-                    Function function = getServices().getTypeConverter().getHeapLDT()
+                    JFunction function = getServices().getTypeConverter().getHeapLDT()
                             .getFieldSymbolForPV((LocationVariable) programVariable, getServices());
                     return tb.staticDot(programVariable.sort(), function);
                 } else {

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractUpdateExtractor.java

@@ -20,7 +20,6 @@
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.IProgramMethod;
 import de.uka.ilkd.key.logic.op.IProgramVariable;
-import de.uka.ilkd.key.logic.sort.Sort;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.NodeInfo;
 import de.uka.ilkd.key.proof.Proof;
@@ -34,10 +33,11 @@
 import de.uka.ilkd.key.symbolic_execution.model.IExecutionTermination.TerminationKind;
 import de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicEquivalenceClass;
 import de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicLayout;
-import de.uka.ilkd.key.util.Pair;
 
+import org.key_project.logic.sort.Sort;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
+import org.key_project.util.collection.Pair;
 import org.key_project.util.java.CollectionUtil;
 
 import org.xml.sax.Attributes;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeReader.java

@@ -19,10 +19,10 @@
 import de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionValue;
 import de.uka.ilkd.key.symbolic_execution.model.impl.AbstractExecutionVariable;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
-import de.uka.ilkd.key.util.Pair;
 
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
+import org.key_project.util.collection.Pair;
 
 /**
  * Extracts the current state and represents it as {@link IExecutionVariable}s.

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionVariableExtractor.java

@@ -36,10 +36,10 @@
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 import de.uka.ilkd.key.util.MiscTools;
 import de.uka.ilkd.key.util.NodePreorderIterator;
-import de.uka.ilkd.key.util.Pair;
 
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
+import org.key_project.util.collection.Pair;
 import org.key_project.util.java.ArrayUtil;
 
 /**

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicExecutionTreeBuilder.java

@@ -25,6 +25,7 @@
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 import de.uka.ilkd.key.util.ProofStarter;
 
+import org.key_project.logic.Name;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/SymbolicLayoutExtractor.java

@@ -18,7 +18,6 @@
 
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.op.IProgramVariable;
-import de.uka.ilkd.key.logic.sort.Sort;
 import de.uka.ilkd.key.symbolic_execution.object_model.IModelSettings;
 import de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicAssociation;
 import de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicAssociationValueContainer;
@@ -29,6 +28,7 @@
 import de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicState;
 import de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicValue;
 
+import org.key_project.logic.sort.Sort;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;