StatsTracker: remove NumObjects, fix assignment of and always write ArrayHashTime

* fix binding order for assignments when KLEE_ARRAY_DEBUG enabled
* always write ArrayHashTime column to run.stats, assign -1 when KLEE_ARRAY_DEBUG disabled
* remove unused NumObjects column from run.stats
* remove NumObjects panel from Grafana

1 files changed, 13 insertions, 181 deletions

diff --git a/utils/grafana/klee_dashboard.json b/utils/grafana/klee_dashboard.json
index c895dce0..3b653bab 100644
--- a/utils/grafana/klee_dashboard.json
+++ b/utils/grafana/klee_dashboard.json
@@ -1885,174 +1885,6 @@
         "x": 0,
         "y": 79
       },
-      "id": 50,
-      "interval": null,
-      "links": [],
-      "mappingType": 1,
-      "mappingTypes": [
-        {
-          "name": "value to text",
-          "value": 1
-        },
-        {
-          "name": "range to text",
-          "value": 2
-        }
-      ],
-      "maxDataPoints": 100,
-      "nullPointMode": "connected",
-      "nullText": null,
-      "options": {},
-      "postfix": "",
-      "postfixFontSize": "50%",
-      "prefix": "",
-      "prefixFontSize": "50%",
-      "rangeMaps": [
-        {
-          "from": "null",
-          "text": "N/A",
-          "to": "null"
-        }
-      ],
-      "sparkline": {
-        "fillColor": "rgba(31, 118, 189, 0.18)",
-        "full": false,
-        "lineColor": "rgb(31, 120, 193)",
-        "show": false,
-        "ymax": null,
-        "ymin": null
-      },
-      "tableColumn": "",
-      "targets": [
-        {
-          "refId": "A",
-          "target": "NumObjects",
-          "type": "timeserie"
-        }
-      ],
-      "thresholds": "",
-      "timeFrom": null,
-      "timeShift": null,
-      "title": "Num Objects ",
-      "type": "singlestat",
-      "valueFontSize": "80%",
-      "valueMaps": [
-        {
-          "op": "=",
-          "text": "N/A",
-          "value": "null"
-        }
-      ],
-      "valueName": "current"
-    },
-    {
-      "aliasColors": {},
-      "bars": false,
-      "dashLength": 10,
-      "dashes": false,
-      "fill": 1,
-      "fillGradient": 0,
-      "gridPos": {
-        "h": 8,
-        "w": 15,
-        "x": 7,
-        "y": 79
-      },
-      "id": 48,
-      "legend": {
-        "avg": false,
-        "current": false,
-        "max": false,
-        "min": false,
-        "show": true,
-        "total": false,
-        "values": false
-      },
-      "lines": true,
-      "linewidth": 1,
-      "nullPointMode": "null",
-      "options": {
-        "dataLinks": []
-      },
-      "percentage": false,
-      "pointradius": 2,
-      "points": false,
-      "renderer": "flot",
-      "seriesOverrides": [],
-      "spaceLength": 10,
-      "stack": false,
-      "steppedLine": false,
-      "targets": [
-        {
-          "refId": "A",
-          "target": "NumObjects",
-          "type": "timeserie"
-        }
-      ],
-      "thresholds": [],
-      "timeFrom": null,
-      "timeRegions": [],
-      "timeShift": null,
-      "title": "Num Objects",
-      "tooltip": {
-        "shared": true,
-        "sort": 0,
-        "value_type": "individual"
-      },
-      "type": "graph",
-      "xaxis": {
-        "buckets": null,
-        "mode": "time",
-        "name": null,
-        "show": true,
-        "values": []
-      },
-      "yaxes": [
-        {
-          "format": "short",
-          "label": null,
-          "logBase": 1,
-          "max": null,
-          "min": null,
-          "show": true
-        },
-        {
-          "format": "short",
-          "label": null,
-          "logBase": 1,
-          "max": null,
-          "min": null,
-          "show": true
-        }
-      ],
-      "yaxis": {
-        "align": false,
-        "alignLevel": null
-      }
-    },
-    {
-      "cacheTimeout": null,
-      "colorBackground": true,
-      "colorValue": false,
-      "colors": [
-        "#3274D9",
-        "#3274D9",
-        "#d44a3a"
-      ],
-      "format": "locale",
-      "gauge": {
-        "maxValue": 100,
-        "minValue": 0,
-        "show": false,
-        "thresholdLabels": false,
-        "thresholdMarkers": true
-      },
-      "gridPos": {
-        "h": 8,
-        "w": 7,
-        "x": 0,
-        "y": 87
-      },
       "id": 64,
       "interval": null,
       "links": [],
@@ -2124,7 +1956,7 @@
         "h": 8,
         "w": 15,
         "x": 7,
-        "y": 87
+        "y": 79
       },
       "id": 62,
       "legend": {
@@ -2219,7 +2051,7 @@
         "h": 8,
         "w": 7,
         "x": 0,
-        "y": 95
+        "y": 87
       },
       "id": 66,
       "interval": null,
@@ -2290,7 +2122,7 @@
         "h": 8,
         "w": 15,
         "x": 7,
-        "y": 95
+        "y": 87
       },
       "id": 60,
       "legend": {
@@ -2385,7 +2217,7 @@
         "h": 8,
         "w": 7,
         "x": 0,
-        "y": 103
+        "y": 95
       },
       "id": 68,
       "interval": null,
@@ -2456,7 +2288,7 @@
         "h": 8,
         "w": 15,
         "x": 7,
-        "y": 103
+        "y": 95
       },
       "id": 58,
       "legend": {
@@ -2551,7 +2383,7 @@
         "h": 7,
         "w": 7,
         "x": 0,
-        "y": 111
+        "y": 103
       },
       "id": 70,
       "interval": null,
@@ -2622,7 +2454,7 @@
         "h": 7,
         "w": 15,
         "x": 7,
-        "y": 111
+        "y": 103
       },
       "id": 56,
       "legend": {
@@ -2718,7 +2550,7 @@
         "h": 8,
         "w": 7,
         "x": 0,
-        "y": 118
+        "y": 110
       },
       "id": 72,
       "interval": null,
@@ -2789,7 +2621,7 @@
         "h": 8,
         "w": 15,
         "x": 7,
-        "y": 118
+        "y": 110
       },
       "id": 52,
       "legend": {
@@ -2886,7 +2718,7 @@
         "h": 7,
         "w": 7,
         "x": 0,
-        "y": 126
+        "y": 118
       },
       "id": 74,
       "interval": null,
@@ -2957,7 +2789,7 @@
         "h": 7,
         "w": 15,
         "x": 7,
-        "y": 126
+        "y": 118
       },
       "id": 54,
       "legend": {
@@ -3052,7 +2884,7 @@
         "h": 7,
         "w": 7,
         "x": 0,
-        "y": 133
+        "y": 125
       },
       "id": 76,
       "interval": null,
@@ -3123,7 +2955,7 @@
         "h": 7,
         "w": 15,
         "x": 7,
-        "y": 133
+        "y": 125
       },
       "id": 34,
       "legend": {