Adding in printing code for each unwind

Author: thk123

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -34,7 +34,8 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert(
       equation,
       options,
       path_storage,
-      guard_manager),
+      guard_manager,
+      ui_message_handler.get_ui()),
     property_decider(options, ui_message_handler, equation, ns)
 {
   setup_symex(symex, ns, options, ui_message_handler);

src/goto-checker/symex_bmc_incremental_one_loop.cpp

@@ -19,7 +19,8 @@ symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
   symex_target_equationt &target,
   const optionst &options,
   path_storaget &path_storage,
-  guard_managert &guard_manager)
+  guard_managert &guard_manager,
+  ui_message_handlert::uit output_xml)
   : symex_bmct(
       message_handler,
       outer_symbol_table,
@@ -33,7 +34,8 @@ symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
                                    : std::numeric_limits<unsigned>::max()),
     incr_min_unwind(
       options.is_set("unwind-min") ? options.get_signed_int_option("unwind-min")
-                                   : 0)
+                                   : 0),
+    output_xml(output_xml)
 {
   ignore_assertions =
     incr_min_unwind >= 1 &&
@@ -56,6 +58,7 @@ bool symex_bmc_incremental_one_loopt::should_stop_unwind(
     this_loop_limit = incr_max_unwind;
     if(unwind + 1 >= incr_min_unwind)
       ignore_assertions = false;
+
     abort_unwind_decision = tvt(unwind >= this_loop_limit);
   }
   else
@@ -85,6 +88,14 @@ 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_xml == ui_message_handlert::uit::XML_UI)
+  {
+    xmlt xml("current-unwinding");
+    xml.data = std::to_string(unwind);
+    log.statistics() << xml;
+  }
+
   log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
                    << " iteration " << unwind;
 

src/goto-checker/symex_bmc_incremental_one_loop.h

@@ -10,6 +10,7 @@
 #define CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H
 
 #include "symex_bmc.h"
+#include <util/ui_message.h>
 
 class symex_bmc_incremental_one_loopt : public symex_bmct
 {
@@ -20,7 +21,8 @@ class symex_bmc_incremental_one_loopt : public symex_bmct
     symex_target_equationt &,
     const optionst &,
     path_storaget &,
-    guard_managert &);
+    guard_managert &,
+    ui_message_handlert::uit output_xml);
 
   /// Return true if symex can be resumed
   bool from_entry_point_of(
@@ -44,6 +46,8 @@ class symex_bmc_incremental_one_loopt : public symex_bmct
     const symex_targett::sourcet &source,
     const call_stackt &context,
     unsigned unwind) override;
+
+  ui_message_handlert::uit output_xml;
 };
 
 #endif // CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H