Package de.uka.ilkd.key.java

Failed tests

• TestJP2KeY. { 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; }
• TestJP2KeY. { 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; } }
• TestJP2KeY. { int x = 1; {java.util.List l;} }
• TestJP2KeY. {int[] a; a=new int[3]; a=new int[]{2,3,4}; int j=a[2]; j=a.length;}
• TestJP2KeY. class A1 { public A1() { }}
• TestJP2KeY. 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);} }
• TestJP2KeY. public class B extends Object {class E { public E(Object s) {super();} }}
• TestJP2KeY. class circ_A { static int a = circ_B.b; } class circ_B { static int b = circ_A.a; }
• TestJP2KeY. class circ2_A { static final int a = circ2_B.b; } class circ2_B { static final int b = circ2_A.a; }
• TestJP2KeY. class Cycle1 { void m(Cycle2 c) {} } class Cycle2 { void m(Cycle1 c) {} }
• TestJP2KeY. class EmptyConstr { EmptyConstr(); }
• TestJP2KeY. testReadBlockWithContext()
• TestJavaCardDLJavaExtensions. testTypeNotInScopeShouldNotBeFound()
• TestJavaInfo. testFindImplicitAttributesForClassTypesOnly()

Ignored tests

• TestJP2KeY. xtestFileInput()

Classes