Merge pull request #5629 from martin-cs/feature/verify-prints-history

goto_analyzer --verify now prints histories in the XML and JSON output

Author: martin-cs

regression/goto-analyzer/history-output/json.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--verify --recursive-interprocedural --one-domain-per-history --vsd --branching 4 --json -
+^EXIT=0$
+^SIGNAL=0$
+\"falseHistories\": \[ \"local_control_flow_history : location \d+ after \d+ not taken after \d+ taken\" \]
+\"unknownHistories\": \[ \"local_control_flow_history : location \d+ after \d+ taken after \d+ taken\" \]
+--
+^warning: ignoring
+--
+Make sure that the JSON output contains the histories in which the assertion is false and unknown

regression/goto-analyzer/history-output/main.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  int nondet1;
+  int nondet2;
+  int x;
+
+  if(nondet1)
+  {
+    // Taking this path the assertion clearly holds
+    x = 1;
+  }
+  else
+  {
+    if(nondet2)
+    {
+      // Taking this path the assertion clearly fails
+      x = 0;
+    }
+    // Not taking the branch means the assertion is unknown
+    // because x is non-deterministic
+  }
+
+  assert(x);
+
+  return 0;
+}

regression/goto-analyzer/history-output/xml.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--verify --recursive-interprocedural --one-domain-per-history --vsd --branching 4 --xml -
+^EXIT=0$
+^SIGNAL=0$
+<history>local_control_flow_history : location \d+ after \d+ taken after \d+ taken<\/history>
+<history>local_control_flow_history : location \d+ after \d+ not taken after \d+ taken<\/history>
+--
+^warning: ignoring
+--
+Make sure that the JSON output contains the histories in which the assertion is false and unknown