adding two rules for final fields.

a final field reference in a created object points to null or to a created object.
KeYProject · Dec 20, 2024 · dad8aca · dad8aca
1 parent f88dd46
commit dad8aca
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 1 deletion.
diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSetsRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSetsRules.key
@@ -1329,6 +1329,37 @@
         \heuristics(concrete)
     };
 
+    referencedObjectIsCreatedRightFinal {
+        \schemaVar \term Heap h;
+        \schemaVar \term Object o;
+        \schemaVar \term Field f;
+
+        \assumes( ==> deltaObject::final(o, f) = null)
+        \find( ==> boolean::select(h,
+                deltaObject::final(o, f),
+                java.lang.Object::<created>) = TRUE )
+
+        \replacewith( ==> boolean::select(h, o, java.lang.Object::<created>) = TRUE )
+
+        \heuristics(concrete)
+    };
+
+    referencedObjectIsCreatedRighFinalEQ {
+        \schemaVar \term Heap h;
+        \schemaVar \term Object o;
+        \schemaVar \term Field f;
+        \schemaVar \term Object EQ;
+
+        \assumes(deltaObject::final(o, f) = EQ ==> EQ = null)
+        \find( ==> boolean::select(h,
+                EQ,
+                java.lang.Object::<created>) = TRUE)
+
+        \replacewith( ==> boolean::select(h, o, java.lang.Object::<created>) = TRUE )
+
+        \heuristics(concrete)
+    };
+
     // --------------------------------------------------------------------------
     // some other lemmata
     // --------------------------------------------------------------------------

diff --git a/key.core/src/test/resources/de/uka/ilkd/key/proof/runallproofs/automaticJAVADL.properties b/key.core/src/test/resources/de/uka/ilkd/key/proof/runallproofs/automaticJAVADL.properties
@@ -33,5 +33,5 @@
 [SMTSettings]instantiateHierarchyAssumptions=true
 [SMTSettings]useUninterpretedMultiplication=true
 [SMTSettings]SelectedTaclets=
-[Choice]DefaultChoices=assertions-assertions:on , intRules-intRules:arithmeticSemanticsIgnoringOF , initialisation-initialisation:disableStaticInitialisation , programRules-programRules:Java , runtimeExceptions-runtimeExceptions:ban , JavaCard-JavaCard:on , Strings-Strings:on , modelFields-modelFields:showSatisfiability , bigint-bigint:on , sequences-sequences:on , reach-reach:on , integerSimplificationRules-integerSimplificationRules:full , wdOperator-wdOperator:L , wdChecks-wdChecks:off , permissions-permissions:off , moreSeqRules-moreSeqRules:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal:off , javaLoopTreatment-javaLoopTreatment:efficient
+[Choice]DefaultChoices=assertions-assertions:on , intRules-intRules:arithmeticSemanticsIgnoringOF , initialisation-initialisation:disableStaticInitialisation , programRules-programRules:Java , runtimeExceptions-runtimeExceptions:ban , JavaCard-JavaCard:on , Strings-Strings:on , modelFields-modelFields:showSatisfiability , bigint-bigint:on , sequences-sequences:on , reach-reach:on , integerSimplificationRules-integerSimplificationRules:full , wdOperator-wdOperator:L , wdChecks-wdChecks:off , permissions-permissions:off , moreSeqRules-moreSeqRules:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal:off , javaLoopTreatment-javaLoopTreatment:efficient , finalFields-finalFields:immutable 
 [Strategy]ActiveStrategy=JavaCardDLStrategy