From b94715f453f601fad8828ec5ff6b33a79b8935d2 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 17 Sep 2021 09:50:51 +0200
Subject: [PATCH] [libc] assert terminates

---
 share/libc/assert.h                    | 3 +--
 tests/libc/oracle/fc_libc.1.res.oracle | 1 -
 2 files changed, 1 insertion(+), 3 deletions(-)

diff --git a/share/libc/assert.h b/share/libc/assert.h
index 26ee575269c..0c4f0639509 100644
--- a/share/libc/assert.h
+++ b/share/libc/assert.h
@@ -29,7 +29,6 @@ __BEGIN_DECLS
 
 /*@
   requires nonnull_c: c != 0;
-  terminates c != 0;
   assigns \nothing;
 */
 extern void __FC_assert(int c, const char* file, int line, const char*expr);
@@ -42,7 +41,7 @@ __POP_FC_STDLIB
 #endif
 
 #undef assert
-#ifdef NDEBUG 
+#ifdef NDEBUG
 #define assert(ignore) ((void)0)
 #else
 #ifndef __FRAMAC__
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 8ce7b3829c6..5a35c61690f 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -2505,7 +2505,6 @@ void __FC_assert(int c, char const *file, int line, char const *expr);
 extern void Frama_C_show_each_warning();
 
 /*@ requires nonnull_c: c ≢ 0;
-    terminates c ≢ 0;
     assigns \nothing; */
 void __FC_assert(int c, char const *file, int line, char const *expr)
 {
-- 
GitLab