Merge branch 'main' into weigl/recordsftw

# Conflicts:
#	keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java

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

@@ -70,16 +70,16 @@ subprojects {
     }
 
     dependencies {
-        implementation("org.slf4j:slf4j-api:2.0.11")
+        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.0")
+        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/src/main/java/de/uka/ilkd/key/java/Comment.java

@@ -5,6 +5,9 @@
 
 import de.uka.ilkd.key.java.visitor.Visitor;
 
+/**
+ * Comment element of Java source code.
+ */
 public class Comment extends JavaSourceElement {
 
     private final String text;

key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java

@@ -22,12 +22,35 @@
 public class MethodDeclaration extends JavaDeclaration implements MemberDeclaration,
         TypeReferenceContainer, NamedProgramElement, ParameterContainer, Method, VariableScope {
 
+    /**
+     * The return type of the method.
+     */
     protected final TypeReference returnType;
+    /**
+     * In case of void return type: comments associated with the method.
+     */
     protected final Comment[] voidComments;
+    /**
+     * The name of the method.
+     */
     protected final ProgramElementName name;
+    /**
+     * Parameters of the method.
+     */
     protected final ImmutableArray<ParameterDeclaration> parameters;
+    /**
+     * 'throws' part of the method. Indicates which exceptions the method may throw.
+     * May be null.
+     */
     protected final Throws exceptions;
+    /**
+     * Body of the method.
+     * May be null, in which case the body is referenced in a file using {@link #posInfo}.
+     */
     protected final StatementBlock body;
+    /**
+     * JML modifiers of the referenced method. Includes e.g. {@code pure}.
+     */
     protected final JMLModifiers jmlModifiers;
 
     /**
@@ -53,12 +76,14 @@ public record JMLModifiers(boolean pure, boolean strictlyPure, boolean helper,
     /**
      * Method declaration.
      *
-     * @param children an ExtList of children. May include: a TypeReference (as a reference to the
-     *        return type), a de.uka.ilkd.key.logic.ProgramElementName (as Name of the method),
-     *        several ParameterDeclaration (as parameters of the declared method), a StatementBlock
-     *        (as body of the declared method), several Modifier (taken as modifiers of the
-     *        declaration), a Comment
+     * @param children an ExtList of children. Must include: a TypeReference (as a reference to the
+     *        return type),
+     *        a {@link ProgramElementName} (as Name of the method),
+     *        one or more {@link ParameterDeclaration} (as parameters of the declared method),
+     *        optionally a {@link StatementBlock} (as body of the declared method),
+     *        optionally a {@link Throws} to indicate exceptional behaviour
      * @param parentIsInterfaceDeclaration a boolean set true iff parent is an InterfaceDeclaration
+     * @param voidComments in case of void return type: comments associated with the method
      */
     public MethodDeclaration(ExtList children, boolean parentIsInterfaceDeclaration,
             Comment[] voidComments) {
@@ -266,6 +291,12 @@ public TypeReference getTypeReference() {
     }
 
 
+    /**
+     * Get the "void comments" of this method declaration.
+     * Only non-null if the method has void return type.
+     *
+     * @return the "void comments"
+     */
     public Comment[] getVoidComments() {
         return voidComments;
     }

key.core/src/main/java/de/uka/ilkd/key/java/declaration/Throws.java

@@ -23,7 +23,7 @@ public class Throws extends JavaNonTerminalProgramElement implements TypeReferen
 
 
     /**
-     * Exceptions.
+     * Exceptions thrown.
      */
     protected final ImmutableArray<TypeReference> exceptions;
 

key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java

@@ -3,6 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.logic;
 
+import java.util.Collection;
 import java.util.Iterator;
 
 import org.key_project.util.collection.ImmutableList;
@@ -27,11 +28,10 @@ private Semisequent() {
         seqList = ImmutableSLList.nil();
     }
 
-
     /**
-     * creates a new Semisequent with the Semisequent elements in seqList; the provided list must be
-     * redundancy free, i.e., the created sequent must be exactly the same as when creating the
-     * sequent by subsequently inserting all formulas
+     * Create a new Semisequent from an ordered collection of formulas.
+     * The provided list must be redundancy free, i.e., the created sequent must be exactly
+     * the same as when creating the sequent by subsequently inserting all formulas
      *
      * @param seqList list of sequent formulas
      */
@@ -40,6 +40,33 @@ public Semisequent(ImmutableList<SequentFormula> seqList) {
         this.seqList = seqList;
     }
 
+    /**
+     * Create a new Semisequent from an ordered collection of formulas.
+     * The provided collection must be redundancy free, i.e., the created sequent must be exactly
+     * the same as when creating the sequent by subsequently inserting all formulas
+     *
+     * @param seqList list of sequent formulas
+     */
+    public Semisequent(Collection<SequentFormula> seqList) {
+        assert !seqList.isEmpty();
+        this.seqList = ImmutableList.fromList(seqList);
+    }
+
+    /**
+     * Create a new Semisequent from an ordered collection of formulas (possibly empty).
+     * The provided collection must be redundancy free, i.e., the created sequent must be exactly
+     * the same as when creating the
+     * sequent by subsequently inserting all formulas.
+     *
+     * @param seqList list of sequent formulas
+     */
+    public static Semisequent create(Collection<SequentFormula> seqList) {
+        if (seqList.isEmpty()) {
+            return EMPTY_SEMISEQUENT;
+        }
+        return new Semisequent(seqList);
+    }
+
 
     /**
      * creates a new Semisequent with the Semisequent elements in seqList

key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java

@@ -22,24 +22,31 @@
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
+import org.key_project.util.collection.ImmutableSet;
 
-import org.slf4j.Logger;
-import org.slf4j.LoggerFactory;
 
 /**
  * The program method represents a (pure) method in the logic. In case of a non-static method the
  * first argument represents the object on which the method is invoked.
+ * <p>
+ * This data is used in
+ * {@link de.uka.ilkd.key.speclang.QueryAxiom#getTaclets(ImmutableSet, Services)}.
  */
 public final class ProgramMethod extends ObserverFunction
         implements ProgramInLogic, IProgramMethod {
 
-    private static final Logger LOGGER = LoggerFactory.getLogger(ProgramMethod.class);
 
+    /**
+     * The referenced method.
+     */
     private final MethodDeclaration method;
     /**
      * Return type of the method. Must not be null. Use KeYJavaType.VOID_TYPE for void methods.
      */
     private final KeYJavaType returnType;
+    /**
+     * Where the method is located in a .java file.
+     */
     private final PositionInfo pi;
 
     // -------------------------------------------------------------------------
@@ -63,6 +70,12 @@ public ProgramMethod(MethodDeclaration method, KeYJavaType container, KeYJavaTyp
     // internal methods
     // -------------------------------------------------------------------------
 
+    /**
+     * Get the java types of the parameters required by the method md.
+     *
+     * @param md some method declaration
+     * @return java types of the parameters required by md
+     */
     private static ImmutableArray<KeYJavaType> getParamTypes(MethodDeclaration md) {
         KeYJavaType[] result = new KeYJavaType[md.getParameterDeclarationCount()];
         for (int i = 0; i < result.length; i++) {
@@ -80,11 +93,6 @@ private static ImmutableArray<KeYJavaType> getParamTypes(MethodDeclaration md) {
     // MethodDeclaration
     // in a direct way
 
-    /*
-     * (non-Javadoc)
-     *
-     * @see de.uka.ilkd.key.logic.op.IProgramMethod#getMethodDeclaration()
-     */
     @Override
     public MethodDeclaration getMethodDeclaration() {
         return method;

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java

@@ -66,7 +66,7 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) {
                 : null;
         var origin = BuilderHelpers.getPosition(ctx);
         var s = new SortImpl(new Name(name), ImmutableSet.empty(), false, doc, origin);
-        sorts().add(s);
+        sorts().addSafely(s);
         return null;
     }
 

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java

@@ -7,6 +7,7 @@
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Name;
+import de.uka.ilkd.key.logic.Namespace;
 import de.uka.ilkd.key.logic.NamespaceSet;
 import de.uka.ilkd.key.logic.op.Function;
 import de.uka.ilkd.key.logic.op.SortDependingFunction;
@@ -52,16 +53,30 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) {
         // weigl: all datatypes are free ==> functions are unique!
         // boolean freeAdt = ctx.FREE() != null;
         var sort = sorts().lookup(ctx.name.getText());
+        var dtNamespace = new Namespace<Function>();
         for (KeYParser.Datatype_constructorContext constructorContext : ctx
                 .datatype_constructor()) {
             Name name = new Name(constructorContext.name.getText());
             Sort[] args = new Sort[constructorContext.sortId().size()];
+            var argNames = constructorContext.argName;
             for (int i = 0; i < args.length; i++) {
-                args[i] = accept(constructorContext.sortId(i));
+                Sort argSort = accept(constructorContext.sortId(i));
+                args[i] = argSort;
+                var argName = argNames.get(i).getText();
+                var alreadyDefinedFn = dtNamespace.lookup(argName);
+                if (alreadyDefinedFn != null
+                        && (!alreadyDefinedFn.sort().equals(argSort)
+                                || !alreadyDefinedFn.argSort(0).equals(sort))) {
+                    throw new RuntimeException("Name already in namespace: " + argName);
+                }
+                Function fn = new Function(new Name(argName), argSort, new Sort[] { sort }, null,
+                    false, false);
+                dtNamespace.add(fn);
             }
             Function function = new Function(name, sort, args, null, true, false);
-            namespaces().functions().add(function);
+            namespaces().functions().addSafely(function);
         }
+        namespaces().functions().addSafely(dtNamespace.allElements());
         return null;
     }