Anonymize ghost variables in loop

key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java

@@ -1652,7 +1652,7 @@ public JTerm term(int index) {
          * @param index the index of the term in {@code terms()}
          * @return a term updated with {@code self} and the {@code vars()}.
          */
-        public JTerm getTerm(Services services, JTerm self, int index) {
+        public JTerm getTerm(Services services, @Nullable JTerm self, int index) {
             var term = term(index);
 
             final TermFactory termFactory = services.getTermFactory();

key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java

@@ -26,6 +26,7 @@
 import de.uka.ilkd.key.java.reference.TypeReference;
 import de.uka.ilkd.key.java.statement.LoopStatement;
 import de.uka.ilkd.key.java.statement.MethodFrame;
+import de.uka.ilkd.key.java.statement.SetStatement;
 import de.uka.ilkd.key.java.visitor.JavaASTVisitor;
 import de.uka.ilkd.key.ldt.HeapLDT;
 import de.uka.ilkd.key.logic.*;
@@ -626,6 +627,14 @@ protected void doDefaultAction(SourceElement node) {
                     assert !writtenPVs.contains(pv);
                     declaredPVs = declaredPVs.add(pv);
                 }
+            } else if (node instanceof SetStatement s) {
+                var spec = services.getSpecificationRepository().getStatementSpec(s);
+                if (spec != null) {
+                    var targetTerm = spec.getTerm(services, null, SetStatement.INDEX_TARGET);
+                    if (targetTerm.op() instanceof LocationVariable lv) {
+                        writtenPVs = writtenPVs.add(lv);
+                    }
+                }
             }
         }
 

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

@@ -405,6 +405,7 @@ public static ProofCollection automaticJavaDL() throws IOException {
         g.provable("standard_key/unicode_test.key");
         g.provable("heap/strictlyModular/mayExpand.key");
         g.notprovable("heap/strictlyModular/modularOnly.key");
+        g.notprovable("standard_key/GhostSetInLoop/set_ghost.key");
 
 
         g = c.group("SmansEtAl");

key.ui/examples/standard_key/GhostSetInLoop/SetGhost.java

@@ -0,0 +1,31 @@
+import java.util.List;
+
+public class SetGhost {
+    /*@ public normal_behavior
+      @ requires \invariant_for(l);
+      @ ensures \result == l.seq.length;
+      @*/
+    static int counter(List l) {
+        int listSize = l.size();
+        int counter = 0;
+        //@ ghost int iter;
+        //@ set iter = 0;
+
+        /*@ loop_invariant
+          @ i >= 0 && i <= listSize && listSize == l.size()
+          @  && i == counter
+          @  && iter == counter
+          @ ;
+          @ decreases listSize - i;
+          @ assignable counter,iter;
+          @*/
+        for (int i = 0; i < listSize; i++) {
+            counter++;
+            //@ set iter = iter + 1;
+            //@ assert iter == 1;
+            assert counter == 1;
+        }
+        //@ assert iter == counter;
+        return counter;
+    }
+}

key.ui/examples/standard_key/GhostSetInLoop/set_ghost.key

@@ -0,0 +1,86 @@
+\profile "Java Profile";
+
+\settings // Proof-Settings-Config-File
+{ 
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:safe",
+        "bigint" : "bigint:on",
+        "finalFields" : "finalFields:immutable",
+        "floatRules" : "floatRules:strictfpOnly",
+        "initialisation" : "initialisation:disableStaticInitialisation",
+        "intRules" : "intRules:arithmeticSemanticsIgnoringOF",
+        "integerSimplificationRules" : "integerSimplificationRules:full",
+        "javaLoopTreatment" : "javaLoopTreatment:efficient",
+        "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
+        "methodExpansion" : "methodExpansion:modularOnly",
+        "modelFields" : "modelFields:treatAsAxiom",
+        "moreSeqRules" : "moreSeqRules:off",
+        "permissions" : "permissions:off",
+        "programRules" : "programRules:Java",
+        "reach" : "reach:on",
+        "runtimeExceptions" : "runtimeExceptions:ban",
+        "sequences" : "sequences:on",
+        "soundDefaultContracts" : "soundDefaultContracts:on",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+     },
+    "Labels" : { 
+        "UseOriginLabels" : true
+     },
+    "NewSMT" : { 
+
+     },
+    "SMTSettings" : { 
+        "SelectedTaclets" : [ 
+
+         ],
+        "UseBuiltUniqueness" : false,
+        "explicitTypeHierarchy" : false,
+        "instantiateHierarchyAssumptions" : true,
+        "integersMaximum" : 2147483645,
+        "integersMinimum" : -2147483645,
+        "invariantForall" : false,
+        "maxGenericSorts" : 2,
+        "useConstantsForBigOrSmallIntegers" : true,
+        "useUninterpretedMultiplication" : true
+     },
+    "Strategy" : { 
+        "ActiveStrategy" : "JavaCardDLStrategy",
+        "MaximumNumberOfAutomaticApplications" : 10000,
+        "Timeout" : -1,
+        "options" : { 
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
+            "DEP_OPTIONS_KEY" : "DEP_ON",
+            "INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
+            "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET",
+            "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT",
+            "MPS_OPTIONS_KEY" : "MPS_MERGE",
+            "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_NONE",
+            "OSS_OPTIONS_KEY" : "OSS_ON",
+            "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
+            "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
+            "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
+            "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
+            "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
+            "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
+            "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
+            "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
+            "VBT_PHASE" : "VBT_SYM_EX"
+         }
+     }
+ } 
+
+
+\javaSource ".";\proofObligation 
+// 
+{ 
+    "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
+    "contract" : "SetGhost[SetGhost::counter(java.util.List)].JML normal_behavior operation contract.0",
+    "name" : "SetGhost[SetGhost::counter(java.util.List)].JML normal_behavior operation contract.0"
+ }