diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java index 404a945b60..cc18318108 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java +++ b/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; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java index 1760227c2a..37d492e47c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java +++ b/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,10 +589,43 @@ private static void replaceVariable(ProgramVariable var, EmptySeqLiteral init, services.getTypeConverter().getSeqLDT().translateLiteral(init, services)); } + private static void replaceVariableDefault(ProgramVariable var, Expression init, + Map preReplacementMap, Map 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 preReplacementMap, Map 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, @@ -600,7 +633,7 @@ private static void replaceVariable(ProgramVariable var, Expression init, case EMPTY_SEQ_LITERAL -> replaceVariable(var, (EmptySeqLiteral) init, preReplacementMap, postReplacementMap, r, services); - default -> throw new AssertionError(); + default -> replaceVariableDefault(var, init, preReplacementMap, postReplacementMap, r, services); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java index 44c1ad4eca..4c2c67bf68 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java +++ b/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())); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java index 4ab46d564c..4b68bbb102 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java +++ b/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 diff --git a/key.ui/examples/heap/block_loop_contracts/ListsWithIterators/src/IntIterator.java b/key.ui/examples/heap/block_loop_contracts/ListsWithIterators/src/IntIterator.java index 7b81d27eb3..1d3cf7205d 100755 --- a/key.ui/examples/heap/block_loop_contracts/ListsWithIterators/src/IntIterator.java +++ b/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; diff --git a/key.ui/examples/heap/block_loop_contracts/ListsWithIterators/src/IntLinkedList.java b/key.ui/examples/heap/block_loop_contracts/ListsWithIterators/src/IntLinkedList.java index 60142d8d7b..ced76b7e1d 100755 --- a/key.ui/examples/heap/block_loop_contracts/ListsWithIterators/src/IntLinkedList.java +++ b/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 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; @*/