[libC] fixes specification of abort and exit functions

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__));

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;