MergeRuleTests

11

tests

0

failures

0

ignored

1m5.12s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 11.446s passed
testDoAutomaticGcdProofWithMergePointStatements() 10.773s passed
testDoManualGcdProof() 18.192s passed
testLoadClosedGcdProofWithMergePointStatements() 3.727s passed
testLoadGcdProof() 3.514s passed
testLoadGcdProofWithPredAbstr() 3.334s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 3.329s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.023s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 2.506s passed
testMergeIndistinguishablePathConditionsWithITE() 2.678s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 2.595s passed

Standard output

392930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
392930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
392930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393029     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
393029     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
393029     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
393029     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
393397     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
396429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
396471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
396473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.4ns 
411122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
411122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
411123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
413963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
414143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 177.31ms 
414145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
414145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.4ns 
414146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
416794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
416796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ns 
425601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
425602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.6ns 
425602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
428295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
428927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 545.13ms 
428929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
428929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
428930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
431755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
432260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 458.81ms 
432264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
432264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.4ns 
432265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
434842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
434858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 411.2ns 
434862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
434862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108ns 
434863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
437349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
437351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 204.9ns 
437368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
437368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
437369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
440045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
441085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 951.59ms 
441096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
441098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.73ms 
441099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
443771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
443773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 372ns 
443774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
443774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
443774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
446413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
446415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ns 
454548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
454548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 475.9ns 
454552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
457407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
458011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 562.67ms