MergeRuleTests

11

tests

0

failures

0

ignored

1m13.37s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.518s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.498s passed
testDoManualGcdProof() 19.865s passed
testLoadClosedGcdProofWithMergePointStatements() 4.305s passed
testLoadGcdProof() 4.127s passed
testLoadGcdProofWithPredAbstr() 3.837s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.542s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.226s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.775s passed
testMergeIndistinguishablePathConditionsWithITE() 2.735s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.946s passed

Standard output

465134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
465134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 663.5ns 
465134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465243     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
465243     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
465243     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
465243     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
465816     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
468929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 
468969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
468971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 
485008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
485008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.7ns 
485008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
487952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
488218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 261.54ms 
488218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
488218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.7ns 
488218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
491477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
491633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.2ns 
501736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
501736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.9ns 
501736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
504682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
505278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 567.39ms 
505278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
505278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 450.9ns 
505278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
508255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
509115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 824.29ms 
509115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
509115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 420.6ns 
509115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
512060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
512060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 809.2ns 
512060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
512060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.5ns 
512060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
514821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
514821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 563.1ns 
514836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
514836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 428.8ns 
514836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
517863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
519141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25s 
519157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
519157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.4ns 
519157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
521878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
521878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 560.2ns 
521878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
521878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 420.7ns 
521894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
524839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
524854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.4ns 
534375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
534375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.5ns 
534375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
537673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
538486     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 789.06ms