MergeRuleTests

11

tests

0

failures

0

ignored

1m40.77s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 17.701s passed
testDoAutomaticGcdProofWithMergePointStatements() 16.606s passed
testDoManualGcdProof() 29.778s passed
testLoadClosedGcdProofWithMergePointStatements() 5.503s passed
testLoadGcdProof() 5.019s passed
testLoadGcdProofWithPredAbstr() 5.550s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.084s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.158s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.690s passed
testMergeIndistinguishablePathConditionsWithITE() 3.675s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.002s passed

Standard output

573771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
573771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 493.9ns 
573771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573930     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
573930     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
573930     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
573930     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
574616     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
578853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.07s 
578900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
578915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ns 
603547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
603547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.8ns 
603563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 
607331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
607706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 362.67ms 
607706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
607706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 449.8ns 
607722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s 
611662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
611662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.7ns 
625407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
625407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.9ns 
625423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s 
629362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
630491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1s 
630507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
630507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 563.1ns 
630507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.99s 
634556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
636041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42s 
636057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
636057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.3ns 
636057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.95s 
640028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
640043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
640043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
640043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.6ns 
640043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 
643686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
643686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
643733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
643733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.1ns 
643733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.88s 
647673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
649221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5s 
649236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
649236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3ms 
649236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 
652911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
652911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 932.3ns 
652911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
652911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.9ns 
652926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
656367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
656460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
656460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.7ns 
669517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
669517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 438.9ns 
669517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 
673223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
674536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27s