testJBlocks()
de.uka.ilkd.key.java.ConvertException: Encountered "this=" at line 4, column 155.
Was expecting one of:
<DL_EMBEDDED_FUNCTION> ...
<MAP_FUNCTION> ...
"++" ...
"--" ...
"+" ...
"-" ...
"\\indexOf" ...
"\\seq_length" ...
"\\seq_get" ...
"~" ...
"!" ...
"(" ...
<INTEGER_LITERAL> ...
<FLOATING_POINT_LITERAL> ...
<CHARACTER_LITERAL> ...
<STRING_LITERAL> ...
"true" ...
"false" ...
"null" ...
"\\empty" ...
"\\seq_empty" ...
"\\map_empty" ...
"this" ...
"super" ...
"@(" ...
"new" ...
"void" ...
"boolean" ...
"char" ...
"byte" ...
"short" ...
"int" ...
"long" ...
"\\bigint" ...
"\\real" ...
"float" ...
"double" ...
"\\locset" ...
"\\seq" ...
"\\free" ...
"\\map" ...
<IDENTIFIER> ...
"\\singleton" ...
"\\set_union" ...
"\\intersect" ...
"\\set_minus" ...
"\\all_fields" ...
"\\all_objects" ...
"\\seq_singleton" ...
"\\seq_concat" ...
"\\seq_sub" ...
"\\seq_reverse" ...
"\\seq_put" ...
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.java.TestRecoder2KeY.testJBlocks(TestRecoder2KeY.java:123)
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.parser.proofjava.ParseException: Encountered "this=" at line 4, column 155.
Was expecting one of:
<DL_EMBEDDED_FUNCTION> ...
<MAP_FUNCTION> ...
"++" ...
"--" ...
"+" ...
"-" ...
"\\indexOf" ...
"\\seq_length" ...
"\\seq_get" ...
"~" ...
"!" ...
"(" ...
<INTEGER_LITERAL> ...
<FLOATING_POINT_LITERAL> ...
<CHARACTER_LITERAL> ...
<STRING_LITERAL> ...
"true" ...
"false" ...
"null" ...
"\\empty" ...
"\\seq_empty" ...
"\\map_empty" ...
"this" ...
"super" ...
"@(" ...
"new" ...
"void" ...
"boolean" ...
"char" ...
"byte" ...
"short" ...
"int" ...
"long" ...
"\\bigint" ...
"\\real" ...
"float" ...
"double" ...
"\\locset" ...
"\\seq" ...
"\\free" ...
"\\map" ...
<IDENTIFIER> ...
"\\singleton" ...
"\\set_union" ...
"\\intersect" ...
"\\set_minus" ...
"\\all_fields" ...
"\\all_objects" ...
"\\seq_singleton" ...
"\\seq_concat" ...
"\\seq_sub" ...
"\\seq_reverse" ...
"\\seq_put" ...
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.UnaryExpression(ProofJavaParser.java:3388)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.MultiplicativeExpression(ProofJavaParser.java:3297)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.AdditiveExpression(ProofJavaParser.java:3254)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.ShiftExpression(ProofJavaParser.java:3211)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.RelationalExpression(ProofJavaParser.java:3162)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.InstanceOfExpression(ProofJavaParser.java:3140)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.EqualityExpression(ProofJavaParser.java:3098)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.AndExpression(ProofJavaParser.java:3068)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.ExclusiveOrExpression(ProofJavaParser.java:3038)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.InclusiveOrExpression(ProofJavaParser.java:3008)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.ConditionalAndExpression(ProofJavaParser.java:2978)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.ConditionalOrExpression(ProofJavaParser.java:2948)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.ConditionalExpression(ProofJavaParser.java:2919)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.Expression(ProofJavaParser.java:2820)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.PrimaryPrefix(ProofJavaParser.java:3888)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.PrimaryExpression(ProofJavaParser.java:3662)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.PostfixExpression(ProofJavaParser.java:3594)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.UnaryExpressionNotPlusMinus(ProofJavaParser.java:3455)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.UnaryExpression(ProofJavaParser.java:3386)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.UnaryExpressionNotPlusMinus(ProofJavaParser.java:3447)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.UnaryExpression(ProofJavaParser.java:3386)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.MultiplicativeExpression(ProofJavaParser.java:3297)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.AdditiveExpression(ProofJavaParser.java:3254)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.ShiftExpression(ProofJavaParser.java:3211)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.RelationalExpression(ProofJavaParser.java:3162)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.InstanceOfExpression(ProofJavaParser.java:3140)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.EqualityExpression(ProofJavaParser.java:3098)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.AndExpression(ProofJavaParser.java:3068)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.ExclusiveOrExpression(ProofJavaParser.java:3038)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.InclusiveOrExpression(ProofJavaParser.java:3008)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.ConditionalAndExpression(ProofJavaParser.java:2978)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.ConditionalOrExpression(ProofJavaParser.java:2961)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.ConditionalExpression(ProofJavaParser.java:2919)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.Expression(ProofJavaParser.java:2820)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.WhileStatement(ProofJavaParser.java:5162)
at app//de.uka.ilkd.key.parser.proofjava.ProofJavaParser.Statement(ProofJavaParser.java:4547)
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)
... 88 more