MergeRuleTests

11

tests

0

failures

0

ignored

1m37.56s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 16.681s passed
testDoAutomaticGcdProofWithMergePointStatements() 16.087s passed
testDoManualGcdProof() 28.504s passed
testLoadClosedGcdProofWithMergePointStatements() 5.441s passed
testLoadGcdProof() 5.081s passed
testLoadGcdProofWithPredAbstr() 5.615s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.019s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.266s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.581s passed
testMergeIndistinguishablePathConditionsWithITE() 3.846s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.439s passed

Standard output

579107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
579107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 709ns 
579119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579322     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
579322     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
579322     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
579322     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
579979     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
584232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s 
584294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
584294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ns 
607605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
607605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.5ns 
607605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s 
611356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
611856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 498.52ms 
611872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
611872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.9ns 
611872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.67s 
615609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
615609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.5ns 
628553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
628553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.3ns 
628569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s 
632556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
633572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 979.01ms 
633572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
633572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.5ns 
633572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.96s 
637590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
639171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54s 
639187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
639187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 485.9ns 
639187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
642611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
642626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
642626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
642626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.4ns 
642626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
646176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
646192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.46ms 
646207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
646207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 757.3ns 
646223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.84s 
650101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
651648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49s 
651648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
651648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.7ns 
651663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.82s 
655494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
655494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 821.6ns 
655494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
655494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 417.7ns 
655510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
659012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
659012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.8ns 
671581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
671581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 445.8ns 
671581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.71s 
675333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
676662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28s