MergeRuleTests

11

tests

0

failures

0

ignored

1m19.13s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 12.331s passed
testDoAutomaticGcdProofWithMergePointStatements() 11.849s passed
testDoManualGcdProof() 19.766s passed
testLoadClosedGcdProofWithMergePointStatements() 4.941s passed
testLoadGcdProof() 4.673s passed
testLoadGcdProofWithPredAbstr() 4.787s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.640s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 4.339s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.868s passed
testMergeIndistinguishablePathConditionsWithITE() 3.943s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.992s passed

Standard output

616893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
616893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.8ns 
616893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617049     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
617049     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
617049     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
617049     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
617609     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
621950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.05s 
621981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
621981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 
636652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
636652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.4ns 
636652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.04s 
640741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
640991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 245.8ms 
640991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
640991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.1ns 
640991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.11s 
645155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
645155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.7ns 
653322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
653322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 417.2ns 
653322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.05s 
657413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
657963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 411.57ms 
657963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
657963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.8ns 
657963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
662083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.11s 
662114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
662750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 549.34ms 
662750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
662750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.4ns 
662750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
666711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.96s 
666727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
666727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 325.2ns 
666742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
666742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.9ns 
666742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
670578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.84s 
670594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
670594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 216.4ns 
670625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
670625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.7ns 
670629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
674737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.11s 
674768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
675536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 689.51ms 
675551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
675551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.3ns 
675551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.92s 
679478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
679494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 202.3ns 
679494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
679494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.4ns 
679494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.93s 
683462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
683462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.1ns 
691343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
691343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.6ns 
691343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.98s 
695367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
696016     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 571.97ms