MergeRuleTests

11

tests

0

failures

0

ignored

1m43.14s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.244s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.630s passed
testDoManualGcdProof() 26.252s passed
testLoadClosedGcdProofWithMergePointStatements() 6.155s passed
testLoadGcdProof() 5.864s passed
testLoadGcdProofWithPredAbstr() 6.408s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.002s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.392s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.146s passed
testMergeIndistinguishablePathConditionsWithITE() 5.058s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.989s passed

Standard output

748393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
748393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.9ns 
748394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748592     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
748593     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
748594     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
748594     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
749494     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
754813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.42s 
754873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
754876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 
774645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
774645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.3ns 
774645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
779701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.06s 
779752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
780035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 277.05ms 
780037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
780038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.61ns 
780039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
785129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.09s 
785180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
785183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.1ns 
796281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
796282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.7ns 
796282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
801546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.26s 
801598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
802281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 624.73ms 
802283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
802283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104ns 
802284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
807528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.24s 
807578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
808688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02s 
808691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
808691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
808692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
813653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.96s 
813675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
813677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 484.31ns 
813679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
813679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
813680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
818777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 
818796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
818798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 305.4ns 
818826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
818826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.8ns 
818827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
823862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.04s 
823906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
824973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 981.49ms 
824982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
824982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.7ns 
824983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
830014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 
830035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
830037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 306.2ns 
830039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
830039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
830040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
835116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.08s 
835164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
835166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.9ns 
845669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
845669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.4ns 
845670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
850563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 
850609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
851529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 840.71ms