MergeRuleTests

11

tests

0

failures

0

ignored

1m32.58s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.200s passed
testDoAutomaticGcdProofWithMergePointStatements() 14.760s passed
testDoManualGcdProof() 26.912s passed
testLoadClosedGcdProofWithMergePointStatements() 5.580s passed
testLoadGcdProof() 4.687s passed
testLoadGcdProofWithPredAbstr() 5.267s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.858s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.298s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.553s passed
testMergeIndistinguishablePathConditionsWithITE() 3.613s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.852s passed

Standard output

548259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
548259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.8ns 
548259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548477     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
548477     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
548478     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
548478     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
549272     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
553491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.23s 
553583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
553605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.9ns 
575171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
575171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
575171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.97s 
579186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
579467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 277.88ms 
579469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
579469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364ns 
579470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.53s 
583076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
583079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.8ns 
594669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
594670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 406.7ns 
594673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 
598419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
599524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04s 
599528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
599529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395ns 
599530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
603252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.72s 
603298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
604789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33s 
604803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
604803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.9ns 
604804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.82s 
608649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
608652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 627.9ns 
608655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
608655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 476.4ns 
608656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
612154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
612163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 352.6ns 
612207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
612212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 5.57ms 
612213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.79s 
616063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
617774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61s 
617788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
617788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 549.9ns 
617789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 
621394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
621397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 466.7ns 
621399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
621399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
621400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.85s 
625304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
625306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16ns 
636160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
636160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.2ns 
636161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
639677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
640842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06s