From 228c01920a2815fd246256903a83d45616b2d95b Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 11 Apr 2018 10:30:44 +0100
Subject: [PATCH 1/3] Fix duplicate message output in json-ui

---
 src/util/ui_message.cpp | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp
index 61771eb6c70..83c5473fe78 100644
--- a/src/util/ui_message.cpp
+++ b/src/util/ui_message.cpp
@@ -294,11 +294,6 @@ void ui_message_handlert::json_ui_msg(
   const std::string timestamp = time->stamp();
   if(!timestamp.empty())
     result["timestamp"] = json_stringt(timestamp);
-
-  // By convention a leading comma is created by every new array entry.
-  // The first entry is generated in the constructor and does not have
-  //  a trailing comma.
-  std::cout << ",\n" << result;
 }
 
 void ui_message_handlert::flush(unsigned level)

From de0644d170ba5d118a1b609a18081a413f13b908 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 11 Apr 2018 11:33:56 +0100
Subject: [PATCH 2/3] Only force end of previous message if there actually is
 one.

This avoids outputting empty messages on messaget::eom.
---
 src/util/message.h | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/util/message.h b/src/util/message.h
index 528233145be..3f637ba837a 100644
--- a/src/util/message.h
+++ b/src/util/message.h
@@ -209,7 +209,8 @@ class messaget
 
     mstreamt &operator << (const xmlt &data)
     {
-      *this << eom; // force end of previous message
+      if(this->tellp() > 0)
+        *this << eom; // force end of previous message
       if(message.message_handler)
       {
         message.message_handler->print(message_level, data);
@@ -219,7 +220,8 @@ class messaget
 
     mstreamt &operator << (const json_objectt &data)
     {
-      *this << eom; // force end of previous message
+      if(this->tellp() > 0)
+        *this << eom; // force end of previous message
       if(message.message_handler)
       {
         message.message_handler->print(message_level, data);
@@ -243,7 +245,8 @@ class messaget
     /// Returns a reference to the top-level JSON array stream
     json_stream_arrayt &json_stream()
     {
-      *this << eom; // force end of previous message
+      if(this->tellp() > 0)
+        *this << eom; // force end of previous message
       return message.message_handler->get_json_stream();
     }
 

From 822c75761044e29ef8923c05d5e4ea783e07636d Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 11 Apr 2018 12:59:14 +0100
Subject: [PATCH 3/3] Regression test for redundant JSON message output

---
 regression/cbmc/json1/main.c    |  6 ++++++
 regression/cbmc/json1/test.desc | 12 ++++++++++++
 2 files changed, 18 insertions(+)
 create mode 100644 regression/cbmc/json1/main.c
 create mode 100644 regression/cbmc/json1/test.desc

diff --git a/regression/cbmc/json1/main.c b/regression/cbmc/json1/main.c
new file mode 100644
index 00000000000..0262b496b9c
--- /dev/null
+++ b/regression/cbmc/json1/main.c
@@ -0,0 +1,6 @@
+int main()
+{
+  unsigned x;
+  assert(x==0);
+  return 0;
+}
diff --git a/regression/cbmc/json1/test.desc b/regression/cbmc/json1/test.desc
new file mode 100644
index 00000000000..54927fab2be
--- /dev/null
+++ b/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.