MergeRuleTests

11

tests

0

failures

0

ignored

1m21.27s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 12.860s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.546s passed
testDoManualGcdProof() 21.945s passed
testLoadClosedGcdProofWithMergePointStatements() 5.174s passed
testLoadGcdProof() 4.694s passed
testLoadGcdProofWithPredAbstr() 4.861s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.373s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.020s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.689s passed
testMergeIndistinguishablePathConditionsWithITE() 3.533s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.570s passed

Standard output

544784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
544784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119ns 
544785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544916     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
544917     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
544917     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
544917     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
545561     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
549599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.81s 
549643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
549645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
566730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
566730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.4ns 
566731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 
570438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
570743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 301.86ms 
570750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
570751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350ns 
570753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 
574459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
574461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.9ns 
583610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
583611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.3ns 
583612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
587257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
587980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 691.23ms 
587983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
587983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.2ns 
587984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.71s 
591744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
592841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05s 
592844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
592845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.4ns 
592846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 
596409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
596412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
596415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
596415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
596416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 
600075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
600078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 630.2ns 
600103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
600103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.7ns 
600104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s 
603836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
605270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39s 
605277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
605277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
605278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
608806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
608808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 590.4ns 
608810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
608810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
608811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
612365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
612367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.3ns 
621356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
621356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
621357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.62s 
625021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
626047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 985.7ms