MergeRuleTests

11

tests

0

failures

0

ignored

1m35.02s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 17.199s passed
testDoAutomaticGcdProofWithMergePointStatements() 16.450s passed
testDoManualGcdProof() 27.681s passed
testLoadClosedGcdProofWithMergePointStatements() 4.863s passed
testLoadGcdProof() 4.438s passed
testLoadGcdProofWithPredAbstr() 5.082s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.534s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.954s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.627s passed
testMergeIndistinguishablePathConditionsWithITE() 3.704s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.487s passed

Standard output

539652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
539652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 566.2ns 
539652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539808     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
539808     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
539808     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
539824     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
540449     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
544561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.91s 
544608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
544623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 
567329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
567329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.4ns 
567329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
570940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
571283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 337.97ms 
571283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
571283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.5ns 
571283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
574880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
574880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15ns 
588482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
588482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 585.1ns 
588482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 
592266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
593017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 696.45ms 
593017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
593017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 462.1ns 
593032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.93s 
597003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
598083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01s 
598099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
598099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 257.1ns 
598099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
601570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
601586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 941.2ns 
601586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
601586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.1ns 
601586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 
605182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
605182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 356ns 
605213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
605213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.3ns 
605213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.67s 
608934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
610060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09s 
610076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
610076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 502.5ns 
610076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.67s 
613780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
613780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 472.3ns 
613780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
613780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.5ns 
613780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
617315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
617315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.2ns 
630230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
630230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 636.4ns 
630245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
633794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
634669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 829.18ms