TestTacletIndex

5

tests

0

failures

1

ignored

0.513s

duration

100%

successful

Tests

Test Duration Result
disabled_testNonInteractiveIsShownOnlyIfHeuristicIsMissed() - ignored
testMatchConflictOccurs() 0.003s passed
testNoMatchingFindRule() 0.002s passed
testNotFreeInYConflict() 0.014s passed
testShownIfHeuristicFits() 0.494s passed

Standard error

75555      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
75555      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Object, formerNode: java.lang.Object 
75555      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Object, formerNode: java.lang.Object 
75555      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Annotation, formerNode: Annotation 
75555      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArithmeticException, formerNode: ArithmeticException 
75555      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArrayIndexOutOfBoundsException, formerNode: ArrayIndexOutOfBoundsException 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArrayStoreException, formerNode: ArrayStoreException 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: AssertionError, formerNode: AssertionError 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Character, formerNode: Character 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Class, formerNode: java.lang.Class 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Class, formerNode: java.lang.Class 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ClassCastException, formerNode: ClassCastException 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: CloneNotSupportedException, formerNode: CloneNotSupportedException 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Cloneable, formerNode: Cloneable 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Comparable, formerNode: Comparable 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Double, formerNode: Double 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Enum, formerNode: java.lang.Enum 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Enum, formerNode: java.lang.Enum 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Error, formerNode: Error 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Exception, formerNode: Exception 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ExceptionInInitializerError, formerNode: java.lang.ExceptionInInitializerError 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ExceptionInInitializerError, formerNode: java.lang.ExceptionInInitializerError 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Float, formerNode: Float 
75571      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: IllegalArgumentException, formerNode: IllegalArgumentException 
75586      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: IndexOutOfBoundsException, formerNode: IndexOutOfBoundsException 
75586      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Integer, formerNode: java.lang.Integer 
75586      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Integer, formerNode: java.lang.Integer 
75586      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: InterruptedException, formerNode: InterruptedException 
75586      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Iterable, formerNode: Iterable 
75586      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: LinkageError, formerNode: LinkageError 
75620      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Math, formerNode: Math 
75621      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NegativeArraySizeException, formerNode: NegativeArraySizeException 
75622      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NoClassDefFoundError, formerNode: java.lang.NoClassDefFoundError 
75622      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NoClassDefFoundError, formerNode: java.lang.NoClassDefFoundError 
75624      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NullPointerException, formerNode: NullPointerException 
75625      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Number, formerNode: Number 
75626      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: NumberFormatException, formerNode: NumberFormatException 
75627      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: VirtualMachineError, formerNode: VirtualMachineError 
75629      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: OutOfMemoryError, formerNode: OutOfMemoryError 
75630      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Runnable, formerNode: Runnable 
75631      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: RuntimeException, formerNode: RuntimeException 
75631      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
75634      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
75635      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
75642      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
75650      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: String, formerNode: java.lang.String 
75665      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: String, formerNode: java.lang.String 
75667      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: char, formerNode: /*@ helper */
char 
75668      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: StringBuffer, formerNode: StringBuffer 
75671      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: System, formerNode: System 
75672      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Thread, formerNode: Thread 
75674      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Throwable, formerNode: java.lang.Throwable 
75674      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Throwable, formerNode: java.lang.Throwable 
75679      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Collection, formerNode: Collection 
75680      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Iterator, formerNode: java.util.Iterator 
75680      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Iterator, formerNode: java.util.Iterator 
75684      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: List, formerNode: java.util.List 
75684      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: List, formerNode: java.util.List 
75686      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ListIterator, formerNode: java.util.ListIterator 
75686      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ListIterator, formerNode: java.util.ListIterator 
75687      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Long, formerNode: Long 
75688      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Boolean, formerNode: Boolean 
75691      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Map, formerNode: Map 
75695      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Set, formerNode: java.util.Set 
75695      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Set, formerNode: java.util.Set 
75696      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: FilterOutputStream, formerNode: FilterOutputStream 
75697      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: InputStream, formerNode: java.io.InputStream 
75697      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: InputStream, formerNode: java.io.InputStream 
75699      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: IOException, formerNode: IOException 
75699      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: OutputStream, formerNode: java.io.OutputStream 
75700      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: OutputStream, formerNode: java.io.OutputStream 
75704      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: PrintStream, formerNode: java.io.PrintStream 
75704      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: PrintStream, formerNode: java.io.PrintStream 
75705      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Serializable, formerNode: Serializable 
75706      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: BigInteger, formerNode: java.math.BigInteger 
75707      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: BigInteger, formerNode: java.math.BigInteger 
75708      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ArrayList, formerNode: ArrayList 
75711      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
75726      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Arrays, formerNode: Arrays 
75727      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: ListIteratorImpl, formerNode: ListIteratorImpl 
75727      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: Date, formerNode: Date 
75728      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: LinkedHashMap, formerNode: LinkedHashMap 
75729      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: /*@strictly_pure*/
java.lang.String 
75730      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: LinkedList, formerNode: LinkedList 
75896      INFO  Test worker     d.u.i.k.n.KeyIO           Parsing took 0 ms 
75896      DEBUG Test worker     d.u.i.k.n.KeyIO           Load declarations of de.uka.ilkd.key.nparser.KeyAst$File:  D:\a\key\key\key.core\src\test\resources\testcase\..\de\uka\ilkd\key\proof\ruleForTestTacletIndex.taclet:7#1 
75897      INFO  Test worker     d.u.i.k.n.KeyIO           MODE: declarations took 1 ms 
75897      DEBUG Test worker     d.u.i.k.n.KeyIO           MODE: 2nd degree decls took 0 
75903      DEBUG Test worker     d.u.i.k.n.KeyIO           MODE: taclets took 6ms