From 6fe3b4cd19c79b6dd79c66507d9829a57ee8e18a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 21 Jul 2025 09:04:18 +0200 Subject: [PATCH] format_hook for next_symbol expressions This formats next_symbol expressions as next(identifier). --- src/ebmc/Makefile | 1 + src/ebmc/ebmc_parse_options.cpp | 2 ++ src/ebmc/format_hooks.cpp | 25 +++++++++++++++++++++++++ src/ebmc/format_hooks.h | 14 ++++++++++++++ 4 files changed, 42 insertions(+) create mode 100644 src/ebmc/format_hooks.cpp create mode 100644 src/ebmc/format_hooks.h diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile index 6497d7b0a..44193f002 100644 --- a/src/ebmc/Makefile +++ b/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 \ diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 3e243e5fc..38ac372bc 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #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")) { diff --git a/src/ebmc/format_hooks.cpp b/src/ebmc/format_hooks.cpp new file mode 100644 index 000000000..79b778a7c --- /dev/null +++ b/src/ebmc/format_hooks.cpp @@ -0,0 +1,25 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "format_hooks.h" + +#include + +#include + +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; + }); +} diff --git a/src/ebmc/format_hooks.h b/src/ebmc/format_hooks.h new file mode 100644 index 000000000..5c9acf86f --- /dev/null +++ b/src/ebmc/format_hooks.h @@ -0,0 +1,14 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef EBMC_FORMAT_HOOKS_H +#define EBMC_FORMAT_HOOKS_H + +void format_hooks(); + +#endif // EBMC_FORMAT_HOOKS_H