MergeRuleTests

11

tests

0

failures

0

ignored

1m12.34s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 12.304s passed
testDoAutomaticGcdProofWithMergePointStatements() 11.847s passed
testDoManualGcdProof() 20.377s passed
testLoadClosedGcdProofWithMergePointStatements() 3.988s passed
testLoadGcdProof() 3.955s passed
testLoadGcdProofWithPredAbstr() 4.080s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.751s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.269s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.734s passed
testMergeIndistinguishablePathConditionsWithITE() 2.974s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.065s passed

Standard output

448160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
448160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.6ns 
448160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448285     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
448285     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
448285     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
448285     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
448755     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
452037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.87s 
452084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
452084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.9ns 
468545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
468545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.4ns 
468545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
471517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
471814     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 298.43ms 
471814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
471814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.4ns 
471830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
474831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
474831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19ns 
484118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
484118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 472.1ns 
484118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
487217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
487870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 620.88ms 
487870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
487870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 425.1ns 
487885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
490950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
491950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 946.06ms 
491950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
491950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 455.5ns 
491950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
494999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
495015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
495015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
495015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.2ns 
495015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
497719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
497719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 608.5ns 
497750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
497750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.4ns 
497750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
500658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
501721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02s 
501737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
501737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.86ms 
501737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
504707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
504707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 677.5ns 
504707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
504707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.9ns 
504723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
507601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
507601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.3ns 
516558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
516558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.1ns 
516558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
519638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
520513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 826.96ms