MergeRuleTests

11

tests

0

failures

0

ignored

1m57.10s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 19.623s passed
testDoAutomaticGcdProofWithMergePointStatements() 18.191s passed
testDoManualGcdProof() 31.033s passed
testLoadClosedGcdProofWithMergePointStatements() 6.889s passed
testLoadGcdProof() 6.628s passed
testLoadGcdProofWithPredAbstr() 6.792s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.148s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 6.039s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.368s passed
testMergeIndistinguishablePathConditionsWithITE() 5.138s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.248s passed

Standard output

804749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
804750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 441.7ns 
804751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
804961     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
804961     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
804961     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
804961     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
805750     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
811601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.85s 
811660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
811662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 
835783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
835784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.91ns 
835785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
841403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.62s 
841462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
841820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 351.11ms 
841823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
841823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 544.41ns 
841830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
847700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.87s 
847766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
847769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.8ns 
861446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
861446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 421.11ns 
861447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
866784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.34s 
866843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
867588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 669.57ms 
867593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
867593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.2ns 
867595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
873018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.42s 
873081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
874378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19s 
874385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
874385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
874386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
879592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.21s 
879619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
879630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 715.61ns 
879634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
879634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 432.81ns 
879635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
884943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.31s 
884967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
884970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 469.7ns 
885001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
885002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 727.61ns 
885003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
890445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.44s 
890501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
891878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28s 
891890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
891890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.7ns 
891891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
897004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.11s 
897024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
897026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 320ns 
897028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
897028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
897029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
902367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.34s 
902419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
902421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.3ns 
915219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
915219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.4ns 
915220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
920679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.46s 
920730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
921843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02s