MergeRuleTests

11

tests

0

failures

0

ignored

1m19.40s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.441s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.534s passed
testDoManualGcdProof() 21.759s passed
testLoadClosedGcdProofWithMergePointStatements() 4.404s passed
testLoadGcdProof() 4.134s passed
testLoadGcdProofWithPredAbstr() 4.136s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.014s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.823s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.243s passed
testMergeIndistinguishablePathConditionsWithITE() 3.476s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.434s passed

Standard output

525862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
525862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.6ns 
525862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525987     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
525987     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
525987     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
525987     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
526644     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
530277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.41s 
530324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
530324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
547616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
547616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 464.5ns 
547616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
551127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
551440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 310.91ms 
551440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
551455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 500.6ns 
551455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
554914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
554914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.8ns 
564881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
564881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.8ns 
564881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
568426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
568895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 440.77ms 
568911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
568911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.3ns 
568911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
572390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
573015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 574.86ms 
573031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
573031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 443.4ns 
573031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
576465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
576465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 332.5ns 
576465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
576465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384.8ns 
576481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
579693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
579693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 244ns 
579708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
579708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.8ns 
579708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 
583321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
584112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 739.16ms 
584112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
584112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 451.9ns 
584128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
587588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
587588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 275ns 
587588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
587588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.7ns 
587588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
590944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
590944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.5ns 
601122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
601122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 516.9ns 
601122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
604610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
605240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 601.22ms