MergeRuleTests

11

tests

0

failures

0

ignored

1m38.82s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.057s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.141s passed
testDoManualGcdProof() 24.819s passed
testLoadClosedGcdProofWithMergePointStatements() 6.190s passed
testLoadGcdProof() 5.952s passed
testLoadGcdProofWithPredAbstr() 5.987s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.667s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.218s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.941s passed
testMergeIndistinguishablePathConditionsWithITE() 4.973s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.876s passed

Standard output

779217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
779217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.8ns 
779218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
779410     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
779410     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
779410     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
779411     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
780154     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
785723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.51s 
785770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
785772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
804037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
804037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.7ns 
804038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
808972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.93s 
809018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
809252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 229.99ms 
809254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
809254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
809260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
814319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.06s 
814366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
814368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.3ns 
824311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
824311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 772.3ns 
824312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
829338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.03s 
829383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
829975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 534.26ms 
829978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
829978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.9ns 
829979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
835120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.14s 
835162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
835961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 711.6ms 
835965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
835965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
835965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
840817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.85s 
840836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
840839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 410.7ns 
840841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
840841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
840841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
845735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 
845754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
845756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 377.6ns 
845782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
845782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.3ns 
845783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
850927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.14s 
850971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
851964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 910.46ms 
851972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
851972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
851972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
856923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.95s 
856941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
856943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 260.3ns 
856944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
856944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
856945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
862000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.05s 
862045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
862047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.1ns 
872086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
872086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.7ns 
872086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
877186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 
877230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
878035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 720.69ms