| Subject | XML-security (1.0.4) from SIR with 92 junit tests | |||||||||||||||
| Scenario | Test
No. 66 passed in the fixed code of version1-seed2 but failed in the buggy
code; case study was performed on the buggy code. |
|||||||||||||||
| The full sequence of events (in terms of Jimple IR statement ids); * indicateds subsequence corresponding to detailed change propagation via helper function invocations, which are added up to the landmark sequence to make this full sequence of events) |
5621
( the original value of name=="xmlns" || value==""
changed from false to true, causing the removal of the key "xmlns"
) -> 5622 ( the removal of key "xmlns" from the inscopeNamespaces map ) -> *5624, 5625, 5626, 5627, 5628 ( indirectly affected by the condition change in 5621, causing addition of key:value pair that should not be added) -> *5646,5647,5648,5649,5650,5651,5652,5653,5654,5655 (affected by change in the inscopeNamespace map, causing change in pairs fetched from the map then eventually causing the change in the return value of the enclosing method – the ns list) -> *5357,5358,5359,5360,5361,5362,5364,5365, 5667,5668,5669,5670, 5676,5677,7812,7813,7814,7815,7816,7817,7818,7819,7820 ( above change affected parameters passed to helper functions “utilizedOrIncluded”, “namespaceIsRelative” and helper class “CanonicalizationException”, which caused condition changes that in turn affected the eventual return value of the enclosing method – the ns list) -> *5687,5688,5689,5690 (the propagation of change in the inscopeNamespace map to the ns list) -> 5691 ( ns changed ) -> 5699 ( ns sorted ) -> *5476,5477,5501,5502,5503,5504,5566,5567,5568,5569,5571,5572,5573,5574,5575,5576,5577,5578,5579,5585,5586,5587,5588,5589,5590, 5593 (above changes affected parameters passed to helper function “getAttrs” to propagate changes to the eventual return value via another helper function “visiblyUtilized”) -> *5740,5741,5742,5743,5744,5745,5746,5747,5748,5749,5750,5751,5753,5754,5755,5756,5757,5758,5759,5760,5761,5762,5763,5764,5765, 5766,5767,5768,5769,5770,5771,5772,5779 ( above changes affected parameters passed to helper function “visiblyUtilized”, which caused condition changes that eventually impacted the ns list ) -> *5597, 5614, 5615, 5616,5617,5619,5620, 5841 ( changed ns passed to CanonicalizerSubTree ) -> 5886 ( ns passed back to attrs in CanonicalizerSubTree ) -> 5888 (attrs.size() changed due to the change before in ns ) -> 5889,5890,5891,5892,5893,5894,5895,5897 ( consequent changes due to change in attrs) -> 6024,6025,6026,6027,6028,6029,6030,6031,6032,6033,6034,6035,6036,6037,6056,6057,6058,6060,6061 ( changes in attrs written to baos in function outputAttrToWritter) -> 5905, 5906 ( iteratively causing changes in attrs again, primarily ) and 5907,5908 ( iteratively causing changes in attrs again, secondarily) -> *5406,5407,5408,5411,5412,5413,5414,5415,5419,5420,5421,5422,5434,5435,5442 (helper function “engineCanonicalizeXPathNodeSet” propagated above changes via virtual call to helper function “canonicalizeXPathNodeSet”) -> *5927,5928, 5942, 5943, 5968, 5969, 5991, 5992, 5994, 5995, 5996, 5997,5998,6000 ( helper function “canonicalizeXPathNodeSet” propagated above changes eventually to _baos through a instance member routine “_writer”) -> *5337,5338,5339,5340 (helper function “canonicalizeXPathNodeSet” wrote to _baos via helper class “EC14nCtx” and its instance member routines) -> 5398 ( baos transformed after changes in attrs reflected to it ) -> *13320,13321,13322,13323,13324,13325,13326,13327,13328,13329,13330,13331,13332,13333,13334,13335,13336,13337,13340,13341,13343 (changes in _baos propagated to _signedinfo via the initializer of the class SignedInfo and its instance member routine getSignatureMethodElement) -> 13628, 13630 ( _signedInfo changed in its _c14nizedBytes member ) -> *13433,13434,13435,13437,13438,13439,13440,13442,13443,13444,13445,13446,13447,13448,13449,13450,13451,13452,13453,13454, 13455,13456,13457,13458,13459,13460,13461,13462,13463,13464,13465,13466,13467,13468,13469,13470,13471,13472,13473,13475, 13476,13478,13479,13480,13481,13482,13483,13484,13485,13486,13487 (changes in __signedinfo propagated to signature.PublicKey via the class XMLSignature::checkSignatureValue) -> 17134, 17135 (the changed _sigedinfo reflected to signature.PublicKey ) -> *13515,13516,13517 (change in signature.PublicKey propagated to a boolean variable verify via XMLSignature::getSignatureValue) -> 17136, 17137, 17141,17142,17143 ( change propagated to the boolean variable verify due to failure in signature verification, the reflected in an output of verify's value ) -> 17145 ( change of verify from originally true to false caused a condition failure here ) -> *13571,13572,13808,13809,13810 (changes in the resulted signature transmitted to helper function getSignedInfo and then another helper getVerificationResult, which returns to _refVerify) -> 17155 ( refVerify falsified and further caused a condition failure ) -> *13831,13837,13838,13839,13840,13841,13842,13846,13847,13848,13849,13850,13851,13852,13857,13858,13859,13860,13861,13862, 13923,13954,13956,13989,13996 (transform the resulted signature for error message dumping) -> *17172, 17173, 17174,17175,17176,17177,17178,17179,17180,17181,17183,17184,17185,17186,17187,17188,17189,17190,17191,17192,17193, 17194,17195,17196,17197,17198,17199,17200,17202,17203,17204 (changes in signature propagated to _sb, the eventual return value of the method of t()) -> 17171 ( sb changed ) -> 17205 ( sb.toString().trim() passed to string r, and then r.length()!=0 caused non-null string to return ) -> 17273, 17274 ( the non-null string r passed to success in test_Y1 after returning from t() ) -> *17275 (value of success pruned another branch of the predicate on which the branch for assertTrue to reach failure is dependent) -> 17277 ( success!= null caused 0 passed to assertTrue ) -> 17278 ( assertion failed ) -> test case failed. |
|||||||||||||||
| Statements in the failure sequence (with those in the landmark sequence yellowed) |
Ranking by different techniques | |||||||||||||||
| SensA_rand | SensA_inc | Static slicing | Dynamic slicing | |||||||||||||
| 5621 | 62.5 | 62.5 | 1.0 | 1.0 | ||||||||||||
| 5622 | 62.5 | 62.5 | 3.5 | 10167.0 | ||||||||||||
| 5624 | 62.5 | 62.5 | 3.5 | 2.5 | ||||||||||||
| 5625 | 62.5 | 62.5 | 3.5 | 2.5 | ||||||||||||
| 5626 | 62.5 | 62.5 | 12.5 | 6.5 | ||||||||||||
| 5627 | 62.5 | 62.5 | 12.5 | 6.5 | ||||||||||||
| 5628 | 62.5 | 62.5 | 12.5 | 6.5 | ||||||||||||
| 5646 | 62.5 | 62.5 | 12.5 | 12.5 | ||||||||||||
| 5647 | 62.5 | 62.5 | 23.5 | 19.0 | ||||||||||||
| 5648 | 62.5 | 62.5 | 40.0 | 26.5 | ||||||||||||
| 5649 | 62.5 | 62.5 | 349.5 | 107.0 | ||||||||||||
| 5650 | 62.5 | 62.5 | 40.0 | 127.5 | ||||||||||||
| 5651 | 62.5 | 62.5 | 349.5 | 127.5 | ||||||||||||
| 5652 | 62.5 | 62.5 | 12.5 | 19.0 | ||||||||||||
| 5653 | 62.5 | 62.5 | 23.5 | 26.5 | ||||||||||||
| 5654 | 62.5 | 62.5 | 1137.0 | 127.5 | ||||||||||||
| 5655 | 62.5 | 62.5 | 1137.0 | 127.5 | ||||||||||||
| 5357 | 62.5 | 62.5 | 1137.0 | 143.5 | ||||||||||||
| 5358 | 62.5 | 62.5 | 1137.0 | 143.5 | ||||||||||||
| 5359 | 62.5 | 62.5 | 1137.0 | 143.5 | ||||||||||||
| 5360 | 62.5 | 62.5 | 1137.0 | 143.5 | ||||||||||||
| 5361 | 62.5 | 62.5 | 1137.0 | 143.5 | ||||||||||||
| 5362 | 62.5 | 62.5 | 1137.0 | 143.5 | ||||||||||||
| 5364 | 62.5 | 62.5 | 4672.0 | 164.0 | ||||||||||||
| 5365 | 62.5 | 62.5 | 2520.0 | 143.5 | ||||||||||||
| 5667 | 62.5 | 62.5 | 4672.0 | 164.0 | ||||||||||||
| 5668 | 62.5 | 62.5 | 1137.0 | 143.5 | ||||||||||||
| 5669 | 62.5 | 62.5 | 349.5 | 78.0 | ||||||||||||
| 5670 | 62.5 | 62.5 | 1137.0 | 84.0 | ||||||||||||
| 5676 | 62.5 | 62.5 | 2520.0 | 107.0 | ||||||||||||
| 5677 | 62.5 | 62.5 | 1137.0 | 92.5 | ||||||||||||
| 7812 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 7813 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 7814 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 7815 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 7816 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 7817 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 7818 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 7819 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 7820 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 5687 | 62.5 | 62.5 | 40.0 | 84.0 | ||||||||||||
| 5688 | 62.5 | 62.5 | 2520.0 | 107.0 | ||||||||||||
| 5689 | 62.5 | 62.5 | 349.5 | 107.0 | ||||||||||||
| 5690 | 62.5 | 62.5 | 40.0 | 107.0 | ||||||||||||
| 5691 | 62.5 | 62.5 | 349.5 | 107.0 | ||||||||||||
| 5699 | 62.5 | 62.5 | 40.0 | 19.0 | ||||||||||||
| 5476 | 153.5 | 1134.0 | 2520.0 | 345.0 | ||||||||||||
| 5477 | 153.5 | 1134.0 | 349.5 | 293.5 | ||||||||||||
| 5501 | 1153.5 | 1134.0 | 1137.0 | 345.0 | ||||||||||||
| 5502 | 1153.5 | 1134.0 | 2520.0 | 421.0 | ||||||||||||
| 5503 | 153.5 | 1134.0 | 4672.0 | 421.0 | ||||||||||||
| 5504 | 153.5 | 1134.0 | 1137.0 | 345.0 | ||||||||||||
| 5566 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 5567 | 1153.5 | 1134.0 | 1137.0 | 10167.0 | ||||||||||||
| 5568 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 5569 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 5571 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 5572 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 5573 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 5574 | 1153.5 | 1134.0 | 1137.0 | 10167.0 | ||||||||||||
| 5575 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 5576 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 5577 | 1153.5 | 1134.0 | 1137.0 | 10167.0 | ||||||||||||
| 5578 | 1153.5 | 1134.0 | 1137.0 | 10167.0 | ||||||||||||
| 5579 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 5585 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 5586 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 5587 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 5588 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 5589 | 1153.5 | 1134.0 | 1137.0 | 10167.0 | ||||||||||||
| 5590 | 1153.5 | 1134.0 | 349.5 | 10167.0 | ||||||||||||
| 5593 | 1153.5 | 1134.0 | 1137.0 | 421.0 | ||||||||||||
| 5740 | 62.5 | 62.5 | 2520.0 | 153.5 | ||||||||||||
| 5741 | 62.5 | 62.5 | 2520.0 | 153.5 | ||||||||||||
| 5742 | 62.5 | 62.5 | 2520.0 | 153.5 | ||||||||||||
| 5743 | 62.5 | 62.5 | 2520.0 | 153.5 | ||||||||||||
| 5744 | 62.5 | 62.5 | 2520.0 | 153.5 | ||||||||||||
| 5745 | 62.5 | 62.5 | 2520.0 | 153.5 | ||||||||||||
| 5746 | 62.5 | 62.5 | 2520.0 | 153.5 | ||||||||||||
| 5747 | 62.5 | 62.5 | 349.5 | 164.0 | ||||||||||||
| 5748 | 62.5 | 62.5 | 1137.0 | 164.0 | ||||||||||||
| 5749 | 62.5 | 62.5 | 349.5 | 164.0 | ||||||||||||
| 5750 | 62.5 | 62.5 | 1137.0 | 174.0 | ||||||||||||
| 5751 | 1153.5 | 1134.0 | 2520.0 | 293.5 | ||||||||||||
| 5753 | 62.5 | 62.5 | 2520.0 | 183.5 | ||||||||||||
| 5754 | 62.5 | 62.5 | 2520.0 | 183.5 | ||||||||||||
| 5755 | 62.5 | 62.5 | 2520.0 | 183.5 | ||||||||||||
| 5756 | 62.5 | 62.5 | 1137.0 | 174.0 | ||||||||||||
| 5757 | 62.5 | 62.5 | 2520.0 | 183.5 | ||||||||||||
| 5758 | 62.5 | 62.5 | 2520.0 | 164.0 | ||||||||||||
| 5759 | 62.5 | 62.5 | 349.5 | 164.0 | ||||||||||||
| 5760 | 62.5 | 62.5 | 1137.0 | 164.0 | ||||||||||||
| 5761 | 62.5 | 62.5 | 4672.0 | 164.0 | ||||||||||||
| 5762 | 62.5 | 62.5 | 2520.0 | 164.0 | ||||||||||||
| 5763 | 62.5 | 62.5 | 1137.0 | 174.0 | ||||||||||||
| 5764 | 62.5 | 62.5 | 2520.0 | 174.0 | ||||||||||||
| 5765 | 62.5 | 62.5 | 4672.0 | 174.0 | ||||||||||||
| 5766 | 62.5 | 62.5 | 4672.0 | 174.0 | ||||||||||||
| 5767 | 62.5 | 62.5 | 4672.0 | 183.5 | ||||||||||||
| 5768 | 62.5 | 62.5 | 7200.0 | 183.5 | ||||||||||||
| 5769 | 62.5 | 62.5 | 7200.0 | 194.0 | ||||||||||||
| 5770 | 62.5 | 62.5 | 9732.5 | 194.0 | ||||||||||||
| 5771 | 62.5 | 62.5 | 7200.0 | 194.0 | ||||||||||||
| 5772 | 62.5 | 62.5 | 9732.5 | 206.5 | ||||||||||||
| 5779 | 62.5 | 62.5 | 4672.0 | 174.0 | ||||||||||||
| 5597 | 62.5 | 62.5 | 2520.0 | 228.5 | ||||||||||||
| 5614 | 10526.0 | 10526.0 | 23.5 | 12.5 | ||||||||||||
| 5615 | 10526.0 | 10526.0 | 40.0 | 19.0 | ||||||||||||
| 5616 | 10526.0 | 10526.0 | 40.0 | 19.0 | ||||||||||||
| 5617 | 10526.0 | 10526.0 | 349.5 | 10167.0 | ||||||||||||
| 5619 | 10526.0 | 10526.0 | 40.0 | 19.0 | ||||||||||||
| 5620 | 10526.0 | 10526.0 | 349.5 | 26.5 | ||||||||||||
| 5841 | 62.5 | 62.5 | 2520.0 | 194.0 | ||||||||||||
| 5886 | 62.5 | 62.5 | 2520.0 | 143.5 | ||||||||||||
| 5888 | 62.5 | 62.5 | 349.5 | 26.5 | ||||||||||||
| 5889 | 62.5 | 62.5 | 1137.0 | 35.5 | ||||||||||||
| 5890 | 62.5 | 62.5 | 349.5 | 35.5 | ||||||||||||
| 5891 | 62.5 | 62.5 | 1137.0 | 53.5 | ||||||||||||
| 5892 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 5893 | 62.5 | 62.5 | 349.5 | 53.5 | ||||||||||||
| 5894 | 62.5 | 62.5 | 1137.0 | 53.5 | ||||||||||||
| 5895 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 5897 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 6024 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 6025 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 6026 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 6027 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 6028 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 6029 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 6030 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 6031 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 6032 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 6033 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 6034 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 6035 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 6036 | 62.5 | 62.5 | 4672.0 | 71.0 | ||||||||||||
| 6037 | 62.5 | 62.5 | 4672.0 | 71.0 | ||||||||||||
| 6056 | 62.5 | 62.5 | 4672.0 | 71.0 | ||||||||||||
| 6057 | 62.5 | 62.5 | 2520.0 | 71.0 | ||||||||||||
| 6058 | 62.5 | 62.5 | 4672.0 | 71.0 | ||||||||||||
| 6060 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 6061 | 62.5 | 62.5 | 2520.0 | 53.5 | ||||||||||||
| 5905 | 62.5 | 62.5 | 4672.0 | 206.5 | ||||||||||||
| 5906 | 62.5 | 62.5 | 12.5 | 26.5 | ||||||||||||
| 5907 | 153.5 | 133.5 | 4672.0 | 206.5 | ||||||||||||
| 5908 | 153.5 | 133.5 | 349.5 | 53.5 | ||||||||||||
| 5406 | 1153.5 | 1134.0 | 12199.5 | 10167.0 | ||||||||||||
| 5407 | 153.5 | 1134.0 | 12199.5 | 10167.0 | ||||||||||||
| 5408 | 1153.5 | 1134.0 | 7200.0 | 10167.0 | ||||||||||||
| 5411 | 153.5 | 1134.0 | 12199.5 | 10167.0 | ||||||||||||
| 5412 | 1153.5 | 1134.0 | 12199.5 | 10167.0 | ||||||||||||
| 5413 | 153.5 | 1134.0 | 12199.5 | 10167.0 | ||||||||||||
| 5414 | 153.5 | 1134.0 | 7200.0 | 10167.0 | ||||||||||||
| 5415 | 153.5 | 1134.0 | 1137.0 | 345.0 | ||||||||||||
| 5419 | 153.5 | 1134.0 | 4672.0 | 516.0 | ||||||||||||
| 5420 | 153.5 | 1134.0 | 1137.0 | 421.0 | ||||||||||||
| 5421 | 153.5 | 1134.0 | 1137.0 | 516.0 | ||||||||||||
| 5422 | 153.5 | 1134.0 | 2520.0 | 516.0 | ||||||||||||
| 5434 | 1153.5 | 1134.0 | 9732.5 | 657.0 | ||||||||||||
| 5435 | 1153.5 | 1134.0 | 4672.0 | 516.0 | ||||||||||||
| 5442 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 5927 | 153.5 | 1134.0 | 2520.0 | 421.0 | ||||||||||||
| 5928 | 153.5 | 1134.0 | 349.5 | 293.5 | ||||||||||||
| 5942 | 153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 5943 | 153.5 | 1134.0 | 349.5 | 10167.0 | ||||||||||||
| 5968 | 153.5 | 1134.0 | 2520.0 | 345.0 | ||||||||||||
| 5969 | 153.5 | 1134.0 | 349.5 | 293.5 | ||||||||||||
| 5991 | 1153.5 | 1134.0 | 7200.0 | 516.0 | ||||||||||||
| 5992 | 1153.5 | 1134.0 | 1137.0 | 345.0 | ||||||||||||
| 5994 | 1153.5 | 1134.0 | 2520.0 | 345.0 | ||||||||||||
| 5995 | 1153.5 | 1134.0 | 1137.0 | 10167.0 | ||||||||||||
| 5996 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 5997 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 5998 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 6000 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 5337 | 1153.5 | 1134.0 | 4672.0 | 516.0 | ||||||||||||
| 5338 | 1153.5 | 1134.0 | 4672.0 | 516.0 | ||||||||||||
| 5339 | 1153.5 | 1134.0 | 2520.0 | 516.0 | ||||||||||||
| 5340 | 1153.5 | 1134.0 | 4672.0 | 516.0 | ||||||||||||
| 5398 | 62.5 | 62.5 | 4672.0 | 10167.0 | ||||||||||||
| 13320 | 1153.5 | 1134.0 | 12199.5 | 10167.0 | ||||||||||||
| 13321 | 1153.5 | 1134.0 | 12199.5 | 10167.0 | ||||||||||||
| 13322 | 1153.5 | 1134.0 | 349.5 | 10167.0 | ||||||||||||
| 13323 | 1153.5 | 1134.0 | 12199.5 | 10167.0 | ||||||||||||
| 13324 | 1153.5 | 1134.0 | 1137.0 | 10167.0 | ||||||||||||
| 13325 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 13326 | 1153.5 | 1134.0 | 1137.0 | 10167.0 | ||||||||||||
| 13327 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13328 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13329 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13330 | 1153.5 | 1134.0 | 1137.0 | 10167.0 | ||||||||||||
| 13331 | 1153.5 | 1134.0 | 349.5 | 10167.0 | ||||||||||||
| 13332 | 1153.5 | 1134.0 | 1137.0 | 10167.0 | ||||||||||||
| 13333 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 13334 | 1153.5 | 1134.0 | 349.5 | 10167.0 | ||||||||||||
| 13335 | 1153.5 | 1134.0 | 1137.0 | 10167.0 | ||||||||||||
| 13336 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 13337 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 13340 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 13341 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 13343 | 1153.5 | 1134.0 | 2520.0 | 10167.0 | ||||||||||||
| 13628 | 1153.5 | 1134.0 | 12199.5 | 10167.0 | ||||||||||||
| 13630 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13433 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13434 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13435 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 13437 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13438 | 1153.5 | 1134.0 | 12199.5 | 10167.0 | ||||||||||||
| 13439 | 1153.5 | 1134.0 | 7200.0 | 10167.0 | ||||||||||||
| 13440 | 1153.5 | 1134.0 | 7200.0 | 10167.0 | ||||||||||||
| 13442 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13443 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13444 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13445 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13446 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13447 | 1153.5 | 1134.0 | 14225.0 | 10167.0 | ||||||||||||
| 13448 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13449 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13450 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13451 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13452 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13453 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13454 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13455 | 1153.5 | 1134.0 | 14225.0 | 10167.0 | ||||||||||||
| 13456 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13457 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13458 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13459 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13460 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13461 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13462 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13463 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13464 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13465 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13466 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13467 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13468 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13469 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13470 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13471 | 1153.5 | 1134.0 | 14225.0 | 10167.0 | ||||||||||||
| 13472 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13473 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13475 | 1153.5 | 1134.0 | 7200.0 | 10167.0 | ||||||||||||
| 13476 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13478 | 1153.5 | 1134.0 | 12199.5 | 10167.0 | ||||||||||||
| 13479 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13480 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13481 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13482 | 1153.5 | 1134.0 | 12199.5 | 10167.0 | ||||||||||||
| 13483 | 1153.5 | 1134.0 | 9732.5 | 10167.0 | ||||||||||||
| 13484 | 1153.5 | 1134.0 | 9732.5 | 10167.0 | ||||||||||||
| 13485 | 1153.5 | 1134.0 | 12199.5 | 10167.0 | ||||||||||||
| 13486 | 1153.5 | 1134.0 | 14225.0 | 10167.0 | ||||||||||||
| 13487 | 1153.5 | 1134.0 | 12199.5 | 10167.0 | ||||||||||||
| 17134 | 1153.5 | 1134.0 | 12199.5 | 10167.0 | ||||||||||||
| 17135 | 1153.5 | 1134.0 | 14225.0 | 1003.5 | ||||||||||||
| 13515 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 13516 | 1153.5 | 1134.0 | 7200.0 | 10167.0 | ||||||||||||
| 13517 | 1153.5 | 1134.0 | 7200.0 | 10167.0 | ||||||||||||
| 17136 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 17137 | 1153.5 | 1134.0 | 15832.5 | 10167.0 | ||||||||||||
| 17141 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 17142 | 1153.5 | 1134.0 | 18058.5 | 10167.0 | ||||||||||||
| 17143 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 17145 | 1153.5 | 1134.0 | 17203.0 | 10167.0 | ||||||||||||
| 13571 | 1153.5 | 1134.0 | 14225.0 | 1144.0 | ||||||||||||
| 13572 | 1153.5 | 1134.0 | 7200.0 | 1144.0 | ||||||||||||
| 13808 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13810 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 17155 | 10526.0 | 10526.0 | 15832.5 | 10167.0 | ||||||||||||
| 13831 | 153.5 | 1134.0 | 4672.0 | 723.0 | ||||||||||||
| 13837 | 1153.5 | 1134.0 | 4672.0 | 796.5 | ||||||||||||
| 13838 | 1153.5 | 1134.0 | 4672.0 | 723.0 | ||||||||||||
| 13839 | 1153.5 | 1134.0 | 4672.0 | 753.0 | ||||||||||||
| 13840 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13841 | 1153.5 | 1134.0 | 7200.0 | 10167.0 | ||||||||||||
| 13842 | 1153.5 | 1134.0 | 9732.5 | 10167.0 | ||||||||||||
| 13846 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13847 | 1153.5 | 1134.0 | 7200.0 | 10167.0 | ||||||||||||
| 13848 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13849 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13850 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13851 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13852 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13857 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13858 | 1153.5 | 1134.0 | 7200.0 | 10167.0 | ||||||||||||
| 13859 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13860 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13861 | 1153.5 | 1134.0 | 7200.0 | 10167.0 | ||||||||||||
| 13862 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13923 | 153.5 | 1134.0 | 4672.0 | 723.0 | ||||||||||||
| 13954 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13956 | 1153.5 | 1134.0 | 4672.0 | 10167.0 | ||||||||||||
| 13989 | 153.5 | 1134.0 | 2520.0 | 687.0 | ||||||||||||
| 13996 | 153.5 | 1134.0 | 2520.0 | 687.0 | ||||||||||||
| 17172 | 10526.0 | 10526.0 | 12199.5 | 10167.0 | ||||||||||||
| 17173 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17174 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17175 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17176 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17177 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17178 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17179 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17180 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17181 | 10526.0 | 10526.0 | 9732.5 | 10167.0 | ||||||||||||
| 17183 | 10526.0 | 10526.0 | 12199.5 | 10167.0 | ||||||||||||
| 17184 | 10526.0 | 10526.0 | 15832.5 | 10167.0 | ||||||||||||
| 17185 | 10526.0 | 10526.0 | 14225.0 | 10167.0 | ||||||||||||
| 17186 | 10526.0 | 10526.0 | 7200.0 | 10167.0 | ||||||||||||
| 17187 | 10526.0 | 10526.0 | 14225.0 | 10167.0 | ||||||||||||
| 17188 | 10526.0 | 10526.0 | 9732.5 | 10167.0 | ||||||||||||
| 17189 | 10526.0 | 10526.0 | 9732.5 | 10167.0 | ||||||||||||
| 17190 | 10526.0 | 10526.0 | 14225.0 | 10167.0 | ||||||||||||
| 17191 | 10526.0 | 10526.0 | 15832.5 | 10167.0 | ||||||||||||
| 17192 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17193 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17194 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17195 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17196 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17197 | 10526.0 | 10526.0 | 15832.5 | 10167.0 | ||||||||||||
| 17198 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17199 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17200 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17202 | 10526.0 | 10526.0 | 18058.5 | 10167.0 | ||||||||||||
| 17203 | 10526.0 | 10526.0 | 18058.5 | 10167.0 | ||||||||||||
| 17204 | 10526.0 | 10526.0 | 18058.5 | 10167.0 | ||||||||||||
| 17171 | 10526.0 | 10526.0 | 17203.0 | 10167.0 | ||||||||||||
| 17205 | 10526.0 | 10526.0 | 18058.5 | 10167.0 | ||||||||||||
| 17273 | 1153.5 | 1134.0 | 18486.5 | 10167.0 | ||||||||||||
| 17274 | 1153.5 | 1134.0 | 18801.0 | 10167.0 | ||||||||||||
| 17275 | 1153.5 | 1134.0 | 19032.0 | 10167.0 | ||||||||||||
| 17277 | 10526.0 | 10526.0 | 19032.0 | 10167.0 | ||||||||||||
| 17278 | 10526.0 | 10526.0 | 18801.0 | 10167.0 | ||||||||||||
| Average cost of inspecting the whole sequence in the ranking | 10.31% | 10.62% | 35.24% | 30.98% | ||||||||||||
| Number of statements to be examined in order to inspect the whole sequence | 1951.3 | 2009.9 | 6669.5 | 5863.3 | ||||||||||||