MergeRuleTests

11

tests

0

failures

0

ignored

1m23.57s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.196s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.624s passed
testDoManualGcdProof() 20.430s passed
testLoadClosedGcdProofWithMergePointStatements() 5.381s passed
testLoadGcdProof() 4.981s passed
testLoadGcdProofWithPredAbstr() 5.178s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.847s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.536s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.075s passed
testMergeIndistinguishablePathConditionsWithITE() 4.115s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.202s passed

Standard output

643383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
643383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.7ns 
643383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643540     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
643540     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
643540     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
643540     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
644102     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
648671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.29s 
648719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
648719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 
663820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
663820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.1ns 
663820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.21s 
668073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
668341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 261.39ms 
668356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
668356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.8ns 
668356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.33s 
672727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
672727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.8ns 
681553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
681553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156ns 
681555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.32s 
685921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
686399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 427.62ms 
686399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
686399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.1ns 
686399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
690889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.48s 
690920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
691561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 563.58ms 
691577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
691577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.1ns 
691577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.18s 
695779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
695779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 315.5ns 
695779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
695779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
695779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.02s 
699814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
699830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 233.5ns 
699854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
699854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 397.5ns 
699854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.41s 
704293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
705235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 860.85ms 
705235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
705235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.5ns 
705235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 
709334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
709334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 238.9ns 
709350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
709350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.7ns 
709350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.23s 
713620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
713620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.7ns 
721974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
721989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.08ms 
721989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.33s 
726361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
726955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 522.08ms