From 290033e73ed6bd2e79e9dbed88b46bac732ed7c1 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 4 May 2021 11:51:57 +0200
Subject: [PATCH] [libc] move some macro definitions to sys/select.h
---
share/libc/__fc_define_fd_set_t.h | 34 -------------------------------
share/libc/sys/select.h | 34 +++++++++++++++++++++++++++++++
2 files changed, 34 insertions(+), 34 deletions(-)
diff --git a/share/libc/__fc_define_fd_set_t.h b/share/libc/__fc_define_fd_set_t.h
index 5f9b7c721b2..5e6bbe02725 100644
--- a/share/libc/__fc_define_fd_set_t.h
+++ b/share/libc/__fc_define_fd_set_t.h
@@ -29,40 +29,6 @@ __PUSH_FC_STDLIB
__BEGIN_DECLS
typedef struct __fc_fd_set { long __fc_fd_set[FD_SETSIZE / NFDBITS]; } fd_set;
-/*@
- requires valid_fdset: \valid(fdset);
- requires initialization: \initialized(fdset);
- assigns *fdset \from *fdset, indirect:fd;
-*/
-extern void FD_CLR(int fd, fd_set *fdset);
-#define FD_CLR FD_CLR
-
-// Note: the 2nd argument in FD_ISSET is not const in some implementations
-// due to historical and compatibility reasons.
-/*@
- requires valid_fdset: \valid_read(fdset);
- requires initialization: \initialized(fdset);
- assigns \result \from indirect:*fdset, indirect:fd;
-*/
-extern int FD_ISSET(int fd, const fd_set *fdset);
-#define FD_ISSET FD_ISSET
-
-/*@
- requires valid_fdset: \valid(fdset);
- requires initialization: \initialized(fdset);
- assigns *fdset \from *fdset, indirect:fd;
-*/
-extern void FD_SET(int fd, fd_set *fdset);
-#define FD_SET FD_SET
-
-/*@
- requires valid_fdset: \valid(fdset);
- assigns *fdset \from \nothing;
- ensures initialization: \initialized(fdset);
-*/
-extern void FD_ZERO(fd_set *fdset);
-#define FD_ZERO FD_ZERO
-
__END_DECLS
__POP_FC_STDLIB
#endif
diff --git a/share/libc/sys/select.h b/share/libc/sys/select.h
index c680c04d2e2..d3ceb4b5848 100644
--- a/share/libc/sys/select.h
+++ b/share/libc/sys/select.h
@@ -28,6 +28,40 @@ __BEGIN_DECLS
#include "../__fc_select.h"
+/*@
+ requires valid_fdset: \valid(fdset);
+ requires initialization: \initialized(fdset);
+ assigns *fdset \from *fdset, indirect:fd;
+*/
+extern void FD_CLR(int fd, fd_set *fdset);
+#define FD_CLR FD_CLR
+
+// Note: the 2nd argument in FD_ISSET is not const in some implementations
+// due to historical and compatibility reasons.
+/*@
+ requires valid_fdset: \valid_read(fdset);
+ requires initialization: \initialized(fdset);
+ assigns \result \from indirect:*fdset, indirect:fd;
+*/
+extern int FD_ISSET(int fd, const fd_set *fdset);
+#define FD_ISSET FD_ISSET
+
+/*@
+ requires valid_fdset: \valid(fdset);
+ requires initialization: \initialized(fdset);
+ assigns *fdset \from *fdset, indirect:fd;
+*/
+extern void FD_SET(int fd, fd_set *fdset);
+#define FD_SET FD_SET
+
+/*@
+ requires valid_fdset: \valid(fdset);
+ assigns *fdset \from \nothing;
+ ensures initialization: \initialized(fdset);
+*/
+extern void FD_ZERO(fd_set *fdset);
+#define FD_ZERO FD_ZERO
+
__END_DECLS
__POP_FC_STDLIB
#endif
--
GitLab