From a8a94c1c190b3e93ed57d05a3145756599c00226 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 13 Jan 2023 17:32:07 +0100
Subject: [PATCH] [libc] add _SS_MAXSIZE and fix stub for recvfrom
---
share/libc/sys/socket.c | 9 ++++-----
share/libc/sys/socket.h | 4 ++++
2 files changed, 8 insertions(+), 5 deletions(-)
diff --git a/share/libc/sys/socket.c b/share/libc/sys/socket.c
index ca4cf1c5b55..e1cfd553a5a 100644
--- a/share/libc/sys/socket.c
+++ b/share/libc/sys/socket.c
@@ -90,15 +90,14 @@ ssize_t recvfrom(int sockfd, void *buf, size_t len, int flags,
// 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);
+ Frama_C_make_unknown((char*)addrbuf, *addrbuf_len);
/* 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;
+ greater than was supplied to the call."
+ Here we use _SS_MAXSIZE as the maximum address struct size. */
+ *addrbuf_len = Frama_C_unsigned_int_interval(0, _SS_MAXSIZE);
}
return Frama_C_long_interval(0, len);
}
diff --git a/share/libc/sys/socket.h b/share/libc/sys/socket.h
index 93472efdd30..5885125caaf 100644
--- a/share/libc/sys/socket.h
+++ b/share/libc/sys/socket.h
@@ -42,8 +42,12 @@ typedef __UINT_LEAST32_T socklen_t;
#include "../__fc_define_ssize_t.h"
#include "../features.h"
+// Non-POSIX; value taken from Linux implementation
+#define _SS_MAXSIZE 128
+
struct sockaddr_storage {
sa_family_t ss_family;
+ char __sa_data[_SS_MAXSIZE - sizeof(sa_family_t)]; /* non-POSIX */
};
#include "./uio.h"
--
GitLab