MergeRuleTests

11

tests

0

failures

0

ignored

1m12.83s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 11.984s passed
testDoAutomaticGcdProofWithMergePointStatements() 11.571s passed
testDoManualGcdProof() 20.662s passed
testLoadClosedGcdProofWithMergePointStatements() 4.241s passed
testLoadGcdProof() 4.073s passed
testLoadGcdProofWithPredAbstr() 4.258s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.768s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.291s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.956s passed
testMergeIndistinguishablePathConditionsWithITE() 3.010s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.020s passed

Standard output

463072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
463072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
463072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463182     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
463182     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
463182     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
463183     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
463623     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
466975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.9s 
467017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
467019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 
483733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
483733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.2ns 
483734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
486787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
487023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 231.74ms 
487025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
487025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.9ns 
487026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
490103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
490105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.5ns 
499009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
499010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.9ns 
499011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
502121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
502774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 622.91ms 
502777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
502777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
502778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
506083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
507031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 899.3ms 
507034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
507035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.5ns 
507035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
510051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
510053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 888.41ns 
510055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
510055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
510055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
512988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
512990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 588.81ns 
513011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
513011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.2ns 
513012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
516215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
517244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 981.79ms 
517252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
517252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.81ns 
517253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
520257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
520260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 651.11ns 
520262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
520262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.81ns 
520263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
523441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
523442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ns 
531833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
531833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.9ns 
531834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
535006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
535903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 853.3ms