TestJavaCardDLJavaExtensions
Failed tests
testMethodFrameRedirectsScope()
Could not parse java: '{
method-frame(source=setSize(int)@test.TestJavaCardDLExtensions) : {
TestJavaCardDLExtensions t = null;
}
}' at /home/runner/work/key/key/key.core/src/test/resources/testcase/javacardDLExtensions/typeResolutionInMethodFrame2.key:9:2 (/home/runner/work/key/key/key.core/src/test/resources/testcase/javacardDLExtensions/typeResolutionInMethodFrame2.key:9:2)
at app//de.uka.ilkd.key.nparser.builder.ExpressionBuilder.getJavaBlock(ExpressionBuilder.java:576)
at app//de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitModality_term(ExpressionBuilder.java:1060)
at app//de.uka.ilkd.key.nparser.KeYParser$Modality_termContext.accept(KeYParser.java:4566)
at app//org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at app//de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitTerm60(KeYParserBaseVisitor.java:380)
at app//de.uka.ilkd.key.nparser.KeYParser$Term60Context.accept(KeYParser.java:4432)
at app//de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:45)
at app//de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:35)
at app//de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitConjunction_term(ExpressionBuilder.java:230)
at app//de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitConjunction_term(ExpressionBuilder.java:49)
at app//de.uka.ilkd.key.nparser.KeYParser$Conjunction_termContext.accept(KeYParser.java:4367)
at app//de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:45)
at app//de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:35)
at app//de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitDisjunction_term(ExpressionBuilder.java:221)
at app//de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitDisjunction_term(ExpressionBuilder.java:49)
at app//de.uka.ilkd.key.nparser.KeYParser$Disjunction_termContext.accept(KeYParser.java:4295)
at app//de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:45)
at app//de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:35)
at app//de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitImplication_term(ExpressionBuilder.java:214)
at app//de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitImplication_term(ExpressionBuilder.java:49)
at app//de.uka.ilkd.key.nparser.KeYParser$Implication_termContext.accept(KeYParser.java:4228)
at app//de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:45)
at app//de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:35)
at app//de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquivalence_term(ExpressionBuilder.java:191)
at app//de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitEquivalence_term(ExpressionBuilder.java:49)
at app//de.uka.ilkd.key.nparser.KeYParser$Equivalence_termContext.accept(KeYParser.java:4160)
at app//de.uka.ilkd.key.nparser.builder.AbstractBuilder.accept(AbstractBuilder.java:45)
at app//de.uka.ilkd.key.nparser.builder.DefaultBuilder.accept(DefaultBuilder.java:35)
at app//de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitElementary_update_term(ExpressionBuilder.java:181)
at app//de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitElementary_update_term(ExpressionBuilder.java:49)
at app//de.uka.ilkd.key.nparser.KeYParser$Elementary_update_termContext.accept(KeYParser.java:4094)
at app//de.uka.ilkd.key.nparser.builder.AbstractBuilder.lambda$mapOf$0(AbstractBuilder.java:112)
at java.base@11.0.18/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:195)
at java.base@11.0.18/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1655)
at java.base@11.0.18/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:484)
at java.base@11.0.18/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:474)
at java.base@11.0.18/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:913)
at java.base@11.0.18/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.base@11.0.18/java.util.stream.ReferencePipeline.collect(ReferencePipeline.java:578)
at app//de.uka.ilkd.key.nparser.builder.AbstractBuilder.mapOf(AbstractBuilder.java:112)
at app//de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitParallel_term(ExpressionBuilder.java:166)
at app//de.uka.ilkd.key.nparser.builder.ExpressionBuilder.visitParallel_term(ExpressionBuilder.java:49)
at app//de.uka.ilkd.key.nparser.KeYParser$Parallel_termContext.accept(KeYParser.java:4027)
at app//org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at app//de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitTerm(KeYParserBaseVisitor.java:331)
at app//de.uka.ilkd.key.nparser.KeYParser$TermContext.accept(KeYParser.java:3974)
at app//org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at app//de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitProblem(KeYParserBaseVisitor.java:37)
at app//de.uka.ilkd.key.nparser.KeYParser$ProblemContext.accept(KeYParser.java:685)
at app//org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
at app//de.uka.ilkd.key.nparser.KeYParserBaseVisitor.visitFile(KeYParserBaseVisitor.java:23)
at app//de.uka.ilkd.key.nparser.KeYParser$FileContext.accept(KeYParser.java:306)
at app//de.uka.ilkd.key.nparser.KeyAst.accept(KeyAst.java:41)
at app//de.uka.ilkd.key.proof.io.KeYFile.readContracts(KeYFile.java:327)
at app//de.uka.ilkd.key.proof.init.KeYUserProblemFile.read(KeYUserProblemFile.java:111)
at app//de.uka.ilkd.key.proof.init.ProblemInitializer.readEnvInput(ProblemInitializer.java:331)
at app//de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:551)
at app//de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:455)
at app//de.uka.ilkd.key.proof.init.ProblemInitializer.startProver(ProblemInitializer.java:592)
at app//de.uka.ilkd.key.util.HelperClassForTests.parseThrowException(HelperClassForTests.java:95)
at app//de.uka.ilkd.key.util.HelperClassForTests.parseThrowException(HelperClassForTests.java:87)
at app//de.uka.ilkd.key.java.TestJavaCardDLJavaExtensions.testMethodFrameRedirectsScope(TestJavaCardDLJavaExtensions.java:36)
at java.base@11.0.18/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at java.base@11.0.18/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
at java.base@11.0.18/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.base@11.0.18/java.lang.reflect.Method.invoke(Method.java:566)
at app//org.junit.platform.commons.util.ReflectionUtils.invokeMethod(ReflectionUtils.java:725)
at app//org.junit.jupiter.engine.execution.MethodInvocation.proceed(MethodInvocation.java:60)
at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$ValidatingInvocation.proceed(InvocationInterceptorChain.java:131)
at app//org.junit.jupiter.engine.extension.TimeoutExtension.intercept(TimeoutExtension.java:149)
at app//org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestableMethod(TimeoutExtension.java:140)
at app//org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestMethod(TimeoutExtension.java:84)
at app//org.junit.jupiter.engine.execution.ExecutableInvoker$ReflectiveInterceptorCall.lambda$ofVoidMethod$0(ExecutableInvoker.java:115)
at app//org.junit.jupiter.engine.execution.ExecutableInvoker.lambda$invoke$0(ExecutableInvoker.java:105)
at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain$InterceptedInvocation.proceed(InvocationInterceptorChain.java:106)
at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.proceed(InvocationInterceptorChain.java:64)
at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.chainAndInvoke(InvocationInterceptorChain.java:45)
at app//org.junit.jupiter.engine.execution.InvocationInterceptorChain.invoke(InvocationInterceptorChain.java:37)
at app//org.junit.jupiter.engine.execution.ExecutableInvoker.invoke(ExecutableInvoker.java:104)
at app//org.junit.jupiter.engine.execution.ExecutableInvoker.invoke(ExecutableInvoker.java:98)
at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.lambda$invokeTestMethod$7(TestMethodTestDescriptor.java:214)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.invokeTestMethod(TestMethodTestDescriptor.java:210)
at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:135)
at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:66)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:151)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141)
at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95)
at java.base@11.0.18/java.util.ArrayList.forEach(ArrayList.java:1541)
at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:155)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141)
at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95)
at java.base@11.0.18/java.util.ArrayList.forEach(ArrayList.java:1541)
at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.invokeAll(SameThreadHierarchicalTestExecutorService.java:41)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$6(NodeTestTask.java:155)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$8(NodeTestTask.java:141)
at app//org.junit.platform.engine.support.hierarchical.Node.around(Node.java:137)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.lambda$executeRecursively$9(NodeTestTask.java:139)
at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.executeRecursively(NodeTestTask.java:138)
at app//org.junit.platform.engine.support.hierarchical.NodeTestTask.execute(NodeTestTask.java:95)
at app//org.junit.platform.engine.support.hierarchical.SameThreadHierarchicalTestExecutorService.submit(SameThreadHierarchicalTestExecutorService.java:35)
at app//org.junit.platform.engine.support.hierarchical.HierarchicalTestExecutor.execute(HierarchicalTestExecutor.java:57)
at app//org.junit.platform.engine.support.hierarchical.HierarchicalTestEngine.execute(HierarchicalTestEngine.java:54)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:107)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:88)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:54)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:67)
at org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:52)
at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114)
at org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86)
at org.junit.platform.launcher.core.DefaultLauncherSession$DelegatingLauncher.execute(DefaultLauncherSession.java:86)
at org.junit.platform.launcher.core.SessionPerRequestLauncher.execute(SessionPerRequestLauncher.java:53)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.processAllTestClasses(JUnitPlatformTestClassProcessor.java:99)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.access$000(JUnitPlatformTestClassProcessor.java:79)
at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor.stop(JUnitPlatformTestClassProcessor.java:75)
at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.stop(SuiteTestClassProcessor.java:62)
at java.base@11.0.18/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at java.base@11.0.18/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
at java.base@11.0.18/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.base@11.0.18/java.lang.reflect.Method.invoke(Method.java:566)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:36)
at org.gradle.internal.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24)
at org.gradle.internal.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:33)
at org.gradle.internal.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:94)
at com.sun.proxy.$Proxy2.stop(Unknown Source)
at org.gradle.api.internal.tasks.testing.worker.TestWorker$3.run(TestWorker.java:193)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.executeAndMaintainThreadName(TestWorker.java:129)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:100)
at org.gradle.api.internal.tasks.testing.worker.TestWorker.execute(TestWorker.java:60)
at org.gradle.process.internal.worker.child.ActionExecutionWorker.execute(ActionExecutionWorker.java:56)
at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:113)
at org.gradle.process.internal.worker.child.SystemApplicationClassLoaderWorker.call(SystemApplicationClassLoaderWorker.java:65)
at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.run(GradleWorkerMain.java:69)
at app//worker.org.gradle.process.internal.worker.GradleWorkerMain.main(GradleWorkerMain.java:74)
Caused by: de.uka.ilkd.key.java.ConvertException: Encountered ":" at line 2, column 69.
Was expecting:
"{" ...
at app//de.uka.ilkd.key.java.Recoder2KeY.reportErrorWithPositionInFile(Recoder2KeY.java:1246)
at app//de.uka.ilkd.key.java.Recoder2KeY.reportError(Recoder2KeY.java:1236)
at app//de.uka.ilkd.key.java.Recoder2KeY.recoderBlock(Recoder2KeY.java:1091)
at app//de.uka.ilkd.key.java.Recoder2KeY.readBlock(Recoder2KeY.java:1121)
at app//de.uka.ilkd.key.java.Recoder2KeY.readBlockWithEmptyContext(Recoder2KeY.java:1133)
at app//de.uka.ilkd.key.nparser.builder.ExpressionBuilder.getJavaBlock(ExpressionBuilder.java:572)
... 146 more
Caused by: de.uka.ilkd.key.parser.proofjava.ParseException: Encountered ":" at line 2, column 69.
Was expecting:
"{" ...
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.generateParseException(ProofJavaParser.java:11909)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.jj_consume_token(ProofJavaParser.java:11777)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.Block(ProofJavaParser.java:4766)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.MethodCallStatement(ProofJavaParser.java:4665)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.Statement(ProofJavaParser.java:4523)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.BlockStatement(ProofJavaParser.java:4818)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.StartBlock(ProofJavaParser.java:4801)
at app//de.uka.ilkd.key.java.recoderext.ProofJavaProgramFactory.parseStatementBlock(ProofJavaProgramFactory.java:470)
at app//de.uka.ilkd.key.java.Recoder2KeY.recoderBlock(Recoder2KeY.java:1071)
... 149 more
Tests
| Test |
Duration |
Result |
| testMethodFrameRedirectsScope() |
2.862s |
failed |
| testTypeNotInScopeShouldNotBeFound() |
2.947s |
passed |