TestProofBundleIO

3

tests

0

failures

0

ignored

8.653s

duration

100%

successful

Tests

Test Duration Result
testComplexBundleGeneration() 1.665s passed
testSimpleBundleGeneration() 6.938s passed
testSimpleFileRepo() 0.050s passed

Standard output

544634     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\proofBundle\complexBundleGeneration\src\Client.java 
544634     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\proofBundle\complexBundleGeneration\src\Test.java 
544634     DEBUG Test worker     d.u.i.k.s.TermLabelSettings TermLabelSettings: Failure while reading the setting "UseOriginLabels".Using the default value: true.The string read was: null 
544634     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file D:\a\key\key\key.core\src\test\resources\testcase\proofBundle\complexBundleGeneration\test.key 
544822     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Read specifications obtained when parsing the Java files (usually JML and Strings.key) from D:\a\key\key\key.core\src\test\resources\testcase\proofBundle\complexBundleGeneration\test.key 
545072     DEBUG Thread-52       d.u.i.k.j.TypeConverter   typeconverter: (prefix this;, class class de.uka.ilkd.key.java.reference.ThisReference) 
545650     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip14445465381334682309\src\Client.java 
545650     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip14445465381334682309\src\Test.java 
545665     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip14445465381334682309\Test(Test__constant()).JML normal_behavior operation contract.0.proof 
545837     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Read specifications obtained when parsing the Java files (usually JML and Strings.key) from C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip14445465381334682309\Test(Test__constant()).JML normal_behavior operation contract.0.proof 
545884     DEBUG Test worker     d.u.i.k.j.TypeConverter   typeconverter: (prefix this;, class class de.uka.ilkd.key.java.reference.ThisReference) 
547076     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\proofBundle\simpleBundleGeneration\src\Client.java 
547076     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now D:\a\key\key\key.core\src\test\resources\testcase\proofBundle\simpleBundleGeneration\src\Test.java 
547076     DEBUG Test worker     d.u.i.k.s.TermLabelSettings TermLabelSettings: Failure while reading the setting "UseOriginLabels".Using the default value: true.The string read was: null 
547076     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file D:\a\key\key\key.core\src\test\resources\testcase\proofBundle\simpleBundleGeneration\test.key 
547076     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
547092     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Read specifications obtained when parsing the Java files (usually JML and Strings.key) from file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
549320     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Read specifications obtained when parsing the Java files (usually JML and Strings.key) from D:\a\key\key\key.core\src\test\resources\testcase\proofBundle\simpleBundleGeneration\test.key 
550620     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip5526239553910099680\src\Client.java 
550620     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip5526239553910099680\src\Test.java 
550635     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip5526239553910099680\Test(Test__constant()).JML normal_behavior operation contract.0.proof 
550635     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
550635     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Read specifications obtained when parsing the Java files (usually JML and Strings.key) from file:/D:/a/key/key/key.core/build/resources/main/de/uka/ilkd/key/java/JavaRedux/java/lang/String.key 
552789     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Read specifications obtained when parsing the Java files (usually JML and Strings.key) from C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip5526239553910099680\Test(Test__constant()).JML normal_behavior operation contract.0.proof