MergeRuleTests

11

tests

0

failures

0

ignored

1m42.15s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 15.406s passed
testDoAutomaticGcdProofWithMergePointStatements() 15.528s passed
testDoManualGcdProof() 25.617s passed
testLoadClosedGcdProofWithMergePointStatements() 6.632s passed
testLoadGcdProof() 6.200s passed
testLoadGcdProofWithPredAbstr() 6.607s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 5.722s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 5.146s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 4.939s passed
testMergeIndistinguishablePathConditionsWithITE() 5.159s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.189s passed

Standard output

793748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.key 
793748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.8ns 
793749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
793943     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
793943     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
793944     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
793944     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
794802     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
800355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.61s 
800405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
800407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ns 
819366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/A.differentVarsWithSameName.MPS.cut.closed.proof 
819366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.9ns 
819367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
824173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.81s 
824220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
824510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 284.22ms 
824512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.MPSAndBlockContract.key 
824513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.5ns 
824518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
829280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.76s 
829331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
829334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29ns 
839920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateAbstractionWithUserChoices.proof 
839920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.9ns 
839922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
844936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.01s 
844978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
845638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 595.09ms 
845642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.predicateabstraction.proof 
845642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 342.2ns 
845643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
851076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.43s 
851133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
852244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 867.85ms 
852248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.twoJoins.proof 
852248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
852249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
857412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.16s 
857432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
857435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 406.7ns 
857437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
857437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
857437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
862320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.88s 
862340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
862343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 316.9ns 
862376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.closed.proof 
862376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.9ns 
862377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
867879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.5s 
867926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
868999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 989.63ms 
869008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/IndistinguishablePathConditions.proof 
869008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.6ns 
869009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
874144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.14s 
874162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
874165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 292.7ns 
874166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.mergePointStatements.key 
874167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
874167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
879286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.12s 
879333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
879336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.7ns 
889695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/merge/gcd.closed.proof 
889695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.1ns 
889696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
894896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.2s 
894945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
895892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 865.21ms