From 51251cad3242679063890c8d320854c915b7dee0 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 23 Sep 2024 16:09:08 +0200
Subject: [PATCH] [Libc] fixes and improvements after review
---
share/libc/dirent.h | 12 ++++++------
share/libc/ifaddrs.h | 7 +++++--
share/libc/utmp.h | 38 +++++++++++++++++++-------------------
3 files changed, 30 insertions(+), 27 deletions(-)
diff --git a/share/libc/dirent.h b/share/libc/dirent.h
index 6502d82e23..bd4e1f4f7c 100644
--- a/share/libc/dirent.h
+++ b/share/libc/dirent.h
@@ -59,7 +59,7 @@ extern int alphasort(const struct dirent **a, const struct dirent **b);
/*@
requires dirp_valid_dir_stream: \subset(dirp,&__fc_opendir[0 .. __FC_FOPEN_MAX-1]);
assigns \result \from dirp, *dirp, __fc_p_opendir;
- assigns __fc_errno \from dirp, *dirp, __fc_p_opendir;
+ assigns errno \from dirp, *dirp, __fc_p_opendir;
assigns *dirp \from dirp, *dirp, __fc_p_opendir;
ensures err_or_closed_on_success:
(\result == 0 && dirp->__fc_dir_inode == \null) || \result == -1;
@@ -73,13 +73,14 @@ extern int dirfd(DIR *fd);
/*@
assigns \result \from __fc_p_opendir;
+ assigns errno \from indirect:__fc_opendir[0 .. __FC_FOPEN_MAX-1];
assigns __fc_opendir[0 .. __FC_FOPEN_MAX-1] \from __fc_opendir[0 .. __FC_FOPEN_MAX-1];
*/
extern DIR *fdopendir(int fd);
/*@
assigns \result \from path[0..], __fc_p_opendir;
- assigns __fc_errno \from path[0..], __fc_p_opendir;
+ assigns errno \from path[0..], __fc_p_opendir;
ensures result_null_or_valid: \result == \null || \valid(\result);
ensures valid_dir_stream_on_success:
\result != \null ==> \result == &__fc_opendir[\result->__fc_dir_id];
@@ -92,17 +93,16 @@ extern DIR *opendir(const char *path);
requires dirp_valid_dir_stream: \subset(dirp, &__fc_opendir[0 .. __FC_FOPEN_MAX-1]);
assigns \result \from *dirp, __fc_p_opendir;
assigns dirp->__fc_dir_position \from dirp->__fc_dir_position;
- assigns __fc_errno \from dirp, *dirp, __fc_p_opendir;
+ assigns errno \from dirp, *dirp, __fc_p_opendir;
ensures result_null_or_valid: \result == \null || \valid(\result);
*/
extern struct dirent *readdir(DIR *dirp);
/*@
assigns \result \from *dirp, __fc_p_opendir;
- assigns *dirp \from *dirp;
- assigns *entry \from *entry;
+ assigns *dirp, *entry \from *dirp;
assigns *result \from entry;
- assigns __fc_errno \from indirect:*dirp, indirect:*entry;
+ assigns errno \from indirect:*dirp, indirect:*entry;
*/
extern int readdir_r(DIR * dirp, struct dirent * entry,
struct dirent ** result);
diff --git a/share/libc/ifaddrs.h b/share/libc/ifaddrs.h
index 3103c22978..f51042afb7 100644
--- a/share/libc/ifaddrs.h
+++ b/share/libc/ifaddrs.h
@@ -26,6 +26,7 @@
__PUSH_FC_STDLIB
#include "__fc_define_sockaddr.h"
+#include "errno.h"
__BEGIN_DECLS
@@ -59,7 +60,8 @@ struct ifmaddrs {
/*@
allocates *ifap;
- assigns \result, *ifap \from \nothing; // missing: \from 'system interfaces'
+ assigns \result, *ifap, errno \from \nothing;
+ // missing: \from 'system interfaces'
*/
extern int getifaddrs(struct ifaddrs **ifap);
@@ -71,7 +73,8 @@ extern void freeifaddrs(struct ifaddrs *ifa);
/*@
allocates *ifmap;
- assigns \result, *ifmap \from \nothing; // missing: \from 'system interfaces'
+ assigns \result, *ifmap, errno \from \nothing;
+ // missing: \from 'system interfaces'
*/
extern int getifmaddrs(struct ifmaddrs **ifmap);
diff --git a/share/libc/utmp.h b/share/libc/utmp.h
index 3f7894f0e6..a0db12304b 100644
--- a/share/libc/utmp.h
+++ b/share/libc/utmp.h
@@ -115,16 +115,16 @@ extern void setutent (void);
extern void endutent (void);
/*@
- assigns \result \from &__fc_get, indirect:__fc_utmp, indirect:*id;
- assigns __fc_get \from __fc_get, indirect:__fc_utmp, indirect:*id;
+ assigns \result \from &__fc_get, indirect:__fc_utmp, indirect:*ut;
+ assigns __fc_get \from __fc_get, indirect:__fc_utmp, indirect:*ut;
*/
-extern struct utmp *getutid (const struct utmp *id);
+extern struct utmp *getutid (const struct utmp *ut);
/*@
- assigns \result \from &__fc_get, indirect:__fc_utmp, indirect:*line;
- assigns __fc_get \from __fc_get, indirect:__fc_utmp, indirect:*line;
+ assigns \result \from &__fc_get, indirect:__fc_utmp, indirect:*ut;
+ assigns __fc_get \from __fc_get, indirect:__fc_utmp, indirect:*ut;
*/
-extern struct utmp *getutline (const struct utmp *line);
+extern struct utmp *getutline (const struct utmp *ut);
/*@
assigns __fc_utmp \from __fc_utmp, *utmp_ptr;
@@ -134,26 +134,26 @@ extern struct utmp *pututline (const struct utmp *utmp_ptr);
/*@
assigns \result \from indirect:__fc_utmp;
- assigns *buffer \from __fc_utmp;
- assigns *result \from &__fc_utmp;
+ assigns *ubuf \from __fc_utmp;
+ assigns *ubufp \from &__fc_utmp;
*/
-extern int getutent_r (struct utmp *buffer, struct utmp **result);
+extern int getutent_r (struct utmp *ubuf, struct utmp **ubufp);
/*@
- assigns \result \from indirect:*id, indirect:__fc_utmp;
- assigns *buffer \from indirect:*id, __fc_utmp;
- assigns *result \from indirect:*id, &__fc_utmp;
+ assigns \result \from indirect:*ut, indirect:__fc_utmp;
+ assigns *ubuf \from indirect:*ut, __fc_utmp;
+ assigns *ubufp \from indirect:*ut, &__fc_utmp;
*/
-extern int getutid_r (const struct utmp *id, struct utmp *buffer,
- struct utmp **result);
+extern int getutid_r (const struct utmp *ut, struct utmp *ubuf,
+ struct utmp **ubufp);
/*@
- assigns \result \from indirect:*line, indirect:__fc_utmp;
- assigns *buffer \from indirect:*line, __fc_utmp;
- assigns *result \from indirect:*line, &__fc_utmp;
+ assigns \result \from indirect:*ut, indirect:__fc_utmp;
+ assigns *ubuf \from indirect:*ut, __fc_utmp;
+ assigns *ubufp \from indirect:*ut, &__fc_utmp;
*/
-extern int getutline_r (const struct utmp *line,
- struct utmp *buffer, struct utmp **result);
+extern int getutline_r (const struct utmp *ut,
+ struct utmp *ubuf, struct utmp **ubufp);
__END_DECLS
--
GitLab