[libc] add C stubs for socket functions and getopt

share/dune

@@ -236,6 +236,7 @@
 (libc/sys/sendfile.h as libc/sys/sendfile.h)
 (libc/sys/shm.h as libc/sys/shm.h)
 (libc/sys/signal.h as libc/sys/signal.h)
+(libc/sys/socket.c as libc/sys/socket.c)
 (libc/sys/socket.h as libc/sys/socket.h)
 (libc/sys/stat.h as libc/sys/stat.h)
 (libc/sys/statvfs.h as libc/sys/statvfs.h)

share/libc/__fc_runtime.c

@@ -35,6 +35,7 @@
 #include "netinet/in.c"
 #include "pwd.c"
 #include "signal.c"
+#include "sys/socket.c"
 #include "stdatomic.c"
 #include "stdio.c"
 #include "stdlib.c"

share/libc/getopt.c

@@ -23,6 +23,6 @@
 #include "getopt.h"
 __PUSH_FC_STDLIB
 
-int optind = 1;
+//int optind = 1;
 
 __POP_FC_STDLIB

share/libc/sys/socket.c

+/**************************************************************************/
+/*                                                                        */
+/*  This file is part of Frama-C.                                         */
+/*                                                                        */
+/*  Copyright (C) 2007-2023                                               */
+/*    CEA (Commissariat à l'énergie atomique et aux énergies              */
+/*         alternatives)                                                  */
+/*                                                                        */
+/*  you can redistribute it and/or modify it under the terms of the GNU   */
+/*  Lesser General Public License as published by the Free Software       */
+/*  Foundation, version 2.1.                                              */
+/*                                                                        */
+/*  It is distributed in the hope that it will be useful,                 */
+/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
+/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
+/*  GNU Lesser General Public License for more details.                   */
+/*                                                                        */
+/*  See the GNU Lesser General Public License version 2.1                 */
+/*  for more details (enclosed in the file licenses/LGPLv2.1).            */
+/*                                                                        */
+/**************************************************************************/
+
+#include "socket.h"
+#include "../__fc_builtin.h"
+__PUSH_FC_STDLIB
+
+ssize_t sendto(int sockfd, const void *buf, size_t len, int flags,
+               const struct sockaddr *address, socklen_t address_len) {
+  // assuming preconditions already checked
+  if (Frama_C_nondet(0, 1)) {
+    // error
+    int possible_errors[] = {
+      EACCES,
+      EAFNOSUPPORT,
+      EAGAIN,
+      EBADF,
+      ECONNRESET,
+      EDESTADDRREQ,
+      EHOSTUNREACH,
+      EINTR,
+      EINVAL,
+      EIO,
+      EISCONN,
+      ELOOP,
+      EMSGSIZE,
+      ENAMETOOLONG,
+      ENETDOWN,
+      ENETUNREACH,
+      ENOBUFS,
+      ENOENT,
+      ENOMEM,
+      ENOTCONN,
+      ENOTDIR,
+      ENOTSOCK,
+      EOPNOTSUPP,
+      EPIPE,
+      EWOULDBLOCK,
+    };
+    errno = possible_errors[Frama_C_interval(0, sizeof(possible_errors)/sizeof(int)-1)];
+    return -1;
+  } else {
+    // non-error
+    return Frama_C_long_interval(0, len);
+  }
+}
+
+ssize_t recvfrom(int sockfd, void *buf, size_t len, int flags,
+                 struct sockaddr *addrbuf, socklen_t *addrbuf_len) {
+  // assuming preconditions already checked
+  if (Frama_C_nondet(0, 1)) {
+    // error
+    int possible_errors[] = {
+      EAGAIN,
+      EBADF,
+      ECONNRESET,
+      EINTR,
+      EINVAL,
+      EIO,
+      ENOBUFS,
+      ENOMEM,
+      ENOTCONN,
+      ENOTSOCK,
+      EOPNOTSUPP,
+      ETIMEDOUT,
+      EWOULDBLOCK,
+    };
+    errno = possible_errors[Frama_C_interval(0, sizeof(possible_errors)/sizeof(int)-1)];
+    return -1;
+  } else {
+    // non-error
+    ((char*)buf)[Frama_C_interval(0, len-1)] = Frama_C_interval(0, 255);
+    if (addrbuf) {
+      // simulate writing source address
+      socklen_t addrlen = *addrbuf_len > sizeof(struct sockaddr) ? *addrbuf_len : sizeof(struct sockaddr);
+      Frama_C_make_unknown((char*)addrbuf, addrlen);
+      /* From the "Linux Programmer's Manual:
+         "Upon return, 'addrbuf_len' is updated to contain the actual size of
+         the source address. The returned address is truncated if the buffer
+         provided is too small; in this case, 'addrbuf_len' will return a value
+         greater than was supplied to the call. */
+      *addrbuf_len = addrlen;
+    }
+    return Frama_C_long_interval(0, len);
+  }
+
+}
+
+__POP_FC_STDLIB

share/libc/unistd.c

@@ -22,7 +22,22 @@
 
 #include "unistd.h"
 #include "__fc_builtin.h"
+#include "string.h"
 __PUSH_FC_STDLIB
 
 volatile char __fc_ttyname[TTY_NAME_MAX];
+
+int optind = 1;
+char *optarg;
+int opterr = 1; // initial value is not zero (zero silences error messages)
+
+int getopt(int argc, char * const argv[], const char *optstring) {
+  if (argc == 0) {
+    return -1;
+  }
+  optind = Frama_C_interval(1, argc - 1);
+  optarg = Frama_C_nondet_ptr(0, &argv[optind][Frama_C_interval(0, strlen(argv[optind])-1)]);
+  return Frama_C_nondet(-1, Frama_C_char_interval(CHAR_MIN, CHAR_MAX));
+}
+
 __POP_FC_STDLIB

tests/libc/unistd_c.c

+#include "unistd.c"
+
+int main() {
+  int argc = 4;
+  char *argv[] = {"program_name", "-this", "is a", "Test0"};
+  int r = getopt(argc, argv, "tes:");
+  return 0;
+}