diff --git a/share/dune b/share/dune
index 098d41e97818127a223d5a9a46b21a30fc9acd30..6ae783ccbd6e00b9138922d1e83c90b462fa28b1 100644
--- a/share/dune
+++ b/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)
diff --git a/share/libc/__fc_runtime.c b/share/libc/__fc_runtime.c
index 2852dae1905cdc8f89ba1ff63494e8e396590076..e266ed9e0f44b3b747f56ccb0fd83adfbbb733c8 100644
--- a/share/libc/__fc_runtime.c
+++ b/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"
diff --git a/share/libc/getopt.c b/share/libc/getopt.c
index 741109e43a762820608e1fd503ea7c91b35ddc1e..472a8c9455e0aa36897a083bf3451f9580ff81af 100644
--- a/share/libc/getopt.c
+++ b/share/libc/getopt.c
@@ -23,6 +23,6 @@
#include "getopt.h"
__PUSH_FC_STDLIB
-int optind = 1;
+//int optind = 1;
__POP_FC_STDLIB
diff --git a/share/libc/sys/socket.c b/share/libc/sys/socket.c
new file mode 100644
index 0000000000000000000000000000000000000000..ca4cf1c5b5590b5e399d550e9c14fc4d493d2ed7
--- /dev/null
+++ b/share/libc/sys/socket.c
@@ -0,0 +1,108 @@
+/**************************************************************************/
+/* */
+/* 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
diff --git a/share/libc/unistd.c b/share/libc/unistd.c
index 00793690ace93fb32c4a1a51feb76c062f131739..ab6770c0ad8fba00e7f5fda3897ce0639105ef6a 100644
--- a/share/libc/unistd.c
+++ b/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
diff --git a/tests/libc/unistd_c.c b/tests/libc/unistd_c.c
new file mode 100644
index 0000000000000000000000000000000000000000..0bb8b52e1d9b9374e3f1ea3538bc92f363f21301
--- /dev/null
+++ b/tests/libc/unistd_c.c
@@ -0,0 +1,8 @@
+#include "unistd.c"
+
+int main() {
+ int argc = 4;
+ char *argv[] = {"program_name", "-this", "is a", "Test0"};
+ int r = getopt(argc, argv, "tes:");
+ return 0;
+}