TestProofBundleIO

3

tests

0

failures

0

ignored

9.176s

duration

100%

successful

Tests

Test Duration Result
testComplexBundleGeneration() 1.780s passed
testSimpleBundleGeneration() 7.367s passed
testSimpleFileRepo() 0.029s passed

Standard output

537737     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 
538066     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 
538066     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 
538081     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 
538346     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 
538487     DEBUG Thread-52       d.u.i.k.j.TypeConverter   typeconverter: (prefix this;, class class de.uka.ilkd.key.java.reference.ThisReference) 
538847     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip1777852361698835644\Test(Test__constant()).JML normal_behavior operation contract.0.proof 
539175     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip1777852361698835644\src\Client.java 
539175     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip1777852361698835644\src\Test.java 
539487     DEBUG Test worker     d.u.i.k.j.TypeConverter   typeconverter: (prefix this;, class class de.uka.ilkd.key.java.reference.ThisReference) 
539503     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip1777852361698835644\Test(Test__constant()).JML normal_behavior operation contract.0.proof 
539519     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 
540692     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 
540692     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 
540707     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 
540707     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 
543116     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 
543241     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip7430652692516337975\Test(Test__constant()).JML normal_behavior operation contract.0.proof 
544414     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip7430652692516337975\src\Client.java 
544414     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip7430652692516337975\src\Test.java 
544430     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 
546884     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip7430652692516337975\Test(Test__constant()).JML normal_behavior operation contract.0.proof