MergeRuleTests

11

tests

0

failures

0

ignored

1m13.25s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 12.230s passed
testDoAutomaticGcdProofWithMergePointStatements() 12.198s passed
testDoManualGcdProof() 20.949s passed
testLoadClosedGcdProofWithMergePointStatements() 4.059s passed
testLoadGcdProof() 3.833s passed
testLoadGcdProofWithPredAbstr() 3.912s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.551s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.523s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.919s passed
testMergeIndistinguishablePathConditionsWithITE() 3.094s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.978s passed

Standard output

489218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
489218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns 
489219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489335     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
489335     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
489335     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
489335     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
489839     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
493262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.04s 
493300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
493302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ns 
510167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
510167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 458.9ns 
510168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
513490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
513687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 194.42ms 
513690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
513690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.9ns 
513691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
516869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
516871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.2ns 
525919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
525920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.4ns 
525921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
529046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
529467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 393.35ms 
529470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
529470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299ns 
529471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
532646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
533380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 691.43ms 
533382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
533383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
533383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
536357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
536359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 360ns 
536360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
536361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
536361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
539255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
539257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 339.8ns 
539279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
539279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.9ns 
539280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
542524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
543331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 765.08ms 
543338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
543338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.5ns 
543339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
546428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
546430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 231.1ns 
546433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
546433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.6ns 
546434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
549617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
549619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16ns 
558630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
558630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128ns 
558631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
561832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
562460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 558.89ms