Regression test for redundant JSON message output

Author: peterschrammel

regression/cbmc/json1/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  unsigned x;
+  assert(x==0);
+  return 0;
+}

regression/cbmc/json1/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--json-ui --stop-on-fail
+activate-multi-line-match
+EXIT=10
+SIGNAL=0
+\[\n  \{\n    "program": "CBMC .*"\n  \},\n  \{\n    "messageText": "CBMC .*",\n    "messageType": "STATUS-MESSAGE"\n  \},\n  \{\n    "messageText": "Parsing main\.c",\n    "messageType": "STATUS-MESSAGE"\n  \},
+\]\n  \},\n  \{\n    "messageText": "VERIFICATION FAILED",\n    "messageType": "STATUS-MESSAGE"\n  \},\n  \{\n    "cProverStatus": "failure"\n  \}\n\]
+--
+--
+The purpose of this test is to catch duplicate output of messages and
+output of empty messages on flushing the message stream.