MergeRuleTests

11

tests

0

failures

0

ignored

1m25.79s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.644s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.860s passed
testDoManualGcdProof() 23.171s passed
testLoadClosedGcdProofWithMergePointStatements() 5.175s passed
testLoadGcdProof() 5.456s passed
testLoadGcdProofWithPredAbstr() 5.074s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.659s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.967s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.612s passed
testMergeIndistinguishablePathConditionsWithITE() 3.715s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.456s passed

Standard output

553588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
553588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 537.2ns 
553588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553744     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
553744     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
553744     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
553744     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
554328     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
558290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.7s 
558337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
558353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.1ns 
576755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
576755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 544.5ns 
576755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
580403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
580723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 312.98ms 
580723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
580723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.1ns 
580738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 
584357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
584357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23ns 
594367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
594367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 571.4ns 
594367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 
598167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
599027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 837.92ms 
599043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
599043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 475.4ns 
599043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.8s 
602896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
604085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15s 
604101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
604101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 431ns 
604101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
607542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
607557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 995.8ns 
607557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
607557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133ns 
607557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
611137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
611153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 765.8ns 
611169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
611169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 522.8ns 
611169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.81s 
615037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
616329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24s 
616344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
616344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.8ns 
616344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.68s 
620044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
620044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 668.1ns 
620059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
620059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 472.1ns 
620059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
623626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
623704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.5ns 
633919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
633919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 645.7ns 
633919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 
637677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
639312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59s