Description
The file key.ui/examples/heap/block_loop_contracts/ListsWithIterators/src/IntLinkedList.java is not loadable. This file uses an enhanced for loop with the \values keyword.
Reproducible
always
Steps to reproduce
- Load the file mentioned above
What is your expected behavior and what was the actual behavior?
Expected: it works
Actual: error message "term has sort: Seq; type has sort: IntLinkedList"
Additional information
Stacktrace
Details
java.lang.IllegalArgumentException: term has sort: Seq; type has sort: IntLinkedList
at de.uka.ilkd.key.speclang.translation.SLExpression.<init>(SLExpression.java:25)
at de.uka.ilkd.key.speclang.translation.SLExpression.<init>(SLExpression.java:33)
at de.uka.ilkd.key.speclang.njml.JmlTermFactory.values(JmlTermFactory.java:842)
at de.uka.ilkd.key.speclang.njml.Translator.visitPrimaryValues(Translator.java:1499)
at de.uka.ilkd.key.speclang.njml.JmlParser$PrimaryValuesContext.accept(JmlParser.java:10485)
at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at de.uka.ilkd.key.speclang.njml.JmlParserBaseVisitor.visitPrimaryexpr(JmlParserBaseVisitor.java:752)
at de.uka.ilkd.key.speclang.njml.JmlParser$PrimaryexprContext.accept(JmlParser.java:8750)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.visitPostfixexpr(Translator.java:876)
at de.uka.ilkd.key.speclang.njml.Translator.visitPostfixexpr(Translator.java:68)
at de.uka.ilkd.key.speclang.njml.JmlParser$PostfixexprContext.accept(JmlParser.java:8663)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.visitUnaryexprnotplusminus(Translator.java:862)
at de.uka.ilkd.key.speclang.njml.JmlParser$UnaryexprnotplusminusContext.accept(JmlParser.java:8491)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.oneOf(Translator.java:157)
at de.uka.ilkd.key.speclang.njml.Translator.visitUnaryexpr(Translator.java:822)
at de.uka.ilkd.key.speclang.njml.Translator.visitUnaryexpr(Translator.java:68)
at de.uka.ilkd.key.speclang.njml.JmlParser$UnaryexprContext.accept(JmlParser.java:8347)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.lambda$mapOf$0(Translator.java:143)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
at de.uka.ilkd.key.speclang.njml.Translator.mapOf(Translator.java:143)
at de.uka.ilkd.key.speclang.njml.Translator.visitMultexpr(Translator.java:759)
at de.uka.ilkd.key.speclang.njml.JmlParser$MultexprContext.accept(JmlParser.java:8266)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.lambda$mapOf$0(Translator.java:143)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
at de.uka.ilkd.key.speclang.njml.Translator.mapOf(Translator.java:143)
at de.uka.ilkd.key.speclang.njml.Translator.visitAdditiveexpr(Translator.java:742)
at de.uka.ilkd.key.speclang.njml.JmlParser$AdditiveexprContext.accept(JmlParser.java:8174)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.lambda$mapOf$0(Translator.java:143)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
at de.uka.ilkd.key.speclang.njml.Translator.mapOf(Translator.java:143)
at de.uka.ilkd.key.speclang.njml.Translator.visitShiftexpr(Translator.java:725)
at de.uka.ilkd.key.speclang.njml.JmlParser$ShiftexprContext.accept(JmlParser.java:8087)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.oneOf(Translator.java:157)
at de.uka.ilkd.key.speclang.njml.Translator.visitRelationalexpr(Translator.java:505)
at de.uka.ilkd.key.speclang.njml.JmlParser$RelationalexprContext.accept(JmlParser.java:7689)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.lambda$mapOf$0(Translator.java:143)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
at de.uka.ilkd.key.speclang.njml.Translator.mapOf(Translator.java:143)
at de.uka.ilkd.key.speclang.njml.Translator.visitEqualityexpr(Translator.java:573)
at de.uka.ilkd.key.speclang.njml.Translator.visitEqualityexpr(Translator.java:68)
at de.uka.ilkd.key.speclang.njml.JmlParser$EqualityexprContext.accept(JmlParser.java:7615)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.visitAndexpr(Translator.java:555)
at de.uka.ilkd.key.speclang.njml.JmlParser$AndexprContext.accept(JmlParser.java:7546)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.visitExclusiveorexpr(Translator.java:540)
at de.uka.ilkd.key.speclang.njml.JmlParser$ExclusiveorexprContext.accept(JmlParser.java:7477)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.visitInclusiveorexpr(Translator.java:525)
at de.uka.ilkd.key.speclang.njml.JmlParser$InclusiveorexprContext.accept(JmlParser.java:7408)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.visitLogicalandexpr(Translator.java:512)
at de.uka.ilkd.key.speclang.njml.JmlParser$LogicalandexprContext.accept(JmlParser.java:7339)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.visitLogicalorexpr(Translator.java:493)
at de.uka.ilkd.key.speclang.njml.Translator.visitLogicalorexpr(Translator.java:68)
at de.uka.ilkd.key.speclang.njml.JmlParser$LogicalorexprContext.accept(JmlParser.java:7270)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.visitImpliesexpr(Translator.java:457)
at de.uka.ilkd.key.speclang.njml.JmlParser$ImpliesexprContext.accept(JmlParser.java:7009)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.lambda$mapOf$0(Translator.java:143)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
at de.uka.ilkd.key.speclang.njml.Translator.mapOf(Translator.java:143)
at de.uka.ilkd.key.speclang.njml.Translator.visitEquivalenceexpr(Translator.java:437)
at de.uka.ilkd.key.speclang.njml.JmlParser$EquivalenceexprContext.accept(JmlParser.java:6932)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.visitConditionalexpr(Translator.java:423)
at de.uka.ilkd.key.speclang.njml.Translator.visitConditionalexpr(Translator.java:68)
at de.uka.ilkd.key.speclang.njml.JmlParser$ConditionalexprContext.accept(JmlParser.java:6863)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.visitExpression(Translator.java:413)
at de.uka.ilkd.key.speclang.njml.Translator.visitExpression(Translator.java:68)
at de.uka.ilkd.key.speclang.njml.JmlParser$ExpressionContext.accept(JmlParser.java:6810)
at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:138)
at de.uka.ilkd.key.speclang.njml.Translator.lambda$mapOf$0(Translator.java:143)
at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197)
at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708)
at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509)
at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499)
at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921)
at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:682)
at de.uka.ilkd.key.speclang.njml.Translator.mapOf(Translator.java:143)
at de.uka.ilkd.key.speclang.njml.Translator.visitVariant_function(Translator.java:2533)
at de.uka.ilkd.key.speclang.njml.Translator.visitVariant_function(Translator.java:68)
at de.uka.ilkd.key.speclang.njml.JmlParser$Variant_functionContext.accept(JmlParser.java:5416)
at de.uka.ilkd.key.speclang.njml.JmlIO.interpret(JmlIO.java:177)
at de.uka.ilkd.key.speclang.njml.JmlIO.translateTerm(JmlIO.java:194)
at de.uka.ilkd.key.speclang.njml.JmlIO.translateTerm(JmlIO.java:220)
at de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory.translateDecreases(JMLSpecFactory.java:891)
at de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory.translateJMLClauses(JMLSpecFactory.java:427)
at de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory.createJMLLoopContracts(JMLSpecFactory.java:1436)
at de.uka.ilkd.key.speclang.jml.JMLSpecExtractor.createLoopContracts(JMLSpecExtractor.java:646)
at de.uka.ilkd.key.speclang.jml.JMLSpecExtractor.extractLoopContracts(JMLSpecExtractor.java:568)
at de.uka.ilkd.key.speclang.SLEnvInput.addLoopContracts(SLEnvInput.java:189)
at de.uka.ilkd.key.speclang.SLEnvInput.createSpecs(SLEnvInput.java:357)
at de.uka.ilkd.key.speclang.SLEnvInput.read(SLEnvInput.java:400)
at de.uka.ilkd.key.proof.init.ProblemInitializer.readEnvInput(ProblemInitializer.java:328)
at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:560)
at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:452)
at de.uka.ilkd.key.proof.io.AbstractProblemLoader.createInitConfig(AbstractProblemLoader.java:497)
at de.uka.ilkd.key.proof.io.AbstractProblemLoader.loadEnvironment(AbstractProblemLoader.java:304)
at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:268)
at de.uka.ilkd.key.proof.io.ProblemLoader.doWork(ProblemLoader.java:75)
at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:125)
at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:118)
at java.desktop/javax.swing.SwingWorker$1.call(SwingWorker.java:305)
at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:317)
at java.desktop/javax.swing.SwingWorker.run(SwingWorker.java:342)
at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
at java.base/java.lang.Thread.run(Thread.java:1583)
Tag: @flo2702 because you added this example. Did it use to load?
Description
The file
key.ui/examples/heap/block_loop_contracts/ListsWithIterators/src/IntLinkedList.javais not loadable. This file uses an enhanced for loop with the \values keyword.Reproducible
always
Steps to reproduce
Expected: it works
Actual: error message "term has sort: Seq; type has sort: IntLinkedList"
Additional information
Stacktrace
Details
Tag: @flo2702 because you added this example. Did it use to load?