MergeRuleTests

11

tests

0

failures

0

ignored

1m11.67s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 11.960s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.414s passed
testDoManualGcdProof() 19.562s passed
testLoadClosedGcdProofWithMergePointStatements() 4.093s passed
testLoadGcdProof() 3.992s passed
testLoadGcdProofWithPredAbstr() 4.023s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.761s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.140s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.733s passed
testMergeIndistinguishablePathConditionsWithITE() 3.128s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.864s passed

Standard output

465328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
465328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.6ns 
465328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465426     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
465426     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
465426     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
465426     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
465860     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
469109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.78s 
469156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
469156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ns 
484884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
484884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 471.2ns 
484884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
487774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
488024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 237.92ms 
488024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
488024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 388.8ns 
488024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
491011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
491011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.9ns 
499985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
499985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.3ns 
499985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
503179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
503746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 534.34ms 
503746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
503746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.1ns 
503746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
506955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
507769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 767.8ms 
507769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
507769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.1ns 
507769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
510631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
510631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 573ns 
510631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
510631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.2ns 
510647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
513351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
513351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 532.9ns 
513367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
513367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.9ns 
513367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
516540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
517460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 881.28ms 
517460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
517475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.42ms 
517475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
520588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
520588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 593.5ns 
520588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
520588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.3ns 
520588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
523610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
523626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19ns 
533034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
533034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136ns 
533034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
536125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
536994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 701.52ms