diff --git a/share/libc/stdlib.h b/share/libc/stdlib.h
index 5d903a44e9dbe994c36705a2f06681347ee5175c..a41a685c5321cca6c0ff95c1b67f97c9d8492494 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 d0942621eceadea65324eea022577dd0fad7f0f9..f1bb1d42421189f8e087c94215e6f4d70d1cf335 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;