TestProofBundleIO

3

tests

0

failures

0

ignored

6.993s

duration

100%

successful

Tests

Test Duration Result
testComplexBundleGeneration() 1.230s passed
testSimpleBundleGeneration() 5.694s passed
testSimpleFileRepo() 0.069s passed

Standard output

402049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\src\test\resources\testcase\proofBundle\complexBundleGeneration\test.key 
402049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.2ns 
402053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 388.58ms 
402476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Test[Test::constant()].JML normal_behavior operation contract.0 
402476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
402485     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
402485     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
402485     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
402485     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
402501     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
402501     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
402501     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
402501     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
402516     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
402516     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
402516     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
402516     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
402594     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source this.d.constant();) 
402594     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source this.d.constant();) 
402594     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source this.d.constant();) 
402594     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source this.d.constant();) 
402610     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source this.d;) 
402610     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source this.d;) 
402610     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source this.d;) 
402610     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source this.d;) 
402610     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source d.constant();) 
402610     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source d.constant();) 
402610     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source d.constant();) 
402610     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source d.constant();) 
402610     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source d.constant();) 
402610     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source d.constant();) 
402610     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source d.constant();) 
402610     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source d.constant();) 
402626     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source result_constant_0) 
402626     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source result_constant_0) 
402626     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source result_constant_0) 
402626     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source result_constant_0) 
402672     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source result_constant_0) 
402672     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source result_constant_0) 
402672     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source result_constant_0) 
402672     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source result_constant_0) 
402688     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source i) 
402688     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source i) 
402688     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source i) 
402688     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source i) 
402777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\src\test\resources\testcase\proofBundle\complexBundleGeneration\test.zproof 
402815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 42.03ms 
402815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 368.99ms 
403209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Test[Test::constant()].JML normal_behavior operation contract.0 
403272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.28ms 
403272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\src\test\resources\testcase\proofBundle\simpleBundleGeneration\test.key 
403272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.4ns 
403272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
406082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Test[Test::constant()].JML normal_behavior operation contract.0 
406082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
406082     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
406082     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
406082     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
406082     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
406098     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
406098     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
406098     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
406098     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
406098     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
406098     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
406098     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
406098     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
406129     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source 5) 
406129     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source 5) 
406129     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source 5) 
406129     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source 5) 
406192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from D:\a\key\key\key.core\src\test\resources\testcase\proofBundle\simpleBundleGeneration\test.zproof 
406192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.41ms 
406208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
408941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Test[Test::constant()].JML normal_behavior operation contract.0 
408973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.57ms