Fix handling of \values keyword

key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java

@@ -151,21 +151,18 @@ public final SortDependingFunction getExactInstanceofSymbol(Sort sort, TermServi
     @Override
     public boolean isResponsible(Operator op, JTerm[] subs, Services services,
             ExecutionContext ec) {
-        assert false;
         return false;
     }
 
     @Override
     public boolean isResponsible(Operator op, JTerm left, JTerm right, Services services,
             ExecutionContext ec) {
-        assert false;
         return false;
     }
 
     @Override
     public boolean isResponsible(Operator op, JTerm sub, TermServices services,
             ExecutionContext ec) {
-        assert false;
         return false;
     }
 

key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java

@@ -553,7 +553,7 @@ public static LoopContractImpl.ReplaceTypes fromClass(Class<?> cls) {
                 }
             }
 
-            throw new AssertionError();
+            return null;
         }
     }
 
@@ -589,18 +589,51 @@ private static void replaceVariable(ProgramVariable var, EmptySeqLiteral init,
             services.getTypeConverter().getSeqLDT().translateLiteral(init, services));
     }
 
+    private static void replaceVariableDefault(ProgramVariable var, Expression init,
+                                        Map<JTerm, JTerm> preReplacementMap, Map<JTerm, JTerm> postReplacementMap,
+                                        LoopContractImpl r, Services services) {
+        // Do nothing.
+        // A variable whose initializer isn't another variable nor a literal cannot be replaced by that initializer in
+        // a logical expression.
+        // In realistic programs, this mainly occurs with variables like {@code \index} and {@code \values}.
+        // Since these aren't allowed to occur in a precondition or {@code \old} expression anyway, we don't need to
+        // do anything with them.
+    }
+
+    /**
+     * Helper function for {@link #toBlockContract()} to replaces variables defined in a for-loop's head statement
+     * by their initializer expressions where necessary, i.e., in the block contract's precondition and in the
+     * postcondition if part of an {@code \old} expression.
+     *
+     * @param var the variable to replace
+     * @param init the variable's initializer
+     * @param preReplacementMap a map mapping variables to their replacements for the block contract's precondition
+     * @param postReplacementMap a map mapping {@code \old} variable to their replacements for the block contract's
+     *                           postcondirion
+     * @param r the loop contract that is being converted to a block contract (see {@link #toBlockContract()})
+     * @param services services
+     */
     private static void replaceVariable(ProgramVariable var, Expression init,
             Map<JTerm, JTerm> preReplacementMap, Map<JTerm, JTerm> postReplacementMap,
             LoopContractImpl r, Services services) {
-        switch (ReplaceTypes.fromClass(init.getClass())) {
+        ReplaceTypes replaceTypes = ReplaceTypes.fromClass(init.getClass());
+
+        if (replaceTypes == null) {
+            // A variable whose initializer isn't another variable nor a literal cannot be replaced
+            // and isn't allowed to occur in a precondition or {@code \old} expression.
+            // We simply leave it as is here, which will cause an error later during name resolution.
+            return;
+        }
+
+        switch (replaceTypes) {
             case PROGRAM_VARIABLE -> replaceVariable(var, (ProgramVariable) init, preReplacementMap,
                 postReplacementMap, r, services);
             case ABSTRACT_INTEGER_LITERAL -> replaceVariable(var, (AbstractIntegerLiteral) init,
                 preReplacementMap, postReplacementMap, r, services);
             case EMPTY_SEQ_LITERAL ->
                 replaceVariable(var, (EmptySeqLiteral) init, preReplacementMap,
                     postReplacementMap, r, services);
-            default -> throw new AssertionError();
+            default -> replaceVariableDefault(var, init, preReplacementMap, postReplacementMap, r, services);
         }
     }
 

key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java

@@ -838,8 +838,9 @@ public SLExpression index() {
         return new SLExpression(tb.index(), t);
     }
 
-    public SLExpression values(KeYJavaType t) {
-        return new SLExpression(tb.values(), t);
+    public SLExpression values() {
+        return new SLExpression(tb.values(), services.getJavaInfo()
+                .getKeYJavaType(services.getTypeConverter().getSeqLDT().targetSort()));
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java

@@ -1496,7 +1496,7 @@ public Object visitPrimaryIndex(JmlParser.PrimaryIndexContext ctx) {
 
     @Override
     public Object visitPrimaryValues(JmlParser.PrimaryValuesContext ctx) {
-        return termFactory.values(this.containerType);
+        return termFactory.values();
     }
 
     @Override

key.ui/examples/heap/block_loop_contracts/ListsWithIterators/src/IntIterator.java

@@ -1,6 +1,6 @@
 import java.util.Iterator;
 
-public class IntIterator implements Iterator {
+public final class IntIterator implements Iterator {
 
     private final IntLinkedList list;
     private /*@nullable@*/ IntNode next;

key.ui/examples/heap/block_loop_contracts/ListsWithIterators/src/IntLinkedList.java

@@ -10,9 +10,9 @@ public final class IntLinkedList implements IntList {
       @ invariant footprint == \set_union(this.*,
       @      \infinite_union(int i; 0<=i && i<size; ((IntNode)nodeseq[i]).*));
       @
-      @ invariant (\forall int i; 0<=i && i<size; 
+      @ invariant (\forall int i; 0<=i && i<size;
       @         ((IntNode)nodeseq[i]) != null  // this implies \typeof(nodeseq[i]) == \type(IntNode)
-      @      && ((IntNode)nodeseq[i]).data == (int)seq[i] 
+      @      && ((IntNode)nodeseq[i]).data == (int)seq[i]
       @      && (\forall int j; 0<=j && j<size; (IntNode)nodeseq[i] == (IntNode)nodeseq[j] ==> i == j)
       @      && ((IntNode)nodeseq[i]).next == (i==size-1 ? null : (IntNode)nodeseq[i+1]));
       @
@@ -32,7 +32,7 @@ public IntIterator iterator() {
       @*/
     public int sum_loopContract() {
         int result = 0;
-        
+
         /*@ loop_contract normal_behavior
           @ requires \invariant_for(this);
           @ ensures \invariant_for(this);
@@ -55,8 +55,10 @@ public int sum_loopContract() {
       @*/
     public int sum_loopInvariant() {
         int result = 0;
-
-        /*@ loop_invariant true;
+
+        /*@ loop_invariant result == (\sum int i; 0 <= i && i < \values.length; (int)seq[i]);
+          @ loop_invariant \values.length <= seq.length;
+          @ loop_invariant \values == seq[0 .. (\values.length - 1)];
           @ decreases seq.length - \values.length;
           @ assignable \nothing;
           @*/