MergeRuleTests

11

tests

0

failures

0

ignored

1m31.89s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.761s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.012s passed
testDoManualGcdProof() 25.752s passed
testLoadClosedGcdProofWithMergePointStatements() 5.190s passed
testLoadGcdProof() 4.926s passed
testLoadGcdProofWithPredAbstr() 5.659s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.737s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.909s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.549s passed
testMergeIndistinguishablePathConditionsWithITE() 3.737s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.659s passed

Standard output

604651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
604651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.7ns 
604651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604932     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
604932     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
604932     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
604932     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
605573     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
609513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.86s 
609560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
609560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
630398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
630398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.2ns 
630398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
633978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
634291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 313.65ms 
634307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
634307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 396.5ns 
634307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
637918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
637918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.8ns 
650068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
650068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 459ns 
650084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 
653774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
654805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 992.5ms 
654821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
654821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139ns 
654821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.04s 
658901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
660464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51s 
660464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
660464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.7ns 
660480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.62s 
664123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
664123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 952.3ns 
664123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
664123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.8ns 
664123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
667641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
667657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 659.8ns 
667672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
667672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.1ns 
667688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
671331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
672847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47s 
672878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
672878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 711.4ns 
672878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.69s 
676584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
676599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 685.1ns 
676599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
676599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.9ns 
676599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
680149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
680149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.5ns 
691611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
691611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 540ns 
691611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.63s 
695286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
696537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19s