repairing the check of inner class constructor calls and updating test cases

Author: mattulbrich

key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidator.java

@@ -11,6 +11,7 @@
 import de.uka.ilkd.key.java.abstraction.ClassType;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
 import de.uka.ilkd.key.java.abstraction.Type;
+import de.uka.ilkd.key.java.declaration.ClassDeclaration;
 import de.uka.ilkd.key.java.expression.Assignment;
 import de.uka.ilkd.key.java.expression.operator.New;
 import de.uka.ilkd.key.java.reference.*;
@@ -171,7 +172,7 @@ private void validateNew(New _new) {
 
         TypeReference typeRef = _new.getTypeReference();
         Type type = typeRef.getKeYJavaType().getJavaType();
-        if (type instanceof ClassType classType && !classType.isStatic()) {
+        if (type instanceof ClassDeclaration classType && classType.isInnerClass() && !classType.isStatic()) {
             // This also disallows things like "a.new B()" which would not like this. However,
             // KeY cannot deal with this anyway, so we can do the easy check here.
             throw new FinalViolationException(

key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsTestUnit.java

@@ -121,6 +121,7 @@ public TestResult runTest(JunitXmlWriter xml) throws Exception {
 
         boolean success = true;
         StringBuilder message = new StringBuilder("group " + testName + ":\n");
+        StringBuilder summary = new StringBuilder("Summary of test results:\n");
         for (int i = 0; i < testResults.size(); i++) {
             var start = System.currentTimeMillis();
             TestFile file = testFiles.get(i);
@@ -133,7 +134,12 @@ public TestResult runTest(JunitXmlWriter xml) throws Exception {
                 !testResult.success() ? "error" : "", testResult.message(), "", time / 1000.0);
             success &= testResult.success();
             message.append(testResult.message()).append("\n");
+            summary.append(String.format("  %s (%s): %s%n",
+                            file.getKeYFile().getName(),
+                            file.getTestProperty(),
+                            testResult.success() ? "success" : "FAILURE"));
         }
+        message.insert(0, summary);
         return new TestResult(message.toString(), success);
     }
 

key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt

@@ -1,5 +1,5 @@
 # This files contains representation of taclets, which are accepted and revised.
-# Date: Fri Dec 13 23:01:56 CET 2024
+# Date: Mon Mar 03 18:42:58 CET 2025
 
 == abortJavaCardTransactionAPI (abortJavaCardTransactionAPI) =========================================
 abortJavaCardTransactionAPI {
@@ -1906,7 +1906,7 @@ assignment_read_static_attribute {
 \sameUpdateLevel\varcond(\hasSort(#sv (program StaticVariable), G),  \not \final(#sv (program StaticVariable)))
 \replacewith(update-application(elem-update(#v0 (program Variable))(G::select(heap,null,#memberPVToField(#sv))),#allmodal(post))) 
 \heuristics(simplify_prog_subset, simplify_prog)
-Choices: programRules:Java}
+Choices: (programRules:Java & finalFields:immutable)}
 -----------------------------------------------------
 == assignment_read_static_attribute_final (assignment_read_static_attribute_final) =========================================
 assignment_read_static_attribute_final {
@@ -1916,7 +1916,7 @@ assignment_read_static_attribute_final {
 \sameUpdateLevel\varcond(\hasSort(#sv (program StaticVariable), G), \final(#sv (program StaticVariable)))
 \replacewith(update-application(elem-update(#v0 (program Variable))(G::final(null,#memberPVToField(#sv))),#allmodal(post))) 
 \heuristics(simplify_prog_subset, simplify_prog)
-Choices: programRules:Java}
+Choices: (programRules:Java & finalFields:immutable)}
 -----------------------------------------------------
 == assignment_read_static_attribute_with_variable_prefix (assignment) =========================================
 assignment_read_static_attribute_with_variable_prefix {
@@ -7278,6 +7278,13 @@ equal_literals {
 \heuristics(simplify_literals)
 Choices: true}
 -----------------------------------------------------
+== equalityOfSingleton (equalityOfSingleton) =========================================
+equalityOfSingleton {
+\find(equals(singleton(o1,f1),singleton(o2,f2)))
+\replacewith(and(equals(o1,o2),equals(f1,f2))) 
+\heuristics(simplify)
+Choices: programRules:Java}
+-----------------------------------------------------
 == equalityToElementOf (equalityToElementOf) =========================================
 equalityToElementOf {
 \find(equals(s,s2))
@@ -15150,6 +15157,14 @@ reference_type_cast {
 \heuristics(simplify_prog)
 Choices: (programRules:Java & runtimeExceptions:ban)}
 -----------------------------------------------------
+== referencedObjectIsCreatedRighFinalEQ (referencedObjectIsCreatedRighFinalEQ) =========================================
+referencedObjectIsCreatedRighFinalEQ {
+\assumes ([equals(deltaObject::final(o,f),EQ)]==>[equals(EQ,null)]) 
+\find(==>equals(boolean::select(h,EQ,java.lang.Object::<created>),TRUE))
+\add []==>[or(equals(boolean::select(h,o,java.lang.Object::<created>),TRUE),equals(o,null))] 
+\heuristics(concrete)
+Choices: programRules:Java}
+-----------------------------------------------------
 == referencedObjectIsCreatedRight (referencedObjectIsCreatedRight) =========================================
 referencedObjectIsCreatedRight {
 \assumes ([]==>[equals(deltaObject::select(h,o,f),null)]) 
@@ -15166,6 +15181,14 @@ referencedObjectIsCreatedRightEQ {
 \heuristics(concrete)
 Choices: programRules:Java}
 -----------------------------------------------------
+== referencedObjectIsCreatedRightFinal (referencedObjectIsCreatedRightFinal) =========================================
+referencedObjectIsCreatedRightFinal {
+\assumes ([]==>[equals(deltaObject::final(o,f),null)]) 
+\find(==>equals(boolean::select(h,deltaObject::final(o,f),java.lang.Object::<created>),TRUE))
+\replacewith([]==>[or(equals(boolean::select(h,o,java.lang.Object::<created>),TRUE),equals(o,null))]) 
+\heuristics(simplify_enlarging)
+Choices: programRules:Java}
+-----------------------------------------------------
 == regExAxiom (regExAxiom) =========================================
 regExAxiom {
 \find(match(regEx(stringAsPattern),string))