enabling static final fields

KeYProject · Jan 20, 2025 · 27f1584 · 27f1584
1 parent 3e8fbbd
commit 27f1584
Show file tree

Hide file tree

Showing 3 changed files with 1,483 additions and 6,048 deletions.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java
@@ -1658,7 +1658,7 @@ public Term staticDot(Sort asSort, JFunction f) {
     }
 
     /**
-     * Get a term for a accessing a final field.
+     * Get a term for accessing a final field.
      * This can be used for ordinary fields and model fields.
      * The results are quite different!
      *
@@ -1675,6 +1675,22 @@ public Term finalDot(Sort sort, Term o, JFunction f) {
                 : func(f, getBaseHeap(), o);
     }
 
+    /**
+     * Get a term for accessing a static final field.
+     * This can be used for ordinary fields.
+     *
+     * @param sort the sort of the result.
+     * @param f the field to access
+     * @return the term representing the static access "C.f"
+     * @see #finalDot(Sort, Term, Term) for accessing final Java or ghost fields
+     * @see #dot(Sort, Term, JFunction) for accessing final model fields
+     */
+    public Term staticFinalDot(Sort sort, JFunction f) {
+        final Sort fieldSort = services.getTypeConverter().getHeapLDT().getFieldSort();
+        return f.sort() == fieldSort ? finalDot(sort, NULL(), func(f))
+                : func(f, getBaseHeap(), NULL());
+    }
+
     /**
      * Final fields can be treated differently outside the heap.
      * This methods creates a heap-independent read access to final field.

diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLAttributeResolver.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLAttributeResolver.java
@@ -134,8 +134,15 @@ protected SLExpression doResolving(SLExpression receiver, String name, SLParamet
                         heapLDT.getFieldSymbolForPV((LocationVariable) attribute, services);
                     Term attributeTerm;
                     if (attribute.isStatic()) {
-                        attributeTerm =
-                            services.getTermBuilder().staticDot(attribute.sort(), fieldSymbol);
+                        if (attribute.isFinal() &&
+                                FinalHeapResolution.recallIsFinalEnabled()) {
+                            attributeTerm =
+                                services.getTermBuilder().staticFinalDot(attribute.sort(),
+                                    fieldSymbol);
+                        } else {
+                            attributeTerm =
+                                services.getTermBuilder().staticDot(attribute.sort(), fieldSymbol);
+                        }
                     } else if (attribute.isFinal() &&
                             FinalHeapResolution.recallIsFinalEnabled()) {
                         attributeTerm = services.getTermBuilder().finalDot(attribute.sort(),