MergeRuleTests

11

tests

0

failures

0

ignored

1m7.70s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 11.178s passed
testDoAutomaticGcdProofWithMergePointStatements() 10.860s passed
testDoManualGcdProof() 18.468s passed
testLoadClosedGcdProofWithMergePointStatements() 3.971s passed
testLoadGcdProof() 3.846s passed
testLoadGcdProofWithPredAbstr() 4.017s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.516s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.158s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.829s passed
testMergeIndistinguishablePathConditionsWithITE() 2.945s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.909s passed

Standard output

434514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
434514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.2ns 
434529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434639     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
434639     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
434639     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
434639     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
435186     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
438219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.7s 
438266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
438266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
452992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
452992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.2ns 
452992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
455885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
456150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 264.78ms 
456150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
456150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.5ns 
456150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
459090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
459106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.5ns 
467328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
467328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.9ns 
467343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
470234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
470844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 582.95ms 
470844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
470844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.4ns 
470859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
473970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
474861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 841.37ms 
474861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
474861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.7ns 
474861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
477768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
477768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
477768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
477768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177ns 
477768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
480568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
480568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 545.9ns 
480599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
480599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.2ns 
480599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
483554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
484570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 971.51ms 
484570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
484570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.67ms 
484585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
487509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
487524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 610.2ns 
487524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
487524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361ns 
487524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
490402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
490402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 
498376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
498376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169ns 
498376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
501269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
502206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 897.39ms