MergeRuleTests

11

tests

0

failures

0

ignored

1m29.93s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.672s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.045s passed
testDoManualGcdProof() 25.790s passed
testLoadClosedGcdProofWithMergePointStatements() 5.014s passed
testLoadGcdProof() 4.747s passed
testLoadGcdProofWithPredAbstr() 5.025s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.463s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.929s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.351s passed
testMergeIndistinguishablePathConditionsWithITE() 3.592s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.299s passed

Standard output

528572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
528572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
528573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528718     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
528718     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
528719     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
528719     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
529319     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
533214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.64s 
533264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
533267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 
554362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
554363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.9ns 
554363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
557976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
558289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 307.17ms 
558294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
558294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 421.4ns 
558295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
561890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
561892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.1ns 
573965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
573966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.3ns 
573967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 
577591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
578424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 800.81ms 
578428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
578428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.4ns 
578430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.61s 
582083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
583449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31s 
583452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
583452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
583453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
586747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
586750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
586751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
586752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
586752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
590075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
590078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 679.9ns 
590102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
590103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.2ns 
590103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
593660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
593712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
595109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35s 
595117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
595118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.6ns 
595119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 
598705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
598707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 642.7ns 
598709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
598709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.6ns 
598709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
602208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
602210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ns 
613754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
613754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.5ns 
613754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
617266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
618497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18s