diff --git a/share/libc/fcntl.h b/share/libc/fcntl.h
index b5dabf3d70c9ccdc206c122459d2cff06b7c6b38..5e90adad1c48f5ec25e8129baec0a905ef30a79c 100644
--- a/share/libc/fcntl.h
+++ b/share/libc/fcntl.h
@@ -72,6 +72,9 @@ __PUSH_FC_STDLIB
 #define O_RSYNC 0x101000
 #define O_SYNC 0x101000
 
+// Non-POSIX
+#define O_PATH 010000000
+
 #define O_ACCMODE 3
 
 //#define O_EXEC
@@ -81,15 +84,19 @@ __PUSH_FC_STDLIB
 #define O_WRONLY 1
 
 #define AT_FDCWD -100
-
 #define AT_EACCESS 0x200
-
 #define AT_SYMLINK_NOFOLLOW 0x100
-
 #define AT_SYMLINK_FOLLOW 0x400
-
 #define AT_REMOVEDIR 0x200
 
+// Non-POSIX (GNU extensions)
+#define AT_EMPTY_PATH 0x1000
+#define AT_RECURSIVE 0x8000
+#define AT_STATX_DONT_SYNC 0x4000
+#define AT_STATX_FORCE_SYNC 0x2000
+#define AT_STATX_SYNC_AS_STAT 0x0000
+#define AT_STATX_SYNC_TYPE 0x6000
+
 #define POSIX_FADV_DONTNEED 4
 #define POSIX_FADV_NOREUSE 5
 #define POSIX_FADV_NORMAL 0
diff --git a/share/libc/signal.h b/share/libc/signal.h
index b594a4b53e1d83fbd0f41dabec244dd9237f9ce4..09ee3a57aaeb3ff8f979e5136acbae00c784545e 100644
--- a/share/libc/signal.h
+++ b/share/libc/signal.h
@@ -31,6 +31,7 @@ __PUSH_FC_STDLIB
 #include "__fc_define_pid_t.h"
 #include "__fc_define_uid_and_gid.h"
 #include "__fc_define_pthread_types.h"
+#include "errno.h"
 
 __BEGIN_DECLS
 
@@ -243,6 +244,16 @@ extern int sigaction(int signum, const struct sigaction *restrict act,
 extern int sigprocmask(int how, const sigset_t * restrict set,
                        sigset_t *restrict oldset);
 
+/*@ // missing: assigns 'current signal mask'
+    // missing: assigns \result from 'possible thread interruption'
+    // missing: terminates 'only when interrupted'
+  requires valid_mask_or_null: sigmask == \null || \valid_read(sigmask);
+  assigns __fc_errno, \result \from indirect:sigmask;
+  ensures result_means_interrupted: \result == -1;
+  ensures errno_set: __fc_errno == EINTR;
+*/
+extern int sigsuspend(const sigset_t *sigmask);
+
 /*@ // missing: errno may be set to EINVAL, EPERM, ESRCH
     // missing: assigns 'other processes' \from 'other processes'
   assigns \result \from indirect:pid, indirect: sig;
diff --git a/share/libc/sys/socket.h b/share/libc/sys/socket.h
index 114226d440b98d6ddeb1f02ee7ef9249709a3be9..846a297f0d77a28f582529c6a34c0cd14975f5bb 100644
--- a/share/libc/sys/socket.h
+++ b/share/libc/sys/socket.h
@@ -66,6 +66,17 @@ struct msghdr {
   int            msg_flags;
 };
 
+// POSIX requires these as macros; early uses of these macros (e.g. when
+// computing the size of arrays) prevent us from leaving them undefined and
+// using a function prototype. The following definitions are based on the
+// Linux version of the GNU libc.
+#define CMSG_DATA(cmsg) ((unsigned char *) ((struct cmsghdr *) (cmsg) + 1))
+#define CMSG_ALIGN(len) (((len) + sizeof (size_t) - 1) \
+                     & (size_t) ~(sizeof (size_t) - 1))
+#define CMSG_SPACE(len) (CMSG_ALIGN (len) \
+                       + CMSG_ALIGN (sizeof (struct cmsghdr)))
+#define CMSG_LEN(len)   (CMSG_ALIGN (sizeof (struct cmsghdr)) + (len))
+
 // POSIX.1-2008 requires these to be defined as macros, but we have no body
 // for them, so we declare them as prototypes as well.
 #ifndef CMSG_FIRSTHDR
@@ -76,22 +87,6 @@ extern struct cmsghdr *CMSG_FIRSTHDR(struct msghdr *msgh);
 extern struct cmsghdr *CMSG_NXTHDR(struct msghdr *msgh, struct cmsghdr *cmsg);
 # define CMSG_NXTHDR(h, c) CMSG_NXTHDR(h, c)
 #endif
-#ifndef CMSG_ALIGN
-extern size_t CMSG_ALIGN(size_t length);
-# define CMSG_ALIGN(l) CMSG_ALIGN(l)
-#endif
-#ifndef CMSG_SPACE
-extern size_t CMSG_SPACE(size_t length);
-# define CMSG_SPACE(l) CMSG_SPACE(l)
-#endif
-#ifndef CMSG_LEN
-extern size_t CMSG_LEN(size_t length);
-# define CMSG_LEN(l) CMSG_LEN(l)
-#endif
-#ifndef CMSG_DATA
-extern unsigned char *CMSG_DATA(struct cmsghdr *cmsg);
-# define CMSG_DATA(c) CMSG_DATA(c)
-#endif
 
 /* Socket types. */
 #define SOCK_STREAM	1		/* stream (connection) socket	*/
@@ -295,6 +290,12 @@ struct __fc_sockfds_type { int x; };
 
 // __fc_sockfds represents the state of open socket descriptors.
 //@ ghost volatile int __fc_open_sock_fds;
+
+struct linger {
+  int l_onoff;
+  int l_linger;
+};
+
 // TODO: Model the state of some functions more precisely.
 
 /*@
diff --git a/share/libc/sys/types.h b/share/libc/sys/types.h
index 68f3deb924a44b5d0c31a326c7e575391ee1a745..be288c41c42ad0374b801625116759fbe8432a17 100644
--- a/share/libc/sys/types.h
+++ b/share/libc/sys/types.h
@@ -59,6 +59,11 @@ typedef unsigned char u_char;
 #define __u_char_defined
 #endif
 
+// Non-POSIX
+#ifndef caddr_t
+typedef char *caddr_t;
+#endif
+
 __END_DECLS
 __POP_FC_STDLIB
 #endif
diff --git a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
index ff5a912894d02533eca168e09c1a0d527f8aa8ef..bb16be630f99af99d6d13c3be855b349dc69e1ea 100644
--- a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121: 
+[variadic] FRAMAC_SHARE/libc/fcntl.h:128: 
   Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:131: 
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:138: 
   Declaration of variadic function openat.
 [variadic] fcntl.c:8: 
   Translating call to the specialized version fcntl(int, int).
diff --git a/src/plugins/variadic/tests/known/oracle/open.res.oracle b/src/plugins/variadic/tests/known/oracle/open.res.oracle
index 9b5c71ca58f9f5128de42393fbd4e864502a471e..190fa3b120e3a946cc6391c65da74033c2769a65 100644
--- a/src/plugins/variadic/tests/known/oracle/open.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121: 
+[variadic] FRAMAC_SHARE/libc/fcntl.h:128: 
   Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:131: 
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:138: 
   Declaration of variadic function openat.
 [variadic] open.c:7: 
   Translating call to the specialized version open(char const *, int, mode_t).
diff --git a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
index 1f4b8a7cd11d50816dc9c19df5ed3ca045374332..a3eb22c271660f3a9a834373baaf5fdad1e0c1e9 100644
--- a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121: 
+[variadic] FRAMAC_SHARE/libc/fcntl.h:128: 
   Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:131: 
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:138: 
   Declaration of variadic function openat.
 [variadic:prototype] open_wrong.c:13: Warning: 
   No matching prototype found for this call to open.
diff --git a/src/plugins/variadic/tests/known/oracle/openat.res.oracle b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
index 30a3448710c4d06aee7faf364f4c40d6b0b32137..96183ba11078a119dcde3ec9072e083d1063d929 100644
--- a/src/plugins/variadic/tests/known/oracle/openat.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
@@ -1,7 +1,7 @@
-[variadic] FRAMAC_SHARE/libc/fcntl.h:121: 
+[variadic] FRAMAC_SHARE/libc/fcntl.h:128: 
   Declaration of variadic function fcntl.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:124: Declaration of variadic function open.
-[variadic] FRAMAC_SHARE/libc/fcntl.h:131: 
+[variadic] FRAMAC_SHARE/libc/fcntl.h:131: Declaration of variadic function open.
+[variadic] FRAMAC_SHARE/libc/fcntl.h:138: 
   Declaration of variadic function openat.
 [variadic] openat.c:8: 
   Translating call to the specialized version openat(int, char const *, int, mode_t).
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index a081af020567740d163a884cea6fb8618fb442ad..4e29fd1c1c8fa3eba10a011955ab5ddfd1e7dff7 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -4465,6 +4465,15 @@ extern int sigaction(int signum, struct sigaction const * restrict act,
 extern int sigprocmask(int how, sigset_t const * restrict set,
                        sigset_t * restrict oldset);
 
+/*@ requires valid_mask_or_null: sigmask ≡ \null ∨ \valid_read(sigmask);
+    ensures result_means_interrupted: \result ≡ -1;
+    ensures errno_set: __fc_errno ≡ 4;
+    assigns __fc_errno, \result;
+    assigns __fc_errno \from (indirect: sigmask);
+    assigns \result \from (indirect: sigmask);
+ */
+extern int sigsuspend(sigset_t const *sigmask);
+
 /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1;
     assigns \result;
     assigns \result \from (indirect: pid), (indirect: sig);
diff --git a/tests/libc/oracle/signal_h.res.oracle b/tests/libc/oracle/signal_h.res.oracle
index 0141d180b8fb97c279280f379a382b1fb4c2f4dc..7c70744fb716464287f0a4115e9fc8b0831f7884 100644
--- a/tests/libc/oracle/signal_h.res.oracle
+++ b/tests/libc/oracle/signal_h.res.oracle
@@ -126,7 +126,7 @@
   function sigaction: precondition 'valid_read_act_or_null' got status valid.
 [eva] signal_h.c:48: 
   function sigaction: precondition 'separation,separated_acts' got status valid.
-[eva] FRAMAC_SHARE/libc/signal.h:222: 
+[eva] FRAMAC_SHARE/libc/signal.h:223: 
   cannot evaluate ACSL term, unsupported ACSL construct: logic coercion struct sigaction -> set<struct sigaction>
 [eva] Done for function sigaction
 [eva] computing for function sigaction <- main.
@@ -143,10 +143,19 @@
   Completely invalid destination for assigns clause *oldact. Ignoring.
 [eva] Done for function sigaction
 [eva] signal_h.c:55: assertion 'valid_nsig' got status valid.
+[eva] computing for function sigsuspend <- main.
+  Called from signal_h.c:59.
+[eva] using specification for function sigsuspend
+[eva] signal_h.c:59: 
+  function sigsuspend: precondition 'valid_mask_or_null' got status valid.
+[eva] Done for function sigsuspend
+[eva] signal_h.c:60: assertion 'sigsuspend_errno_eintr' got status valid.
+[eva] signal_h.c:61: assertion 'sigsuspend_return' got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
+  __fc_errno ∈ [--..--]
   __fc_sigaction[0]{.sa_handler; .sa_sigaction} ∈ {0}
                 [0]{.sa_mask; .sa_flags} ∈ [--..--]
                 [1]{.sa_handler; .sa_sigaction} ∈ {0}
diff --git a/tests/libc/signal_h.c b/tests/libc/signal_h.c
index bfb2fb979f9a27cfa6932a29b6430b9caeb9df99..0ece2aacd9036295377516406ea8a3edb28e1ccb 100644
--- a/tests/libc/signal_h.c
+++ b/tests/libc/signal_h.c
@@ -1,8 +1,8 @@
 /* run.config
    STDOPT: #"-eva-slevel 2"
 */
+#include <errno.h>
 #include <signal.h>
-
 volatile int nondet;
 
 int main() {
@@ -54,5 +54,12 @@ int main() {
 
   //@ assert valid_nsig: NSIG >= 0;
 
+  if (nondet) {
+    errno = 0;
+    int r = sigsuspend(&s);
+    //@ assert sigsuspend_errno_eintr: errno == EINTR;
+    //@ assert sigsuspend_return: r == -1;
+  }
+
   return 0;
 }
diff --git a/tests/syntax/oracle/signal.res.oracle b/tests/syntax/oracle/signal.res.oracle
index 8ce74a3d6137f430ed592c8d9a9b5af0899c7f27..cda400014c7a2aeb65862097577fc1e0e9372e64 100644
--- a/tests/syntax/oracle/signal.res.oracle
+++ b/tests/syntax/oracle/signal.res.oracle
@@ -1,5 +1,6 @@
 [kernel] Parsing signal.c (with preprocessing)
 /* Generated by Frama-C */
+#include "errno.h"
 #include "signal.h"
 void f(void)
 {