MergeRuleTests

11

tests

0

failures

0

ignored

1m25.08s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.222s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.655s passed
testDoManualGcdProof() 20.554s passed
testLoadClosedGcdProofWithMergePointStatements() 5.586s passed
testLoadGcdProof() 5.323s passed
testLoadGcdProofWithPredAbstr() 5.526s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.084s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.621s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.150s passed
testMergeIndistinguishablePathConditionsWithITE() 4.194s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.166s passed

Standard output

683612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
683612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.5ns 
683612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683769     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
683769     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
683769     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
683769     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
684444     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
689014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.41s 
689061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
689061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 
704158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
704158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 476.6ns 
704158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.32s 
708528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
708779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 250.53ms 
708779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
708779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.2ns 
708779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.29s 
713122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
713122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.2ns 
722001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
722001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159ns 
722001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.37s 
726413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
727085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 610.52ms 
727085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
727085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.3ns 
727085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.42s 
731556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
732611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 974.44ms 
732611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
732611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.2ns 
732611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 
736761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
736777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 684.3ns 
736777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
736777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.8ns 
736777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.12s 
740911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
740911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 497ns 
740927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
740942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.8ns 
740942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
745289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.35s 
745336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
746513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1s 
746513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
746529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.6ms 
746529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.16s 
750707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
750707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 534ns 
750707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
750707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.3ns 
750707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
755008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.3s 
755102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
755102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.6ns 
763362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
763362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 632.2ns 
763377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
767747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.37s 
767779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
768685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 823.43ms