MergeRuleTests

11

tests

0

failures

0

ignored

1m25.21s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 12.949s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.553s passed
testDoManualGcdProof() 20.687s passed
testLoadClosedGcdProofWithMergePointStatements() 5.589s passed
testLoadGcdProof() 5.297s passed
testLoadGcdProofWithPredAbstr() 5.557s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.208s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.549s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.239s passed
testMergeIndistinguishablePathConditionsWithITE() 4.322s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.264s passed

Standard output

655175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
655175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.9ns 
655175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655331     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
655331     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
655331     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
655331     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
655925     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
660553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.38s 
660603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
660603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.1ns 
675856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
675856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.3ns 
675856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 
680130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
680405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 267.05ms 
680405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
680405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.7ns 
680405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 
684799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
684799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.6ns 
693354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
693369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 22.33ms 
693369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.41s 
697828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
698563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 677.86ms 
698578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
698578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 476.8ns 
698578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
703086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.51s 
703133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
704120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 913.25ms 
704120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
704120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.6ns 
704136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.24s 
708384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
708384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 801.2ns 
708384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
708399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 495.2ns 
708399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 
712591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
712591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 578.6ns 
712623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
712623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 441.4ns 
712623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
717076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.46s 
717123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
718197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01s 
718212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
718212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.8ns 
718212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
722518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.3s 
722534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
722534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 580.6ns 
722534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
722549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.9ns 
722549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.19s 
726777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
726777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.5ns 
735087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
735087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 646.6ns 
735087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.32s 
739454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
740384     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 854.22ms