[libc] assert terminates

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__

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)
 {