format_hook for next_symbol expressions

src/ebmc/Makefile

@@ -17,6 +17,7 @@ SRC = \
       ebmc_properties.cpp \
       ebmc_solver_factory.cpp \
       ebmc_version.cpp \
+      format_hooks.cpp \
       instrument_past.cpp \
       instrument_buechi.cpp \
       k_induction.cpp \

src/ebmc/ebmc_parse_options.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include "ebmc_base.h"
 #include "ebmc_error.h"
 #include "ebmc_version.h"
+#include "format_hooks.h"
 #include "instrument_buechi.h"
 #include "liveness_to_safety.h"
 #include "netlist.h"
@@ -71,6 +72,7 @@ int ebmc_parse_optionst::doit()
   }
 
   register_languages();
+  format_hooks();
 
   if(cmdline.isset("version"))
   {

src/ebmc/format_hooks.cpp

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "format_hooks.h"
+
+#include <util/format_expr.h>
+
+#include <trans-word-level/next_symbol.h>
+
+void format_hooks()
+{
+  add_format_hook(
+    ID_next_symbol,
+    [](std::ostream &os, const exprt &expr) -> std::ostream &
+    {
+      const auto &next_symbol_expr = to_next_symbol_expr(expr);
+      os << "next(" << next_symbol_expr.identifier() << ')';
+      return os;
+    });
+}

src/ebmc/format_hooks.h

@@ -0,0 +1,14 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef EBMC_FORMAT_HOOKS_H
+#define EBMC_FORMAT_HOOKS_H
+
+void format_hooks();
+
+#endif // EBMC_FORMAT_HOOKS_H