MergeRuleTests

11

tests

0

failures

0

ignored

1m35.17s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.778s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.909s passed
testDoManualGcdProof() 27.644s passed
testLoadClosedGcdProofWithMergePointStatements() 5.413s passed
testLoadGcdProof() 5.330s passed
testLoadGcdProofWithPredAbstr() 5.712s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.386s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.872s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.220s passed
testMergeIndistinguishablePathConditionsWithITE() 3.360s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.541s passed

Standard output

529592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
529592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.6ns 
529592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529740     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
529740     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
529740     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
529740     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
530403     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
534241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.65s 
534288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
534288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
557227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
557227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 482.8ns 
557243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
560709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
561099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 392.19ms 
561099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
561099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
561099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
564696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
564758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.5ns 
577877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
577877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 532.1ns 
577877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
581387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
582264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 841.8ms 
582264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
582264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 449.8ns 
582279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 
586020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
587976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68s 
587976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
587976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.3ns 
587976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
591501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
591517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 890.7ns 
591517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
591517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 480.8ns 
591517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
594703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
594703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
594738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
594738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.3ns 
594740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
598320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
600134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76s 
600150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
600150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.33ms 
600150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
603510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
603510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 566.7ns 
603510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
603510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.7ns 
603510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s 
607250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
607265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.7ns 
619450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
619450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 453.8ns 
619450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.98s 
623480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
624670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09s