MergeRuleTests

11

tests

0

failures

0

ignored

1m17.86s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.110s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.601s passed
testDoManualGcdProof() 21.783s passed
testLoadClosedGcdProofWithMergePointStatements() 4.309s passed
testLoadGcdProof() 4.137s passed
testLoadGcdProofWithPredAbstr() 4.377s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.901s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.673s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.406s passed
testMergeIndistinguishablePathConditionsWithITE() 3.343s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.220s passed

Standard output

466586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
466586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.1ns 
466586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466707     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
466707     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
466707     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
466707     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
467308     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
470758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 
470797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
470799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
488369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
488369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.3ns 
488370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
491819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
492039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 216.74ms 
492041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
492042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309ns 
492042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
495445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
495448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.2ns 
505152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
505152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.3ns 
505153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
508396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
509049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 622.11ms 
509052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
509053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.5ns 
509053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
512439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
513426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 936.82ms 
513433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
513433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.6ns 
513434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
516644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
516651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 757.39ns 
516652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
516653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 372ns 
516653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
520037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
520040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 648.79ns 
520060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
520060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365.4ns 
520061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
523299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
524361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02s 
524367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
524367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
524368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
527707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
527709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 509.7ns 
527711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
527711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
527711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
530876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
530878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.8ns 
540312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
540312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.6ns 
540312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
543554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
544446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 851.7ms