TestProofBundleIO

3

tests

0

failures

0

ignored

6.615s

duration

100%

successful

Tests

Test Duration Result
testComplexBundleGeneration() 1.170s passed
testSimpleBundleGeneration() 5.415s passed
testSimpleFileRepo() 0.030s passed

Standard output

386232     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 
386466     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 
386482     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 
386482     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 
386638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ns 
386638     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 
386999     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip9555002395918545140\Test(Test__constant()).JML normal_behavior operation contract.0.proof 
387234     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip9555002395918545140\src\Client.java 
387234     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip9555002395918545140\src\Test.java 
387407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.44ms 
387408     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip9555002395918545140\Test(Test__constant()).JML normal_behavior operation contract.0.proof 
387411     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 
388319     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 
388319     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 
388335     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 
388335     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 
390050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 
390050     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 
390164     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip17078395302956259707\Test(Test__constant()).JML normal_behavior operation contract.0.proof 
391049     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip17078395302956259707\src\Client.java 
391049     DEBUG Test worker     d.u.i.k.j.Recoder2KeY     converting now C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip17078395302956259707\src\Test.java 
391049     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 
392824     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.23ms 
392824     DEBUG Test worker     d.u.i.k.p.i.KeYFile       Reading KeY file C:\Users\RUNNER~1\AppData\Local\Temp\KeYunzip17078395302956259707\Test(Test__constant()).JML normal_behavior operation contract.0.proof