MergeRuleTests

11

tests

0

failures

0

ignored

1m35.89s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.232s passed
testDoAutomaticGcdProofWithMergePointStatements() 16.665s passed
testDoManualGcdProof() 27.083s passed
testLoadClosedGcdProofWithMergePointStatements() 5.351s passed
testLoadGcdProof() 5.408s passed
testLoadGcdProofWithPredAbstr() 5.229s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.676s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.276s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.529s passed
testMergeIndistinguishablePathConditionsWithITE() 3.817s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.623s passed

Standard output

570596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
570596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
570597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570743     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
570743     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
570744     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
570744     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
571342     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
575384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.79s 
575432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
575433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 
597680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
597681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 389.9ns 
597682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.91s 
601649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
601954     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 300.89ms 
601956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
601957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 423.9ns 
601958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s 
605923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
605925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.2ns 
618188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
618188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
618189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 
621889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
622861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 924.78ms 
622864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
622865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.7ns 
622866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 
626785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
628089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24s 
628093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
628093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.9ns 
628094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
631711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
631714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
631716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
631716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
631716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
635216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
635219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 608.9ns 
635244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
635244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.6ns 
635245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.83s 
639130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
640586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38s 
640596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
640596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.5ns 
640597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 
644409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
644411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 633.2ns 
644412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
644412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
644413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.01s 
648477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
648480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.3ns 
661079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
661079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.8ns 
661080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.82s 
664981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
666482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4s