MergeRuleTests

11

tests

0

failures

0

ignored

1m18.55s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.275s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.077s passed
testDoManualGcdProof() 22.379s passed
testLoadClosedGcdProofWithMergePointStatements() 5.139s passed
testLoadGcdProof() 4.182s passed
testLoadGcdProofWithPredAbstr() 4.669s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.604s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.322s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.764s passed
testMergeIndistinguishablePathConditionsWithITE() 3.021s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.121s passed

Standard output

468306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
468306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.8ns 
468306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468431     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
468431     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
468431     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
468431     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
468996     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
472388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 
472435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
472451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.3ns 
490692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
490692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.5ns 
490708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
493691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
494014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 315.13ms 
494014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
494014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148ns 
494014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
497371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
497371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.7ns 
507291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
507291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204ns 
507293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
510236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
510893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 636.98ms 
510909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
510909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 476.5ns 
510909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
514095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
515565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32s 
515580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
515580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 468.7ns 
515580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
518681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
518697     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 938ns 
518697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
518697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.3ns 
518697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
521433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
521433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 773.5ns 
521464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
521464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.1ns 
521464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
524616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
526554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85s 
526601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
526601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 760.8ns 
526601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
529608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
529623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 713ns 
529623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
529623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 409.2ns 
529623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
532565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
532580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.4ns 
542700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
542700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.1ns 
542700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
545911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
546882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 945.97ms