From 4741217071fd45b1526b542ebd8bbc2ab2251728 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Tue, 25 Oct 2022 15:05:49 +0200 Subject: [PATCH] Try to make the abort() inconditionnal in failed xbt_assert, to please the checkers --- include/xbt/asserts.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/include/xbt/asserts.h b/include/xbt/asserts.h index 314c5ec978..e51ed8a2cf 100644 --- a/include/xbt/asserts.h +++ b/include/xbt/asserts.h @@ -49,6 +49,8 @@ XBT_ATTRIB_NORETURN XBT_PUBLIC void xbt_abort(void); * * Unlike the standard assert, xbt_assert is never disabled, even if the macro NDEBUG is defined at compile time. So * it's safe to have a condition with side effects. + * + * In model-checking mode, a failed xbt_assert() is reported as a failed MC_assert(). */ /** @brief The condition which failed will be displayed. @hideinitializer */ @@ -63,8 +65,7 @@ XBT_ATTRIB_NORETURN XBT_PUBLIC void xbt_abort(void); xbt_backtrace_display_current(); \ if (MC_is_active()) \ MC_assert(0); \ - else \ - abort(); \ + abort(); \ } \ } while (0) -- 2.20.1