adding missing rule for final static fields

KeYProject · Mar 1, 2025 · fe0954a · fe0954a
1 parent 9bb8e45
commit fe0954a
Showing 1 changed file with 15 additions and 2 deletions.
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key
@@ -3807,11 +3807,10 @@
 }
 
 \rules(programRules:Java, finalFields:onHeap) {
-    // TODO 2 variants with different taclet options
     assignment_read_static_attribute {
         \find(\modality{#allmodal}{.. #v0 = @(#sv); ...}\endmodality (post))
         \sameUpdateLevel
-        \varcond(\hasSort(#sv, G), \not \final(#sv))
+        \varcond(\hasSort(#sv, G))
         \replacewith({#v0 := G::select(heap, null, #memberPVToField(#sv))}\modality{#allmodal}{.. ...}\endmodality (post))
         ;
         (permissions:on) {
@@ -3824,6 +3823,20 @@
 }
 
 \rules(programRules:Java, finalFields:immutable) {
+    assignment_read_static_attribute {
+        \find(\modality{#allmodal}{.. #v0 = @(#sv); ...}\endmodality (post))
+        \sameUpdateLevel
+        \varcond(\hasSort(#sv, G), \not\final(#sv))
+        \replacewith({#v0 := G::select(heap, null, #memberPVToField(#sv))}\modality{#allmodal}{.. ...}\endmodality (post))
+        ;
+        (permissions:on) {
+            "Read Permission to #sv":
+                \replacewith(\modality{#allmodal}{.. assert false : "Access permission check-point (static read)."; ...}\endmodality (post))
+                \add( ==> readPermission(Permission::select(permissions, null, #memberPVToField(#sv))))
+        }
+        \heuristics(simplify_prog, simplify_prog_subset)
+    };
+
     assignment_read_static_attribute_final {
         \find(\modality{#allmodal}{.. #v0 = @(#sv); ...}\endmodality (post))
         \sameUpdateLevel