MergeRuleTests

11

tests

0

failures

0

ignored

1m58.31s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 19.231s passed
testDoAutomaticGcdProofWithMergePointStatements() 18.464s passed
testDoManualGcdProof() 31.033s passed
testLoadClosedGcdProofWithMergePointStatements() 6.972s passed
testLoadGcdProof() 6.736s passed
testLoadGcdProofWithPredAbstr() 7.004s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 6.552s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 6.067s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 5.414s passed
testMergeIndistinguishablePathConditionsWithITE() 5.348s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 5.486s passed

Standard output

844667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
844667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 475.7ns 
844667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
844886     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
844886     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
844886     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
844886     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
845715     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
851686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.03s 
851749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
851749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.7ns 
875715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
875715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.8ns 
875715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
881203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.49s 
881266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
881766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 484.72ms 
881766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
881766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.5ns 
881781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
887270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.5s 
887332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
887348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22ns 
900997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
900997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.1ns 
900997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
906624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.63s 
906687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
907549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 780.54ms 
907549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
907549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 549.8ns 
907549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
913287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.73s 
913333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
914553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11s 
914553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
914553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 514.4ns 
914568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
919992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.44s 
920023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
920039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.75ms 
920039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
920039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.4ns 
920039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
925391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.35s 
925422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
925422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 606.8ns 
925469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
925469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 559.8ns 
925469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
930957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.5s 
931019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
932411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24s 
932426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
932426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 530.1ns 
932426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
937742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.32s 
937758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
937774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 419.2ns 
937774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
937774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 463.8ns 
937774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
943152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.37s 
943199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
943199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.7ns 
956254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
956254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 616.3ns 
956254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
961850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.6s 
961912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
962975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 975.51ms