MergeRuleTests

11

tests

0

failures

0

ignored

1m22.49s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.156s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.615s passed
testDoManualGcdProof() 22.802s passed
testLoadClosedGcdProofWithMergePointStatements() 4.681s passed
testLoadGcdProof() 4.496s passed
testLoadGcdProofWithPredAbstr() 4.740s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.244s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.742s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.246s passed
testMergeIndistinguishablePathConditionsWithITE() 3.569s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.202s passed

Standard output

530930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
530930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 425.8ns 
530945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531079     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
531079     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
531079     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
531079     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
531702     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
535457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.52s 
535504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
535504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
553742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
553742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.9ns 
553742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
557172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
557485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 301.86ms 
557485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
557485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.4ns 
557485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
561054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
561054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.5ns 
571641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
571641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 453.3ns 
571641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
575230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
575886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 615.79ms 
575886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
575886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 431.5ns 
575886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.68s 
579626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
580611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 950.25ms 
580626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
580626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.8ns 
580626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
583812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
583828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 715.3ns 
583828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
583828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.4ns 
583828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
587058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
587058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 573.1ns 
587074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
587074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.1ns 
587089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
590654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
591739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06s 
591755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
591755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.05ms 
591755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
595324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
595324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 559.9ns 
595339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
595339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 421.1ns 
595339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
598689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
598689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.9ns 
608939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
608939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 466.6ns 
608954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
612496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
613435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 900.19ms