Class de.uka.ilkd.key.java.TestJP2KeY

all > de.uka.ilkd.key.java > TestJP2KeY
12

tests
1

failures
0

ignored
0.315s

duration
91%

successful

Failed tests

testReadBlockWithContext()

org.opentest4j.AssertionFailedError: ProgramVariables should be the same ones. ==> expected: de.uka.ilkd.key.logic.op.LocationVariable@7d6e2366<i> but was: de.uka.ilkd.key.logic.op.LocationVariable@4528a871<i>
	at app//org.junit.jupiter.api.AssertionFailureBuilder.build(AssertionFailureBuilder.java:151)
	at app//org.junit.jupiter.api.AssertionFailureBuilder.buildAndThrow(AssertionFailureBuilder.java:132)
	at app//org.junit.jupiter.api.AssertSame.failNotSame(AssertSame.java:50)
	at app//org.junit.jupiter.api.AssertSame.assertSame(AssertSame.java:35)
	at app//org.junit.jupiter.api.Assertions.assertSame(Assertions.java:2860)
	at app//de.uka.ilkd.key.java.TestJP2KeY.testReadBlockWithContext(TestJP2KeY.java:144)
	at java.base@17.0.7/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base@17.0.7/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:77)
	at java.base@17.0.7/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base@17.0.7/java.lang.reflect.Method.invoke(Method.java:568)
	at app//org.junit.platform.commons.util.ReflectionUtils.invokeMethod(ReflectionUtils.java:727)
	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:156)
	at app//org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestableMethod(TimeoutExtension.java:147)
	at app//org.junit.jupiter.engine.extension.TimeoutExtension.interceptTestMethod(TimeoutExtension.java:86)
	at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker$ReflectiveInterceptorCall.lambda$ofVoidMethod$0(InterceptingExecutableInvoker.java:103)
	at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.lambda$invoke$0(InterceptingExecutableInvoker.java:93)
	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.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:92)
	at app//org.junit.jupiter.engine.execution.InterceptingExecutableInvoker.invoke(InterceptingExecutableInvoker.java:86)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.lambda$invokeTestMethod$7(TestMethodTestDescriptor.java:217)
	at app//org.junit.platform.engine.support.hierarchical.ThrowableCollector.execute(ThrowableCollector.java:73)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.invokeTestMethod(TestMethodTestDescriptor.java:213)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:138)
	at app//org.junit.jupiter.engine.descriptor.TestMethodTestDescriptor.execute(TestMethodTestDescriptor.java:68)
	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@17.0.7/java.util.ArrayList.forEach(ArrayList.java:1511)
	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@17.0.7/java.util.ArrayList.forEach(ArrayList.java:1511)
	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 app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:107)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:88)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.lambda$execute$0(EngineExecutionOrchestrator.java:54)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.withInterceptedStreams(EngineExecutionOrchestrator.java:67)
	at app//org.junit.platform.launcher.core.EngineExecutionOrchestrator.execute(EngineExecutionOrchestrator.java:52)
	at app//org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:114)
	at app//org.junit.platform.launcher.core.DefaultLauncher.execute(DefaultLauncher.java:86)
	at app//org.junit.platform.launcher.core.DefaultLauncherSession$DelegatingLauncher.execute(DefaultLauncherSession.java:86)
	at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.processAllTestClasses(JUnitPlatformTestClassProcessor.java:110)
	at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor$CollectAllTestClassesExecutor.access$000(JUnitPlatformTestClassProcessor.java:90)
	at org.gradle.api.internal.tasks.testing.junitplatform.JUnitPlatformTestClassProcessor.stop(JUnitPlatformTestClassProcessor.java:85)
	at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.stop(SuiteTestClassProcessor.java:62)
	at java.base@17.0.7/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base@17.0.7/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:77)
	at java.base@17.0.7/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base@17.0.7/java.lang.reflect.Method.invoke(Method.java:568)
	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 jdk.proxy2/jdk.proxy2.$Proxy5.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)

Tests

Test Method name Duration Result
{ int j = 7; int i; i=1; byte d = 0; short f = 1; long l = 123; for (i=0, j=1; (i<42) && (i>0); i++, j--) { i=13; j=1; } while ((-i<7) || (i++==7--) | (--i==++7) ||(!true && false) || ('a'=='d') || ("asd"=="as"+"d") & (d==f) ^ (d/f+2>=f*d-f%d)|| (l<=~i) || !(this==null) || ((this!=null) ? (8<<j<8>>i) : (7&5>8>>>7L) || (7|5!=8^4)) && (i+=j) && (i=j) && (i/=j) && (i%=j) && (i-=j) && (i*=j) && (i<<=j) && (i>>=j) && (i >>>= j) && (i &= j) && (i ^= j) && (i |= j)) j=7; } testJBlocks()[1] 0.103s passed
{ int j=7; int i; i=1;do { j++; } while (i==1);if (j==42) j=7; else {i=7; j=43;}; ; label0: j=42; switch (j-i) {case 7: j=2; case 42: j=3; default: j=4; } while (j==42) loop1:{ if (j==7) break; if (j==43) break loop1; if (j==42) continue; if (j==41) continue loop1;} if (j>42) return;synchronized(null) { j=7; } } testJBlocks()[2] 0.040s passed
{ int x = 1; {java.util.List l;} } testJBlocks()[3] 0.007s passed
{int[] a; a=new int[3]; a=new int[]{2,3,4}; int j=a[2]; j=a.length;} testJBlocks()[4] 0.006s passed
class A1 { public A1() { }} testJClasses()[1] 0.009s passed
package qwe.rty; import qwe.rty.A; import dfg.hjk.*; import java.util.*; public abstract class A implements Z { static { d=3; Object v = new Object();} public static int d;A (int j) { d=5; } public A (int j, long k) {this(j); d=5; } private static final A[] b=new A[]{null}; long f; java.util.List s; public void abc() { Object z=new A(4, 5) { public int d=7; }; abc(); A a=(A)null; a=def(a); a=def(a).ghi(a).ghi(a); } { int x = 1; {int i = "\".length}"; } } protected A def(A a) {a=ghi(a); return new A(3);} private synchronized A ghi(A a) { a=ghi(a); ghi(a); A a1=null; a1=ghi(a1); a=def(a); return null;} protected abstract int[] jkl(A a, int i); protected Object o() {if (s instanceof Cloneable) return A.class;}} interface Z { public int d=0; } interface Z0 extends Z {} class A1 extends A { public static A a=new A(4); A1 (int j) {super(j);} } testJClasses()[2] 0.041s passed
public class B extends Object {class E { public E(Object s) {super();} }} testJClasses()[3] 0.025s passed
class circ_A { static int a = circ_B.b; } class circ_B { static int b = circ_A.a; } testJClasses()[4] 0.029s passed
class circ2_A { static final int a = circ2_B.b; } class circ2_B { static final int b = circ2_A.a; } testJClasses()[5] 0.017s passed
class Cycle1 { void m(Cycle2 c) {} } class Cycle2 { void m(Cycle1 c) {} } testJClasses()[6] 0.013s passed
class EmptyConstr { EmptyConstr(); } testJClasses()[7] 0.010s passed
testReadBlockWithContext() testReadBlockWithContext() 0.015s failed

Standard error

4163       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
4343       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
4349       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
4351       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
4365       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
4369       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
4389       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
4446       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
4456       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
4527       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
4538       DEBUG Test worker     d.u.i.k.j.JavaService     Reading class A1 { public A1() { }}  
4544       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: A1, formerNode: A1 
4548       DEBUG Test worker     d.u.i.k.j.JavaService     Reading package qwe.rty;
import qwe.rty.A;
import dfg.hjk.*;
import java.util.*;
public abstract class A implements Z {
    static { d=3; Object v = new [...] 
4579       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: s instanceof Cloneable, formerNode: other instanceof String 
4591       DEBUG Test worker     d.u.i.k.j.JavaService     Reading public class B extends Object {class E  { public E(Object s) {super();} }} 
4614       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: B, formerNode: B 
4616       DEBUG Test worker     d.u.i.k.j.JavaService     Reading  class circ_A {   static int a = circ_B.b;   } class circ_B {   static int b = circ_A.a;   } 
4641       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: circ_A, formerNode: circ_A 
4644       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: circ_B, formerNode: circ_B 
4645       DEBUG Test worker     d.u.i.k.j.JavaService     Reading  class circ2_A {   static final int a = circ2_B.b;   } class circ2_B {   static final int b = circ2_A.a;   } 
4651       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: circ2_A, formerNode: circ2_A 
4662       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: circ2_B, formerNode: circ2_B 
4664       DEBUG Test worker     d.u.i.k.j.JavaService     Reading class Cycle1 { void m(Cycle2 c) {} } class Cycle2 { void m(Cycle1 c) {} } 
4669       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Cycle1, formerNode: Cycle1 
4675       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Cycle2, formerNode: Cycle2 
4683       DEBUG Test worker     d.u.i.k.j.JavaService     Reading class EmptyConstr { EmptyConstr(); }  
4687       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: EmptyConstr, formerNode: EmptyConstr 
4735       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: j = 7;, formerNode: j = 7 
4824       ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: j = 42;, formerNode: j = 42