MergeRuleTests

11

tests

0

failures

0

ignored

1m55.17s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 18.454s passed
testDoAutomaticGcdProofWithMergePointStatements() 18.067s passed
testDoManualGcdProof() 29.953s passed
testLoadClosedGcdProofWithMergePointStatements() 7.260s passed
testLoadGcdProof() 6.549s passed
testLoadGcdProofWithPredAbstr() 6.794s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.307s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.855s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.218s passed
testMergeIndistinguishablePathConditionsWithITE() 5.410s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.306s passed

Standard output

901090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
901091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 790.9ns 
901092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
901319     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
901319     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
901320     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
901320     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
902336     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
908303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.21s 
908414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
908418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
931044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
931044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364ns 
931045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
936538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.49s 
936597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
936895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 291.81ms 
936898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
936898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.4ns 
936899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
942366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.47s 
942425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
942428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25ns 
955353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
955353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.9ns 
955354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
960805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.45s 
960860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
961656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 730.2ms 
961660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
961660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104ns 
961660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
967206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.55s 
967258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
968449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09s 
968453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
968453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.9ns 
968454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
973728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.27s 
973751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
973756     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 746.1ns 
973759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
973759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.4ns 
973760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
978919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.16s 
978942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
978944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 329.8ns 
978978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
978978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.2ns 
978979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
984724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.74s 
984782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
986228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34s 
986237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
986238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
986239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
991621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.38s 
991644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
991646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 288.2ns 
991647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
991648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
991648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
997200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.55s 
997251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
997253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.1ns 
1009714    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
1009715    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387ns 
1009716    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1015177    DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.46s 
1015227    INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
1016259    DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 930.87ms