TestProofBundleIO

3

tests

0

failures

0

ignored

8.550s

duration

100%

successful

Tests

Test Duration Result
testComplexBundleGeneration() 1.680s passed
testSimpleBundleGeneration() 6.818s passed
testSimpleFileRepo() 0.052s passed

Standard output

479158     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 
479158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.4ns 
479158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 519.81ms 
479736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Test[Test::constant()].JML normal_behavior operation contract.0 
479736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
479752     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
479752     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
479752     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
479752     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
479783     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
479783     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
479783     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
479783     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
479783     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
479783     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
479783     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
479783     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
479877     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source this.d.constant();) 
479877     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source this.d.constant();) 
479877     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source this.d.constant();) 
479877     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source this.d.constant();) 
479877     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source this.d;) 
479877     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source this.d;) 
479877     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source this.d;) 
479877     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source this.d;) 
479892     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source d.constant();) 
479892     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source d.constant();) 
479892     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source d.constant();) 
479892     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source d.constant();) 
479892     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source d.constant();) 
479892     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source d.constant();) 
479892     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source d.constant();) 
479892     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source d.constant();) 
479908     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source result_constant_0) 
479908     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source result_constant_0) 
479908     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source result_constant_0) 
479908     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source result_constant_0) 
479970     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source result_constant_0) 
479970     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source result_constant_0) 
479970     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source result_constant_0) 
479970     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source result_constant_0) 
479986     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source i) 
479986     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source i) 
479986     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source i) 
479986     DEBUG Thread-52       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source i) 
480205     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 
480252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.92ms 
480267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 476.22ms 
480768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Test[Test::constant()].JML normal_behavior operation contract.0 
480830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.49ms 
480846     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 
480846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.5ns 
480846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
484162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Test[Test::constant()].JML normal_behavior operation contract.0 
484162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
484178     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
484178     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
484178     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
484178     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
484178     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
484178     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
484178     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
484178     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
484178     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
484178     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
484178     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source null;) 
484178     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source null;) 
484209     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source 5) 
484209     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source 5) 
484209     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern true;, source 5) 
484209     DEBUG Thread-56       d.u.i.k.j.JavaProgramElement Program match failed (pattern false;, source 5) 
484271     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 
484287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.06ms 
484287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
487633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Test[Test::constant()].JML normal_behavior operation contract.0 
487664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.84ms