MergeRuleTests

11

tests

0

failures

0

ignored

1m24.83s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.165s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.667s passed
testDoManualGcdProof() 20.754s passed
testLoadClosedGcdProofWithMergePointStatements() 5.274s passed
testLoadGcdProof() 5.055s passed
testLoadGcdProofWithPredAbstr() 5.283s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.051s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.672s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.315s passed
testMergeIndistinguishablePathConditionsWithITE() 4.321s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.275s passed

Standard output

659008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
659008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.4ns 
659008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659173     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
659173     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
659173     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
659173     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
659762     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
664427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.41s 
664473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
664473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ns 
679769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
679769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.2ns 
679769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.38s 
684189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
684441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 242.32ms 
684441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
684441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118ns 
684441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.36s 
688859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
688862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.8ns 
697607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
697608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.5ns 
697610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
702109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.51s 
702172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
702657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 434.63ms 
702657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
702657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.6ns 
702657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
707237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.57s 
707268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
707940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 581ms 
707940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
707940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.1ns 
707940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.26s 
712215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
712215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 347.9ns 
712215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
712215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.1ns 
712215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.26s 
716499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
716499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 281.3ns 
716530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
716530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.9ns 
716530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.42s 
720991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
721789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 733.75ms 
721804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
721804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.01ms 
721804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.29s 
726125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
726125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 234.7ns 
726125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
726125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.4ns 
726125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 
730390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
730390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.7ns 
738792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
738792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 632.1ns 
738792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.31s 
743150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
743847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 628.65ms