Merge branch 'feature/andre/libc-posix-non-posix' into 'master'

[libc] improve POSIX and non-POSIX compatibility

See merge request frama-c/frama-c!3944

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

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;

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.
 
 /*@

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

src/plugins/variadic/tests/known/oracle/fcntl.res.oracle

-[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).

src/plugins/variadic/tests/known/oracle/open.res.oracle

-[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).

src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle

-[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.

src/plugins/variadic/tests/known/oracle/openat.res.oracle

-[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).

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

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}

tests/libc/signal_h.c

 /* 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;
 }

tests/syntax/oracle/signal.res.oracle

 [kernel] Parsing signal.c (with preprocessing)
 /* Generated by Frama-C */
+#include "errno.h"
 #include "signal.h"
 void f(void)
 {