MergeRuleTests

11

tests

0

failures

0

ignored

1m37.99s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.147s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.852s passed
testDoManualGcdProof() 23.717s passed
testLoadClosedGcdProofWithMergePointStatements() 6.081s passed
testLoadGcdProof() 6.124s passed
testLoadGcdProofWithPredAbstr() 5.808s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.663s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.222s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.932s passed
testMergeIndistinguishablePathConditionsWithITE() 4.705s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 4.739s passed

Standard output

707948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
707948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.4ns 
707949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708122     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
708123     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
708123     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
708123     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
708799     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
713877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.93s 
713927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
713929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 
731665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
731665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.7ns 
731666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
736558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.89s 
736603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
736885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 276.59ms 
736887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
736888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 562ns 
736897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
741819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.92s 
741866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
741869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.5ns 
752033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
752034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144ns 
752034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.92s 
757121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
757694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 515.13ms 
757698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
757698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 437.5ns 
757699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
762618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.92s 
762664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
763501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 749.07ms 
763504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
763505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns 
763505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
768218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.71s 
768239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
768242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 466.7ns 
768244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
768244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
768245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
773124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.88s 
773147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
773149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 322.1ns 
773176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
773176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.3ns 
773177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
778041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.86s 
778086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
779250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08s 
779257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
779257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.5ns 
779258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
783936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.68s 
783957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
783960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 484.2ns 
783962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
783962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.2ns 
783963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
789170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.21s 
789219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
789221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.7ns 
799814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
799814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.4ns 
799815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
804943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.13s 
804994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
805934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 856.07ms