experiment_results.ipynb

{
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "2bvwCHGfDn2E"
      },
      "source": [
        "# verify-c-common Empirical Results\n",
        "This notebook is an alternative report of empirical results made on a case study paper \"Verifying Verified Code\".\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "KZJCoUdrK692"
      },
      "source": [
        "## Part one: Benckmark Prepration and Setup"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "\n",
        "|  | CBMC | SeaHorn | SMACK | Symbiotic | KLEE | libfuzzer\n",
        "| :- |:------------- | :------------- | :------------- | :------------- | :------------- | :-------------\n",
        "| Tool version | [CBMC 5.30.1](https://github.com/diffblue/cbmc/releases/tag/cbmc-5.30.1) | Staged on newest [dev10](https://github.com/seahorn/seahorn/tree/dev10) branch | [SMACK 2.6.3](https://github.com/smackers/smack/tree/fcd846efe9521b4254cd84e2c677b8bbb4745051) | [Symbiotic 8.0.0](https://github.com/staticafi/symbiotic/tree/792b3b8112cb837a58d878129e8bc7a919d1a2f7) | [KLEE 2.2](https://github.com/klee/klee/releases/tag/v2.2) | --\n",
        "| # Benchmark Covered| 168  | 168 | 159 | 155 | 153 | 78 \n",
        "| Timeout | 2000 seconds| 300 seconds | 300 seconds | 5000 seconds | -- | --\n",
        "| Total Running Time | 6476 seconds | 631 seconds | 8525 seconds | 10946 seconds | 8577 seconds | --\n",
        "| Benchmark Source | [aws-c-common](https://github.com/awslabs/aws-c-common/tree/main/verification/cbmc/proofs) | [verify-c-common](https://github.com/seahorn/verify-c-common/tree/master/seahorn/jobs) | [verify-c-common](https://github.com/seahorn/verify-c-common/tree/master/seahorn/jobs)| [verify-c-common](https://github.com/seahorn/verify-c-common/tree/master/seahorn/jobs) | [verify-c-common](https://github.com/seahorn/verify-c-common/tree/master/seahorn/jobs) | [verify-c-common](https://github.com/seahorn/verify-c-common/tree/master/seahorn/jobs)\n",
        "| Options | Inidividual: <br/>`make results ` <br/> Unit Test: <br/> a python scripts used to traverse all harnnesses | Inidividual: <br/>`./verify [options] <BC_FILE_NAME> ` <br/> Unit Test: <br/> `ctest -D ExperimentalTest -R . --timeout 300` | Inidividual: <br/>`smack --check assertions --time-limit 300 --no-memory-splitting --integer-encoding unbounded-integer --pointer-encoding unbounded-integer [options] <SMACK_LL_FILE_NAME>` <br/> Unit Test: <br/> `ctest -D ExperimentalTest -R smack_ --timeout 300` | Inidividual: <br/>`symbiotic --replay-error --report=short --prp=assert [options] <SYMBIOTIC_BC_FILE_NAME>` <br/> Unit Test: <br/> `ctest -D ExperimentalTest -R symbiotic_ --timeout 5000` | Inidividual: <br/>`klee --libc=uclibc --exit-on-error <KLEE_BC_FILE_NAME> ` <br/> Unit Test: <br/> `ctest -D ExperimentalTest -R klee_` | --\n",
        "| Results | [aws-cbmc.csv](https://github.com/seahorn/verify-c-common/tree/master/res/aws-cbmc.csv) | [seahorn.csv](https://github.com/seahorn/verify-c-common/tree/master/res/seahorn.csv) |[smack.csv](https://github.com/seahorn/verify-c-common/tree/master/res/smack.csv) | [symbiotic.csv](https://github.com/seahorn/verify-c-common/tree/master/res/symbiotic.csv) | [klee.csv](https://github.com/seahorn/verify-c-common/tree/master/res/klee.csv) | [Coverage report](https://seahorn.github.io/verify-c-common/fuzzing_coverage/index.html)\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 1,
      "metadata": {
        "id": "ggGMpPViDemc"
      },
      "outputs": [],
      "source": [
        "import pandas as pd\n",
        "import numpy as np\n",
        "import seaborn as sns\n",
        "import matplotlib.pyplot as plt\n",
        "import copy\n",
        "from matplotlib.backends.backend_pdf import PdfPages\n",
        "\n",
        "# Do not limit number of rows displayed\n",
        "pd.set_option('display.max_rows', None)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 2,
      "metadata": {
        "id": "B20LokpCad_w"
      },
      "outputs": [],
      "source": [
        "# Include data files\n",
        "SEAHORN_CSV = 'https://raw.githubusercontent.com/seahorn/verify-c-common/master/res/seahorn.csv'\n",
        "CBMC_CSV = 'https://raw.githubusercontent.com/seahorn/verify-c-common/master/res/aws-cbmc.csv'\n",
        "SMACK_CSV = 'https://raw.githubusercontent.com/seahorn/verify-c-common/master/res/smack.csv'\n",
        "SYMBIOTIC_CSV = 'https://raw.githubusercontent.com/seahorn/verify-c-common/master/res/symbiotic.csv'\n",
        "KLEE_CSV = 'https://raw.githubusercontent.com/seahorn/verify-c-common/master/res/klee.csv'\n",
        "LOC_CSV = 'https://raw.githubusercontent.com/seahorn/verify-c-common/master/res/loc.csv'"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 3,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 1000
        },
        "id": "BAgYKbMDbNxj",
        "outputId": "8d97b0cf-af8f-4588-a970-d41c70d5f516"
      },
      "outputs": [
        {
          "data": {
            "text/html": [
              "<div>\n",
              "<style scoped>\n",
              "    .dataframe tbody tr th:only-of-type {\n",
              "        vertical-align: middle;\n",
              "    }\n",
              "\n",
              "    .dataframe tbody tr th {\n",
              "        vertical-align: top;\n",
              "    }\n",
              "\n",
              "    .dataframe thead th {\n",
              "        text-align: right;\n",
              "    }\n",
              "</style>\n",
              "<table border=\"1\" class=\"dataframe\">\n",
              "  <thead>\n",
              "    <tr style=\"text-align: right;\">\n",
              "      <th></th>\n",
              "      <th>job name</th>\n",
              "      <th>loc</th>\n",
              "      <th>CBMC time (s)</th>\n",
              "      <th>Seahorn normal time (s)</th>\n",
              "      <th>Smack time (s)</th>\n",
              "      <th>Smack result</th>\n",
              "      <th>Symbiotic time (s)</th>\n",
              "      <th>Symbiotic result</th>\n",
              "      <th>Klee time (s)</th>\n",
              "    </tr>\n",
              "  </thead>\n",
              "  <tbody>\n",
              "    <tr>\n",
              "      <th>0</th>\n",
              "      <td>aws_is_power_of_two</td>\n",
              "      <td>11</td>\n",
              "      <td>3.443</td>\n",
              "      <td>0.444965</td>\n",
              "      <td>7.21547</td>\n",
              "      <td>failed</td>\n",
              "      <td>1.515958</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.718919</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>1</th>\n",
              "      <td>aws_round_up_to_power_of_two</td>\n",
              "      <td>37</td>\n",
              "      <td>3.459</td>\n",
              "      <td>0.642792</td>\n",
              "      <td>7.41379</td>\n",
              "      <td>failed</td>\n",
              "      <td>4.046049</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.794902</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>2</th>\n",
              "      <td>aws_ptr_eq</td>\n",
              "      <td>10</td>\n",
              "      <td>3.504</td>\n",
              "      <td>0.500028</td>\n",
              "      <td>4.44428</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.671042</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.727793</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>3</th>\n",
              "      <td>aws_array_eq_ignore_case</td>\n",
              "      <td>78</td>\n",
              "      <td>5.536</td>\n",
              "      <td>2.080760</td>\n",
              "      <td>200.02300</td>\n",
              "      <td>timeout</td>\n",
              "      <td>6.290933</td>\n",
              "      <td>passed</td>\n",
              "      <td>33.526500</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>4</th>\n",
              "      <td>aws_array_list_capacity</td>\n",
              "      <td>107</td>\n",
              "      <td>5.530</td>\n",
              "      <td>0.786557</td>\n",
              "      <td>11.60290</td>\n",
              "      <td>passed</td>\n",
              "      <td>5.474102</td>\n",
              "      <td>passed</td>\n",
              "      <td>13.619400</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>5</th>\n",
              "      <td>aws_array_list_back</td>\n",
              "      <td>129</td>\n",
              "      <td>13.785</td>\n",
              "      <td>0.952469</td>\n",
              "      <td>12.32640</td>\n",
              "      <td>passed</td>\n",
              "      <td>8.467914</td>\n",
              "      <td>passed</td>\n",
              "      <td>90.595000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>6</th>\n",
              "      <td>aws_array_list_clean_up</td>\n",
              "      <td>89</td>\n",
              "      <td>5.523</td>\n",
              "      <td>0.498641</td>\n",
              "      <td>10.87460</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.724258</td>\n",
              "      <td>passed</td>\n",
              "      <td>13.826800</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>7</th>\n",
              "      <td>aws_add_size_saturating</td>\n",
              "      <td>37</td>\n",
              "      <td>3.447</td>\n",
              "      <td>0.549630</td>\n",
              "      <td>5.47448</td>\n",
              "      <td>passed</td>\n",
              "      <td>8.886539</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.811040</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>8</th>\n",
              "      <td>aws_array_list_clear</td>\n",
              "      <td>77</td>\n",
              "      <td>5.511</td>\n",
              "      <td>1.423880</td>\n",
              "      <td>10.55720</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.150718</td>\n",
              "      <td>passed</td>\n",
              "      <td>13.905400</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>9</th>\n",
              "      <td>aws_array_eq</td>\n",
              "      <td>100</td>\n",
              "      <td>5.630</td>\n",
              "      <td>2.196110</td>\n",
              "      <td>16.68940</td>\n",
              "      <td>passed</td>\n",
              "      <td>9.633242</td>\n",
              "      <td>passed</td>\n",
              "      <td>34.978200</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>10</th>\n",
              "      <td>aws_array_list_comparator_string</td>\n",
              "      <td>110</td>\n",
              "      <td>7.624</td>\n",
              "      <td>6.306280</td>\n",
              "      <td>19.72590</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.348738</td>\n",
              "      <td>passed</td>\n",
              "      <td>121.267000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>11</th>\n",
              "      <td>aws_add_size_checked</td>\n",
              "      <td>40</td>\n",
              "      <td>3.444</td>\n",
              "      <td>0.624538</td>\n",
              "      <td>8.06627</td>\n",
              "      <td>passed</td>\n",
              "      <td>11.656799</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.740112</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>12</th>\n",
              "      <td>aws_array_eq_c_str</td>\n",
              "      <td>112</td>\n",
              "      <td>5.534</td>\n",
              "      <td>1.700990</td>\n",
              "      <td>6.43832</td>\n",
              "      <td>passed</td>\n",
              "      <td>12.400516</td>\n",
              "      <td>passed</td>\n",
              "      <td>37.000100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>13</th>\n",
              "      <td>aws_array_eq_c_str_ignore_case</td>\n",
              "      <td>100</td>\n",
              "      <td>5.534</td>\n",
              "      <td>0.670247</td>\n",
              "      <td>7.09141</td>\n",
              "      <td>passed</td>\n",
              "      <td>15.828431</td>\n",
              "      <td>passed</td>\n",
              "      <td>23.555400</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>14</th>\n",
              "      <td>aws_array_list_front</td>\n",
              "      <td>128</td>\n",
              "      <td>7.594</td>\n",
              "      <td>1.094380</td>\n",
              "      <td>11.82420</td>\n",
              "      <td>passed</td>\n",
              "      <td>6.972152</td>\n",
              "      <td>passed</td>\n",
              "      <td>89.584100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>15</th>\n",
              "      <td>aws_array_list_length</td>\n",
              "      <td>105</td>\n",
              "      <td>7.590</td>\n",
              "      <td>0.785986</td>\n",
              "      <td>11.55540</td>\n",
              "      <td>passed</td>\n",
              "      <td>5.479497</td>\n",
              "      <td>passed</td>\n",
              "      <td>13.734800</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>16</th>\n",
              "      <td>aws_array_list_get_at_ptr</td>\n",
              "      <td>125</td>\n",
              "      <td>11.730</td>\n",
              "      <td>0.813469</td>\n",
              "      <td>13.09160</td>\n",
              "      <td>passed</td>\n",
              "      <td>8.745562</td>\n",
              "      <td>passed</td>\n",
              "      <td>13.380200</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>17</th>\n",
              "      <td>aws_array_list_get_at</td>\n",
              "      <td>128</td>\n",
              "      <td>11.728</td>\n",
              "      <td>0.709902</td>\n",
              "      <td>13.58510</td>\n",
              "      <td>passed</td>\n",
              "      <td>9.530712</td>\n",
              "      <td>passed</td>\n",
              "      <td>89.813300</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>18</th>\n",
              "      <td>aws_array_list_pop_back</td>\n",
              "      <td>124</td>\n",
              "      <td>13.775</td>\n",
              "      <td>1.308630</td>\n",
              "      <td>17.05080</td>\n",
              "      <td>passed</td>\n",
              "      <td>10.120248</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.183500</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>19</th>\n",
              "      <td>aws_array_list_pop_front</td>\n",
              "      <td>137</td>\n",
              "      <td>17.929</td>\n",
              "      <td>1.375760</td>\n",
              "      <td>15.87950</td>\n",
              "      <td>passed</td>\n",
              "      <td>17.798371</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.335100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>20</th>\n",
              "      <td>aws_array_list_pop_front_n</td>\n",
              "      <td>129</td>\n",
              "      <td>20.003</td>\n",
              "      <td>2.238250</td>\n",
              "      <td>13.11020</td>\n",
              "      <td>passed</td>\n",
              "      <td>23.865669</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.311600</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>21</th>\n",
              "      <td>aws_array_list_sort</td>\n",
              "      <td>112</td>\n",
              "      <td>26.189</td>\n",
              "      <td>0.811297</td>\n",
              "      <td>10.87240</td>\n",
              "      <td>passed</td>\n",
              "      <td>8.093429</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.340100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>22</th>\n",
              "      <td>aws_array_list_erase</td>\n",
              "      <td>166</td>\n",
              "      <td>172.636</td>\n",
              "      <td>2.095370</td>\n",
              "      <td>13.46420</td>\n",
              "      <td>passed</td>\n",
              "      <td>40.334799</td>\n",
              "      <td>passed</td>\n",
              "      <td>15.621800</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>23</th>\n",
              "      <td>aws_array_list_init_static</td>\n",
              "      <td>128</td>\n",
              "      <td>9.639</td>\n",
              "      <td>0.990409</td>\n",
              "      <td>12.17270</td>\n",
              "      <td>passed</td>\n",
              "      <td>43.936742</td>\n",
              "      <td>passed</td>\n",
              "      <td>60.675600</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>24</th>\n",
              "      <td>aws_byte_buf_advance</td>\n",
              "      <td>110</td>\n",
              "      <td>7.628</td>\n",
              "      <td>0.700093</td>\n",
              "      <td>69.98620</td>\n",
              "      <td>passed</td>\n",
              "      <td>8.880398</td>\n",
              "      <td>passed</td>\n",
              "      <td>57.667000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>25</th>\n",
              "      <td>aws_array_list_swap_contents</td>\n",
              "      <td>123</td>\n",
              "      <td>13.817</td>\n",
              "      <td>1.636210</td>\n",
              "      <td>13.95710</td>\n",
              "      <td>passed</td>\n",
              "      <td>16.766813</td>\n",
              "      <td>passed</td>\n",
              "      <td>51.240800</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>26</th>\n",
              "      <td>aws_array_list_swap</td>\n",
              "      <td>111</td>\n",
              "      <td>83.886</td>\n",
              "      <td>13.352000</td>\n",
              "      <td>12.10000</td>\n",
              "      <td>passed</td>\n",
              "      <td>18.280318</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.588200</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>27</th>\n",
              "      <td>aws_array_list_push_back</td>\n",
              "      <td>181</td>\n",
              "      <td>259.178</td>\n",
              "      <td>1.463280</td>\n",
              "      <td>13.74180</td>\n",
              "      <td>passed</td>\n",
              "      <td>44.513344</td>\n",
              "      <td>passed</td>\n",
              "      <td>70.661700</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>28</th>\n",
              "      <td>aws_byte_buf_clean_up</td>\n",
              "      <td>50</td>\n",
              "      <td>5.560</td>\n",
              "      <td>0.534919</td>\n",
              "      <td>10.23340</td>\n",
              "      <td>passed</td>\n",
              "      <td>2.055410</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.219600</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>29</th>\n",
              "      <td>aws_array_list_shrink_to_fit</td>\n",
              "      <td>149</td>\n",
              "      <td>38.556</td>\n",
              "      <td>1.567210</td>\n",
              "      <td>11.65050</td>\n",
              "      <td>passed</td>\n",
              "      <td>40.644580</td>\n",
              "      <td>passed</td>\n",
              "      <td>41.323900</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>30</th>\n",
              "      <td>aws_byte_buf_append</td>\n",
              "      <td>85</td>\n",
              "      <td>5.548</td>\n",
              "      <td>0.624864</td>\n",
              "      <td>24.36980</td>\n",
              "      <td>passed</td>\n",
              "      <td>11.664072</td>\n",
              "      <td>passed</td>\n",
              "      <td>17.381200</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>31</th>\n",
              "      <td>aws_byte_buf_clean_up_secure</td>\n",
              "      <td>61</td>\n",
              "      <td>7.601</td>\n",
              "      <td>0.538965</td>\n",
              "      <td>10.20340</td>\n",
              "      <td>passed</td>\n",
              "      <td>2.457513</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.791000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>32</th>\n",
              "      <td>aws_byte_buf_append_with_lookup</td>\n",
              "      <td>105</td>\n",
              "      <td>7.597</td>\n",
              "      <td>1.094130</td>\n",
              "      <td>26.90020</td>\n",
              "      <td>passed</td>\n",
              "      <td>9.295327</td>\n",
              "      <td>passed</td>\n",
              "      <td>18.123400</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>33</th>\n",
              "      <td>aws_mul_size_saturating</td>\n",
              "      <td>38</td>\n",
              "      <td>5.509</td>\n",
              "      <td>0.761364</td>\n",
              "      <td>6.15913</td>\n",
              "      <td>passed</td>\n",
              "      <td>77.413389</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.450430</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>34</th>\n",
              "      <td>aws_byte_buf_from_array</td>\n",
              "      <td>52</td>\n",
              "      <td>5.531</td>\n",
              "      <td>0.566631</td>\n",
              "      <td>11.18790</td>\n",
              "      <td>passed</td>\n",
              "      <td>2.407168</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.097200</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>35</th>\n",
              "      <td>aws_byte_buf_eq</td>\n",
              "      <td>127</td>\n",
              "      <td>5.542</td>\n",
              "      <td>2.254840</td>\n",
              "      <td>105.37700</td>\n",
              "      <td>passed</td>\n",
              "      <td>13.762205</td>\n",
              "      <td>passed</td>\n",
              "      <td>94.835300</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>36</th>\n",
              "      <td>aws_byte_buf_eq_c_str</td>\n",
              "      <td>142</td>\n",
              "      <td>5.571</td>\n",
              "      <td>0.698345</td>\n",
              "      <td>8.05915</td>\n",
              "      <td>passed</td>\n",
              "      <td>13.874403</td>\n",
              "      <td>passed</td>\n",
              "      <td>77.557800</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>37</th>\n",
              "      <td>aws_byte_buf_from_empty_array</td>\n",
              "      <td>52</td>\n",
              "      <td>5.529</td>\n",
              "      <td>0.560820</td>\n",
              "      <td>11.99540</td>\n",
              "      <td>passed</td>\n",
              "      <td>2.245510</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.233100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>38</th>\n",
              "      <td>aws_byte_buf_eq_c_str_ignore_case</td>\n",
              "      <td>130</td>\n",
              "      <td>5.543</td>\n",
              "      <td>0.677644</td>\n",
              "      <td>8.27622</td>\n",
              "      <td>passed</td>\n",
              "      <td>16.806220</td>\n",
              "      <td>passed</td>\n",
              "      <td>99.036600</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>39</th>\n",
              "      <td>aws_byte_buf_init</td>\n",
              "      <td>53</td>\n",
              "      <td>5.516</td>\n",
              "      <td>0.551112</td>\n",
              "      <td>12.23750</td>\n",
              "      <td>passed</td>\n",
              "      <td>3.228677</td>\n",
              "      <td>passed</td>\n",
              "      <td>52.602700</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>40</th>\n",
              "      <td>aws_byte_buf_eq_ignore_case</td>\n",
              "      <td>101</td>\n",
              "      <td>5.560</td>\n",
              "      <td>1.596800</td>\n",
              "      <td>200.02500</td>\n",
              "      <td>timeout</td>\n",
              "      <td>16.878187</td>\n",
              "      <td>passed</td>\n",
              "      <td>NaN</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>41</th>\n",
              "      <td>aws_byte_buf_from_c_str</td>\n",
              "      <td>188</td>\n",
              "      <td>5.532</td>\n",
              "      <td>1.812950</td>\n",
              "      <td>13.85310</td>\n",
              "      <td>passed</td>\n",
              "      <td>5.665581</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.431300</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>42</th>\n",
              "      <td>aws_array_list_copy</td>\n",
              "      <td>106</td>\n",
              "      <td>34.392</td>\n",
              "      <td>3.284130</td>\n",
              "      <td>11.88310</td>\n",
              "      <td>passed</td>\n",
              "      <td>80.543497</td>\n",
              "      <td>passed</td>\n",
              "      <td>155.075000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>43</th>\n",
              "      <td>aws_byte_buf_reset</td>\n",
              "      <td>71</td>\n",
              "      <td>5.538</td>\n",
              "      <td>0.615145</td>\n",
              "      <td>15.24990</td>\n",
              "      <td>passed</td>\n",
              "      <td>2.297113</td>\n",
              "      <td>passed</td>\n",
              "      <td>15.083100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>44</th>\n",
              "      <td>aws_byte_buf_init_copy_from_cursor</td>\n",
              "      <td>89</td>\n",
              "      <td>5.537</td>\n",
              "      <td>0.666797</td>\n",
              "      <td>22.23290</td>\n",
              "      <td>passed</td>\n",
              "      <td>3.744924</td>\n",
              "      <td>passed</td>\n",
              "      <td>57.582300</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>45</th>\n",
              "      <td>aws_byte_buf_init_copy</td>\n",
              "      <td>106</td>\n",
              "      <td>7.616</td>\n",
              "      <td>3.489740</td>\n",
              "      <td>34.86940</td>\n",
              "      <td>passed</td>\n",
              "      <td>5.961528</td>\n",
              "      <td>passed</td>\n",
              "      <td>18.848100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>46</th>\n",
              "      <td>aws_byte_buf_reserve</td>\n",
              "      <td>58</td>\n",
              "      <td>5.538</td>\n",
              "      <td>0.557796</td>\n",
              "      <td>9.56929</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.830248</td>\n",
              "      <td>passed</td>\n",
              "      <td>190.261000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>47</th>\n",
              "      <td>aws_byte_buf_secure_zero</td>\n",
              "      <td>61</td>\n",
              "      <td>9.662</td>\n",
              "      <td>0.629752</td>\n",
              "      <td>13.00540</td>\n",
              "      <td>passed</td>\n",
              "      <td>2.274849</td>\n",
              "      <td>passed</td>\n",
              "      <td>15.144100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>48</th>\n",
              "      <td>aws_byte_buf_write_be16</td>\n",
              "      <td>91</td>\n",
              "      <td>5.533</td>\n",
              "      <td>0.600137</td>\n",
              "      <td>18.51750</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.390989</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.498300</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>49</th>\n",
              "      <td>aws_byte_buf_reserve_relative</td>\n",
              "      <td>78</td>\n",
              "      <td>5.538</td>\n",
              "      <td>0.618307</td>\n",
              "      <td>16.21760</td>\n",
              "      <td>passed</td>\n",
              "      <td>8.028613</td>\n",
              "      <td>passed</td>\n",
              "      <td>204.610000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>50</th>\n",
              "      <td>aws_byte_buf_write_be32</td>\n",
              "      <td>91</td>\n",
              "      <td>5.531</td>\n",
              "      <td>0.603630</td>\n",
              "      <td>17.44820</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.821084</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.457000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>51</th>\n",
              "      <td>aws_byte_buf_write_be64</td>\n",
              "      <td>97</td>\n",
              "      <td>5.560</td>\n",
              "      <td>0.602039</td>\n",
              "      <td>22.48950</td>\n",
              "      <td>passed</td>\n",
              "      <td>6.426368</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.413400</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>52</th>\n",
              "      <td>aws_byte_buf_write</td>\n",
              "      <td>104</td>\n",
              "      <td>22.035</td>\n",
              "      <td>0.771093</td>\n",
              "      <td>25.56620</td>\n",
              "      <td>passed</td>\n",
              "      <td>8.537576</td>\n",
              "      <td>passed</td>\n",
              "      <td>23.641000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>53</th>\n",
              "      <td>aws_byte_buf_write_u8</td>\n",
              "      <td>86</td>\n",
              "      <td>5.545</td>\n",
              "      <td>0.626129</td>\n",
              "      <td>19.67880</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.161123</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.721800</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>54</th>\n",
              "      <td>aws_byte_buf_write_from_whole_string</td>\n",
              "      <td>135</td>\n",
              "      <td>11.750</td>\n",
              "      <td>3.581160</td>\n",
              "      <td>56.68580</td>\n",
              "      <td>passed</td>\n",
              "      <td>6.698325</td>\n",
              "      <td>passed</td>\n",
              "      <td>200.086000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>55</th>\n",
              "      <td>aws_byte_buf_write_from_whole_buffer</td>\n",
              "      <td>104</td>\n",
              "      <td>7.605</td>\n",
              "      <td>1.025240</td>\n",
              "      <td>139.10300</td>\n",
              "      <td>passed</td>\n",
              "      <td>13.066588</td>\n",
              "      <td>passed</td>\n",
              "      <td>117.722000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>56</th>\n",
              "      <td>aws_byte_buf_write_from_whole_cursor</td>\n",
              "      <td>124</td>\n",
              "      <td>5.532</td>\n",
              "      <td>0.928373</td>\n",
              "      <td>111.48500</td>\n",
              "      <td>passed</td>\n",
              "      <td>10.569678</td>\n",
              "      <td>passed</td>\n",
              "      <td>24.473100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>57</th>\n",
              "      <td>aws_byte_cursor_advance</td>\n",
              "      <td>75</td>\n",
              "      <td>5.545</td>\n",
              "      <td>0.678511</td>\n",
              "      <td>21.00780</td>\n",
              "      <td>passed</td>\n",
              "      <td>8.597914</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.854539</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>58</th>\n",
              "      <td>aws_array_list_init_dynamic</td>\n",
              "      <td>119</td>\n",
              "      <td>5.521</td>\n",
              "      <td>0.942406</td>\n",
              "      <td>11.18080</td>\n",
              "      <td>passed</td>\n",
              "      <td>96.177627</td>\n",
              "      <td>passed</td>\n",
              "      <td>61.918200</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>59</th>\n",
              "      <td>aws_byte_cursor_compare_lexical</td>\n",
              "      <td>117</td>\n",
              "      <td>5.556</td>\n",
              "      <td>1.332620</td>\n",
              "      <td>33.53630</td>\n",
              "      <td>passed</td>\n",
              "      <td>10.832756</td>\n",
              "      <td>passed</td>\n",
              "      <td>3.321880</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>60</th>\n",
              "      <td>aws_byte_cursor_eq</td>\n",
              "      <td>113</td>\n",
              "      <td>5.538</td>\n",
              "      <td>1.343270</td>\n",
              "      <td>34.22320</td>\n",
              "      <td>passed</td>\n",
              "      <td>7.796607</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.675450</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>61</th>\n",
              "      <td>aws_byte_cursor_compare_lookup</td>\n",
              "      <td>95</td>\n",
              "      <td>22.086</td>\n",
              "      <td>2.102970</td>\n",
              "      <td>26.26510</td>\n",
              "      <td>passed</td>\n",
              "      <td>10.614911</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.472990</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>62</th>\n",
              "      <td>aws_byte_cursor_from_array</td>\n",
              "      <td>47</td>\n",
              "      <td>6.154</td>\n",
              "      <td>0.556183</td>\n",
              "      <td>11.74340</td>\n",
              "      <td>passed</td>\n",
              "      <td>2.209961</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.076700</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>63</th>\n",
              "      <td>aws_byte_cursor_eq_byte_buf_ignore_case</td>\n",
              "      <td>108</td>\n",
              "      <td>5.563</td>\n",
              "      <td>1.965900</td>\n",
              "      <td>200.02800</td>\n",
              "      <td>timeout</td>\n",
              "      <td>8.434086</td>\n",
              "      <td>passed</td>\n",
              "      <td>33.023100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>64</th>\n",
              "      <td>aws_byte_cursor_eq_byte_buf</td>\n",
              "      <td>133</td>\n",
              "      <td>5.549</td>\n",
              "      <td>1.079570</td>\n",
              "      <td>57.82580</td>\n",
              "      <td>passed</td>\n",
              "      <td>9.833303</td>\n",
              "      <td>passed</td>\n",
              "      <td>36.155500</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>65</th>\n",
              "      <td>aws_byte_cursor_from_string</td>\n",
              "      <td>67</td>\n",
              "      <td>5.530</td>\n",
              "      <td>0.626926</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>2.432238</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.696300</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>66</th>\n",
              "      <td>aws_byte_cursor_from_buf</td>\n",
              "      <td>91</td>\n",
              "      <td>5.537</td>\n",
              "      <td>0.593421</td>\n",
              "      <td>32.33440</td>\n",
              "      <td>passed</td>\n",
              "      <td>5.969487</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.105600</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>67</th>\n",
              "      <td>aws_byte_cursor_eq_ignore_case</td>\n",
              "      <td>87</td>\n",
              "      <td>5.595</td>\n",
              "      <td>2.099110</td>\n",
              "      <td>200.02600</td>\n",
              "      <td>timeout</td>\n",
              "      <td>7.181199</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.172310</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>68</th>\n",
              "      <td>aws_byte_cursor_from_c_str</td>\n",
              "      <td>179</td>\n",
              "      <td>5.546</td>\n",
              "      <td>1.344770</td>\n",
              "      <td>12.91860</td>\n",
              "      <td>passed</td>\n",
              "      <td>5.822280</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.048800</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>69</th>\n",
              "      <td>aws_hash_ptr</td>\n",
              "      <td>118</td>\n",
              "      <td>3.460</td>\n",
              "      <td>0.541866</td>\n",
              "      <td>8.78063</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.709792</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.699002</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>70</th>\n",
              "      <td>aws_byte_cursor_eq_c_str</td>\n",
              "      <td>126</td>\n",
              "      <td>5.556</td>\n",
              "      <td>0.680068</td>\n",
              "      <td>7.90012</td>\n",
              "      <td>passed</td>\n",
              "      <td>12.348951</td>\n",
              "      <td>passed</td>\n",
              "      <td>35.235000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>71</th>\n",
              "      <td>aws_byte_cursor_left_trim_pred</td>\n",
              "      <td>65</td>\n",
              "      <td>5.840</td>\n",
              "      <td>0.601832</td>\n",
              "      <td>12.09670</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.030737</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.044740</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>72</th>\n",
              "      <td>aws_hash_string</td>\n",
              "      <td>154</td>\n",
              "      <td>7.607</td>\n",
              "      <td>0.918162</td>\n",
              "      <td>8.99937</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.728197</td>\n",
              "      <td>passed</td>\n",
              "      <td>13.440100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>73</th>\n",
              "      <td>aws_byte_cursor_satisfies_pred</td>\n",
              "      <td>69</td>\n",
              "      <td>5.587</td>\n",
              "      <td>0.589605</td>\n",
              "      <td>11.82750</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.100969</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.943669</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>74</th>\n",
              "      <td>aws_hash_array_ignore_case</td>\n",
              "      <td>36</td>\n",
              "      <td>5.529</td>\n",
              "      <td>0.597737</td>\n",
              "      <td>6.48574</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.963496</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.955100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>75</th>\n",
              "      <td>aws_byte_cursor_right_trim_pred</td>\n",
              "      <td>64</td>\n",
              "      <td>5.558</td>\n",
              "      <td>0.646027</td>\n",
              "      <td>12.19890</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.875386</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.182200</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>76</th>\n",
              "      <td>aws_hash_byte_cursor_ptr_ignore_case</td>\n",
              "      <td>55</td>\n",
              "      <td>5.541</td>\n",
              "      <td>0.650201</td>\n",
              "      <td>11.04390</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.883511</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.901374</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>77</th>\n",
              "      <td>aws_hash_c_string</td>\n",
              "      <td>266</td>\n",
              "      <td>5.558</td>\n",
              "      <td>1.617140</td>\n",
              "      <td>10.00300</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.683140</td>\n",
              "      <td>passed</td>\n",
              "      <td>2.494060</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>78</th>\n",
              "      <td>aws_byte_cursor_trim_pred</td>\n",
              "      <td>77</td>\n",
              "      <td>5.535</td>\n",
              "      <td>0.975555</td>\n",
              "      <td>19.88190</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.919954</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.347420</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>79</th>\n",
              "      <td>aws_hash_byte_cursor_ptr</td>\n",
              "      <td>149</td>\n",
              "      <td>5.593</td>\n",
              "      <td>2.634890</td>\n",
              "      <td>19.13910</td>\n",
              "      <td>passed</td>\n",
              "      <td>2.999034</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.888240</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>80</th>\n",
              "      <td>aws_hash_callback_string_destroy</td>\n",
              "      <td>49</td>\n",
              "      <td>5.547</td>\n",
              "      <td>0.738508</td>\n",
              "      <td>6.01216</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.168506</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.729700</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>81</th>\n",
              "      <td>aws_byte_cursor_eq_c_str_ignore_case</td>\n",
              "      <td>114</td>\n",
              "      <td>5.545</td>\n",
              "      <td>0.679927</td>\n",
              "      <td>8.36866</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.858831</td>\n",
              "      <td>passed</td>\n",
              "      <td>40.128500</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>82</th>\n",
              "      <td>aws_hash_iter_begin</td>\n",
              "      <td>169</td>\n",
              "      <td>9.673</td>\n",
              "      <td>2.113270</td>\n",
              "      <td>121.73100</td>\n",
              "      <td>passed</td>\n",
              "      <td>6.505089</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.799900</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>83</th>\n",
              "      <td>aws_hash_callback_string_eq</td>\n",
              "      <td>100</td>\n",
              "      <td>15.869</td>\n",
              "      <td>7.203580</td>\n",
              "      <td>13.20670</td>\n",
              "      <td>passed</td>\n",
              "      <td>7.542276</td>\n",
              "      <td>passed</td>\n",
              "      <td>72.696900</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>84</th>\n",
              "      <td>aws_hash_iter_done</td>\n",
              "      <td>170</td>\n",
              "      <td>9.655</td>\n",
              "      <td>1.075460</td>\n",
              "      <td>200.03500</td>\n",
              "      <td>timeout</td>\n",
              "      <td>17.416712</td>\n",
              "      <td>passed</td>\n",
              "      <td>15.555200</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>85</th>\n",
              "      <td>aws_byte_buf_append_dynamic</td>\n",
              "      <td>137</td>\n",
              "      <td>255.243</td>\n",
              "      <td>0.754565</td>\n",
              "      <td>35.56450</td>\n",
              "      <td>passed</td>\n",
              "      <td>93.823807</td>\n",
              "      <td>passed</td>\n",
              "      <td>619.066000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>86</th>\n",
              "      <td>aws_hash_table_clean_up</td>\n",
              "      <td>149</td>\n",
              "      <td>11.816</td>\n",
              "      <td>1.332630</td>\n",
              "      <td>19.96740</td>\n",
              "      <td>passed</td>\n",
              "      <td>2.761062</td>\n",
              "      <td>failed</td>\n",
              "      <td>58.281500</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>87</th>\n",
              "      <td>aws_hash_table_clear</td>\n",
              "      <td>147</td>\n",
              "      <td>32.393</td>\n",
              "      <td>1.335000</td>\n",
              "      <td>41.82110</td>\n",
              "      <td>passed</td>\n",
              "      <td>2.533879</td>\n",
              "      <td>failed</td>\n",
              "      <td>69.859800</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>88</th>\n",
              "      <td>aws_hash_iter_next</td>\n",
              "      <td>184</td>\n",
              "      <td>26.184</td>\n",
              "      <td>1.991080</td>\n",
              "      <td>200.03800</td>\n",
              "      <td>timeout</td>\n",
              "      <td>88.407692</td>\n",
              "      <td>passed</td>\n",
              "      <td>32.045300</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>89</th>\n",
              "      <td>aws_array_list_set_at</td>\n",
              "      <td>173</td>\n",
              "      <td>32.334</td>\n",
              "      <td>10.959900</td>\n",
              "      <td>18.71470</td>\n",
              "      <td>passed</td>\n",
              "      <td>195.126394</td>\n",
              "      <td>passed</td>\n",
              "      <td>164.274000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>90</th>\n",
              "      <td>aws_hash_callback_c_str_eq</td>\n",
              "      <td>198</td>\n",
              "      <td>7.625</td>\n",
              "      <td>6.775550</td>\n",
              "      <td>7.04312</td>\n",
              "      <td>passed</td>\n",
              "      <td>111.641870</td>\n",
              "      <td>passed</td>\n",
              "      <td>104.497000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>91</th>\n",
              "      <td>aws_hash_table_init_bounded</td>\n",
              "      <td>154</td>\n",
              "      <td>5.580</td>\n",
              "      <td>2.863630</td>\n",
              "      <td>200.06000</td>\n",
              "      <td>timeout</td>\n",
              "      <td>2.703048</td>\n",
              "      <td>unknown</td>\n",
              "      <td>0.810937</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>92</th>\n",
              "      <td>aws_hash_table_init_unbounded</td>\n",
              "      <td>139</td>\n",
              "      <td>5.518</td>\n",
              "      <td>1.870230</td>\n",
              "      <td>200.04700</td>\n",
              "      <td>timeout</td>\n",
              "      <td>3.682723</td>\n",
              "      <td>unknown</td>\n",
              "      <td>0.753008</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>93</th>\n",
              "      <td>aws_array_list_ensure_capacity</td>\n",
              "      <td>145</td>\n",
              "      <td>20.008</td>\n",
              "      <td>1.601460</td>\n",
              "      <td>11.99540</td>\n",
              "      <td>passed</td>\n",
              "      <td>286.109320</td>\n",
              "      <td>passed</td>\n",
              "      <td>122.926000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>94</th>\n",
              "      <td>aws_hash_table_remove</td>\n",
              "      <td>249</td>\n",
              "      <td>34.497</td>\n",
              "      <td>10.543500</td>\n",
              "      <td>98.09760</td>\n",
              "      <td>failed</td>\n",
              "      <td>24.564315</td>\n",
              "      <td>failed</td>\n",
              "      <td>NaN</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>95</th>\n",
              "      <td>aws_linked_list_back</td>\n",
              "      <td>155</td>\n",
              "      <td>9.939</td>\n",
              "      <td>1.909550</td>\n",
              "      <td>200.01900</td>\n",
              "      <td>timeout</td>\n",
              "      <td>16.436145</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.888105</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>96</th>\n",
              "      <td>aws_linked_list_begin</td>\n",
              "      <td>155</td>\n",
              "      <td>11.702</td>\n",
              "      <td>1.986690</td>\n",
              "      <td>200.03100</td>\n",
              "      <td>timeout</td>\n",
              "      <td>9.993401</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.698610</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>97</th>\n",
              "      <td>aws_linked_list_end</td>\n",
              "      <td>155</td>\n",
              "      <td>11.702</td>\n",
              "      <td>1.885760</td>\n",
              "      <td>200.02500</td>\n",
              "      <td>timeout</td>\n",
              "      <td>9.966741</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.713081</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>98</th>\n",
              "      <td>aws_hash_table_put</td>\n",
              "      <td>328</td>\n",
              "      <td>131.895</td>\n",
              "      <td>14.029200</td>\n",
              "      <td>200.02900</td>\n",
              "      <td>timeout</td>\n",
              "      <td>127.701653</td>\n",
              "      <td>failed</td>\n",
              "      <td>NaN</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>99</th>\n",
              "      <td>aws_linked_list_init</td>\n",
              "      <td>17</td>\n",
              "      <td>3.473</td>\n",
              "      <td>0.470781</td>\n",
              "      <td>7.60684</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.599962</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.624392</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>100</th>\n",
              "      <td>aws_linked_list_remove</td>\n",
              "      <td>42</td>\n",
              "      <td>3.458</td>\n",
              "      <td>0.459025</td>\n",
              "      <td>7.61812</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.106282</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.628084</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>101</th>\n",
              "      <td>aws_linked_list_front</td>\n",
              "      <td>164</td>\n",
              "      <td>9.670</td>\n",
              "      <td>2.944070</td>\n",
              "      <td>200.05000</td>\n",
              "      <td>timeout</td>\n",
              "      <td>16.340111</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.705006</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>102</th>\n",
              "      <td>aws_linked_list_pop_back</td>\n",
              "      <td>176</td>\n",
              "      <td>897.476</td>\n",
              "      <td>2.945460</td>\n",
              "      <td>83.64470</td>\n",
              "      <td>passed</td>\n",
              "      <td>9.657395</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.710971</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>103</th>\n",
              "      <td>aws_linked_list_prev</td>\n",
              "      <td>30</td>\n",
              "      <td>3.452</td>\n",
              "      <td>0.475934</td>\n",
              "      <td>9.13506</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.065334</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.626040</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>104</th>\n",
              "      <td>aws_linked_list_pop_front</td>\n",
              "      <td>175</td>\n",
              "      <td>17.923</td>\n",
              "      <td>2.635620</td>\n",
              "      <td>60.40960</td>\n",
              "      <td>passed</td>\n",
              "      <td>8.975306</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.713419</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>105</th>\n",
              "      <td>aws_linked_list_next</td>\n",
              "      <td>30</td>\n",
              "      <td>3.458</td>\n",
              "      <td>0.455268</td>\n",
              "      <td>8.93707</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.087559</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.629484</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>106</th>\n",
              "      <td>aws_linked_list_node_reset</td>\n",
              "      <td>22</td>\n",
              "      <td>3.468</td>\n",
              "      <td>0.489041</td>\n",
              "      <td>7.23196</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.676986</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.679178</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>107</th>\n",
              "      <td>aws_linked_list_push_front</td>\n",
              "      <td>174</td>\n",
              "      <td>13.775</td>\n",
              "      <td>2.758750</td>\n",
              "      <td>200.02900</td>\n",
              "      <td>timeout</td>\n",
              "      <td>8.892616</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.712323</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>108</th>\n",
              "      <td>aws_linked_list_push_back</td>\n",
              "      <td>174</td>\n",
              "      <td>9.727</td>\n",
              "      <td>2.149100</td>\n",
              "      <td>200.05900</td>\n",
              "      <td>timeout</td>\n",
              "      <td>9.605682</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.705207</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>109</th>\n",
              "      <td>aws_linked_list_insert_after</td>\n",
              "      <td>37</td>\n",
              "      <td>0.000</td>\n",
              "      <td>0.477970</td>\n",
              "      <td>7.70505</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.242478</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.626635</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>110</th>\n",
              "      <td>aws_linked_list_insert_before</td>\n",
              "      <td>37</td>\n",
              "      <td>5.526</td>\n",
              "      <td>0.459942</td>\n",
              "      <td>7.15392</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.022617</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.628908</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>111</th>\n",
              "      <td>aws_linked_list_swap_contents</td>\n",
              "      <td>219</td>\n",
              "      <td>32.336</td>\n",
              "      <td>9.346610</td>\n",
              "      <td>200.02400</td>\n",
              "      <td>timeout</td>\n",
              "      <td>17.288583</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.842707</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>112</th>\n",
              "      <td>aws_linked_list_rbegin</td>\n",
              "      <td>162</td>\n",
              "      <td>11.739</td>\n",
              "      <td>2.173240</td>\n",
              "      <td>200.02000</td>\n",
              "      <td>timeout</td>\n",
              "      <td>9.989123</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.718538</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>113</th>\n",
              "      <td>aws_string_bytes</td>\n",
              "      <td>11</td>\n",
              "      <td>5.519</td>\n",
              "      <td>0.821445</td>\n",
              "      <td>5.16363</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.265825</td>\n",
              "      <td>passed</td>\n",
              "      <td>23.591000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>114</th>\n",
              "      <td>aws_string_compare</td>\n",
              "      <td>108</td>\n",
              "      <td>7.723</td>\n",
              "      <td>4.471150</td>\n",
              "      <td>16.28260</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.176572</td>\n",
              "      <td>passed</td>\n",
              "      <td>120.523000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>115</th>\n",
              "      <td>aws_linked_list_rend</td>\n",
              "      <td>158</td>\n",
              "      <td>11.704</td>\n",
              "      <td>1.728550</td>\n",
              "      <td>200.02400</td>\n",
              "      <td>timeout</td>\n",
              "      <td>9.922645</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.698063</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>116</th>\n",
              "      <td>aws_string_eq</td>\n",
              "      <td>94</td>\n",
              "      <td>5.525</td>\n",
              "      <td>4.718130</td>\n",
              "      <td>16.58850</td>\n",
              "      <td>passed</td>\n",
              "      <td>6.241330</td>\n",
              "      <td>passed</td>\n",
              "      <td>47.352200</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>117</th>\n",
              "      <td>aws_string_eq_byte_buf</td>\n",
              "      <td>111</td>\n",
              "      <td>5.555</td>\n",
              "      <td>2.866010</td>\n",
              "      <td>17.58230</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.478320</td>\n",
              "      <td>passed</td>\n",
              "      <td>105.376000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>118</th>\n",
              "      <td>aws_string_eq_byte_cursor</td>\n",
              "      <td>111</td>\n",
              "      <td>5.551</td>\n",
              "      <td>2.647340</td>\n",
              "      <td>14.11670</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.290503</td>\n",
              "      <td>passed</td>\n",
              "      <td>21.754400</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>119</th>\n",
              "      <td>aws_string_eq_byte_buf_ignore_case</td>\n",
              "      <td>90</td>\n",
              "      <td>5.547</td>\n",
              "      <td>3.728160</td>\n",
              "      <td>200.01400</td>\n",
              "      <td>timeout</td>\n",
              "      <td>6.450362</td>\n",
              "      <td>passed</td>\n",
              "      <td>124.731000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>120</th>\n",
              "      <td>aws_string_eq_byte_cursor_ignore_case</td>\n",
              "      <td>85</td>\n",
              "      <td>5.542</td>\n",
              "      <td>5.833870</td>\n",
              "      <td>200.03100</td>\n",
              "      <td>timeout</td>\n",
              "      <td>6.969983</td>\n",
              "      <td>passed</td>\n",
              "      <td>27.624300</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>121</th>\n",
              "      <td>aws_string_eq_c_str</td>\n",
              "      <td>110</td>\n",
              "      <td>5.924</td>\n",
              "      <td>4.101140</td>\n",
              "      <td>6.18968</td>\n",
              "      <td>passed</td>\n",
              "      <td>26.331502</td>\n",
              "      <td>passed</td>\n",
              "      <td>152.627000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>122</th>\n",
              "      <td>aws_string_eq_ignore_case</td>\n",
              "      <td>70</td>\n",
              "      <td>7.615</td>\n",
              "      <td>2.097180</td>\n",
              "      <td>200.03500</td>\n",
              "      <td>timeout</td>\n",
              "      <td>10.381399</td>\n",
              "      <td>passed</td>\n",
              "      <td>129.772000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>123</th>\n",
              "      <td>aws_string_new_from_array</td>\n",
              "      <td>74</td>\n",
              "      <td>7.612</td>\n",
              "      <td>2.200290</td>\n",
              "      <td>11.59850</td>\n",
              "      <td>passed</td>\n",
              "      <td>3.381100</td>\n",
              "      <td>failed</td>\n",
              "      <td>368.975000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>124</th>\n",
              "      <td>aws_string_eq_c_str_ignore_case</td>\n",
              "      <td>99</td>\n",
              "      <td>5.545</td>\n",
              "      <td>5.721480</td>\n",
              "      <td>6.44981</td>\n",
              "      <td>passed</td>\n",
              "      <td>41.936581</td>\n",
              "      <td>passed</td>\n",
              "      <td>441.691000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>125</th>\n",
              "      <td>aws_string_new_from_string</td>\n",
              "      <td>60</td>\n",
              "      <td>9.661</td>\n",
              "      <td>2.477130</td>\n",
              "      <td>5.68750</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.955482</td>\n",
              "      <td>passed</td>\n",
              "      <td>482.315000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>126</th>\n",
              "      <td>aws_string_new_from_c_str</td>\n",
              "      <td>209</td>\n",
              "      <td>5.569</td>\n",
              "      <td>0.890971</td>\n",
              "      <td>6.18374</td>\n",
              "      <td>passed</td>\n",
              "      <td>10.277107</td>\n",
              "      <td>passed</td>\n",
              "      <td>15.622500</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>127</th>\n",
              "      <td>aws_string_destroy</td>\n",
              "      <td>11</td>\n",
              "      <td>5.532</td>\n",
              "      <td>0.618144</td>\n",
              "      <td>4.79947</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.006784</td>\n",
              "      <td>passed</td>\n",
              "      <td>17.642900</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>128</th>\n",
              "      <td>aws_priority_queue_size</td>\n",
              "      <td>163</td>\n",
              "      <td>9.682</td>\n",
              "      <td>1.311500</td>\n",
              "      <td>13.71030</td>\n",
              "      <td>passed</td>\n",
              "      <td>3.811704</td>\n",
              "      <td>passed</td>\n",
              "      <td>50.735200</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>129</th>\n",
              "      <td>aws_string_destroy_secure</td>\n",
              "      <td>71</td>\n",
              "      <td>5.532</td>\n",
              "      <td>0.764438</td>\n",
              "      <td>8.99991</td>\n",
              "      <td>passed</td>\n",
              "      <td>8.039869</td>\n",
              "      <td>passed</td>\n",
              "      <td>16.072100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>130</th>\n",
              "      <td>aws_priority_queue_capacity</td>\n",
              "      <td>167</td>\n",
              "      <td>19.978</td>\n",
              "      <td>1.359440</td>\n",
              "      <td>14.21500</td>\n",
              "      <td>passed</td>\n",
              "      <td>3.850561</td>\n",
              "      <td>passed</td>\n",
              "      <td>50.620500</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>131</th>\n",
              "      <td>aws_priority_queue_top</td>\n",
              "      <td>182</td>\n",
              "      <td>17.945</td>\n",
              "      <td>1.423610</td>\n",
              "      <td>14.99640</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.174022</td>\n",
              "      <td>passed</td>\n",
              "      <td>51.337400</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>132</th>\n",
              "      <td>aws_priority_queue_init_static</td>\n",
              "      <td>136</td>\n",
              "      <td>7.581</td>\n",
              "      <td>0.814609</td>\n",
              "      <td>15.51160</td>\n",
              "      <td>passed</td>\n",
              "      <td>34.986989</td>\n",
              "      <td>passed</td>\n",
              "      <td>17.777200</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>133</th>\n",
              "      <td>aws_priority_queue_clean_up</td>\n",
              "      <td>145</td>\n",
              "      <td>5.531</td>\n",
              "      <td>0.578392</td>\n",
              "      <td>12.72330</td>\n",
              "      <td>passed</td>\n",
              "      <td>3.952043</td>\n",
              "      <td>passed</td>\n",
              "      <td>50.677900</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>134</th>\n",
              "      <td>aws_ring_buffer_clean_up</td>\n",
              "      <td>84</td>\n",
              "      <td>5.534</td>\n",
              "      <td>0.727902</td>\n",
              "      <td>11.47400</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.800528</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.210900</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>135</th>\n",
              "      <td>aws_ring_buffer_init</td>\n",
              "      <td>56</td>\n",
              "      <td>5.559</td>\n",
              "      <td>0.724431</td>\n",
              "      <td>12.96420</td>\n",
              "      <td>passed</td>\n",
              "      <td>2.002098</td>\n",
              "      <td>passed</td>\n",
              "      <td>14.947100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>136</th>\n",
              "      <td>aws_priority_queue_s_swap</td>\n",
              "      <td>220</td>\n",
              "      <td>241.020</td>\n",
              "      <td>29.439000</td>\n",
              "      <td>17.77690</td>\n",
              "      <td>passed</td>\n",
              "      <td>3.916949</td>\n",
              "      <td>passed</td>\n",
              "      <td>50.530200</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>137</th>\n",
              "      <td>aws_priority_queue_s_sift_up</td>\n",
              "      <td>150</td>\n",
              "      <td>32.397</td>\n",
              "      <td>4.486220</td>\n",
              "      <td>21.52730</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.364510</td>\n",
              "      <td>passed</td>\n",
              "      <td>50.989600</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>138</th>\n",
              "      <td>aws_priority_queue_s_sift_down</td>\n",
              "      <td>149</td>\n",
              "      <td>253.113</td>\n",
              "      <td>4.264070</td>\n",
              "      <td>16.95470</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.512429</td>\n",
              "      <td>passed</td>\n",
              "      <td>50.913200</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>139</th>\n",
              "      <td>aws_priority_queue_s_sift_either</td>\n",
              "      <td>252</td>\n",
              "      <td>243.144</td>\n",
              "      <td>3.431760</td>\n",
              "      <td>16.58570</td>\n",
              "      <td>passed</td>\n",
              "      <td>1.441041</td>\n",
              "      <td>passed</td>\n",
              "      <td>50.715600</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>140</th>\n",
              "      <td>aws_priority_queue_s_remove_node</td>\n",
              "      <td>231</td>\n",
              "      <td>1068.309</td>\n",
              "      <td>3.838370</td>\n",
              "      <td>200.08600</td>\n",
              "      <td>timeout</td>\n",
              "      <td>1.356146</td>\n",
              "      <td>passed</td>\n",
              "      <td>51.077500</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>141</th>\n",
              "      <td>aws_priority_queue_remove</td>\n",
              "      <td>179</td>\n",
              "      <td>61.314</td>\n",
              "      <td>5.925930</td>\n",
              "      <td>17.77330</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.026698</td>\n",
              "      <td>passed</td>\n",
              "      <td>50.616800</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>142</th>\n",
              "      <td>aws_priority_queue_pop</td>\n",
              "      <td>171</td>\n",
              "      <td>59.176</td>\n",
              "      <td>4.576600</td>\n",
              "      <td>18.26510</td>\n",
              "      <td>passed</td>\n",
              "      <td>3.977713</td>\n",
              "      <td>passed</td>\n",
              "      <td>50.594500</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>143</th>\n",
              "      <td>aws_priority_queue_push</td>\n",
              "      <td>258</td>\n",
              "      <td>498.817</td>\n",
              "      <td>46.723700</td>\n",
              "      <td>14.74630</td>\n",
              "      <td>passed</td>\n",
              "      <td>4.038850</td>\n",
              "      <td>passed</td>\n",
              "      <td>50.831100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>144</th>\n",
              "      <td>aws_priority_queue_push_ref</td>\n",
              "      <td>256</td>\n",
              "      <td>597.828</td>\n",
              "      <td>50.194400</td>\n",
              "      <td>17.88260</td>\n",
              "      <td>passed</td>\n",
              "      <td>3.813849</td>\n",
              "      <td>passed</td>\n",
              "      <td>50.321700</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>145</th>\n",
              "      <td>aws_ring_buffer_release</td>\n",
              "      <td>173</td>\n",
              "      <td>9.698</td>\n",
              "      <td>21.590000</td>\n",
              "      <td>200.01300</td>\n",
              "      <td>timeout</td>\n",
              "      <td>7.493325</td>\n",
              "      <td>passed</td>\n",
              "      <td>60.245200</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>146</th>\n",
              "      <td>aws_priority_queue_init_dynamic</td>\n",
              "      <td>158</td>\n",
              "      <td>5.524</td>\n",
              "      <td>1.057230</td>\n",
              "      <td>18.87820</td>\n",
              "      <td>passed</td>\n",
              "      <td>76.114678</td>\n",
              "      <td>passed</td>\n",
              "      <td>17.677700</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>147</th>\n",
              "      <td>aws_hash_table_find</td>\n",
              "      <td>232</td>\n",
              "      <td>42.719</td>\n",
              "      <td>2.845770</td>\n",
              "      <td>78.86280</td>\n",
              "      <td>passed</td>\n",
              "      <td>358.987994</td>\n",
              "      <td>passed</td>\n",
              "      <td>35.352900</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>148</th>\n",
              "      <td>aws_ring_buffer_acquire</td>\n",
              "      <td>222</td>\n",
              "      <td>40.660</td>\n",
              "      <td>92.885200</td>\n",
              "      <td>200.02500</td>\n",
              "      <td>timeout</td>\n",
              "      <td>11.438466</td>\n",
              "      <td>passed</td>\n",
              "      <td>65.376900</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>149</th>\n",
              "      <td>aws_ring_buffer_buf_belongs_to_pool</td>\n",
              "      <td>172</td>\n",
              "      <td>9.661</td>\n",
              "      <td>38.137100</td>\n",
              "      <td>200.00700</td>\n",
              "      <td>timeout</td>\n",
              "      <td>13.923841</td>\n",
              "      <td>unknown</td>\n",
              "      <td>60.603300</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>150</th>\n",
              "      <td>aws_ring_buffer_acquire_up_to</td>\n",
              "      <td>227</td>\n",
              "      <td>48.958</td>\n",
              "      <td>23.098000</td>\n",
              "      <td>200.00900</td>\n",
              "      <td>timeout</td>\n",
              "      <td>25.983944</td>\n",
              "      <td>passed</td>\n",
              "      <td>73.465900</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>151</th>\n",
              "      <td>aws_mul_size_checked</td>\n",
              "      <td>39</td>\n",
              "      <td>3.460</td>\n",
              "      <td>0.733943</td>\n",
              "      <td>8.80271</td>\n",
              "      <td>passed</td>\n",
              "      <td>705.114054</td>\n",
              "      <td>passed</td>\n",
              "      <td>0.857620</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>152</th>\n",
              "      <td>aws_byte_buf_cat</td>\n",
              "      <td>129</td>\n",
              "      <td>69.512</td>\n",
              "      <td>0.960249</td>\n",
              "      <td>200.02200</td>\n",
              "      <td>timeout</td>\n",
              "      <td>878.966240</td>\n",
              "      <td>passed</td>\n",
              "      <td>NaN</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>153</th>\n",
              "      <td>aws_hash_table_move</td>\n",
              "      <td>132</td>\n",
              "      <td>5.526</td>\n",
              "      <td>0.821381</td>\n",
              "      <td>7.18115</td>\n",
              "      <td>passed</td>\n",
              "      <td>1870.328971</td>\n",
              "      <td>unknown</td>\n",
              "      <td>14.763000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>154</th>\n",
              "      <td>aws_hash_table_create</td>\n",
              "      <td>308</td>\n",
              "      <td>82.071</td>\n",
              "      <td>25.231500</td>\n",
              "      <td>200.02000</td>\n",
              "      <td>timeout</td>\n",
              "      <td>4685.712455</td>\n",
              "      <td>unknown</td>\n",
              "      <td>NaN</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>155</th>\n",
              "      <td>aws_hash_iter_delete</td>\n",
              "      <td>185</td>\n",
              "      <td>5.551</td>\n",
              "      <td>31.780800</td>\n",
              "      <td>91.30580</td>\n",
              "      <td>passed</td>\n",
              "      <td>5000.100000</td>\n",
              "      <td>timeout</td>\n",
              "      <td>NaN</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>156</th>\n",
              "      <td>aws_hash_table_eq</td>\n",
              "      <td>243</td>\n",
              "      <td>40.641</td>\n",
              "      <td>22.015800</td>\n",
              "      <td>200.02900</td>\n",
              "      <td>timeout</td>\n",
              "      <td>5000.010000</td>\n",
              "      <td>timeout</td>\n",
              "      <td>1307.330000</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>157</th>\n",
              "      <td>aws_hash_table_get_entry_count</td>\n",
              "      <td>134</td>\n",
              "      <td>5.559</td>\n",
              "      <td>0.843496</td>\n",
              "      <td>6.80937</td>\n",
              "      <td>passed</td>\n",
              "      <td>5000.010000</td>\n",
              "      <td>timeout</td>\n",
              "      <td>14.994100</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>158</th>\n",
              "      <td>aws_hash_table_swap</td>\n",
              "      <td>139</td>\n",
              "      <td>5.529</td>\n",
              "      <td>2.152910</td>\n",
              "      <td>7.58057</td>\n",
              "      <td>passed</td>\n",
              "      <td>5000.020000</td>\n",
              "      <td>timeout</td>\n",
              "      <td>33.334600</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>159</th>\n",
              "      <td>aws_hash_table_foreach</td>\n",
              "      <td>154</td>\n",
              "      <td>9.687</td>\n",
              "      <td>8.547760</td>\n",
              "      <td>32.96060</td>\n",
              "      <td>passed</td>\n",
              "      <td>5000.070000</td>\n",
              "      <td>timeout</td>\n",
              "      <td>NaN</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>160</th>\n",
              "      <td>aws_nospec_mask</td>\n",
              "      <td>21</td>\n",
              "      <td>3.477</td>\n",
              "      <td>0.538230</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>161</th>\n",
              "      <td>aws_byte_cursor_advance_nospec</td>\n",
              "      <td>88</td>\n",
              "      <td>5.530</td>\n",
              "      <td>0.763237</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>162</th>\n",
              "      <td>aws_byte_cursor_read</td>\n",
              "      <td>112</td>\n",
              "      <td>11.722</td>\n",
              "      <td>0.869950</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>163</th>\n",
              "      <td>aws_byte_cursor_read_and_fill_buffer</td>\n",
              "      <td>132</td>\n",
              "      <td>13.776</td>\n",
              "      <td>0.979490</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>164</th>\n",
              "      <td>aws_byte_cursor_read_be16</td>\n",
              "      <td>100</td>\n",
              "      <td>5.551</td>\n",
              "      <td>0.625419</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>165</th>\n",
              "      <td>aws_byte_cursor_read_be32</td>\n",
              "      <td>100</td>\n",
              "      <td>5.535</td>\n",
              "      <td>1.080750</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>166</th>\n",
              "      <td>aws_byte_cursor_read_be64</td>\n",
              "      <td>108</td>\n",
              "      <td>5.531</td>\n",
              "      <td>1.600060</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>167</th>\n",
              "      <td>aws_byte_cursor_read_u8</td>\n",
              "      <td>94</td>\n",
              "      <td>5.537</td>\n",
              "      <td>0.682532</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "      <td>NaN</td>\n",
              "    </tr>\n",
              "  </tbody>\n",
              "</table>\n",
              "</div>"
            ],
            "text/plain": [
              "                                    job name  loc  CBMC time (s)  \\\n",
              "0                        aws_is_power_of_two   11          3.443   \n",
              "1               aws_round_up_to_power_of_two   37          3.459   \n",
              "2                                 aws_ptr_eq   10          3.504   \n",
              "3                   aws_array_eq_ignore_case   78          5.536   \n",
              "4                    aws_array_list_capacity  107          5.530   \n",
              "5                        aws_array_list_back  129         13.785   \n",
              "6                    aws_array_list_clean_up   89          5.523   \n",
              "7                    aws_add_size_saturating   37          3.447   \n",
              "8                       aws_array_list_clear   77          5.511   \n",
              "9                               aws_array_eq  100          5.630   \n",
              "10          aws_array_list_comparator_string  110          7.624   \n",
              "11                      aws_add_size_checked   40          3.444   \n",
              "12                        aws_array_eq_c_str  112          5.534   \n",
              "13            aws_array_eq_c_str_ignore_case  100          5.534   \n",
              "14                      aws_array_list_front  128          7.594   \n",
              "15                     aws_array_list_length  105          7.590   \n",
              "16                 aws_array_list_get_at_ptr  125         11.730   \n",
              "17                     aws_array_list_get_at  128         11.728   \n",
              "18                   aws_array_list_pop_back  124         13.775   \n",
              "19                  aws_array_list_pop_front  137         17.929   \n",
              "20                aws_array_list_pop_front_n  129         20.003   \n",
              "21                       aws_array_list_sort  112         26.189   \n",
              "22                      aws_array_list_erase  166        172.636   \n",
              "23                aws_array_list_init_static  128          9.639   \n",
              "24                      aws_byte_buf_advance  110          7.628   \n",
              "25              aws_array_list_swap_contents  123         13.817   \n",
              "26                       aws_array_list_swap  111         83.886   \n",
              "27                  aws_array_list_push_back  181        259.178   \n",
              "28                     aws_byte_buf_clean_up   50          5.560   \n",
              "29              aws_array_list_shrink_to_fit  149         38.556   \n",
              "30                       aws_byte_buf_append   85          5.548   \n",
              "31              aws_byte_buf_clean_up_secure   61          7.601   \n",
              "32           aws_byte_buf_append_with_lookup  105          7.597   \n",
              "33                   aws_mul_size_saturating   38          5.509   \n",
              "34                   aws_byte_buf_from_array   52          5.531   \n",
              "35                           aws_byte_buf_eq  127          5.542   \n",
              "36                     aws_byte_buf_eq_c_str  142          5.571   \n",
              "37             aws_byte_buf_from_empty_array   52          5.529   \n",
              "38         aws_byte_buf_eq_c_str_ignore_case  130          5.543   \n",
              "39                         aws_byte_buf_init   53          5.516   \n",
              "40               aws_byte_buf_eq_ignore_case  101          5.560   \n",
              "41                   aws_byte_buf_from_c_str  188          5.532   \n",
              "42                       aws_array_list_copy  106         34.392   \n",
              "43                        aws_byte_buf_reset   71          5.538   \n",
              "44        aws_byte_buf_init_copy_from_cursor   89          5.537   \n",
              "45                    aws_byte_buf_init_copy  106          7.616   \n",
              "46                      aws_byte_buf_reserve   58          5.538   \n",
              "47                  aws_byte_buf_secure_zero   61          9.662   \n",
              "48                   aws_byte_buf_write_be16   91          5.533   \n",
              "49             aws_byte_buf_reserve_relative   78          5.538   \n",
              "50                   aws_byte_buf_write_be32   91          5.531   \n",
              "51                   aws_byte_buf_write_be64   97          5.560   \n",
              "52                        aws_byte_buf_write  104         22.035   \n",
              "53                     aws_byte_buf_write_u8   86          5.545   \n",
              "54      aws_byte_buf_write_from_whole_string  135         11.750   \n",
              "55      aws_byte_buf_write_from_whole_buffer  104          7.605   \n",
              "56      aws_byte_buf_write_from_whole_cursor  124          5.532   \n",
              "57                   aws_byte_cursor_advance   75          5.545   \n",
              "58               aws_array_list_init_dynamic  119          5.521   \n",
              "59           aws_byte_cursor_compare_lexical  117          5.556   \n",
              "60                        aws_byte_cursor_eq  113          5.538   \n",
              "61            aws_byte_cursor_compare_lookup   95         22.086   \n",
              "62                aws_byte_cursor_from_array   47          6.154   \n",
              "63   aws_byte_cursor_eq_byte_buf_ignore_case  108          5.563   \n",
              "64               aws_byte_cursor_eq_byte_buf  133          5.549   \n",
              "65               aws_byte_cursor_from_string   67          5.530   \n",
              "66                  aws_byte_cursor_from_buf   91          5.537   \n",
              "67            aws_byte_cursor_eq_ignore_case   87          5.595   \n",
              "68                aws_byte_cursor_from_c_str  179          5.546   \n",
              "69                              aws_hash_ptr  118          3.460   \n",
              "70                  aws_byte_cursor_eq_c_str  126          5.556   \n",
              "71            aws_byte_cursor_left_trim_pred   65          5.840   \n",
              "72                           aws_hash_string  154          7.607   \n",
              "73            aws_byte_cursor_satisfies_pred   69          5.587   \n",
              "74                aws_hash_array_ignore_case   36          5.529   \n",
              "75           aws_byte_cursor_right_trim_pred   64          5.558   \n",
              "76      aws_hash_byte_cursor_ptr_ignore_case   55          5.541   \n",
              "77                         aws_hash_c_string  266          5.558   \n",
              "78                 aws_byte_cursor_trim_pred   77          5.535   \n",
              "79                  aws_hash_byte_cursor_ptr  149          5.593   \n",
              "80          aws_hash_callback_string_destroy   49          5.547   \n",
              "81      aws_byte_cursor_eq_c_str_ignore_case  114          5.545   \n",
              "82                       aws_hash_iter_begin  169          9.673   \n",
              "83               aws_hash_callback_string_eq  100         15.869   \n",
              "84                        aws_hash_iter_done  170          9.655   \n",
              "85               aws_byte_buf_append_dynamic  137        255.243   \n",
              "86                   aws_hash_table_clean_up  149         11.816   \n",
              "87                      aws_hash_table_clear  147         32.393   \n",
              "88                        aws_hash_iter_next  184         26.184   \n",
              "89                     aws_array_list_set_at  173         32.334   \n",
              "90                aws_hash_callback_c_str_eq  198          7.625   \n",
              "91               aws_hash_table_init_bounded  154          5.580   \n",
              "92             aws_hash_table_init_unbounded  139          5.518   \n",
              "93            aws_array_list_ensure_capacity  145         20.008   \n",
              "94                     aws_hash_table_remove  249         34.497   \n",
              "95                      aws_linked_list_back  155          9.939   \n",
              "96                     aws_linked_list_begin  155         11.702   \n",
              "97                       aws_linked_list_end  155         11.702   \n",
              "98                        aws_hash_table_put  328        131.895   \n",
              "99                      aws_linked_list_init   17          3.473   \n",
              "100                   aws_linked_list_remove   42          3.458   \n",
              "101                    aws_linked_list_front  164          9.670   \n",
              "102                 aws_linked_list_pop_back  176        897.476   \n",
              "103                     aws_linked_list_prev   30          3.452   \n",
              "104                aws_linked_list_pop_front  175         17.923   \n",
              "105                     aws_linked_list_next   30          3.458   \n",
              "106               aws_linked_list_node_reset   22          3.468   \n",
              "107               aws_linked_list_push_front  174         13.775   \n",
              "108                aws_linked_list_push_back  174          9.727   \n",
              "109             aws_linked_list_insert_after   37          0.000   \n",
              "110            aws_linked_list_insert_before   37          5.526   \n",
              "111            aws_linked_list_swap_contents  219         32.336   \n",
              "112                   aws_linked_list_rbegin  162         11.739   \n",
              "113                         aws_string_bytes   11          5.519   \n",
              "114                       aws_string_compare  108          7.723   \n",
              "115                     aws_linked_list_rend  158         11.704   \n",
              "116                            aws_string_eq   94          5.525   \n",
              "117                   aws_string_eq_byte_buf  111          5.555   \n",
              "118                aws_string_eq_byte_cursor  111          5.551   \n",
              "119       aws_string_eq_byte_buf_ignore_case   90          5.547   \n",
              "120    aws_string_eq_byte_cursor_ignore_case   85          5.542   \n",
              "121                      aws_string_eq_c_str  110          5.924   \n",
              "122                aws_string_eq_ignore_case   70          7.615   \n",
              "123                aws_string_new_from_array   74          7.612   \n",
              "124          aws_string_eq_c_str_ignore_case   99          5.545   \n",
              "125               aws_string_new_from_string   60          9.661   \n",
              "126                aws_string_new_from_c_str  209          5.569   \n",
              "127                       aws_string_destroy   11          5.532   \n",
              "128                  aws_priority_queue_size  163          9.682   \n",
              "129                aws_string_destroy_secure   71          5.532   \n",
              "130              aws_priority_queue_capacity  167         19.978   \n",
              "131                   aws_priority_queue_top  182         17.945   \n",
              "132           aws_priority_queue_init_static  136          7.581   \n",
              "133              aws_priority_queue_clean_up  145          5.531   \n",
              "134                 aws_ring_buffer_clean_up   84          5.534   \n",
              "135                     aws_ring_buffer_init   56          5.559   \n",
              "136                aws_priority_queue_s_swap  220        241.020   \n",
              "137             aws_priority_queue_s_sift_up  150         32.397   \n",
              "138           aws_priority_queue_s_sift_down  149        253.113   \n",
              "139         aws_priority_queue_s_sift_either  252        243.144   \n",
              "140         aws_priority_queue_s_remove_node  231       1068.309   \n",
              "141                aws_priority_queue_remove  179         61.314   \n",
              "142                   aws_priority_queue_pop  171         59.176   \n",
              "143                  aws_priority_queue_push  258        498.817   \n",
              "144              aws_priority_queue_push_ref  256        597.828   \n",
              "145                  aws_ring_buffer_release  173          9.698   \n",
              "146          aws_priority_queue_init_dynamic  158          5.524   \n",
              "147                      aws_hash_table_find  232         42.719   \n",
              "148                  aws_ring_buffer_acquire  222         40.660   \n",
              "149      aws_ring_buffer_buf_belongs_to_pool  172          9.661   \n",
              "150            aws_ring_buffer_acquire_up_to  227         48.958   \n",
              "151                     aws_mul_size_checked   39          3.460   \n",
              "152                         aws_byte_buf_cat  129         69.512   \n",
              "153                      aws_hash_table_move  132          5.526   \n",
              "154                    aws_hash_table_create  308         82.071   \n",
              "155                     aws_hash_iter_delete  185          5.551   \n",
              "156                        aws_hash_table_eq  243         40.641   \n",
              "157           aws_hash_table_get_entry_count  134          5.559   \n",
              "158                      aws_hash_table_swap  139          5.529   \n",
              "159                   aws_hash_table_foreach  154          9.687   \n",
              "160                          aws_nospec_mask   21          3.477   \n",
              "161           aws_byte_cursor_advance_nospec   88          5.530   \n",
              "162                     aws_byte_cursor_read  112         11.722   \n",
              "163     aws_byte_cursor_read_and_fill_buffer  132         13.776   \n",
              "164                aws_byte_cursor_read_be16  100          5.551   \n",
              "165                aws_byte_cursor_read_be32  100          5.535   \n",
              "166                aws_byte_cursor_read_be64  108          5.531   \n",
              "167                  aws_byte_cursor_read_u8   94          5.537   \n",
              "\n",
              "     Seahorn normal time (s)  Smack time (s) Smack result  Symbiotic time (s)  \\\n",
              "0                   0.444965         7.21547       failed            1.515958   \n",
              "1                   0.642792         7.41379       failed            4.046049   \n",
              "2                   0.500028         4.44428       passed            4.671042   \n",
              "3                   2.080760       200.02300      timeout            6.290933   \n",
              "4                   0.786557        11.60290       passed            5.474102   \n",
              "5                   0.952469        12.32640       passed            8.467914   \n",
              "6                   0.498641        10.87460       passed            4.724258   \n",
              "7                   0.549630         5.47448       passed            8.886539   \n",
              "8                   1.423880        10.55720       passed            4.150718   \n",
              "9                   2.196110        16.68940       passed            9.633242   \n",
              "10                  6.306280        19.72590       passed            4.348738   \n",
              "11                  0.624538         8.06627       passed           11.656799   \n",
              "12                  1.700990         6.43832       passed           12.400516   \n",
              "13                  0.670247         7.09141       passed           15.828431   \n",
              "14                  1.094380        11.82420       passed            6.972152   \n",
              "15                  0.785986        11.55540       passed            5.479497   \n",
              "16                  0.813469        13.09160       passed            8.745562   \n",
              "17                  0.709902        13.58510       passed            9.530712   \n",
              "18                  1.308630        17.05080       passed           10.120248   \n",
              "19                  1.375760        15.87950       passed           17.798371   \n",
              "20                  2.238250        13.11020       passed           23.865669   \n",
              "21                  0.811297        10.87240       passed            8.093429   \n",
              "22                  2.095370        13.46420       passed           40.334799   \n",
              "23                  0.990409        12.17270       passed           43.936742   \n",
              "24                  0.700093        69.98620       passed            8.880398   \n",
              "25                  1.636210        13.95710       passed           16.766813   \n",
              "26                 13.352000        12.10000       passed           18.280318   \n",
              "27                  1.463280        13.74180       passed           44.513344   \n",
              "28                  0.534919        10.23340       passed            2.055410   \n",
              "29                  1.567210        11.65050       passed           40.644580   \n",
              "30                  0.624864        24.36980       passed           11.664072   \n",
              "31                  0.538965        10.20340       passed            2.457513   \n",
              "32                  1.094130        26.90020       passed            9.295327   \n",
              "33                  0.761364         6.15913       passed           77.413389   \n",
              "34                  0.566631        11.18790       passed            2.407168   \n",
              "35                  2.254840       105.37700       passed           13.762205   \n",
              "36                  0.698345         8.05915       passed           13.874403   \n",
              "37                  0.560820        11.99540       passed            2.245510   \n",
              "38                  0.677644         8.27622       passed           16.806220   \n",
              "39                  0.551112        12.23750       passed            3.228677   \n",
              "40                  1.596800       200.02500      timeout           16.878187   \n",
              "41                  1.812950        13.85310       passed            5.665581   \n",
              "42                  3.284130        11.88310       passed           80.543497   \n",
              "43                  0.615145        15.24990       passed            2.297113   \n",
              "44                  0.666797        22.23290       passed            3.744924   \n",
              "45                  3.489740        34.86940       passed            5.961528   \n",
              "46                  0.557796         9.56929       passed            4.830248   \n",
              "47                  0.629752        13.00540       passed            2.274849   \n",
              "48                  0.600137        18.51750       passed            4.390989   \n",
              "49                  0.618307        16.21760       passed            8.028613   \n",
              "50                  0.603630        17.44820       passed            4.821084   \n",
              "51                  0.602039        22.48950       passed            6.426368   \n",
              "52                  0.771093        25.56620       passed            8.537576   \n",
              "53                  0.626129        19.67880       passed            4.161123   \n",
              "54                  3.581160        56.68580       passed            6.698325   \n",
              "55                  1.025240       139.10300       passed           13.066588   \n",
              "56                  0.928373       111.48500       passed           10.569678   \n",
              "57                  0.678511        21.00780       passed            8.597914   \n",
              "58                  0.942406        11.18080       passed           96.177627   \n",
              "59                  1.332620        33.53630       passed           10.832756   \n",
              "60                  1.343270        34.22320       passed            7.796607   \n",
              "61                  2.102970        26.26510       passed           10.614911   \n",
              "62                  0.556183        11.74340       passed            2.209961   \n",
              "63                  1.965900       200.02800      timeout            8.434086   \n",
              "64                  1.079570        57.82580       passed            9.833303   \n",
              "65                  0.626926             NaN          NaN            2.432238   \n",
              "66                  0.593421        32.33440       passed            5.969487   \n",
              "67                  2.099110       200.02600      timeout            7.181199   \n",
              "68                  1.344770        12.91860       passed            5.822280   \n",
              "69                  0.541866         8.78063       passed            0.709792   \n",
              "70                  0.680068         7.90012       passed           12.348951   \n",
              "71                  0.601832        12.09670       passed            4.030737   \n",
              "72                  0.918162         8.99937       passed            0.728197   \n",
              "73                  0.589605        11.82750       passed            4.100969   \n",
              "74                  0.597737         6.48574       passed            1.963496   \n",
              "75                  0.646027        12.19890       passed            4.875386   \n",
              "76                  0.650201        11.04390       passed            1.883511   \n",
              "77                  1.617140        10.00300       passed            0.683140   \n",
              "78                  0.975555        19.88190       passed            4.919954   \n",
              "79                  2.634890        19.13910       passed            2.999034   \n",
              "80                  0.738508         6.01216       passed            1.168506   \n",
              "81                  0.679927         8.36866       passed           14.858831   \n",
              "82                  2.113270       121.73100       passed            6.505089   \n",
              "83                  7.203580        13.20670       passed            7.542276   \n",
              "84                  1.075460       200.03500      timeout           17.416712   \n",
              "85                  0.754565        35.56450       passed           93.823807   \n",
              "86                  1.332630        19.96740       passed            2.761062   \n",
              "87                  1.335000        41.82110       passed            2.533879   \n",
              "88                  1.991080       200.03800      timeout           88.407692   \n",
              "89                 10.959900        18.71470       passed          195.126394   \n",
              "90                  6.775550         7.04312       passed          111.641870   \n",
              "91                  2.863630       200.06000      timeout            2.703048   \n",
              "92                  1.870230       200.04700      timeout            3.682723   \n",
              "93                  1.601460        11.99540       passed          286.109320   \n",
              "94                 10.543500        98.09760       failed           24.564315   \n",
              "95                  1.909550       200.01900      timeout           16.436145   \n",
              "96                  1.986690       200.03100      timeout            9.993401   \n",
              "97                  1.885760       200.02500      timeout            9.966741   \n",
              "98                 14.029200       200.02900      timeout          127.701653   \n",
              "99                  0.470781         7.60684       passed            0.599962   \n",
              "100                 0.459025         7.61812       passed            4.106282   \n",
              "101                 2.944070       200.05000      timeout           16.340111   \n",
              "102                 2.945460        83.64470       passed            9.657395   \n",
              "103                 0.475934         9.13506       passed            1.065334   \n",
              "104                 2.635620        60.40960       passed            8.975306   \n",
              "105                 0.455268         8.93707       passed            1.087559   \n",
              "106                 0.489041         7.23196       passed            0.676986   \n",
              "107                 2.758750       200.02900      timeout            8.892616   \n",
              "108                 2.149100       200.05900      timeout            9.605682   \n",
              "109                 0.477970         7.70505       passed            4.242478   \n",
              "110                 0.459942         7.15392       passed            4.022617   \n",
              "111                 9.346610       200.02400      timeout           17.288583   \n",
              "112                 2.173240       200.02000      timeout            9.989123   \n",
              "113                 0.821445         5.16363       passed            1.265825   \n",
              "114                 4.471150        16.28260       passed            4.176572   \n",
              "115                 1.728550       200.02400      timeout            9.922645   \n",
              "116                 4.718130        16.58850       passed            6.241330   \n",
              "117                 2.866010        17.58230       passed            4.478320   \n",
              "118                 2.647340        14.11670       passed            4.290503   \n",
              "119                 3.728160       200.01400      timeout            6.450362   \n",
              "120                 5.833870       200.03100      timeout            6.969983   \n",
              "121                 4.101140         6.18968       passed           26.331502   \n",
              "122                 2.097180       200.03500      timeout           10.381399   \n",
              "123                 2.200290        11.59850       passed            3.381100   \n",
              "124                 5.721480         6.44981       passed           41.936581   \n",
              "125                 2.477130         5.68750       passed            1.955482   \n",
              "126                 0.890971         6.18374       passed           10.277107   \n",
              "127                 0.618144         4.79947       passed            1.006784   \n",
              "128                 1.311500        13.71030       passed            3.811704   \n",
              "129                 0.764438         8.99991       passed            8.039869   \n",
              "130                 1.359440        14.21500       passed            3.850561   \n",
              "131                 1.423610        14.99640       passed            4.174022   \n",
              "132                 0.814609        15.51160       passed           34.986989   \n",
              "133                 0.578392        12.72330       passed            3.952043   \n",
              "134                 0.727902        11.47400       passed            1.800528   \n",
              "135                 0.724431        12.96420       passed            2.002098   \n",
              "136                29.439000        17.77690       passed            3.916949   \n",
              "137                 4.486220        21.52730       passed            1.364510   \n",
              "138                 4.264070        16.95470       passed            1.512429   \n",
              "139                 3.431760        16.58570       passed            1.441041   \n",
              "140                 3.838370       200.08600      timeout            1.356146   \n",
              "141                 5.925930        17.77330       passed            4.026698   \n",
              "142                 4.576600        18.26510       passed            3.977713   \n",
              "143                46.723700        14.74630       passed            4.038850   \n",
              "144                50.194400        17.88260       passed            3.813849   \n",
              "145                21.590000       200.01300      timeout            7.493325   \n",
              "146                 1.057230        18.87820       passed           76.114678   \n",
              "147                 2.845770        78.86280       passed          358.987994   \n",
              "148                92.885200       200.02500      timeout           11.438466   \n",
              "149                38.137100       200.00700      timeout           13.923841   \n",
              "150                23.098000       200.00900      timeout           25.983944   \n",
              "151                 0.733943         8.80271       passed          705.114054   \n",
              "152                 0.960249       200.02200      timeout          878.966240   \n",
              "153                 0.821381         7.18115       passed         1870.328971   \n",
              "154                25.231500       200.02000      timeout         4685.712455   \n",
              "155                31.780800        91.30580       passed         5000.100000   \n",
              "156                22.015800       200.02900      timeout         5000.010000   \n",
              "157                 0.843496         6.80937       passed         5000.010000   \n",
              "158                 2.152910         7.58057       passed         5000.020000   \n",
              "159                 8.547760        32.96060       passed         5000.070000   \n",
              "160                 0.538230             NaN          NaN                 NaN   \n",
              "161                 0.763237             NaN          NaN                 NaN   \n",
              "162                 0.869950             NaN          NaN                 NaN   \n",
              "163                 0.979490             NaN          NaN                 NaN   \n",
              "164                 0.625419             NaN          NaN                 NaN   \n",
              "165                 1.080750             NaN          NaN                 NaN   \n",
              "166                 1.600060             NaN          NaN                 NaN   \n",
              "167                 0.682532             NaN          NaN                 NaN   \n",
              "\n",
              "    Symbiotic result  Klee time (s)  \n",
              "0             passed       0.718919  \n",
              "1             passed       0.794902  \n",
              "2             passed       0.727793  \n",
              "3             passed      33.526500  \n",
              "4             passed      13.619400  \n",
              "5             passed      90.595000  \n",
              "6             passed      13.826800  \n",
              "7             passed       0.811040  \n",
              "8             passed      13.905400  \n",
              "9             passed      34.978200  \n",
              "10            passed     121.267000  \n",
              "11            passed       0.740112  \n",
              "12            passed      37.000100  \n",
              "13            passed      23.555400  \n",
              "14            passed      89.584100  \n",
              "15            passed      13.734800  \n",
              "16            passed      13.380200  \n",
              "17            passed      89.813300  \n",
              "18            passed      14.183500  \n",
              "19            passed      14.335100  \n",
              "20            passed      14.311600  \n",
              "21            passed      14.340100  \n",
              "22            passed      15.621800  \n",
              "23            passed      60.675600  \n",
              "24            passed      57.667000  \n",
              "25            passed      51.240800  \n",
              "26            passed      14.588200  \n",
              "27            passed      70.661700  \n",
              "28            passed      14.219600  \n",
              "29            passed      41.323900  \n",
              "30            passed      17.381200  \n",
              "31            passed      14.791000  \n",
              "32            passed      18.123400  \n",
              "33            passed       1.450430  \n",
              "34            passed      14.097200  \n",
              "35            passed      94.835300  \n",
              "36            passed      77.557800  \n",
              "37            passed      14.233100  \n",
              "38            passed      99.036600  \n",
              "39            passed      52.602700  \n",
              "40            passed            NaN  \n",
              "41            passed      14.431300  \n",
              "42            passed     155.075000  \n",
              "43            passed      15.083100  \n",
              "44            passed      57.582300  \n",
              "45            passed      18.848100  \n",
              "46            passed     190.261000  \n",
              "47            passed      15.144100  \n",
              "48            passed      14.498300  \n",
              "49            passed     204.610000  \n",
              "50            passed      14.457000  \n",
              "51            passed      14.413400  \n",
              "52            passed      23.641000  \n",
              "53            passed      14.721800  \n",
              "54            passed     200.086000  \n",
              "55            passed     117.722000  \n",
              "56            passed      24.473100  \n",
              "57            passed       0.854539  \n",
              "58            passed      61.918200  \n",
              "59            passed       3.321880  \n",
              "60            passed       1.675450  \n",
              "61            passed       4.472990  \n",
              "62            passed      14.076700  \n",
              "63            passed      33.023100  \n",
              "64            passed      36.155500  \n",
              "65            passed      14.696300  \n",
              "66            passed      14.105600  \n",
              "67            passed       1.172310  \n",
              "68            passed      14.048800  \n",
              "69            passed       0.699002  \n",
              "70            passed      35.235000  \n",
              "71            passed       1.044740  \n",
              "72            passed      13.440100  \n",
              "73            passed       0.943669  \n",
              "74            passed      14.955100  \n",
              "75            passed       1.182200  \n",
              "76            passed       0.901374  \n",
              "77            passed       2.494060  \n",
              "78            passed       1.347420  \n",
              "79            passed       0.888240  \n",
              "80            passed      14.729700  \n",
              "81            passed      40.128500  \n",
              "82            passed      14.799900  \n",
              "83            passed      72.696900  \n",
              "84            passed      15.555200  \n",
              "85            passed     619.066000  \n",
              "86            failed      58.281500  \n",
              "87            failed      69.859800  \n",
              "88            passed      32.045300  \n",
              "89            passed     164.274000  \n",
              "90            passed     104.497000  \n",
              "91           unknown       0.810937  \n",
              "92           unknown       0.753008  \n",
              "93            passed     122.926000  \n",
              "94            failed            NaN  \n",
              "95            passed       0.888105  \n",
              "96            passed       0.698610  \n",
              "97            passed       0.713081  \n",
              "98            failed            NaN  \n",
              "99            passed       0.624392  \n",
              "100           passed       0.628084  \n",
              "101           passed       0.705006  \n",
              "102           passed       0.710971  \n",
              "103           passed       0.626040  \n",
              "104           passed       0.713419  \n",
              "105           passed       0.629484  \n",
              "106           passed       0.679178  \n",
              "107           passed       0.712323  \n",
              "108           passed       0.705207  \n",
              "109           passed       0.626635  \n",
              "110           passed       0.628908  \n",
              "111           passed       0.842707  \n",
              "112           passed       0.718538  \n",
              "113           passed      23.591000  \n",
              "114           passed     120.523000  \n",
              "115           passed       0.698063  \n",
              "116           passed      47.352200  \n",
              "117           passed     105.376000  \n",
              "118           passed      21.754400  \n",
              "119           passed     124.731000  \n",
              "120           passed      27.624300  \n",
              "121           passed     152.627000  \n",
              "122           passed     129.772000  \n",
              "123           failed     368.975000  \n",
              "124           passed     441.691000  \n",
              "125           passed     482.315000  \n",
              "126           passed      15.622500  \n",
              "127           passed      17.642900  \n",
              "128           passed      50.735200  \n",
              "129           passed      16.072100  \n",
              "130           passed      50.620500  \n",
              "131           passed      51.337400  \n",
              "132           passed      17.777200  \n",
              "133           passed      50.677900  \n",
              "134           passed      14.210900  \n",
              "135           passed      14.947100  \n",
              "136           passed      50.530200  \n",
              "137           passed      50.989600  \n",
              "138           passed      50.913200  \n",
              "139           passed      50.715600  \n",
              "140           passed      51.077500  \n",
              "141           passed      50.616800  \n",
              "142           passed      50.594500  \n",
              "143           passed      50.831100  \n",
              "144           passed      50.321700  \n",
              "145           passed      60.245200  \n",
              "146           passed      17.677700  \n",
              "147           passed      35.352900  \n",
              "148           passed      65.376900  \n",
              "149          unknown      60.603300  \n",
              "150           passed      73.465900  \n",
              "151           passed       0.857620  \n",
              "152           passed            NaN  \n",
              "153          unknown      14.763000  \n",
              "154          unknown            NaN  \n",
              "155          timeout            NaN  \n",
              "156          timeout    1307.330000  \n",
              "157          timeout      14.994100  \n",
              "158          timeout      33.334600  \n",
              "159          timeout            NaN  \n",
              "160              NaN            NaN  \n",
              "161              NaN            NaN  \n",
              "162              NaN            NaN  \n",
              "163              NaN            NaN  \n",
              "164              NaN            NaN  \n",
              "165              NaN            NaN  \n",
              "166              NaN            NaN  \n",
              "167              NaN            NaN  "
            ]
          },
          "execution_count": 3,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "# The result for normal mode...\n",
        "seahorn_norm = pd.read_csv(SEAHORN_CSV)\n",
        "seahorn_norm.loc[seahorn_norm['Timing'] == 'Completed', 'Timing'] = 0.0\n",
        "seahorn_norm['Timing'] = seahorn_norm['Timing'].astype(float)\n",
        "# The result for aws/cbmc...\n",
        "aws_cbmc = pd.read_csv(CBMC_CSV)\n",
        "# The result for smack...\n",
        "smack = pd.read_csv(SMACK_CSV)\n",
        "# The result for symbiotic...\n",
        "symbiotic = pd.read_csv(SYMBIOTIC_CSV)\n",
        "# The result for klee...\n",
        "klee = pd.read_csv(KLEE_CSV)\n",
        "# The result for loc...\n",
        "jobs_loc = pd.read_csv(LOC_CSV)\n",
        "\n",
        "# Rename column's name\n",
        "cbmc_time = aws_cbmc[['bench name', 'total times (s)']].rename(columns = {'total times (s)': 'CBMC time (s)', 'bench name': 'job name'})\n",
        "seahorn_time = seahorn_norm[['Name', 'Timing']].rename(columns = {'Timing':'Seahorn normal time (s)'})\n",
        "smack.loc[smack['Timing'] > 200.0, 'Result'] = 'timeout'\n",
        "smack_time = smack[['Name', 'Timing', 'Result']].rename(columns = {'Timing':'Smack time (s)', 'Result': 'Smack result'})\n",
        "symbiotic.loc[symbiotic['Timing'] > 5000.0, 'Result'] = 'timeout'\n",
        "symbiotic_time = symbiotic[['Name', 'Timing', 'Result']].rename(columns = {'Timing':'Symbiotic time (s)', 'Result': 'Symbiotic result'})\n",
        "klee_time = klee[['Name', 'Timing']].rename(columns = {'Timing': 'Klee time (s)'})\n",
        "jobs_loc = jobs_loc.rename(columns = {'LOC': 'loc'})\n",
        "# Rename job's name\n",
        "seahorn_time['job name'] = seahorn_time['Name'].map(lambda name : 'aws_{}'.format(name[:-11]))\n",
        "smack_time['job name'] = smack_time['Name'].map(lambda name : 'aws_{}'.format(name[6:-5]))\n",
        "symbiotic_time['job name'] = symbiotic_time['Name'].map(lambda name : 'aws_{}'.format(name[10:-5]))\n",
        "klee_time['job name'] = klee_time['Name'].map(lambda name : 'aws_{}'.format(name[5:-5]))\n",
        "jobs_loc['job name'] = jobs_loc['Name'].map(lambda name : 'aws_{}'.format(name))\n",
        "# Drop uncessary columns\n",
        "seahorn_time = seahorn_time.drop(columns=['Name'])\n",
        "smack_time = smack_time.drop(columns=['Name'])\n",
        "symbiotic_time = symbiotic_time.drop(columns=['Name'])\n",
        "klee_time = klee_time.drop(columns=['Name'])\n",
        "\n",
        "# Merge results into one dataframe and rearrange it\n",
        "sea_cbmc = pd.merge(seahorn_time, cbmc_time, how='outer', on='job name')\n",
        "sea_cbmc_smack = pd.merge(smack_time, sea_cbmc, how='outer', on='job name')\n",
        "sea_cbmc_smack_symb = pd.merge(symbiotic_time, sea_cbmc_smack, how='outer', on='job name')\n",
        "sea_cbmc_klee = pd.merge(sea_cbmc_smack_symb, klee_time, how='outer', on='job name')\n",
        "comb_loc = pd.merge(sea_cbmc_klee, jobs_loc, how='outer', on='job name')\n",
        "combined = comb_loc[['job name', 'loc', 'CBMC time (s)', 'Seahorn normal time (s)', 'Smack time (s)', 'Smack result', 'Symbiotic time (s)', 'Symbiotic result', 'Klee time (s)']]\n",
        "\n",
        "# Remove unwanted harnesses res\n",
        "drop_harness_lst = ['aws_hash_iter_begin_done', 'memcpy_using_uint64', 'memset_override_0', \n",
        "                    'memset_using_uint64', 'aws_hash_table_foreach_deep_loose', \n",
        "                    'aws_byte_buf_eq2', 'aws_hash_table_foreach_deep_precise']\n",
        "for drop_harn in drop_harness_lst:\n",
        "  idx = combined.index[combined['job name'] == drop_harn].tolist()\n",
        "  combined = combined.drop(idx)\n",
        "  # combined.drop([combined.loc[combined['job name'] == drop_harn].index[0]], inplace=True)\n",
        "\n",
        "# Save loc as int\n",
        "combined.loc[:,'loc'] = combined.loc[:,'loc'].astype(int)\n",
        "\n",
        "# Reindex\n",
        "combined.index = np.arange(len(combined.index))\n",
        "\n",
        "# Output data combined\n",
        "combined"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 5,
      "metadata": {
        "id": "x3utQ0Im6ZKr"
      },
      "outputs": [],
      "source": [
        "def job_category(job):\n",
        "  \"\"\"\n",
        "  A function to classify job by given name\n",
        "  \"\"\"\n",
        "  if job.startswith('aws_hash_table'):\n",
        "    return 'hash_table'\n",
        "  elif job.startswith('aws_hash_iter'):\n",
        "    return 'hash_iter'\n",
        "  elif job.startswith('aws_hash_callback'):\n",
        "    return 'hash_callback'\n",
        "  elif job.startswith('aws_hash_'):\n",
        "    return 'hash_table'\n",
        "  elif job.startswith('aws_array_list'):\n",
        "    return 'array_list'\n",
        "  elif job.startswith('aws_array'):\n",
        "    return 'array'\n",
        "  elif job.startswith('aws_byte_buf'):\n",
        "    return 'byte_buf'\n",
        "  elif job.startswith('aws_byte_cursor'):\n",
        "    return 'byte_cursor'\n",
        "  elif job.startswith('aws_linked_list'):\n",
        "    return 'linked_list'\n",
        "  elif job.startswith('aws_string'):\n",
        "    return 'string'\n",
        "  elif job.startswith('aws_priority_queue'):\n",
        "    return 'priority_queue'\n",
        "  elif job.startswith('aws_ring_buffer'):\n",
        "    return 'ring_buffer'\n",
        "  elif job.startswith('mem'):\n",
        "    return 'cbmc_mem'\n",
        "  elif 'add' in job or 'mul' in job or 'power_of_two' in job:\n",
        "    return 'arithmetic'\n",
        "  else:\n",
        "    return 'others'\n",
        "\n",
        "combined.loc[:, 'category'] = combined.loc[:, 'job name'].map(job_category)"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 6,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "Lx3tnpcfFybE",
        "outputId": "d7aef35e-7f98-443c-e15b-c5a31c553d0f"
      },
      "outputs": [
        {
          "name": "stdout",
          "output_type": "stream",
          "text": [
            "total number of unit proofs: 168\n",
            " CBMC:168, Seahorn:168, SMACK: 159, Symbiotic: 160, klee: 153, fuzz:76\n"
          ]
        }
      ],
      "source": [
        "# Group data by category\n",
        "combined_by_category = combined.groupby(by='category')\n",
        "sum_table_1 = pd.DataFrame(combined.groupby(by='category').sum())\n",
        "table_1 = pd.DataFrame(combined_by_category.describe(percentiles=[]).round(1))\n",
        "\n",
        "# Get number of covered jobs for each tool\n",
        "smack_covered_num = int(table_1['Smack time (s)']['count'].sum())\n",
        "symbiotic_covered_num = int(table_1['Symbiotic time (s)']['count'].sum())\n",
        "klee_covered_num = int(table_1['Klee time (s)']['count'].sum())\n",
        "fuzz_covered_num = int(table_1['loc'].iloc[2:5, 0].sum())\n",
        "total_num = int(table_1['loc']['count'].sum())\n",
        "print(f'total number of unit proofs: {total_num}\\n CBMC:{total_num}, Seahorn:{total_num}, SMACK: {smack_covered_num}, Symbiotic: {symbiotic_covered_num}, klee: {klee_covered_num}, fuzz:{fuzz_covered_num}')"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 7,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 531
        },
        "id": "9abvuOagGfuj",
        "outputId": "88ed3544-1e70-4fe2-e4fc-4596c0f201b2"
      },
      "outputs": [
        {
          "name": "stdout",
          "output_type": "stream",
          "text": [
            "\t\t\t\t\tTable 1. Verification results for CBMC, SeaHorn, SMACK, Symbiotic, KLEE and libFuzzer.\n"
          ]
        },
        {
          "data": {
            "text/html": [
              "<div>\n",
              "<style scoped>\n",
              "    .dataframe tbody tr th:only-of-type {\n",
              "        vertical-align: middle;\n",
              "    }\n",
              "\n",
              "    .dataframe tbody tr th {\n",
              "        vertical-align: top;\n",
              "    }\n",
              "\n",
              "    .dataframe thead tr th {\n",
              "        text-align: left;\n",
              "    }\n",
              "\n",
              "    .dataframe thead tr:last-of-type th {\n",
              "        text-align: right;\n",
              "    }\n",
              "</style>\n",
              "<table border=\"1\" class=\"dataframe\">\n",
              "  <thead>\n",
              "    <tr>\n",
              "      <th></th>\n",
              "      <th colspan=\"6\" halign=\"left\">loc</th>\n",
              "      <th colspan=\"4\" halign=\"left\">CBMC time (s)</th>\n",
              "      <th>...</th>\n",
              "      <th colspan=\"4\" halign=\"left\">Symbiotic time (s)</th>\n",
              "      <th colspan=\"6\" halign=\"left\">Klee time (s)</th>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th></th>\n",
              "      <th>count</th>\n",
              "      <th>mean</th>\n",
              "      <th>std</th>\n",
              "      <th>min</th>\n",
              "      <th>50%</th>\n",
              "      <th>max</th>\n",
              "      <th>count</th>\n",
              "      <th>mean</th>\n",
              "      <th>std</th>\n",
              "      <th>min</th>\n",
              "      <th>...</th>\n",
              "      <th>std</th>\n",
              "      <th>min</th>\n",
              "      <th>50%</th>\n",
              "      <th>max</th>\n",
              "      <th>count</th>\n",
              "      <th>mean</th>\n",
              "      <th>std</th>\n",
              "      <th>min</th>\n",
              "      <th>50%</th>\n",
              "      <th>max</th>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>category</th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "      <th></th>\n",
              "    </tr>\n",
              "  </thead>\n",
              "  <tbody>\n",
              "    <tr>\n",
              "      <th>arithmetic</th>\n",
              "      <td>6.0</td>\n",
              "      <td>33.7</td>\n",
              "      <td>11.2</td>\n",
              "      <td>11.0</td>\n",
              "      <td>37.5</td>\n",
              "      <td>40.0</td>\n",
              "      <td>6.0</td>\n",
              "      <td>3.8</td>\n",
              "      <td>0.8</td>\n",
              "      <td>3.4</td>\n",
              "      <td>...</td>\n",
              "      <td>280.9</td>\n",
              "      <td>1.5</td>\n",
              "      <td>10.3</td>\n",
              "      <td>705.1</td>\n",
              "      <td>6.0</td>\n",
              "      <td>0.9</td>\n",
              "      <td>0.3</td>\n",
              "      <td>0.7</td>\n",
              "      <td>0.8</td>\n",
              "      <td>1.5</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>array</th>\n",
              "      <td>4.0</td>\n",
              "      <td>97.5</td>\n",
              "      <td>14.2</td>\n",
              "      <td>78.0</td>\n",
              "      <td>100.0</td>\n",
              "      <td>112.0</td>\n",
              "      <td>4.0</td>\n",
              "      <td>5.6</td>\n",
              "      <td>0.0</td>\n",
              "      <td>5.5</td>\n",
              "      <td>...</td>\n",
              "      <td>4.1</td>\n",
              "      <td>6.3</td>\n",
              "      <td>11.0</td>\n",
              "      <td>15.8</td>\n",
              "      <td>4.0</td>\n",
              "      <td>32.3</td>\n",
              "      <td>6.0</td>\n",
              "      <td>23.6</td>\n",
              "      <td>34.3</td>\n",
              "      <td>37.0</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>array_list</th>\n",
              "      <td>23.0</td>\n",
              "      <td>126.1</td>\n",
              "      <td>24.9</td>\n",
              "      <td>77.0</td>\n",
              "      <td>125.0</td>\n",
              "      <td>181.0</td>\n",
              "      <td>23.0</td>\n",
              "      <td>35.8</td>\n",
              "      <td>60.8</td>\n",
              "      <td>5.5</td>\n",
              "      <td>...</td>\n",
              "      <td>68.5</td>\n",
              "      <td>4.2</td>\n",
              "      <td>16.8</td>\n",
              "      <td>286.1</td>\n",
              "      <td>23.0</td>\n",
              "      <td>55.4</td>\n",
              "      <td>49.3</td>\n",
              "      <td>13.4</td>\n",
              "      <td>41.3</td>\n",
              "      <td>164.3</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>byte_buf</th>\n",
              "      <td>29.0</td>\n",
              "      <td>97.1</td>\n",
              "      <td>33.4</td>\n",
              "      <td>50.0</td>\n",
              "      <td>97.0</td>\n",
              "      <td>188.0</td>\n",
              "      <td>29.0</td>\n",
              "      <td>17.6</td>\n",
              "      <td>47.3</td>\n",
              "      <td>5.5</td>\n",
              "      <td>...</td>\n",
              "      <td>162.2</td>\n",
              "      <td>2.1</td>\n",
              "      <td>6.4</td>\n",
              "      <td>879.0</td>\n",
              "      <td>27.0</td>\n",
              "      <td>75.3</td>\n",
              "      <td>124.1</td>\n",
              "      <td>14.1</td>\n",
              "      <td>18.8</td>\n",
              "      <td>619.1</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>byte_cursor</th>\n",
              "      <td>24.0</td>\n",
              "      <td>98.4</td>\n",
              "      <td>28.7</td>\n",
              "      <td>47.0</td>\n",
              "      <td>97.5</td>\n",
              "      <td>179.0</td>\n",
              "      <td>24.0</td>\n",
              "      <td>6.9</td>\n",
              "      <td>3.8</td>\n",
              "      <td>5.5</td>\n",
              "      <td>...</td>\n",
              "      <td>3.6</td>\n",
              "      <td>2.2</td>\n",
              "      <td>7.2</td>\n",
              "      <td>14.9</td>\n",
              "      <td>17.0</td>\n",
              "      <td>12.8</td>\n",
              "      <td>14.4</td>\n",
              "      <td>0.9</td>\n",
              "      <td>4.5</td>\n",
              "      <td>40.1</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>hash_callback</th>\n",
              "      <td>3.0</td>\n",
              "      <td>115.7</td>\n",
              "      <td>75.7</td>\n",
              "      <td>49.0</td>\n",
              "      <td>100.0</td>\n",
              "      <td>198.0</td>\n",
              "      <td>3.0</td>\n",
              "      <td>9.7</td>\n",
              "      <td>5.5</td>\n",
              "      <td>5.5</td>\n",
              "      <td>...</td>\n",
              "      <td>62.0</td>\n",
              "      <td>1.2</td>\n",
              "      <td>7.5</td>\n",
              "      <td>111.6</td>\n",
              "      <td>3.0</td>\n",
              "      <td>64.0</td>\n",
              "      <td>45.5</td>\n",
              "      <td>14.7</td>\n",
              "      <td>72.7</td>\n",
              "      <td>104.5</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>hash_iter</th>\n",
              "      <td>4.0</td>\n",
              "      <td>177.0</td>\n",
              "      <td>8.7</td>\n",
              "      <td>169.0</td>\n",
              "      <td>177.0</td>\n",
              "      <td>185.0</td>\n",
              "      <td>4.0</td>\n",
              "      <td>12.8</td>\n",
              "      <td>9.2</td>\n",
              "      <td>5.6</td>\n",
              "      <td>...</td>\n",
              "      <td>2481.6</td>\n",
              "      <td>6.5</td>\n",
              "      <td>52.9</td>\n",
              "      <td>5000.1</td>\n",
              "      <td>3.0</td>\n",
              "      <td>20.8</td>\n",
              "      <td>9.7</td>\n",
              "      <td>14.8</td>\n",
              "      <td>15.6</td>\n",
              "      <td>32.0</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>hash_table</th>\n",
              "      <td>19.0</td>\n",
              "      <td>172.9</td>\n",
              "      <td>77.9</td>\n",
              "      <td>36.0</td>\n",
              "      <td>149.0</td>\n",
              "      <td>328.0</td>\n",
              "      <td>19.0</td>\n",
              "      <td>23.5</td>\n",
              "      <td>33.3</td>\n",
              "      <td>3.5</td>\n",
              "      <td>...</td>\n",
              "      <td>2198.3</td>\n",
              "      <td>0.7</td>\n",
              "      <td>3.7</td>\n",
              "      <td>5000.1</td>\n",
              "      <td>15.0</td>\n",
              "      <td>104.6</td>\n",
              "      <td>333.4</td>\n",
              "      <td>0.7</td>\n",
              "      <td>14.8</td>\n",
              "      <td>1307.3</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>linked_list</th>\n",
              "      <td>18.0</td>\n",
              "      <td>115.7</td>\n",
              "      <td>71.4</td>\n",
              "      <td>17.0</td>\n",
              "      <td>155.0</td>\n",
              "      <td>219.0</td>\n",
              "      <td>18.0</td>\n",
              "      <td>58.9</td>\n",
              "      <td>209.4</td>\n",
              "      <td>0.0</td>\n",
              "      <td>...</td>\n",
              "      <td>5.4</td>\n",
              "      <td>0.6</td>\n",
              "      <td>9.3</td>\n",
              "      <td>17.3</td>\n",
              "      <td>18.0</td>\n",
              "      <td>0.7</td>\n",
              "      <td>0.1</td>\n",
              "      <td>0.6</td>\n",
              "      <td>0.7</td>\n",
              "      <td>0.9</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>others</th>\n",
              "      <td>2.0</td>\n",
              "      <td>15.5</td>\n",
              "      <td>7.8</td>\n",
              "      <td>10.0</td>\n",
              "      <td>15.5</td>\n",
              "      <td>21.0</td>\n",
              "      <td>2.0</td>\n",
              "      <td>3.5</td>\n",
              "      <td>0.0</td>\n",
              "      <td>3.5</td>\n",
              "      <td>...</td>\n",
              "      <td>NaN</td>\n",
              "      <td>4.7</td>\n",
              "      <td>4.7</td>\n",
              "      <td>4.7</td>\n",
              "      <td>1.0</td>\n",
              "      <td>0.7</td>\n",
              "      <td>NaN</td>\n",
              "      <td>0.7</td>\n",
              "      <td>0.7</td>\n",
              "      <td>0.7</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>priority_queue</th>\n",
              "      <td>15.0</td>\n",
              "      <td>187.8</td>\n",
              "      <td>43.4</td>\n",
              "      <td>136.0</td>\n",
              "      <td>171.0</td>\n",
              "      <td>258.0</td>\n",
              "      <td>15.0</td>\n",
              "      <td>208.1</td>\n",
              "      <td>303.4</td>\n",
              "      <td>5.5</td>\n",
              "      <td>...</td>\n",
              "      <td>20.0</td>\n",
              "      <td>1.4</td>\n",
              "      <td>3.9</td>\n",
              "      <td>76.1</td>\n",
              "      <td>15.0</td>\n",
              "      <td>46.4</td>\n",
              "      <td>11.6</td>\n",
              "      <td>17.7</td>\n",
              "      <td>50.7</td>\n",
              "      <td>51.3</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>ring_buffer</th>\n",
              "      <td>6.0</td>\n",
              "      <td>155.7</td>\n",
              "      <td>70.9</td>\n",
              "      <td>56.0</td>\n",
              "      <td>172.5</td>\n",
              "      <td>227.0</td>\n",
              "      <td>6.0</td>\n",
              "      <td>20.0</td>\n",
              "      <td>19.5</td>\n",
              "      <td>5.5</td>\n",
              "      <td>...</td>\n",
              "      <td>9.0</td>\n",
              "      <td>1.8</td>\n",
              "      <td>9.5</td>\n",
              "      <td>26.0</td>\n",
              "      <td>6.0</td>\n",
              "      <td>48.1</td>\n",
              "      <td>26.4</td>\n",
              "      <td>14.2</td>\n",
              "      <td>60.4</td>\n",
              "      <td>73.5</td>\n",
              "    </tr>\n",
              "    <tr>\n",
              "      <th>string</th>\n",
              "      <td>15.0</td>\n",
              "      <td>87.6</td>\n",
              "      <td>46.4</td>\n",
              "      <td>11.0</td>\n",
              "      <td>90.0</td>\n",
              "      <td>209.0</td>\n",
              "      <td>15.0</td>\n",
              "      <td>6.3</td>\n",
              "      <td>1.3</td>\n",
              "      <td>5.5</td>\n",
              "      <td>...</td>\n",
              "      <td>10.9</td>\n",
              "      <td>1.0</td>\n",
              "      <td>6.2</td>\n",
              "      <td>41.9</td>\n",
              "      <td>15.0</td>\n",
              "      <td>139.7</td>\n",
              "      <td>159.7</td>\n",
              "      <td>15.6</td>\n",
              "      <td>105.4</td>\n",
              "      <td>482.3</td>\n",
              "    </tr>\n",
              "  </tbody>\n",
              "</table>\n",
              "<p>13 rows × 36 columns</p>\n",
              "</div>"
            ],
            "text/plain": [
              "                 loc                                   CBMC time (s)         \\\n",
              "               count   mean   std    min    50%    max         count   mean   \n",
              "category                                                                      \n",
              "arithmetic       6.0   33.7  11.2   11.0   37.5   40.0           6.0    3.8   \n",
              "array            4.0   97.5  14.2   78.0  100.0  112.0           4.0    5.6   \n",
              "array_list      23.0  126.1  24.9   77.0  125.0  181.0          23.0   35.8   \n",
              "byte_buf        29.0   97.1  33.4   50.0   97.0  188.0          29.0   17.6   \n",
              "byte_cursor     24.0   98.4  28.7   47.0   97.5  179.0          24.0    6.9   \n",
              "hash_callback    3.0  115.7  75.7   49.0  100.0  198.0           3.0    9.7   \n",
              "hash_iter        4.0  177.0   8.7  169.0  177.0  185.0           4.0   12.8   \n",
              "hash_table      19.0  172.9  77.9   36.0  149.0  328.0          19.0   23.5   \n",
              "linked_list     18.0  115.7  71.4   17.0  155.0  219.0          18.0   58.9   \n",
              "others           2.0   15.5   7.8   10.0   15.5   21.0           2.0    3.5   \n",
              "priority_queue  15.0  187.8  43.4  136.0  171.0  258.0          15.0  208.1   \n",
              "ring_buffer      6.0  155.7  70.9   56.0  172.5  227.0           6.0   20.0   \n",
              "string          15.0   87.6  46.4   11.0   90.0  209.0          15.0    6.3   \n",
              "\n",
              "                            ... Symbiotic time (s)                     \\\n",
              "                  std  min  ...                std  min   50%     max   \n",
              "category                    ...                                         \n",
              "arithmetic        0.8  3.4  ...              280.9  1.5  10.3   705.1   \n",
              "array             0.0  5.5  ...                4.1  6.3  11.0    15.8   \n",
              "array_list       60.8  5.5  ...               68.5  4.2  16.8   286.1   \n",
              "byte_buf         47.3  5.5  ...              162.2  2.1   6.4   879.0   \n",
              "byte_cursor       3.8  5.5  ...                3.6  2.2   7.2    14.9   \n",
              "hash_callback     5.5  5.5  ...               62.0  1.2   7.5   111.6   \n",
              "hash_iter         9.2  5.6  ...             2481.6  6.5  52.9  5000.1   \n",
              "hash_table       33.3  3.5  ...             2198.3  0.7   3.7  5000.1   \n",
              "linked_list     209.4  0.0  ...                5.4  0.6   9.3    17.3   \n",
              "others            0.0  3.5  ...                NaN  4.7   4.7     4.7   \n",
              "priority_queue  303.4  5.5  ...               20.0  1.4   3.9    76.1   \n",
              "ring_buffer      19.5  5.5  ...                9.0  1.8   9.5    26.0   \n",
              "string            1.3  5.5  ...               10.9  1.0   6.2    41.9   \n",
              "\n",
              "               Klee time (s)                                     \n",
              "                       count   mean    std   min    50%     max  \n",
              "category                                                         \n",
              "arithmetic               6.0    0.9    0.3   0.7    0.8     1.5  \n",
              "array                    4.0   32.3    6.0  23.6   34.3    37.0  \n",
              "array_list              23.0   55.4   49.3  13.4   41.3   164.3  \n",
              "byte_buf                27.0   75.3  124.1  14.1   18.8   619.1  \n",
              "byte_cursor             17.0   12.8   14.4   0.9    4.5    40.1  \n",
              "hash_callback            3.0   64.0   45.5  14.7   72.7   104.5  \n",
              "hash_iter                3.0   20.8    9.7  14.8   15.6    32.0  \n",
              "hash_table              15.0  104.6  333.4   0.7   14.8  1307.3  \n",
              "linked_list             18.0    0.7    0.1   0.6    0.7     0.9  \n",
              "others                   1.0    0.7    NaN   0.7    0.7     0.7  \n",
              "priority_queue          15.0   46.4   11.6  17.7   50.7    51.3  \n",
              "ring_buffer              6.0   48.1   26.4  14.2   60.4    73.5  \n",
              "string                  15.0  139.7  159.7  15.6  105.4   482.3  \n",
              "\n",
              "[13 rows x 36 columns]"
            ]
          },
          "execution_count": 7,
          "metadata": {},
          "output_type": "execute_result"
        }
      ],
      "source": [
        "# Show the result table\n",
        "print(f'\\t\\t\\t\\t\\tTable 1. Verification time results for CBMC, SeaHorn, SMACK, Symbiotic, KLEE and libFuzzer.')\n",
        "table_1"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {
        "id": "Si2cvjkkGPCN"
      },
      "source": [
        "## Part two: Running time per category for CBMC,  SeaHorn and KLEE\n",
        "\n",
        "The following graph shows the running time results based on each category of jobs."
      ]
    },
    {
      "cell_type": "code",
      "execution_count": 1,
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/",
          "height": 1000
        },
        "id": "xQwosnt-I_iM",
        "outputId": "db24f93d-6afe-4cba-e8d8-f93e3c5008ba"
      },
      "outputs": [],
      "source": [
        "categories = combined_by_category.groups.keys()\n",
        "sorted(categories)\n",
        "YLIMS = 150 # Change the y limits here\n",
        "for cat in categories:\n",
        "  # For each category, melt data and draw a line graph with dots\n",
        "  job_ids = combined_by_category.get_group(cat).index.values\n",
        "  df = combined_by_category.get_group(cat).drop(columns=['category', 'loc'])\n",
        "  df = df.rename(columns={\"Seahorn normal time (s)\": \"Seahorn\", \"CBMC time (s)\": \"CBMC\", \"Smack time (s)\": \"SMACK\", \"Symbiotic time (s)\": \"Symbiotic\", \"Klee time (s)\": \"KLEE\"})\n",
        "  df = df.melt('job name', var_name='tools',  value_name='time (s)')\n",
        "  fig, ax = plt.subplots(figsize=(16,4))\n",
        "  fig.tight_layout()\n",
        "  # Uncomment the next line if you want to show detailed comparisons \n",
        "  # plt.ylim(0, min(df['time (s)'].max(), YLIMS))\n",
        "  plt.subplots_adjust(hspace = 2.4)\n",
        "  subg = sns.pointplot(x='job name', y='time (s)', hue='tools', data=df, ax=ax)\n",
        "  subg.set_title(f'\\n\\n\\n\\nFig. {cat}\\n',fontsize=21)\n",
        "  # subg.set_yticklabels(df['time (s)'], fontsize=16)\n",
        "  subg.set_xlabel(\"Job Name\",fontsize=14)\n",
        "  subg.set_ylabel(\"Time (second)\",fontsize=14)\n",
        "  subg.set_xticklabels(df['job name'], rotation='vertical', fontsize=12)\n",
        "  sns.despine()\n",
        "  "
      ]
    }
  ],
  "metadata": {
    "colab": {
      "collapsed_sections": [],
      "name": "experiment_results.ipynb",
      "provenance": []
    },
    "kernelspec": {
      "display_name": "Python 3",
      "name": "python3"
    },
    "language_info": {
      "codemirror_mode": {
        "name": "ipython",
        "version": 3
      },
      "file_extension": ".py",
      "mimetype": "text/x-python",
      "name": "python",
      "nbconvert_exporter": "python",
      "pygments_lexer": "ipython3",
      "version": "3.8.10"
    }
  },
  "nbformat": 4,
  "nbformat_minor": 0
}