MergeRuleTests

11

tests

0

failures

0

ignored

1m1.05s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 10.105s passed
testDoAutomaticGcdProofWithMergePointStatements() 9.887s passed
testDoManualGcdProof() 16.716s passed
testLoadClosedGcdProofWithMergePointStatements() 3.600s passed
testLoadGcdProof() 3.417s passed
testLoadGcdProofWithPredAbstr() 3.546s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.197s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 2.881s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.499s passed
testMergeIndistinguishablePathConditionsWithITE() 2.707s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.499s passed

Standard output

397933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
397933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.8ns 
397933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398053     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
398053     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
398053     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
398053     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
398325     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
401006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
401037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
401037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.7ns 
414641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
414641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 397.3ns 
414641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
417264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
417514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 250.39ms 
417514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
417514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.7ns 
417530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
420108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
420108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.4ns 
427627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
427627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.3ns 
427627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
430277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
430809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 503.94ms 
430824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
430824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 
430824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
433652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
434370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 673.13ms 
434370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
434370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.1ns 
434370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
436867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
436867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 569.1ns 
436867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
436867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.6ns 
436867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
439337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
439353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 377.8ns 
439368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
439368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.8ns 
439368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
442192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
442968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 744.99ms 
442968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
442968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.8ns 
442968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
445682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
445682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 439.8ns 
445682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
445682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348ns 
445682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
448247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
448247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.2ns 
455563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
455563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.9ns 
455563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
458209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
458980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 730.38ms