MergeRuleTests

11

tests

0

failures

0

ignored

1m24.22s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 13.586s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.992s passed
testDoManualGcdProof() 21.848s passed
testLoadClosedGcdProofWithMergePointStatements() 5.095s passed
testLoadGcdProof() 4.737s passed
testLoadGcdProofWithPredAbstr() 5.032s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.659s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.423s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.877s passed
testMergeIndistinguishablePathConditionsWithITE() 3.940s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.034s passed

Standard output

614515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
614515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.9ns 
614515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614655     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
614655     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
614655     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
614655     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
615203     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
619580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.07s 
619642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
619642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
636355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
636355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.5ns 
636355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 
640497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
640778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 265.95ms 
640778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
640778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124ns 
640778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 
644906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
644906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19ns 
654364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
654364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.5ns 
654380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.08s 
658492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
659023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 482.29ms 
659023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
659023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117ns 
659039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.22s 
663289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
664055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 684.86ms 
664055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
664071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 779.4ns 
664071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4s 
668074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
668089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 832.6ns 
668089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
668089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.4ns 
668089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.83s 
671935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
671935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 331.1ns 
671966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
671966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 444.6ns 
671966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.16s 
676171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
677046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 801.99ms 
677061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
677061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.3ns 
677061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s 
681001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
681001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 277.8ns 
681001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
681001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.3ns 
681001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s 
684972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
684972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.4ns 
693993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
693993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221ns 
693993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.03s 
698073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
698714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 582.88ms