MergeRuleTests

11

tests

0

failures

0

ignored

1m42.99s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.633s passed
testDoAutomaticGcdProofWithMergePointStatements() 17.120s passed
testDoManualGcdProof() 30.713s passed
testLoadClosedGcdProofWithMergePointStatements() 5.685s passed
testLoadGcdProof() 5.224s passed
testLoadGcdProofWithPredAbstr() 5.292s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.501s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.241s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.020s passed
testMergeIndistinguishablePathConditionsWithITE() 3.831s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.732s passed

Standard output

602536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
602536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 561.8ns 
602536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602693     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
602693     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
602693     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
602693     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
603355     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
607824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.28s 
607871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
607871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
633247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
633247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 504.1ns 
633247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.91s 
637394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
638489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02s 
638489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
638489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 538.2ns 
638489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.97s 
642520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
642520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16ns 
655122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
655122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.9ns 
655122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.43s 
659622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
660623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 952.12ms 
660623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
660623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.1ns 
660639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.95s 
664628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
665915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24s 
665915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
665931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.13ms 
665931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s 
669647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
669647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
669647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
669647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 398ns 
669662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.96s 
673636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
673651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 547.8ns 
673667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
673667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.5ns 
673667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 
677904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
679336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38s 
679352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
679352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 392.2ns 
679352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.8s 
683167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
683183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 644.8ns 
683183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
683183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.5ns 
683183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
687162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.99s 
687289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
687289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.8ns 
700319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
700319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 566.5ns 
700319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s 
704286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
705527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21s