MergeRuleTests

11

tests

0

failures

0

ignored

1m23.35s

duration

100%

successful

Tests

Test Duration Result
testDoAutomaticGcdProofWithMergePointStatementAndBlockContract() 14.152s passed
testDoAutomaticGcdProofWithMergePointStatements() 13.540s passed
testDoManualGcdProof() 23.203s passed
testLoadClosedGcdProofWithMergePointStatements() 4.908s passed
testLoadGcdProof() 4.550s passed
testLoadGcdProofWithPredAbstr() 4.800s passed
testLoadGcdProofWithPredAbstrAndUserChoices() 4.377s passed
testLoadProofWithDiffVarsWithSameNameAndMPS() 3.830s passed
testMergeIndistinguishablePathConditionsWithFullAnonymization() 3.158s passed
testMergeIndistinguishablePathConditionsWithITE() 3.237s passed
testMergeThreeIndistinguishablePathConditionsWithITE() 3.597s passed

Standard output

512406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.key 
512421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 552.7ns 
512421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512562     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
512562     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
512562     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
512562     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
513047     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
516830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.41s 
516878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
516878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
535622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\A.differentVarsWithSameName.MPS.cut.closed.proof 
535622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.9ns 
535622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
539139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof A[A::m(boolean)].JML operation contract.0 
539436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 306.02ms 
539452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.MPSAndBlockContract.key 
539452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.7ns 
539452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
542923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPSAndBlockContract(int,int)].JML normal_behavior operation contract.0 
542939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16ns 
553604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateAbstractionWithUserChoices.proof 
553604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174ns 
553604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.58s 
557231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
557981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 709.03ms 
557981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.predicateabstraction.proof 
557997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.4ns 
557997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 
561702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
562765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01s 
562781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.twoJoins.proof 
562781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 442.2ns 
562781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 
566378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.twoJoins.proof 
566378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
566393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
566393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.9ns 
566393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
569505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
569505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 658.5ns 
569536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.closed.proof 
569536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.7ns 
569536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
573084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
574444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31s 
574444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\IndistinguishablePathConditions.proof 
574460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.25ms 
574460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
577681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof IndistinguishablePathConditions.proof 
577681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 757.5ns 
577696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.mergePointStatements.key 
577696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.8ns 
577696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
581090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcdMPS(int,int)].JML normal_behavior operation contract.0 
581090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.2ns 
591221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\merge\gcd.closed.proof 
591221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.8ns 
591221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.39s 
594770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Gcd[Gcd::gcd(int,int)].JML normal_behavior operation contract.0 
595755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 941.53ms