Extend the printing to be enabled for both json and plain text ouput

Author: thk123

regression/cbmc-incr-oneloop/alarm2/test-json-output.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--incremental-loop main.0 --unwind-min 5 --unwind-max 10 --json-ui
+^EXIT=10$
+^SIGNAL=0$
+"messageText": "VERIFICATION FAILED"
+"currentUnwinding": 1
+--
+^warning: ignoring

regression/cbmc-incr-oneloop/alarm2/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
 --incremental-loop main.0 --unwind-min 5 --unwind-max 10
+Current unwinding: 1
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

src/goto-checker/symex_bmc_incremental_one_loop.cpp

@@ -88,14 +88,7 @@ bool symex_bmc_incremental_one_loopt::should_stop_unwind(
     abort_unwind_decision.is_known(), "unwind decision should be taken by now");
   bool abort = abort_unwind_decision.is_true();
 
-
-  if(output_ui == ui_message_handlert::uit::XML_UI)
-  {
-    xmlt xml("current-unwinding");
-    xml.data = std::to_string(unwind);
-    log.statistics() << xml;
-  }
-
+  log_unwinding(unwind);
   log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
                    << " iteration " << unwind;
 
@@ -142,3 +135,29 @@ bool symex_bmc_incremental_one_loopt::resume(
 
   return should_pause_symex;
 }
+void symex_bmc_incremental_one_loopt::log_unwinding(unsigned unwind)
+{
+  const std::string unwind_num = std::to_string(unwind);
+  switch(output_ui)
+  {
+  case ui_message_handlert::uit::PLAIN:
+  {
+    log.statistics() << "Current unwinding: " << unwind_num << messaget::eom;
+    break;
+  }
+  case ui_message_handlert::uit::XML_UI:
+  {
+    xmlt xml("current-unwinding");
+    xml.data = unwind_num;
+    log.statistics() << xml << messaget::eom;
+    break;
+  }
+  case ui_message_handlert::uit::JSON_UI:
+  {
+    json_objectt json;
+    json["currentUnwinding"] = json_numbert(unwind_num);
+    log.statistics() << json << messaget::eom;
+    break;
+  }
+  }
+}

src/goto-checker/symex_bmc_incremental_one_loop.h

@@ -47,6 +47,8 @@ class symex_bmc_incremental_one_loopt : public symex_bmct
     const call_stackt &context,
     unsigned unwind) override;
 
+  void log_unwinding(unsigned unwind);
+
   ui_message_handlert::uit output_ui;
 };