From e42bdaeb623d4eebf2573752be018ee963cfdada Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 25 Jul 2019 16:32:19 +0200
Subject: [PATCH] [libC] fixes specification of abort and exit functions
---
share/libc/stdlib.h | 10 +++++++---
tests/libc/oracle/fc_libc.1.res.oracle | 14 ++++++++++----
2 files changed, 17 insertions(+), 7 deletions(-)
diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 5d903a44e9d..a41a685c532 100644
--- a/share/libc/stdlib.h
+++ b/share/libc/stdlib.h
@@ -454,8 +454,11 @@ extern void *realloc(void *ptr, size_t size);
/* ISO C: 7.20.4 */
-/*@ assigns \nothing;
- @ ensures never_terminates: \false; */
+/*@
+ assigns \exit_status \from \nothing;
+ exits status: \exit_status != EXIT_SUCCESS;
+ ensures never_terminates: \false;
+ */
extern void abort(void) __attribute__ ((__noreturn__));
/*@ assigns \result \from \nothing ;*/
@@ -465,7 +468,8 @@ extern int atexit(void (*func)(void));
extern int at_quick_exit(void (*func)(void));
/*@
- assigns \nothing;
+ assigns \exit_status \from status;
+ exits status: \exit_status == status;
ensures never_terminates: \false;
*/
extern void exit(int status) __attribute__ ((__noreturn__));
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index d0942621ece..f1bb1d42421 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -2346,8 +2346,11 @@ extern void free(void *p);
*/
extern void *realloc(void *ptr, size_t size);
-/*@ ensures never_terminates: \false;
- assigns \nothing; */
+/*@ exits status: \exit_status ≢ 0;
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from \nothing;
+ */
extern __attribute__((__noreturn__)) void abort(void);
/*@ assigns \result;
@@ -2358,8 +2361,11 @@ extern int atexit(void (*func)(void));
assigns \result \from \nothing; */
extern int at_quick_exit(void (*func)(void));
-/*@ ensures never_terminates: \false;
- assigns \nothing; */
+/*@ exits status: \exit_status ≡ \old(status);
+ ensures never_terminates: \false;
+
+ assigns \exit_status \from status;
+ */
extern __attribute__((__noreturn__)) void exit(int status);
/*@ ensures never_terminates: \false;
--
GitLab