diff --git a/share/libc/unistd.h b/share/libc/unistd.h
index 49903985e2756a5fddb9d1b29fff8ef208a569c8..43b48cfafc214a5a7f28e866c61ba066fd9a46a1 100644
--- a/share/libc/unistd.h
+++ b/share/libc/unistd.h
@@ -841,9 +841,22 @@ extern int          ftruncate(int, off_t);
 extern char        *getcwd(char *buf, size_t size);
 
 extern int          getdtablesize(void);
+
+/*@ //missing: assigns \result \from 'process effective gid'
+  assigns \result \from \nothing;
+*/
 extern gid_t        getegid(void);
+
+/*@ //missing: assigns \result \from 'process effective uid'
+  assigns \result \from \nothing;
+*/
 extern uid_t        geteuid(void);
+
+/*@ //missing: assigns \result \from 'process gid'
+  assigns \result \from \nothing;
+*/
 extern gid_t        getgid(void);
+
 extern int          getgroups(int, gid_t []);
 extern long         gethostid(void);
 
@@ -873,11 +886,27 @@ extern int          getpagesize(void);
 extern char        *getpass(const char *);
 extern pid_t        getpgid(pid_t);
 extern pid_t        getpgrp(void);
+
+/*@ //missing: assigns \result \from 'process id'
+  assigns \result \from \nothing;
+*/
 extern pid_t        getpid(void);
+
+/*@ //missing: assigns \result \from 'parent process id'
+  assigns \result \from \nothing;
+*/
 extern pid_t        getppid(void);
+
+/*@ //missing: assigns \result \from 'process sid'
+  assigns \result \from \nothing;
+*/
 extern pid_t        getsid(pid_t);
-/*@ assigns \result \from \nothing; */
+
+/*@ //missing: assigns \result \from 'process uid'
+  assigns \result \from \nothing;
+*/
 extern uid_t        getuid(void);
+
 extern char        *getwd(char *);
 extern int          isatty(int);
 extern int          lchown(const char *, uid_t, gid_t);
@@ -924,22 +953,63 @@ extern ssize_t      read(int fd, void *buf, size_t count);
 extern int          readlink(const char *, char *, size_t);
 extern int          rmdir(const char *);
 extern void        *sbrk(intptr_t);
+
+/*@ // missing: may assign errno to EINVAL or EPERM
+    // missing: assigns 'process egid' \from gid
+  assigns \result \from indirect:gid;
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
 extern int setegid(gid_t gid);
+
+/*@ // missing: may assign errno to EINVAL or EPERM
+    // missing: assigns 'process euid' \from uid
+  assigns \result \from indirect:uid;
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
 extern int seteuid(uid_t uid);
-extern int          setgid(gid_t);
+
+/*@ // missing: may assign errno to EINVAL or EPERM
+    // missing: assigns 'process gid' \from gid, 'process permissions'
+    // missing: assigns \result \from 'process permissions'
+  assigns \result \from indirect:gid;
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int          setgid(gid_t gid);
+
 extern int          setpgid(pid_t, pid_t);
 extern pid_t        setpgrp(void);
-extern int          setregid(gid_t, gid_t);
-extern int          setreuid(uid_t, uid_t);
+
+/*@ // missing: may assign errno to EINVAL, EPERM or EAGAIN
+    // missing: assigns 'process real/effective gid' \from gid
+    // missing: assigns \result \from 'process gid and permissions'
+  assigns \result \from indirect:rgid, indirect:egid;
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int          setregid(gid_t rgid, gid_t egid);
+
+/*@ // missing: may assign errno to EINVAL, EPERM or EAGAIN
+    // missing: assigns 'process real/effective uid' \from uid
+    // missing: assigns \result \from 'process uid and permissions'
+  assigns \result \from indirect:ruid, indirect:euid;
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
+extern int          setreuid(uid_t ruid, uid_t euid);
 
 /*@ // missing: may assign errno to EPERM
-    // missing: assigns 'processes' \from 'processes'
+    // missing: assigns \result, 'session, process, gid' \from 'process';
   assigns \result \from \nothing;
-  ensures result_new_proc_group_or_error: \result >= 0 || \result == -1;
-*/
+  ensures result_pgid_or_error: \result == -1 || \result >= 0;
+ */
 extern pid_t        setsid(void);
 
+/*@ // missing: may assign errno to EINVAL, EPERM or EAGAIN
+    // missing: assigns 'process uid' \from uid, 'process permissions'
+    // missing: assigns \result \from 'process permissions'
+  assigns \result \from indirect:uid;
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+*/
 extern int          setuid(uid_t uid);
+
 extern unsigned int sleep(unsigned int);
 extern void         swab(const void *, void *, ssize_t);
 extern int          symlink(const char *, const char *);
@@ -990,6 +1060,59 @@ extern ssize_t      write(int fd, const void *buf, size_t count);
 // setgroups() is not POSIX
 extern int setgroups(size_t size, const gid_t *list);
 
+// The following functions are GNU extensions
+#ifdef _GNU_SOURCE
+
+/*@
+  // missing: assigns \result, *ruid, *euid, *suid \from 'process'
+  // missing: may assign to errno: EFAULT
+  requires valid_ruid: \valid(ruid);
+  requires valid_euid: \valid(suid);
+  requires valid_suid: \valid(euid);
+  assigns *ruid, *euid, *suid \from \nothing;
+  assigns \result \from indirect:ruid, indirect:euid, indirect:suid;
+  ensures initialization:result_ok_or_error:
+    (\result == 0 &&
+     \initialized(ruid) && \initialized(euid) && \initialized(suid))
+    || \result == -1;
+ */
+int getresuid(uid_t *ruid, uid_t *euid, uid_t *suid);
+
+/*@
+  // missing: assigns 'process uid' \from ruid, euid, suid
+  // missing: assigns \result \from 'process permissions'
+  // missing: may assign to errno: EAGAIN, EINVAL, EPERM
+  assigns \result \from indirect:ruid, indirect:euid, indirect:suid;
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+ */
+int setresuid(uid_t ruid, uid_t euid, uid_t suid);
+
+/*@
+  // missing: assigns \result, *ruid, *euid, *suid \from 'process'
+  // missing: may assign to errno: EFAULT
+  requires valid_rgid: \valid(rgid);
+  requires valid_egid: \valid(sgid);
+  requires valid_sgid: \valid(egid);
+  assigns *rgid, *egid, *sgid \from \nothing;
+  assigns \result \from indirect:rgid, indirect:egid, indirect:sgid;
+  ensures initialization:result_ok_or_error:
+    (\result == 0 &&
+     \initialized(rgid) && \initialized(egid) && \initialized(sgid))
+    || \result == -1;
+ */
+int getresgid(gid_t *rgid, gid_t *egid, gid_t *sgid);
+
+/*@
+  // missing: assigns 'process gid' \from rgid, egid, sgid
+  // missing: assigns \result \from 'process permissions'
+  // missing: may assign to errno: EAGAIN, EINVAL, EPERM
+  assigns \result \from indirect:rgid, indirect:egid, indirect:sgid;
+  ensures result_ok_or_error: \result == 0 || \result == -1;
+ */
+int setresgid(gid_t rgid, gid_t egid, gid_t sgid);
+
+#endif
+
 __END_DECLS
 
 __POP_FC_STDLIB
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index c3bd7d502f9ae73e2dce8835804f0d7334950be1..3b2ce123cdf3d1c98f77750087627a1080b07d6e 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -13,7 +13,7 @@
 // functions.
 #define _XOPEN_SOURCE 600
 #define _POSIX_C_SOURCE 200112L
-
+#define _GNU_SOURCE 1
 
 #include "share/libc/fc_runtime.c"
 
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 1059b777a3ec6ebe381431b659f76838e9c5055c..c20ad3c51dd3215ec23183ee400ac4ffd9809d77 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -37,7 +37,7 @@
    wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (0 call);
    wmemset (0 call); 
   
-  Undefined functions (341)
+  Undefined functions (357)
   =========================
    FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
    Frama_C_abort (1 call); Frama_C_char_interval (0 call);
@@ -89,24 +89,26 @@
    ftrylockfile (0 call); funlockfile (0 call); fwrite (0 call);
    gai_strerror (0 call); getc (0 call); getc_unlocked (0 call);
    getchar (0 call); getchar_unlocked (0 call); getcwd (0 call);
-   gethostname (0 call); getitimer (0 call); getopt (0 call);
-   getopt_long (0 call); getopt_long_only (0 call); getpriority (0 call);
-   getpwuid (0 call); getrlimit (0 call); getrusage (0 call); gets (0 call);
-   getsockopt (0 call); gettimeofday (0 call); getuid (0 call);
-   gmtime (0 call); htonl (0 call); htons (0 call); iconv (0 call);
-   iconv_close (0 call); iconv_open (0 call); inet_addr (0 call);
-   inet_ntoa (0 call); inet_ntop (0 call); inet_pton (0 call);
-   isascii (0 call); kill (0 call); labs (0 call); ldiv (0 call);
-   listen (0 call); llabs (0 call); lldiv (0 call); localtime (0 call);
-   log (0 call); log10 (0 call); log10f (0 call); log10l (0 call);
-   log2 (0 call); log2f (0 call); log2l (0 call); logf (0 call); logl (0 call);
-   longjmp (0 call); lrand48 (0 call); malloc (6 calls); mblen (0 call);
-   mbstowcs (0 call); mbtowc (0 call); memoverlap (1 call); mkdir (0 call);
-   mktime (0 call); nan (0 call); nanf (0 call); nanl (0 call);
-   nanosleep (0 call); ntohl (0 call); ntohs (0 call); open (0 call);
-   openat (0 call); opendir (0 call); openlog (0 call); pathconf (0 call);
-   pclose (0 call); perror (0 call); pipe (0 call); poll (0 call);
-   popen (0 call); pow (0 call); powf (0 call);
+   getegid (0 call); geteuid (0 call); getgid (0 call); gethostname (0 call);
+   getitimer (0 call); getopt (0 call); getopt_long (0 call);
+   getopt_long_only (0 call); getpid (0 call); getppid (0 call);
+   getpriority (0 call); getpwuid (0 call); getresgid (0 call);
+   getresuid (0 call); getrlimit (0 call); getrusage (0 call); gets (0 call);
+   getsid (0 call); getsockopt (0 call); gettimeofday (0 call);
+   getuid (0 call); gmtime (0 call); htonl (0 call); htons (0 call);
+   iconv (0 call); iconv_close (0 call); iconv_open (0 call);
+   inet_addr (0 call); inet_ntoa (0 call); inet_ntop (0 call);
+   inet_pton (0 call); isascii (0 call); kill (0 call); labs (0 call);
+   ldiv (0 call); listen (0 call); llabs (0 call); lldiv (0 call);
+   localtime (0 call); log (0 call); log10 (0 call); log10f (0 call);
+   log10l (0 call); log2 (0 call); log2f (0 call); log2l (0 call);
+   logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call);
+   malloc (6 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
+   memoverlap (1 call); mkdir (0 call); mktime (0 call); nan (0 call);
+   nanf (0 call); nanl (0 call); nanosleep (0 call); ntohl (0 call);
+   ntohs (0 call); open (0 call); openat (0 call); opendir (0 call);
+   openlog (0 call); pathconf (0 call); pclose (0 call); perror (0 call);
+   pipe (0 call); poll (0 call); popen (0 call); pow (0 call); powf (0 call);
    pthread_cond_broadcast (0 call); pthread_cond_destroy (0 call);
    pthread_cond_init (0 call); pthread_cond_wait (0 call);
    pthread_create (0 call); pthread_join (0 call);
@@ -118,30 +120,33 @@
    readv (0 call); realloc (3 calls); recv (0 call); recvmsg (0 call);
    remove (0 call); rename (0 call); rewind (0 call); round (0 call);
    roundf (0 call); roundl (0 call); select (0 call); send (0 call);
-   setbuf (0 call); sethostname (0 call); setitimer (0 call); setjmp (0 call);
-   setlogmask (0 call); setpriority (0 call); setrlimit (0 call);
-   setsid (0 call); setsockopt (0 call); settimeofday (0 call);
-   setvbuf (0 call); shutdown (0 call); sigaddset (0 call); sigdelset (0 call);
-   sigemptyset (0 call); sigfillset (0 call); sigismember (0 call);
-   siglongjmp (0 call); signal (0 call); sigprocmask (0 call); sin (0 call);
-   sinf (0 call); sinl (0 call); socket (0 call); socketpair (0 call);
-   sqrt (0 call); sqrtf (0 call); sqrtl (0 call); srand (0 call);
-   srand48 (0 call); srandom (0 call); stat (0 call); strcoll (0 call);
-   strcspn (0 call); strftime (0 call); strncasecmp (0 call); strpbrk (0 call);
-   strsep (0 call); strspn (0 call); strtod (0 call); strtof (0 call);
-   strtoimax (0 call); strtok (0 call); strtok_r (0 call); strtol (0 call);
-   strtold (0 call); strtoll (0 call); strtoul (0 call); strtoull (0 call);
-   strxfrm (0 call); sync (0 call); sysconf (0 call); syslog (0 call);
-   system (0 call); tcgetattr (0 call); tcsetattr (0 call); time (0 call);
-   times (0 call); tmpfile (0 call); tmpnam (0 call); trunc (0 call);
-   truncf (0 call); truncl (0 call); tzset (0 call); umask (0 call);
-   ungetc (0 call); usleep (0 call); utimes (0 call); vfprintf (0 call);
-   vfscanf (0 call); vprintf (0 call); vscanf (0 call); vsnprintf (0 call);
-   vsprintf (0 call); vsyslog (0 call); wait (0 call); waitpid (0 call);
-   wcschr (0 call); wcscmp (0 call); wcscspn (0 call); wcslcat (0 call);
-   wcslcpy (0 call); wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call);
-   wcsspn (0 call); wcsstr (0 call); wcstombs (0 call); wctomb (0 call);
-   wmemchr (0 call); wmemcmp (0 call); wmemmove (0 call); write (0 call); 
+   setbuf (0 call); setegid (0 call); seteuid (0 call); setgid (0 call);
+   sethostname (0 call); setitimer (0 call); setjmp (0 call);
+   setlogmask (0 call); setpriority (0 call); setregid (0 call);
+   setresgid (0 call); setresuid (0 call); setreuid (0 call);
+   setrlimit (0 call); setsid (0 call); setsockopt (0 call);
+   settimeofday (0 call); setuid (0 call); setvbuf (0 call); shutdown (0 call);
+   sigaddset (0 call); sigdelset (0 call); sigemptyset (0 call);
+   sigfillset (0 call); sigismember (0 call); siglongjmp (0 call);
+   signal (0 call); sigprocmask (0 call); sin (0 call); sinf (0 call);
+   sinl (0 call); socket (0 call); socketpair (0 call); sqrt (0 call);
+   sqrtf (0 call); sqrtl (0 call); srand (0 call); srand48 (0 call);
+   srandom (0 call); stat (0 call); strcoll (0 call); strcspn (0 call);
+   strftime (0 call); strncasecmp (0 call); strpbrk (0 call); strsep (0 call);
+   strspn (0 call); strtod (0 call); strtof (0 call); strtoimax (0 call);
+   strtok (0 call); strtok_r (0 call); strtol (0 call); strtold (0 call);
+   strtoll (0 call); strtoul (0 call); strtoull (0 call); strxfrm (0 call);
+   sync (0 call); sysconf (0 call); syslog (0 call); system (0 call);
+   tcgetattr (0 call); tcsetattr (0 call); time (0 call); times (0 call);
+   tmpfile (0 call); tmpnam (0 call); trunc (0 call); truncf (0 call);
+   truncl (0 call); tzset (0 call); umask (0 call); ungetc (0 call);
+   usleep (0 call); utimes (0 call); vfprintf (0 call); vfscanf (0 call);
+   vprintf (0 call); vscanf (0 call); vsnprintf (0 call); vsprintf (0 call);
+   vsyslog (0 call); wait (0 call); waitpid (0 call); wcschr (0 call);
+   wcscmp (0 call); wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call);
+   wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call);
+   wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
+   wmemcmp (0 call); wmemmove (0 call); write (0 call); 
   
   'Extern' global variables (15)
   ==============================
@@ -164,7 +169,7 @@
   Goto = 78
   Assignment = 379
   Exit point = 73
-  Function = 414
+  Function = 430
   Function call = 73
   Pointer dereferencing = 146
   Cyclomatic complexity = 256
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 2187ffd35412361d18154acde76b9021f28c672c..7df313ff573d895684146f84abed98e0fc6a2906 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -6860,6 +6860,18 @@ extern pid_t fork(void);
  */
 extern char *getcwd(char *buf, size_t size);
 
+/*@ assigns \result;
+    assigns \result \from \nothing; */
+extern gid_t getegid(void);
+
+/*@ assigns \result;
+    assigns \result \from \nothing; */
+extern uid_t geteuid(void);
+
+/*@ assigns \result;
+    assigns \result \from \nothing; */
+extern gid_t getgid(void);
+
 extern char volatile __fc_hostname[64];
 
 /*@ requires name_has_room: \valid(name + (0 .. len - 1));
@@ -6882,6 +6894,18 @@ extern int gethostname(char *name, size_t len);
  */
 extern int sethostname(char const *name, size_t len);
 
+/*@ assigns \result;
+    assigns \result \from \nothing; */
+extern pid_t getpid(void);
+
+/*@ assigns \result;
+    assigns \result \from \nothing; */
+extern pid_t getppid(void);
+
+/*@ assigns \result;
+    assigns \result \from \nothing; */
+extern pid_t getsid(pid_t);
+
 /*@ assigns \result;
     assigns \result \from \nothing; */
 extern uid_t getuid(void);
@@ -6918,12 +6942,48 @@ extern int pipe(int * /*[2]*/ pipefd);
  */
 extern ssize_t read(int fd, void *buf, size_t count);
 
-/*@ ensures result_new_proc_group_or_error: \result ≥ 0 ∨ \result ≡ -1;
+/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result \from (indirect: gid);
+ */
+extern int setegid(gid_t gid);
+
+/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result \from (indirect: uid);
+ */
+extern int seteuid(uid_t uid);
+
+/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result \from (indirect: gid);
+ */
+extern int setgid(gid_t gid);
+
+/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result \from (indirect: rgid), (indirect: egid);
+ */
+extern int setregid(gid_t rgid, gid_t egid);
+
+/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result \from (indirect: ruid), (indirect: euid);
+ */
+extern int setreuid(uid_t ruid, uid_t euid);
+
+/*@ ensures result_pgid_or_error: \result ≡ -1 ∨ \result ≥ 0;
     assigns \result;
     assigns \result \from \nothing;
  */
 extern pid_t setsid(void);
 
+/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result \from (indirect: uid);
+ */
+extern int setuid(uid_t uid);
+
 /*@ assigns \nothing; */
 extern void sync(void);
 
@@ -6952,6 +7012,54 @@ extern int usleep(useconds_t usec);
  */
 extern ssize_t write(int fd, void const *buf, size_t count);
 
+/*@ requires valid_ruid: \valid(ruid);
+    requires valid_euid: \valid(suid);
+    requires valid_suid: \valid(euid);
+    ensures
+      initialization: result_ok_or_error:
+        (\result ≡ 0 ∧ \initialized(\old(ruid)) ∧
+         \initialized(\old(euid)) ∧ \initialized(\old(suid))) ∨
+        \result ≡ -1;
+    assigns *ruid, *euid, *suid, \result;
+    assigns *ruid \from \nothing;
+    assigns *euid \from \nothing;
+    assigns *suid \from \nothing;
+    assigns \result
+      \from (indirect: ruid), (indirect: euid), (indirect: suid);
+ */
+int getresuid(uid_t *ruid, uid_t *euid, uid_t *suid);
+
+/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result
+      \from (indirect: ruid), (indirect: euid), (indirect: suid);
+ */
+int setresuid(uid_t ruid, uid_t euid, uid_t suid);
+
+/*@ requires valid_rgid: \valid(rgid);
+    requires valid_egid: \valid(sgid);
+    requires valid_sgid: \valid(egid);
+    ensures
+      initialization: result_ok_or_error:
+        (\result ≡ 0 ∧ \initialized(\old(rgid)) ∧
+         \initialized(\old(egid)) ∧ \initialized(\old(sgid))) ∨
+        \result ≡ -1;
+    assigns *rgid, *egid, *sgid, \result;
+    assigns *rgid \from \nothing;
+    assigns *egid \from \nothing;
+    assigns *sgid \from \nothing;
+    assigns \result
+      \from (indirect: rgid), (indirect: egid), (indirect: sgid);
+ */
+int getresgid(gid_t *rgid, gid_t *egid, gid_t *sgid);
+
+/*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
+    assigns \result;
+    assigns \result
+      \from (indirect: rgid), (indirect: egid), (indirect: sgid);
+ */
+int setresgid(gid_t rgid, gid_t egid, gid_t sgid);
+
 void main(void)
 {
   /*@ assert __fc_p_fopen ≡ (FILE *)(&__fc_fopen); */ ;
diff --git a/tests/libc/oracle/unistd_h.0.res.oracle b/tests/libc/oracle/unistd_h.0.res.oracle
index 67e7fdf33f5021f2543927ebcfb3e339f683fa7b..b3c282aca8b923b282ddb7a0b4b20aef5ee7ef9f 100644
--- a/tests/libc/oracle/unistd_h.0.res.oracle
+++ b/tests/libc/oracle/unistd_h.0.res.oracle
@@ -1,6 +1,21 @@
 [kernel] Parsing tests/libc/unistd_h.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/libc/unistd_h.c:12: Warning: 
-  Calling undeclared function usleep. Old style K&R code?
+[eva] Splitting return states on:
+  \return(access) == 0 (auto)
+  \return(dup) == -1 (auto)
+  \return(getcwd) == 0 (auto)
+  \return(gethostname) == 0 (auto)
+  \return(setegid) == 0 (auto)
+  \return(seteuid) == 0 (auto)
+  \return(setgid) == 0 (auto)
+  \return(setregid) == 0 (auto)
+  \return(setreuid) == 0 (auto)
+  \return(setsid) == 0 (auto)
+  \return(setuid) == 0 (auto)
+  \return(usleep) == 0 (auto)
+  \return(getresuid) == 0 (auto)
+  \return(setresuid) == 0 (auto)
+  \return(getresgid) == 0 (auto)
+  \return(setresgid) == 0 (auto)
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
@@ -8,19 +23,23 @@
   nondet ∈ [--..--]
 [eva] computing for function usleep <- main.
   Called from tests/libc/unistd_h.c:12.
-[kernel:annot:missing-spec] tests/libc/unistd_h.c:12: Warning: 
-  Neither code nor specification for function usleep, generating default assigns from the prototype
 [eva] using specification for function usleep
 [eva] Done for function usleep
 [eva] computing for function usleep <- main.
   Called from tests/libc/unistd_h.c:13.
 [eva] Done for function usleep
+[eva] computing for function usleep <- main.
+  Called from tests/libc/unistd_h.c:13.
+[eva] Done for function usleep
 [eva] computing for function gethostname <- main.
   Called from tests/libc/unistd_h.c:15.
 [eva] using specification for function gethostname
 [eva] tests/libc/unistd_h.c:15: 
   function gethostname: precondition 'name_has_room' got status valid.
 [eva] Done for function gethostname
+[eva] computing for function gethostname <- main.
+  Called from tests/libc/unistd_h.c:15.
+[eva] Done for function gethostname
 [eva] computing for function execv <- main.
   Called from tests/libc/unistd_h.c:17.
 [eva] using specification for function execv
@@ -29,6 +48,9 @@
 [eva] tests/libc/unistd_h.c:17: 
   function execv: precondition 'valid_string_argv0' got status valid.
 [eva] Done for function execv
+[eva] computing for function execv <- main.
+  Called from tests/libc/unistd_h.c:17.
+[eva] Done for function execv
 [eva] computing for function access <- main.
   Called from tests/libc/unistd_h.c:19.
 [eva] using specification for function access
@@ -37,6 +59,9 @@
 [eva] tests/libc/unistd_h.c:19: 
   function access: precondition 'valid_amode' got status valid.
 [eva] Done for function access
+[eva] computing for function access <- main.
+  Called from tests/libc/unistd_h.c:19.
+[eva] Done for function access
 [eva] tests/libc/unistd_h.c:20: assertion got status valid.
 [eva] computing for function dup <- main.
   Called from tests/libc/unistd_h.c:22.
@@ -44,6 +69,9 @@
 [eva] tests/libc/unistd_h.c:22: 
   function dup: precondition 'valid_fildes' got status valid.
 [eva] Done for function dup
+[eva] computing for function dup <- main.
+  Called from tests/libc/unistd_h.c:22.
+[eva] Done for function dup
 [eva] tests/libc/unistd_h.c:23: assertion got status valid.
 [eva] computing for function dup2 <- main.
   Called from tests/libc/unistd_h.c:26.
@@ -53,6 +81,9 @@
 [eva] tests/libc/unistd_h.c:26: 
   function dup2: precondition 'valid_fildes2' got status valid.
 [eva] Done for function dup2
+[eva] computing for function dup2 <- main.
+  Called from tests/libc/unistd_h.c:26.
+[eva] Done for function dup2
 [eva] computing for function dup2 <- main.
   Called from tests/libc/unistd_h.c:28.
 [eva] tests/libc/unistd_h.c:28: 
@@ -60,15 +91,66 @@
 [eva:alarm] tests/libc/unistd_h.c:28: Warning: 
   function dup2: precondition 'valid_fildes2' got status invalid.
 [eva] Done for function dup2
+[eva] computing for function dup2 <- main.
+  Called from tests/libc/unistd_h.c:28.
+[eva] Done for function dup2
+[eva] computing for function dup2 <- main.
+  Called from tests/libc/unistd_h.c:28.
+[eva] Done for function dup2
+[eva] computing for function dup2 <- main.
+  Called from tests/libc/unistd_h.c:28.
+[eva] Done for function dup2
 [eva] computing for function fork <- main.
   Called from tests/libc/unistd_h.c:32.
 [eva] using specification for function fork
 [eva] Done for function fork
+[eva] computing for function fork <- main.
+  Called from tests/libc/unistd_h.c:32.
+[eva] Done for function fork
+[eva] computing for function fork <- main.
+  Called from tests/libc/unistd_h.c:32.
+[eva] Done for function fork
+[eva] computing for function fork <- main.
+  Called from tests/libc/unistd_h.c:32.
+[eva] Done for function fork
 [eva] tests/libc/unistd_h.c:33: assertion got status valid.
 [eva] computing for function setsid <- main.
   Called from tests/libc/unistd_h.c:35.
 [eva] using specification for function setsid
 [eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
 [eva] computing for function sync <- main.
   Called from tests/libc/unistd_h.c:37.
 [eva] using specification for function sync
@@ -91,12 +173,309 @@
 [eva] tests/libc/unistd_h.c:48: 
   function pathconf: precondition 'valid_path' got status valid.
 [eva] Done for function pathconf
+[eva] computing for function pathconf <- main.
+  Called from tests/libc/unistd_h.c:48.
+[eva] Done for function pathconf
+[eva] computing for function getresuid <- main.
+  Called from tests/libc/unistd_h.c:51.
+[eva] using specification for function getresuid
+[eva] tests/libc/unistd_h.c:51: 
+  function getresuid: precondition 'valid_ruid' got status valid.
+[eva] tests/libc/unistd_h.c:51: 
+  function getresuid: precondition 'valid_euid' got status valid.
+[eva] tests/libc/unistd_h.c:51: 
+  function getresuid: precondition 'valid_suid' got status valid.
+[eva] Done for function getresuid
+[eva] computing for function getresuid <- main.
+  Called from tests/libc/unistd_h.c:51.
+[eva] Done for function getresuid
+[eva] computing for function setresuid <- main.
+  Called from tests/libc/unistd_h.c:53.
+[eva] using specification for function setresuid
+[eva] Done for function setresuid
+[eva] computing for function setresuid <- main.
+  Called from tests/libc/unistd_h.c:53.
+[eva] Done for function setresuid
+[eva] tests/libc/unistd_h.c:54: assertion got status valid.
+[eva] computing for function getresgid <- main.
+  Called from tests/libc/unistd_h.c:57.
+[eva] using specification for function getresgid
+[eva] tests/libc/unistd_h.c:57: 
+  function getresgid: precondition 'valid_rgid' got status valid.
+[eva] tests/libc/unistd_h.c:57: 
+  function getresgid: precondition 'valid_egid' got status valid.
+[eva] tests/libc/unistd_h.c:57: 
+  function getresgid: precondition 'valid_sgid' got status valid.
+[eva] Done for function getresgid
+[eva] computing for function getresgid <- main.
+  Called from tests/libc/unistd_h.c:57.
+[eva] Done for function getresgid
+[eva] computing for function getresgid <- main.
+  Called from tests/libc/unistd_h.c:57.
+[eva] Done for function getresgid
+[eva] computing for function getresgid <- main.
+  Called from tests/libc/unistd_h.c:57.
+[eva] Done for function getresgid
+[eva] computing for function getresgid <- main.
+  Called from tests/libc/unistd_h.c:57.
+[eva] Done for function getresgid
+[eva] computing for function getresgid <- main.
+  Called from tests/libc/unistd_h.c:57.
+[eva] Done for function getresgid
+[eva] computing for function setresgid <- main.
+  Called from tests/libc/unistd_h.c:59.
+[eva] using specification for function setresgid
+[eva] Done for function setresgid
+[eva] computing for function setresgid <- main.
+  Called from tests/libc/unistd_h.c:59.
+[eva] Done for function setresgid
+[eva] computing for function setresgid <- main.
+  Called from tests/libc/unistd_h.c:59.
+[eva] Done for function setresgid
+[eva] computing for function setresgid <- main.
+  Called from tests/libc/unistd_h.c:59.
+[eva] Done for function setresgid
+[eva] tests/libc/unistd_h.c:60: assertion got status valid.
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] using specification for function getpid
+[eva] Done for function getpid
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] Done for function getpid
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] Done for function getpid
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] Done for function getpid
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] Done for function getpid
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] Done for function getpid
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] Done for function getpid
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] Done for function getpid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] using specification for function getppid
+[eva] Done for function getppid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] Done for function getppid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] Done for function getppid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] Done for function getppid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] Done for function getppid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] Done for function getppid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] Done for function getppid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] Done for function getppid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] using specification for function getsid
+[eva] Done for function getsid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] Done for function getsid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] Done for function getsid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] Done for function getsid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] Done for function getsid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] Done for function getsid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] Done for function getsid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] Done for function getsid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] using specification for function getuid
+[eva] Done for function getuid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] Done for function getuid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] Done for function getuid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] Done for function getuid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] Done for function getuid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] Done for function getuid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] Done for function getuid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] Done for function getuid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] using specification for function getgid
+[eva] Done for function getgid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] Done for function getgid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] Done for function getgid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] Done for function getgid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] Done for function getgid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] Done for function getgid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] Done for function getgid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] Done for function getgid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] using specification for function geteuid
+[eva] Done for function geteuid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] Done for function geteuid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] Done for function geteuid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] Done for function geteuid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] Done for function geteuid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] Done for function geteuid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] Done for function geteuid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] Done for function geteuid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] using specification for function getegid
+[eva] Done for function getegid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] Done for function getegid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] Done for function getegid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] Done for function getegid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] Done for function getegid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] Done for function getegid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] Done for function getegid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] Done for function getegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] using specification for function setegid
+[eva] Done for function setegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] Done for function setegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] Done for function setegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] Done for function setegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] Done for function setegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] Done for function setegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] Done for function setegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] Done for function setegid
+[eva] computing for function seteuid <- main.
+  Called from tests/libc/unistd_h.c:70.
+[eva] using specification for function seteuid
+[eva] Done for function seteuid
+[eva] computing for function setgid <- main.
+  Called from tests/libc/unistd_h.c:71.
+[eva] using specification for function setgid
+[eva] Done for function setgid
+[eva] computing for function setgid <- main.
+  Called from tests/libc/unistd_h.c:71.
+[eva] Done for function setgid
+[eva] computing for function setuid <- main.
+  Called from tests/libc/unistd_h.c:72.
+[eva] using specification for function setuid
+[eva] Done for function setuid
+[eva] computing for function setuid <- main.
+  Called from tests/libc/unistd_h.c:72.
+[eva] Done for function setuid
+[eva] computing for function setregid <- main.
+  Called from tests/libc/unistd_h.c:73.
+[eva] using specification for function setregid
+[eva] Done for function setregid
+[eva] computing for function setregid <- main.
+  Called from tests/libc/unistd_h.c:73.
+[eva] Done for function setregid
+[eva] computing for function setreuid <- main.
+  Called from tests/libc/unistd_h.c:74.
+[eva] using specification for function setreuid
+[eva] Done for function setreuid
+[eva] computing for function setreuid <- main.
+  Called from tests/libc/unistd_h.c:74.
+[eva] Done for function setreuid
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
-  __fc_fds[0..1023] ∈ [--..--]
-  r ∈ [-1..2147483647]
+  Frama_C_entropy_source ∈ [--..--]
+  __fc_fds[0] ∈ {0}
+          [1..1023] ∈ [--..--]
+  r ∈ {-1; 0}
   hostname[0..255] ∈ [--..--] or UNINITIALIZED
   fd ∈ [-1..1023]
   fd2 ∈ [-1..1023]
@@ -105,4 +484,11 @@
   cwd[0..63] ∈ [--..--] or UNINITIALIZED
   res_getcwd ∈ {{ NULL ; &cwd[0] }}
   pconf ∈ [--..--]
+  ruid ∈ [--..--] or UNINITIALIZED
+  euid ∈ [--..--] or UNINITIALIZED
+  suid ∈ [--..--] or UNINITIALIZED
+  rgid ∈ [--..--] or UNINITIALIZED
+  egid ∈ [--..--] or UNINITIALIZED
+  sgid ∈ [--..--] or UNINITIALIZED
+  p ∈ [--..--]
   __retres ∈ {0; 1}
diff --git a/tests/libc/oracle/unistd_h.1.res.oracle b/tests/libc/oracle/unistd_h.1.res.oracle
index 8f4a84f91072717045aba18c24ba1bf045077bb0..2b8e38fde21be6b2a210316f37aea41ee8d236a8 100644
--- a/tests/libc/oracle/unistd_h.1.res.oracle
+++ b/tests/libc/oracle/unistd_h.1.res.oracle
@@ -1,6 +1,21 @@
 [kernel] Parsing tests/libc/unistd_h.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/libc/unistd_h.c:12: Warning: 
-  Calling undeclared function usleep. Old style K&R code?
+[eva] Splitting return states on:
+  \return(access) == 0 (auto)
+  \return(dup) == -1 (auto)
+  \return(getcwd) == 0 (auto)
+  \return(gethostname) == 0 (auto)
+  \return(setegid) == 0 (auto)
+  \return(seteuid) == 0 (auto)
+  \return(setgid) == 0 (auto)
+  \return(setregid) == 0 (auto)
+  \return(setreuid) == 0 (auto)
+  \return(setsid) == 0 (auto)
+  \return(setuid) == 0 (auto)
+  \return(usleep) == 0 (auto)
+  \return(getresuid) == 0 (auto)
+  \return(setresuid) == 0 (auto)
+  \return(getresgid) == 0 (auto)
+  \return(setresgid) == 0 (auto)
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
@@ -8,19 +23,23 @@
   nondet ∈ [--..--]
 [eva] computing for function usleep <- main.
   Called from tests/libc/unistd_h.c:12.
-[kernel:annot:missing-spec] tests/libc/unistd_h.c:12: Warning: 
-  Neither code nor specification for function usleep, generating default assigns from the prototype
 [eva] using specification for function usleep
 [eva] Done for function usleep
 [eva] computing for function usleep <- main.
   Called from tests/libc/unistd_h.c:13.
 [eva] Done for function usleep
+[eva] computing for function usleep <- main.
+  Called from tests/libc/unistd_h.c:13.
+[eva] Done for function usleep
 [eva] computing for function gethostname <- main.
   Called from tests/libc/unistd_h.c:15.
 [eva] using specification for function gethostname
 [eva] tests/libc/unistd_h.c:15: 
   function gethostname: precondition 'name_has_room' got status valid.
 [eva] Done for function gethostname
+[eva] computing for function gethostname <- main.
+  Called from tests/libc/unistd_h.c:15.
+[eva] Done for function gethostname
 [eva] computing for function execl <- main.
   Called from tests/libc/unistd_h.c:17.
 [eva] using specification for function execl
@@ -29,6 +48,9 @@
 [eva] tests/libc/unistd_h.c:17: 
   function execl: precondition 'valid_string_arg' got status valid.
 [eva] Done for function execl
+[eva] computing for function execl <- main.
+  Called from tests/libc/unistd_h.c:17.
+[eva] Done for function execl
 [eva] computing for function access <- main.
   Called from tests/libc/unistd_h.c:19.
 [eva] using specification for function access
@@ -37,6 +59,9 @@
 [eva] tests/libc/unistd_h.c:19: 
   function access: precondition 'valid_amode' got status valid.
 [eva] Done for function access
+[eva] computing for function access <- main.
+  Called from tests/libc/unistd_h.c:19.
+[eva] Done for function access
 [eva] tests/libc/unistd_h.c:20: assertion got status valid.
 [eva] computing for function dup <- main.
   Called from tests/libc/unistd_h.c:22.
@@ -44,6 +69,9 @@
 [eva] tests/libc/unistd_h.c:22: 
   function dup: precondition 'valid_fildes' got status valid.
 [eva] Done for function dup
+[eva] computing for function dup <- main.
+  Called from tests/libc/unistd_h.c:22.
+[eva] Done for function dup
 [eva] tests/libc/unistd_h.c:23: assertion got status valid.
 [eva] computing for function dup2 <- main.
   Called from tests/libc/unistd_h.c:26.
@@ -53,6 +81,9 @@
 [eva] tests/libc/unistd_h.c:26: 
   function dup2: precondition 'valid_fildes2' got status valid.
 [eva] Done for function dup2
+[eva] computing for function dup2 <- main.
+  Called from tests/libc/unistd_h.c:26.
+[eva] Done for function dup2
 [eva] computing for function dup2 <- main.
   Called from tests/libc/unistd_h.c:28.
 [eva] tests/libc/unistd_h.c:28: 
@@ -60,15 +91,66 @@
 [eva:alarm] tests/libc/unistd_h.c:28: Warning: 
   function dup2: precondition 'valid_fildes2' got status invalid.
 [eva] Done for function dup2
+[eva] computing for function dup2 <- main.
+  Called from tests/libc/unistd_h.c:28.
+[eva] Done for function dup2
+[eva] computing for function dup2 <- main.
+  Called from tests/libc/unistd_h.c:28.
+[eva] Done for function dup2
+[eva] computing for function dup2 <- main.
+  Called from tests/libc/unistd_h.c:28.
+[eva] Done for function dup2
 [eva] computing for function fork <- main.
   Called from tests/libc/unistd_h.c:32.
 [eva] using specification for function fork
 [eva] Done for function fork
+[eva] computing for function fork <- main.
+  Called from tests/libc/unistd_h.c:32.
+[eva] Done for function fork
+[eva] computing for function fork <- main.
+  Called from tests/libc/unistd_h.c:32.
+[eva] Done for function fork
+[eva] computing for function fork <- main.
+  Called from tests/libc/unistd_h.c:32.
+[eva] Done for function fork
 [eva] tests/libc/unistd_h.c:33: assertion got status valid.
 [eva] computing for function setsid <- main.
   Called from tests/libc/unistd_h.c:35.
 [eva] using specification for function setsid
 [eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
+[eva] computing for function setsid <- main.
+  Called from tests/libc/unistd_h.c:35.
+[eva] Done for function setsid
 [eva] computing for function sync <- main.
   Called from tests/libc/unistd_h.c:37.
 [eva] using specification for function sync
@@ -91,12 +173,309 @@
 [eva] tests/libc/unistd_h.c:48: 
   function pathconf: precondition 'valid_path' got status valid.
 [eva] Done for function pathconf
+[eva] computing for function pathconf <- main.
+  Called from tests/libc/unistd_h.c:48.
+[eva] Done for function pathconf
+[eva] computing for function getresuid <- main.
+  Called from tests/libc/unistd_h.c:51.
+[eva] using specification for function getresuid
+[eva] tests/libc/unistd_h.c:51: 
+  function getresuid: precondition 'valid_ruid' got status valid.
+[eva] tests/libc/unistd_h.c:51: 
+  function getresuid: precondition 'valid_euid' got status valid.
+[eva] tests/libc/unistd_h.c:51: 
+  function getresuid: precondition 'valid_suid' got status valid.
+[eva] Done for function getresuid
+[eva] computing for function getresuid <- main.
+  Called from tests/libc/unistd_h.c:51.
+[eva] Done for function getresuid
+[eva] computing for function setresuid <- main.
+  Called from tests/libc/unistd_h.c:53.
+[eva] using specification for function setresuid
+[eva] Done for function setresuid
+[eva] computing for function setresuid <- main.
+  Called from tests/libc/unistd_h.c:53.
+[eva] Done for function setresuid
+[eva] tests/libc/unistd_h.c:54: assertion got status valid.
+[eva] computing for function getresgid <- main.
+  Called from tests/libc/unistd_h.c:57.
+[eva] using specification for function getresgid
+[eva] tests/libc/unistd_h.c:57: 
+  function getresgid: precondition 'valid_rgid' got status valid.
+[eva] tests/libc/unistd_h.c:57: 
+  function getresgid: precondition 'valid_egid' got status valid.
+[eva] tests/libc/unistd_h.c:57: 
+  function getresgid: precondition 'valid_sgid' got status valid.
+[eva] Done for function getresgid
+[eva] computing for function getresgid <- main.
+  Called from tests/libc/unistd_h.c:57.
+[eva] Done for function getresgid
+[eva] computing for function getresgid <- main.
+  Called from tests/libc/unistd_h.c:57.
+[eva] Done for function getresgid
+[eva] computing for function getresgid <- main.
+  Called from tests/libc/unistd_h.c:57.
+[eva] Done for function getresgid
+[eva] computing for function getresgid <- main.
+  Called from tests/libc/unistd_h.c:57.
+[eva] Done for function getresgid
+[eva] computing for function getresgid <- main.
+  Called from tests/libc/unistd_h.c:57.
+[eva] Done for function getresgid
+[eva] computing for function setresgid <- main.
+  Called from tests/libc/unistd_h.c:59.
+[eva] using specification for function setresgid
+[eva] Done for function setresgid
+[eva] computing for function setresgid <- main.
+  Called from tests/libc/unistd_h.c:59.
+[eva] Done for function setresgid
+[eva] computing for function setresgid <- main.
+  Called from tests/libc/unistd_h.c:59.
+[eva] Done for function setresgid
+[eva] computing for function setresgid <- main.
+  Called from tests/libc/unistd_h.c:59.
+[eva] Done for function setresgid
+[eva] tests/libc/unistd_h.c:60: assertion got status valid.
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] using specification for function getpid
+[eva] Done for function getpid
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] Done for function getpid
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] Done for function getpid
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] Done for function getpid
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] Done for function getpid
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] Done for function getpid
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] Done for function getpid
+[eva] computing for function getpid <- main.
+  Called from tests/libc/unistd_h.c:62.
+[eva] Done for function getpid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] using specification for function getppid
+[eva] Done for function getppid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] Done for function getppid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] Done for function getppid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] Done for function getppid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] Done for function getppid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] Done for function getppid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] Done for function getppid
+[eva] computing for function getppid <- main.
+  Called from tests/libc/unistd_h.c:63.
+[eva] Done for function getppid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] using specification for function getsid
+[eva] Done for function getsid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] Done for function getsid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] Done for function getsid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] Done for function getsid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] Done for function getsid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] Done for function getsid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] Done for function getsid
+[eva] computing for function getsid <- main.
+  Called from tests/libc/unistd_h.c:64.
+[eva] Done for function getsid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] using specification for function getuid
+[eva] Done for function getuid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] Done for function getuid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] Done for function getuid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] Done for function getuid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] Done for function getuid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] Done for function getuid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] Done for function getuid
+[eva] computing for function getuid <- main.
+  Called from tests/libc/unistd_h.c:65.
+[eva] Done for function getuid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] using specification for function getgid
+[eva] Done for function getgid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] Done for function getgid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] Done for function getgid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] Done for function getgid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] Done for function getgid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] Done for function getgid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] Done for function getgid
+[eva] computing for function getgid <- main.
+  Called from tests/libc/unistd_h.c:66.
+[eva] Done for function getgid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] using specification for function geteuid
+[eva] Done for function geteuid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] Done for function geteuid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] Done for function geteuid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] Done for function geteuid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] Done for function geteuid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] Done for function geteuid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] Done for function geteuid
+[eva] computing for function geteuid <- main.
+  Called from tests/libc/unistd_h.c:67.
+[eva] Done for function geteuid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] using specification for function getegid
+[eva] Done for function getegid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] Done for function getegid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] Done for function getegid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] Done for function getegid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] Done for function getegid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] Done for function getegid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] Done for function getegid
+[eva] computing for function getegid <- main.
+  Called from tests/libc/unistd_h.c:68.
+[eva] Done for function getegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] using specification for function setegid
+[eva] Done for function setegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] Done for function setegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] Done for function setegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] Done for function setegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] Done for function setegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] Done for function setegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] Done for function setegid
+[eva] computing for function setegid <- main.
+  Called from tests/libc/unistd_h.c:69.
+[eva] Done for function setegid
+[eva] computing for function seteuid <- main.
+  Called from tests/libc/unistd_h.c:70.
+[eva] using specification for function seteuid
+[eva] Done for function seteuid
+[eva] computing for function setgid <- main.
+  Called from tests/libc/unistd_h.c:71.
+[eva] using specification for function setgid
+[eva] Done for function setgid
+[eva] computing for function setgid <- main.
+  Called from tests/libc/unistd_h.c:71.
+[eva] Done for function setgid
+[eva] computing for function setuid <- main.
+  Called from tests/libc/unistd_h.c:72.
+[eva] using specification for function setuid
+[eva] Done for function setuid
+[eva] computing for function setuid <- main.
+  Called from tests/libc/unistd_h.c:72.
+[eva] Done for function setuid
+[eva] computing for function setregid <- main.
+  Called from tests/libc/unistd_h.c:73.
+[eva] using specification for function setregid
+[eva] Done for function setregid
+[eva] computing for function setregid <- main.
+  Called from tests/libc/unistd_h.c:73.
+[eva] Done for function setregid
+[eva] computing for function setreuid <- main.
+  Called from tests/libc/unistd_h.c:74.
+[eva] using specification for function setreuid
+[eva] Done for function setreuid
+[eva] computing for function setreuid <- main.
+  Called from tests/libc/unistd_h.c:74.
+[eva] Done for function setreuid
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
-  __fc_fds[0..1023] ∈ [--..--]
-  r ∈ [-1..2147483647]
+  Frama_C_entropy_source ∈ [--..--]
+  __fc_fds[0] ∈ {0}
+          [1..1023] ∈ [--..--]
+  r ∈ {-1; 0}
   hostname[0..255] ∈ [--..--] or UNINITIALIZED
   fd ∈ [-1..1023]
   fd2 ∈ [-1..1023]
@@ -105,4 +484,11 @@
   cwd[0..63] ∈ [--..--] or UNINITIALIZED
   res_getcwd ∈ {{ NULL ; &cwd[0] }}
   pconf ∈ [--..--]
+  ruid ∈ [--..--] or UNINITIALIZED
+  euid ∈ [--..--] or UNINITIALIZED
+  suid ∈ [--..--] or UNINITIALIZED
+  rgid ∈ [--..--] or UNINITIALIZED
+  egid ∈ [--..--] or UNINITIALIZED
+  sgid ∈ [--..--] or UNINITIALIZED
+  p ∈ [--..--]
   __retres ∈ {0; 1}
diff --git a/tests/libc/unistd_h.c b/tests/libc/unistd_h.c
index 6a3322b6a101d877870f992a5cd88f9428a6f424..d0f26a9bb533cfcd4ecc21ea3368c432382d277c 100644
--- a/tests/libc/unistd_h.c
+++ b/tests/libc/unistd_h.c
@@ -1,10 +1,10 @@
 /*run.config
-  STDOPT:
-  STDOPT: #"-variadic-no-translation"
+  STDOPT: #"-slevel 12" #"-val-split-return auto"
+  STDOPT: #"-variadic-no-translation" #"-slevel 12" #"-val-split-return auto"
 */
-#include <unistd.h>
-
+#define _GNU_SOURCE
 #define _XOPEN_SOURCE 600
+#include <unistd.h>
 
 volatile int nondet;
 
@@ -47,5 +47,31 @@ int main() {
 
   long pconf = pathconf("/tmp/conf.cfg", _PC_NAME_MAX);
 
+  uid_t ruid, euid, suid;
+  r = getresuid(&ruid, &euid, &suid);
+  if (!r) {
+    r = setresuid(ruid, euid, suid);
+    //@ assert r == 0 || r == -1;
+  }
+  gid_t rgid, egid, sgid;
+  r = getresgid(&rgid, &egid, &sgid);
+  if (!r) {
+    r = setresgid(rgid, egid, sgid);
+    //@ assert r == 0 || r == -1;
+  }
+  pid_t p = getpid();
+  p = getppid();
+  p = getsid(0);
+  ruid = getuid();
+  rgid = getgid();
+  euid = geteuid();
+  egid = getegid();
+  r = setegid(egid);
+  r = seteuid(euid);
+  r = setgid(rgid);
+  r = setuid(ruid);
+  r = setregid(rgid, egid);
+  r = setreuid(ruid, euid);
+
   return 0;
 }