MergeRuleTests

11

tests

0

failures

0

ignored

1m26.18s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.042s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.446s passed
testDoManualGcdProof() 23.641s passed
testLoadClosedGcdProofWithMergePointStatements() 4.801s passed
testLoadGcdProof() 4.690s passed
testLoadGcdProofWithPredAbstr() 4.752s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.456s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.863s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.347s passed
testMergeIndistinguishablePathConditionsWithITE() 3.518s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.627s passed

Standard output

527090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
527090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.3ns 
527090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527230     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
527230     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
527230     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
527230     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
527730     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
531639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.55s 
531685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
531685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.6ns 
550725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
550725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.7ns 
550725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
554260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
554588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 308.25ms 
554588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
554588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.4ns 
554588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
558263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
558263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.3ns 
569630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
569630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.2ns 
569630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.65s 
573336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
574086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 718.83ms 
574102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
574102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.8ns 
574102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 
577713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
578838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08s 
578854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
578854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.9ns 
578854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.59s 
582465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
582465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
582465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
582465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176ns 
582465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
585781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
585781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 616.7ns 
585812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
585812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166ns 
585812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
589379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
590598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17s 
590613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
590613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.3ns 
590613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
594116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
594131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 920.7ns 
594131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
594131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.8ns 
594131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
597540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
597540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.9ns 
608577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
608577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.4ns 
608577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
612127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
613252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07s