MergeRuleTests

11

tests

0

failures

0

ignored

1m25.59s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.234s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.990s passed
testDoManualGcdProof() 20.953s passed
testLoadClosedGcdProofWithMergePointStatements() 5.412s passed
testLoadGcdProof() 5.138s passed
testLoadGcdProofWithPredAbstr() 5.223s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.010s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.746s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.274s passed
testMergeIndistinguishablePathConditionsWithITE() 4.260s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.351s passed

Standard output

663421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
663421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 448.5ns 
663421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663581     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
663581     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
663581     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
663581     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
664247     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
668925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.5s 
668958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
668958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 
684369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
684369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.9ns 
684369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.45s 
688865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
689115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 239.55ms 
689115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
689115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.9ns 
689115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.45s 
693623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
693623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.1ns 
702349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
702349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.3ns 
702349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
706827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.47s 
706874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
707359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 435.69ms 
707359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
707359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143ns 
707374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
711889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s 
711935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
712582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 569.35ms 
712582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
712582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.9ns 
712582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.32s 
716933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
716933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 364ns 
716933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
716933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.2ns 
716933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
721160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s 
721191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
721191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 290.5ns 
721207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
721207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 447ns 
721222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
725696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.48s 
725728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
726619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 806.57ms 
726619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
726635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.04ms 
726635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 
730879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
730879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 280.1ns 
730879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
730879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.8ns 
730879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.42s 
735341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
735341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.6ns 
743869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
743869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 660.2ns 
743869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.49s 
748413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
749007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 525.82ms