MergeRuleTests

11

tests

0

failures

0

ignored

1m22.52s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.056s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.729s passed
testDoManualGcdProof() 22.945s passed
testLoadClosedGcdProofWithMergePointStatements() 4.637s passed
testLoadGcdProof() 4.556s passed
testLoadGcdProofWithPredAbstr() 4.731s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.238s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.621s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.426s passed
testMergeIndistinguishablePathConditionsWithITE() 3.275s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.310s passed

Standard output

516462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
516462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
516463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516587     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
516588     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
516588     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
516588     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
517147     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
520925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.46s 
520971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
520973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ns 
539408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
539408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.4ns 
539409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
542774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
543026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 245.58ms 
543028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
543029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323ns 
543030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 
546614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
546616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17ns 
557086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
557087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.8ns 
557088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
560581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
561320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.72ms 
561324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
561324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.3ns 
561325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
564788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
566051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2s 
566055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
566055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.2ns 
566056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
569359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
569362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 931.71ns 
569363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
569363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
569365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
572763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
572765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 640.61ns 
572790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
572790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.6ns 
572790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
576156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
577420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22s 
577427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
577427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
577427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
580698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
580701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 585.81ns 
580702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
580702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
580703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
584192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
584194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.5ns 
594431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
594431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104ns 
594431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
597952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
598984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 985.29ms