From c689bfc5a962e86c4cb7cec2c67b0a9d63dd5630 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 2 May 2024 14:39:01 +0200
Subject: [PATCH] [libc] add several assigns clauses and minor improvements
---
share/compliance/nonstandard_identifiers.json | 8 +
share/dune | 1 +
share/libc/__fc_utmp_constants.h | 65 ++
share/libc/dirent.h | 64 +-
share/libc/ifaddrs.h | 27 +-
share/libc/locale.h | 6 +-
share/libc/netdb.h | 126 +++-
share/libc/pthread.h | 553 ++++++++++++++----
share/libc/pwd.h | 15 +
share/libc/semaphore.h | 62 +-
share/libc/signal.h | 5 +
share/libc/spawn.h | 76 ++-
share/libc/strings.h | 36 +-
share/libc/utmp.h | 80 ++-
share/libc/utmpx.h | 50 +-
tests/libc/fc_libc.c | 1 +
16 files changed, 981 insertions(+), 194 deletions(-)
create mode 100644 share/libc/__fc_utmp_constants.h
diff --git a/share/compliance/nonstandard_identifiers.json b/share/compliance/nonstandard_identifiers.json
index 86e2fa0eb0e..4f4072a4687 100644
--- a/share/compliance/nonstandard_identifiers.json
+++ b/share/compliance/nonstandard_identifiers.json
@@ -7,9 +7,16 @@
"error_at_line": {"header":"error.h"},
"error_message_count": {"header":"error.h"},
"error_one_per_line": {"header":"error.h"},
+ "exit_status": {"header":"utmp.h"},
"facilitynames": {"header":"syslog.h"},
+ "freeifaddrs": {"header":"ifaddrs.h"},
+ "freeifmaddrs": {"header":"ifaddrs.h"},
+ "getifaddrs": {"header":"ifaddrs.h"},
+ "getifmaddrs": {"header":"ifaddrs.h"},
"getresgid": {"header":"unistd.h"},
"getresuid": {"header":"unistd.h"},
+ "ifaddrs": {"header":"ifaddrs.h"},
+ "ifmaddrs": {"header":"ifaddrs.h"},
"makedev": {"header":"sys/types.h"},
"option": {"header":"getopt.h"},
"prioritynames": {"header":"syslog.h"},
@@ -21,6 +28,7 @@
"strcspn": {"header":"string.h"},
"strlcat": {"header":"string.h"},
"strlcpy": {"header":"string.h"},
+ "utmp": {"header":"tmp.h"},
"wcslcat": {"header":"wchar.h"},
"wcslcpy": {"header":"wchar.h"}
}
diff --git a/share/dune b/share/dune
index 95125fc8c20..bdd583e6b68 100644
--- a/share/dune
+++ b/share/dune
@@ -137,6 +137,7 @@
(libc/__fc_runtime.c as libc/__fc_runtime.c)
(libc/__fc_select.h as libc/__fc_select.h)
(libc/__fc_string_axiomatic.h as libc/__fc_string_axiomatic.h)
+(libc/__fc_utmp_constants.h as libc/__fc_utmp_constants.h)
(libc/aio.h as libc/aio.h)
(libc/alloca.h as libc/alloca.h)
(libc/argz.c as libc/argz.c)
diff --git a/share/libc/__fc_utmp_constants.h b/share/libc/__fc_utmp_constants.h
new file mode 100644
index 00000000000..36e64981f35
--- /dev/null
+++ b/share/libc/__fc_utmp_constants.h
@@ -0,0 +1,65 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2024 */
+/* 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). */
+/* */
+/**************************************************************************/
+
+#ifndef __FC_DEFINE_FC_UTMP_CONSTANTS
+#define __FC_DEFINE_FC_UTMP_CONSTANTS
+#include "features.h"
+__PUSH_FC_STDLIB
+__BEGIN_DECLS
+#include "stdio.h"
+
+#define _PATH_UTMP "/var/run/utmp"
+#define UTMP_FILE _PATH_UTMP
+#define UTMP_FILENAME _PATH_UTMP
+#define _PATH_WTMP "/var/log/wtmp"
+#define WTMP_FILE _PATH_WTMP
+#define WTMP_FILENAME _PATH_WTMP
+
+#define UT_LINESIZE 32
+#define UT_NAMESIZE 32
+#define UT_HOSTSIZE 256
+
+#define EMPTY 0
+#define BOOT_TIME 2
+#define OLD_TIME 4
+#define NEW_TIME 3
+#define USER_PROCESS 7
+#define INIT_PROCESS 5
+#define LOGIN_PROCESS 6
+#define DEAD_PROCESS 8
+
+#define ut_name ut_user
+#ifndef _NO_UT_TIME
+# define ut_time ut_tv.tv_sec
+#endif
+#define ut_xtime ut_tv.tv_sec
+#define ut_addr ut_addr_v6[0]
+
+// represents the user accounting database, /var/run/utmp
+extern FILE __fc_utmp;
+
+// represents the user accounting database, /var/run/wtmp
+extern FILE __fc_wtmp;
+
+__END_DECLS
+__POP_FC_STDLIB
+#endif
diff --git a/share/libc/dirent.h b/share/libc/dirent.h
index 29b62b28e9b..6502d82e23f 100644
--- a/share/libc/dirent.h
+++ b/share/libc/dirent.h
@@ -51,7 +51,10 @@ typedef struct DIR {
DIR __fc_opendir[__FC_FOPEN_MAX];
DIR* const __fc_p_opendir = __fc_opendir;
-extern int alphasort(const struct dirent **, const struct dirent **);
+/*@
+ assigns \result \from indirect:*a[0..], indirect:*b[0..];
+*/
+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]);
@@ -61,9 +64,18 @@ extern int alphasort(const struct dirent **, const struct dirent **);
ensures err_or_closed_on_success:
(\result == 0 && dirp->__fc_dir_inode == \null) || \result == -1;
*/
-extern int closedir(DIR *dirp);
-extern int dirfd(DIR *);
-extern DIR *fdopendir(int);
+extern int closedir(DIR *dirp);
+
+/*@
+ assigns \result \from *fd;
+*/
+extern int dirfd(DIR *fd);
+
+/*@
+ assigns \result \from __fc_p_opendir;
+ 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;
@@ -74,7 +86,7 @@ extern DIR *fdopendir(int);
ensures stream_positioned_on_success:
\result != \null ==> \result->__fc_dir_inode != \null;
*/
-extern DIR *opendir(const char *path);
+extern DIR *opendir(const char *path);
/*@
requires dirp_valid_dir_stream: \subset(dirp, &__fc_opendir[0 .. __FC_FOPEN_MAX-1]);
@@ -85,16 +97,40 @@ extern DIR *opendir(const char *path);
*/
extern struct dirent *readdir(DIR *dirp);
-extern int readdir_r(DIR * dirp, struct dirent * entry,
- struct dirent ** result);
-extern void rewinddir(DIR *);
-extern int scandir(const char *, struct dirent ***,
- int (*)(const struct dirent *),
- int (*)(const struct dirent **,
- const struct dirent **));
+/*@
+ assigns \result \from *dirp, __fc_p_opendir;
+ assigns *dirp \from *dirp;
+ assigns *entry \from *entry;
+ assigns *result \from entry;
+ assigns __fc_errno \from indirect:*dirp, indirect:*entry;
+*/
+extern int readdir_r(DIR * dirp, struct dirent * entry,
+ struct dirent ** result);
+
+/*@
+ assigns *dirp \from *dirp;
+*/
+extern void rewinddir(DIR *dirp);
+
+/*@
+ allocates *namelist;
+ assigns \result, *namelist
+ \from indirect:dir[0..], indirect:sel, indirect:compar;
+*/
+extern int scandir(const char *dir, struct dirent ***namelist,
+ int (*sel)(const struct dirent *),
+ int (*compar)(const struct dirent **,
+ const struct dirent **));
-extern void seekdir(DIR *, long);
-extern long telldir(DIR *);
+/*@
+ assigns *dirp \from *dirp, loc;
+*/
+extern void seekdir(DIR *dirp, long loc);
+
+/*@
+ assigns \result \from *dirp;
+*/
+extern long telldir(DIR *dirp);
diff --git a/share/libc/ifaddrs.h b/share/libc/ifaddrs.h
index 47bea2299b9..3103c229785 100644
--- a/share/libc/ifaddrs.h
+++ b/share/libc/ifaddrs.h
@@ -57,10 +57,29 @@ struct ifmaddrs {
struct sockaddr *ifma_lladdr;
};
-extern int getifaddrs(struct ifaddrs **);
-extern void freeifaddrs(struct ifaddrs *);
-extern int getifmaddrs(struct ifmaddrs **);
-extern void freeifmaddrs(struct ifmaddrs *);
+/*@
+ allocates *ifap;
+ assigns \result, *ifap \from \nothing; // missing: \from 'system interfaces'
+*/
+extern int getifaddrs(struct ifaddrs **ifap);
+
+/*@
+ frees ifa;
+ assigns \nothing;
+*/
+extern void freeifaddrs(struct ifaddrs *ifa);
+
+/*@
+ allocates *ifmap;
+ assigns \result, *ifmap \from \nothing; // missing: \from 'system interfaces'
+*/
+extern int getifmaddrs(struct ifmaddrs **ifmap);
+
+/*@
+ frees ifmp;
+ assigns \nothing;
+*/
+extern void freeifmaddrs(struct ifmaddrs *ifmp);
__END_DECLS
diff --git a/share/libc/locale.h b/share/libc/locale.h
index 4d5f79a8339..c5ad18e7f35 100644
--- a/share/libc/locale.h
+++ b/share/libc/locale.h
@@ -149,7 +149,11 @@ extern char *setlocale(int category, const char *locale);
*/
extern struct lconv *localeconv(void);
-extern locale_t duplocale(locale_t);
+/*@
+ allocates \result;
+ assigns *\result \from *locobj;
+ */
+extern locale_t duplocale(locale_t locobj);
extern void freelocale(locale_t);
extern locale_t newlocale(int, const char *, locale_t);
extern locale_t uselocale(locale_t);
diff --git a/share/libc/netdb.h b/share/libc/netdb.h
index 7a5457ec2b3..e726683764f 100644
--- a/share/libc/netdb.h
+++ b/share/libc/netdb.h
@@ -119,10 +119,32 @@ struct addrinfo
# define EAI_SYSTEM -11 /* System error returned in `errno'. */
# define EAI_OVERFLOW -12 /* Argument buffer overflow. */
+// dummy data, used for assigns clauses
+extern struct hostent __fc_dummy_hostent;
+extern struct netent __fc_dummy_netent;
+extern struct protoent __fc_dummy_protoent;
+extern struct servent __fc_dummy_servent;
+
+/*@
+ assigns __fc_dummy_hostent \from \nothing;
+*/
extern void endhostent(void);
+
+/*@
+ assigns __fc_dummy_netent \from \nothing;
+*/
extern void endnetent(void);
+
+/*@
+ assigns __fc_dummy_protoent \from \nothing;
+*/
extern void endprotoent(void);
+
+/*@
+ assigns __fc_dummy_servent \from \nothing;
+*/
extern void endservent(void);
+
/*@ requires addrinfo_valid: \valid(addrinfo);
frees addrinfo;
assigns \nothing;
@@ -178,32 +200,102 @@ extern int getaddrinfo(
const struct addrinfo *restrict hints,
struct addrinfo **restrict res);
-extern struct hostent *gethostbyaddr(const void *, socklen_t, int);
+/*@
+ assigns \result \from &__fc_dummy_hostent;
+ assigns *\result \from __fc_dummy_hostent, len, type;
+*/
+extern struct hostent *gethostbyaddr(const void *addr, socklen_t len, int type);
/*@
- allocates \result;
- assigns *\result \from name[0 .. strlen(name)], Frama_C_entropy_source;
- assigns Frama_C_entropy_source \from Frama_C_entropy_source;
+ assigns \result \from &__fc_dummy_hostent;
+ assigns *\result \from __fc_dummy_hostent, name[0..];
*/
extern struct hostent *gethostbyname(const char *name);
+/*@
+ assigns \result \from &__fc_dummy_hostent;
+*/
extern struct hostent *gethostent(void);
-extern int getnameinfo(const struct sockaddr *restrict, socklen_t,
- char *restrict, socklen_t, char *restrict,
- socklen_t, int);
-extern struct netent *getnetbyaddr(uint32_t, int);
-extern struct netent *getnetbyname(const char *);
+
+/*@
+ assigns \result, host[0..hostlen-1], serv[0..servlen-1]
+ \from ((char*)addr)[0..addrlen-1];
+*/
+extern int getnameinfo(const struct sockaddr *restrict addr, socklen_t addrlen,
+ char *restrict host, socklen_t hostlen,
+ char *restrict serv, socklen_t servlen,
+ int flags);
+
+/*@
+ assigns \result \from &__fc_dummy_netent;
+ assigns __fc_dummy_netent \from __fc_dummy_netent, net, type;
+*/
+extern struct netent *getnetbyaddr(uint32_t net, int type);
+
+/*@
+ assigns \result \from &__fc_dummy_netent;
+ assigns __fc_dummy_netent \from __fc_dummy_netent, name[0..];
+*/
+extern struct netent *getnetbyname(const char *name);
+
+/*@
+ assigns \result \from &__fc_dummy_netent;
+*/
extern struct netent *getnetent(void);
-extern struct protoent *getprotobyname(const char *);
-extern struct protoent *getprotobynumber(int);
+
+/*@
+ assigns \result \from &__fc_dummy_protoent;
+ assigns __fc_dummy_protoent \from __fc_dummy_protoent, name[0..];
+*/
+extern struct protoent *getprotobyname(const char *name);
+
+/*@
+ assigns \result \from &__fc_dummy_protoent;
+ assigns __fc_dummy_protoent \from __fc_dummy_protoent, proto;
+*/
+extern struct protoent *getprotobynumber(int proto);
+
+/*@
+ assigns \result \from &__fc_dummy_protoent;
+*/
extern struct protoent *getprotoent(void);
-extern struct servent *getservbyname(const char *, const char *);
-extern struct servent *getservbyport(int, const char *);
+
+/*@
+ assigns \result \from &__fc_dummy_servent;
+ assigns __fc_dummy_servent \from __fc_dummy_servent, name[0..], proto[0..];
+*/
+extern struct servent *getservbyname(const char *name, const char *proto);
+
+/*@
+ assigns \result \from &__fc_dummy_servent;
+ assigns __fc_dummy_servent \from __fc_dummy_servent, port, proto[0..];
+*/
+extern struct servent *getservbyport(int port, const char *proto);
+
+/*@
+ assigns \result \from &__fc_dummy_servent;
+*/
extern struct servent *getservent(void);
-extern void sethostent(int);
-extern void setnetent(int);
-extern void setprotoent(int);
-extern void setservent(int);
+
+/*@
+ assigns __fc_dummy_hostent \from indirect:stayopen;
+*/
+extern void sethostent(int stayopen);
+
+/*@
+ assigns __fc_dummy_netent \from indirect:stayopen;
+*/
+extern void setnetent(int stayopen);
+
+/*@
+ assigns __fc_dummy_protoent \from indirect:stayopen;
+*/
+extern void setprotoent(int stayopen);
+
+/*@
+ assigns __fc_dummy_servent \from indirect:stayopen;
+*/
+extern void setservent(int stayopen);
__END_DECLS
diff --git a/share/libc/pthread.h b/share/libc/pthread.h
index 12bef61e469..4f3b40e01ba 100644
--- a/share/libc/pthread.h
+++ b/share/libc/pthread.h
@@ -132,43 +132,150 @@ enum __fc_pthread_mutex_pshared
#include "__fc_define_size_t.h"
#include "sched.h"
-extern int pthread_attr_destroy(pthread_attr_t *);
-extern int pthread_attr_getdetachstate(const pthread_attr_t *, int *);
-extern int pthread_attr_getguardsize(const pthread_attr_t *restrict,
- size_t *restrict);
-extern int pthread_attr_getinheritsched(const pthread_attr_t *restrict,
- int *restrict);
-extern int pthread_attr_getschedparam(const pthread_attr_t *restrict,
- struct sched_param *restrict);
-extern int pthread_attr_getschedpolicy(const pthread_attr_t *restrict,
- int *restrict);
-extern int pthread_attr_getscope(const pthread_attr_t *restrict,
- int *restrict);
-extern int pthread_attr_getstack(const pthread_attr_t *restrict,
- void **restrict, size_t *restrict);
-extern int pthread_attr_getstacksize(const pthread_attr_t *restrict,
- size_t *restrict);
-extern int pthread_attr_init(pthread_attr_t *);
-extern int pthread_attr_setdetachstate(pthread_attr_t *, int);
-extern int pthread_attr_setguardsize(pthread_attr_t *, size_t);
-extern int pthread_attr_setinheritsched(pthread_attr_t *, int);
-extern int pthread_attr_setschedparam(pthread_attr_t *restrict,
- const struct sched_param *restrict);
-extern int pthread_attr_setschedpolicy(pthread_attr_t *, int);
-extern int pthread_attr_setscope(pthread_attr_t *, int);
-extern int pthread_attr_setstack(pthread_attr_t *, void *, size_t);
-extern int pthread_attr_setstacksize(pthread_attr_t *, size_t);
-extern int pthread_barrier_destroy(pthread_barrier_t *);
-extern int pthread_barrier_init(pthread_barrier_t *restrict,
- const pthread_barrierattr_t *restrict,
- unsigned);
-extern int pthread_barrier_wait(pthread_barrier_t *);
-extern int pthread_barrierattr_destroy(pthread_barrierattr_t *);
-extern int pthread_barrierattr_getpshared(const pthread_barrierattr_t *restrict,
- int *restrict);
-extern int pthread_barrierattr_init(pthread_barrierattr_t *);
-extern int pthread_barrierattr_setpshared(pthread_barrierattr_t *, int);
-extern int pthread_cancel(pthread_t);
+/*@
+ assigns \result, *attr \from *attr;
+*/
+extern int pthread_attr_destroy(pthread_attr_t *attr);
+
+/*@
+ assigns \result, *detachstate \from *attr;
+*/
+extern int pthread_attr_getdetachstate(const pthread_attr_t *attr,
+ int *detachstate);
+
+/*@
+ assigns \result, *guardsize \from *attr;
+*/
+extern int pthread_attr_getguardsize(const pthread_attr_t *restrict attr,
+ size_t *restrict guardsize);
+
+/*@
+ assigns \result, *inheritsched \from *attr;
+*/
+extern int pthread_attr_getinheritsched(const pthread_attr_t *restrict attr,
+ int *restrict inheritsched);
+
+/*@
+ assigns \result, *schedparam \from *attr;
+*/
+extern int pthread_attr_getschedparam(const pthread_attr_t *restrict attr,
+ struct sched_param *restrict schedparam);
+
+/*@
+ assigns \result, *schedpolicy \from *attr;
+*/
+extern int pthread_attr_getschedpolicy(const pthread_attr_t *restrict attr,
+ int *restrict schedpolicy);
+
+/*@
+ assigns \result, *contentionscope \from *attr;
+*/
+extern int pthread_attr_getscope(const pthread_attr_t *restrict attr,
+ int *restrict contentionscope);
+
+/*@
+ assigns \result, *stackaddr, *stacksize \from *attr;
+*/
+extern int pthread_attr_getstack(const pthread_attr_t *restrict attr,
+ void **restrict stackaddr,
+ size_t *restrict stacksize);
+
+/*@
+ assigns \result, *stacksize \from *attr;
+*/
+extern int pthread_attr_getstacksize(const pthread_attr_t *restrict attr,
+ size_t *restrict stacksize);
+
+/*@
+ assigns \result, *attr \from \nothing;
+*/
+extern int pthread_attr_init(pthread_attr_t *attr);
+
+/*@
+ assigns \result, *attr \from detachstate;
+*/
+extern int pthread_attr_setdetachstate(pthread_attr_t *attr, int detachstate);
+
+/*@
+ assigns \result, *attr \from guardsize;
+*/
+extern int pthread_attr_setguardsize(pthread_attr_t *attr, size_t guardsize);
+
+/*@
+ assigns \result, *attr \from inheritsched;
+*/
+extern int pthread_attr_setinheritsched(pthread_attr_t *attr,
+ int inheritsched);
+
+/*@
+ assigns \result, *attr \from *attr, *schedparam;
+ */
+extern int pthread_attr_setschedparam(pthread_attr_t *restrict attr,
+ const struct sched_param *restrict schedparam);
+
+/*@
+ assigns \result, *attr \from schedpolicy;
+*/
+extern int pthread_attr_setschedpolicy(pthread_attr_t *attr, int schedpolicy);
+
+/*@
+ assigns \result, *attr \from contentionscope;
+*/
+extern int pthread_attr_setscope(pthread_attr_t *attr, int contentionscope);
+
+/*@
+ assigns \result, *attr \from stackaddr, stacksize;
+*/
+extern int pthread_attr_setstack(pthread_attr_t *attr, void *stackaddr,
+ size_t stacksize);
+
+/*@
+ assigns \result, *attr \from stacksize;
+*/
+extern int pthread_attr_setstacksize(pthread_attr_t *attr, size_t stacksize);
+
+/*@
+ assigns \result, *barrier \from *barrier;
+*/
+extern int pthread_barrier_destroy(pthread_barrier_t *barrier);
+
+/*@
+ assigns \result, *barrier \from *attr, count;
+*/
+extern int pthread_barrier_init(pthread_barrier_t *restrict barrier,
+ const pthread_barrierattr_t *restrict attr,
+ unsigned count);
+
+/*@
+ assigns \result, *barrier \from *barrier;
+*/
+extern int pthread_barrier_wait(pthread_barrier_t *barrier);
+
+/*@
+ assigns \result, *attr \from *attr;
+*/
+extern int pthread_barrierattr_destroy(pthread_barrierattr_t *attr);
+
+/*@
+ assigns \result, *pshared \from *attr;
+*/
+extern int pthread_barrierattr_getpshared(const pthread_barrierattr_t *restrict attr,
+ int *restrict pshared);
+
+/*@
+ assigns \result, *attr \from \nothing;
+*/
+extern int pthread_barrierattr_init(pthread_barrierattr_t *attr);
+
+/*@
+ assigns \result, *attr \from pshared;
+*/
+extern int pthread_barrierattr_setpshared(pthread_barrierattr_t *attr, int pshared);
+
+/*@
+ assigns \result \from thread;
+*/
+extern int pthread_cancel(pthread_t thread);
/*@ requires valid_cond: \valid(cond);
assigns \result \from \nothing;
@@ -196,10 +303,17 @@ extern int pthread_cond_destroy(pthread_cond_t * cond);
extern int pthread_cond_init(pthread_cond_t *restrict cond,
const pthread_condattr_t *restrict attr);
-extern int pthread_cond_signal(pthread_cond_t *);
-extern int pthread_cond_timedwait(pthread_cond_t *restrict,
- pthread_mutex_t *restrict,
- const struct timespec *restrict);
+/*@
+ assigns \result, *cond \from *cond;
+*/
+extern int pthread_cond_signal(pthread_cond_t *cond);
+
+/*@
+ assigns \result, *cond, *mutex \from *cond, *mutex, *abstime;
+*/
+extern int pthread_cond_timedwait(pthread_cond_t *restrict cond,
+ pthread_mutex_t *restrict mutex,
+ const struct timespec *restrict abstime);
/*@ requires valid_cond: \valid(cond);
requires valid_mutex: \valid(mutex);
assigns \result \from \nothing;
@@ -209,16 +323,34 @@ extern int pthread_cond_timedwait(pthread_cond_t *restrict,
*/
extern int pthread_cond_wait(pthread_cond_t *restrict cond,
pthread_mutex_t *restrict mutex);
-extern int pthread_condattr_destroy(pthread_condattr_t *);
+
+/*@
+ assigns \result, *attr \from *attr;
+*/
+extern int pthread_condattr_destroy(pthread_condattr_t *attr);
+
//clockid_t not available yet
//extern int pthread_condattr_getclock(const pthread_condattr_t *restrict,
-// clockid_t *restrict);
-extern int pthread_condattr_getpshared(const pthread_condattr_t *restrict,
- int *restrict);
-extern int pthread_condattr_init(pthread_condattr_t *);
+// clockid_t *restrict clock_id);
+
+/*@
+ assigns \result, *pshared \from *attr;
+*/
+extern int pthread_condattr_getpshared(const pthread_condattr_t *restrict attr,
+ int *restrict pshared);
+
+/*@
+ assigns \result, *attr \from \nothing;
+*/
+extern int pthread_condattr_init(pthread_condattr_t *attr);
+
//clockid_t not available yet
-//extern int pthread_condattr_setclock(pthread_condattr_t *, clockid_t);
-extern int pthread_condattr_setpshared(pthread_condattr_t *, int);
+//extern int pthread_condattr_setclock(pthread_condattr_t *attr, clockid_t clock_id);
+
+/*@
+ assigns \result, *attr \from pshared;
+*/
+extern int pthread_condattr_setpshared(pthread_condattr_t *attr, int pshared);
/*@ requires valid_thread: \valid(thread);
requires valid_null_attr: attr == \null || \valid_read(attr);
@@ -234,15 +366,41 @@ extern int pthread_create(pthread_t *restrict thread,
const pthread_attr_t *restrict attr,
void *(*start_routine)(void*),
void *restrict arg);
-extern int pthread_detach(pthread_t);
-extern int pthread_equal(pthread_t, pthread_t);
-extern void pthread_exit(void *);
+
+/*@
+ assigns \result \from thread;
+*/
+extern int pthread_detach(pthread_t thread);
+
+/*@
+ assigns \result \from indirect:t1, indirect:t2;
+*/
+extern int pthread_equal(pthread_t t1, pthread_t t2);
+
+/*@
+ assigns ((char*)value_ptr)[0..\block_length(value_ptr)-\offset(value_ptr)-1]
+ \from \nothing; //missing: \from 'current thread'
+*/
+extern void pthread_exit(void *value_ptr);
+
+/*@
+ assigns \result \from \nothing; //missing: \from 'current thread'
+*/
extern int pthread_getconcurrency(void);
+
//clockid_t not available yet
//extern int pthread_getcpuclockid(pthread_t, clockid_t *);
-extern int pthread_getschedparam(pthread_t, int *restrict,
- struct sched_param *restrict);
-extern void *pthread_getspecific(pthread_key_t);
+
+/*@
+ assigns \result, *policy, *param \from indirect:thread; //missing: \from 'thread data'
+*/
+extern int pthread_getschedparam(pthread_t thread, int *restrict policy,
+ struct sched_param *restrict param);
+
+/*@
+ assigns \result \from indirect:key; //missing: \from 'current thread'
+*/
+extern void *pthread_getspecific(pthread_key_t key);
/*@ requires valid_or_null_retval: retval == \null || \valid(retval);
assigns *retval \from thread;
@@ -262,9 +420,20 @@ extern void *pthread_getspecific(pthread_key_t);
*/
extern int pthread_join(pthread_t thread, void **retval);
-extern int pthread_key_create(pthread_key_t *, void (*)(void*));
-extern int pthread_key_delete(pthread_key_t);
-extern int pthread_mutex_consistent(pthread_mutex_t *);
+/*@
+ assigns \result, *key \from indirect:destruct; //missing: assigns 'current thread'
+*/
+extern int pthread_key_create(pthread_key_t *key, void (*destruct)(void*));
+
+/*@
+ assigns \result \from indirect:key; //missing: assigns 'current thread'
+*/
+extern int pthread_key_delete(pthread_key_t key);
+
+/*@
+ assigns \result, *mutex \from *mutex;
+*/
+extern int pthread_mutex_consistent(pthread_mutex_t *mutex);
/*@ requires mutex_valid: \valid(mutex);
assigns *mutex \from *mutex;
@@ -273,8 +442,11 @@ extern int pthread_mutex_consistent(pthread_mutex_t *);
*/
extern int pthread_mutex_destroy(pthread_mutex_t *mutex);
-extern int pthread_mutex_getprioceiling(const pthread_mutex_t *restrict,
- int *restrict);
+/*@
+ assigns \result, *mutex, *prioceiling \from *mutex;
+*/
+extern int pthread_mutex_getprioceiling(const pthread_mutex_t *restrict mutex,
+ int *restrict prioceiling);
/*@
requires mutex_valid: \valid(mutex);
requires attrs_valid_or_null: attrs == \null || \valid_read(attrs);
@@ -304,11 +476,25 @@ extern int pthread_mutex_init(pthread_mutex_t *restrict mutex,
// exported by our version of errno.h
*/
extern int pthread_mutex_lock(pthread_mutex_t * mutex);
-extern int pthread_mutex_setprioceiling(pthread_mutex_t *restrict, int,
- int *restrict);
-extern int pthread_mutex_timedlock(pthread_mutex_t *restrict,
- const struct timespec *restrict);
-extern int pthread_mutex_trylock(pthread_mutex_t *);
+
+/*@
+ assigns \result, *mutex, *old_ceiling \from *mutex, prioceiling;
+*/
+extern int pthread_mutex_setprioceiling(pthread_mutex_t *restrict mutex,
+ int prioceiling,
+ int *restrict old_ceiling);
+
+/*@
+ assigns \result, *mutex \from *mutex, *abstime;
+*/
+extern int pthread_mutex_timedlock(pthread_mutex_t *restrict mutex,
+ const struct timespec *restrict abstime);
+
+/*@
+ assigns \result, *mutex \from *mutex;
+*/
+extern int pthread_mutex_trylock(pthread_mutex_t *mutex);
+
/*@
requires mutex_valid: \valid(mutex);
assigns *mutex \from *mutex;
@@ -322,69 +508,216 @@ extern int pthread_mutex_unlock(pthread_mutex_t *mutex);
assigns *attr \from *attr;
assigns \result \from indirect:*attr;
ensures success_or_error: \result == 0 || \result == EINVAL;
- */
+*/
extern int pthread_mutexattr_destroy(pthread_mutexattr_t *attr);
-extern int pthread_mutexattr_getprioceiling(const pthread_mutexattr_t *restrict,
- int *restrict);
-extern int pthread_mutexattr_getprotocol(const pthread_mutexattr_t *restrict,
- int *restrict);
-extern int pthread_mutexattr_getpshared(const pthread_mutexattr_t *restrict,
- int *restrict);
-extern int pthread_mutexattr_getrobust(const pthread_mutexattr_t *restrict,
- int *restrict);
-extern int pthread_mutexattr_gettype(const pthread_mutexattr_t *restrict,
- int *restrict);
+/*@
+ assigns \result, *prioceiling \from *attr;
+*/
+extern int pthread_mutexattr_getprioceiling(const pthread_mutexattr_t *restrict attr,
+ int *restrict prioceiling);
+
+/*@
+ assigns \result, *protocol \from *attr;
+*/
+extern int pthread_mutexattr_getprotocol(const pthread_mutexattr_t *restrict attr,
+ int *restrict protocol);
+
+/*@
+ assigns \result, *pshared \from *attr;
+*/
+extern int pthread_mutexattr_getpshared(const pthread_mutexattr_t *restrict attr,
+ int *restrict pshared);
+
+/*@
+ assigns \result, *robust \from *attr;
+*/
+extern int pthread_mutexattr_getrobust(const pthread_mutexattr_t *restrict attr,
+ int *restrict robust);
+
+/*@
+ assigns \result, *type \from *attr;
+*/
+extern int pthread_mutexattr_gettype(const pthread_mutexattr_t *restrict attr,
+ int *restrict type);
/*@
requires valid_attr: \valid(attr);
assigns \result, *attr \from \nothing;
ensures success_or_error: \result == 0 || \result == ENOMEM;
- */
+*/
extern int pthread_mutexattr_init(pthread_mutexattr_t *attr);
-extern int pthread_mutexattr_setprioceiling(pthread_mutexattr_t *, int);
-extern int pthread_mutexattr_setprotocol(pthread_mutexattr_t *, int);
-extern int pthread_mutexattr_setpshared(pthread_mutexattr_t *, int);
-extern int pthread_mutexattr_setrobust(pthread_mutexattr_t *, int);
+/*@
+ assigns \result, *attr \from *attr, prioceiling;
+*/
+extern int pthread_mutexattr_setprioceiling(pthread_mutexattr_t *attr,
+ int prioceiling);
+
+/*@
+ assigns \result, *attr \from *attr, protocol;
+*/
+extern int pthread_mutexattr_setprotocol(pthread_mutexattr_t *attr,
+ int protocol);
+
+/*@
+ assigns \result, *attr \from *attr, pshared;
+*/
+extern int pthread_mutexattr_setpshared(pthread_mutexattr_t *attr,
+ int pshared);
+
+/*@
+ assigns \result, *attr \from *attr, robust;
+*/
+extern int pthread_mutexattr_setrobust(pthread_mutexattr_t *attr,
+ int robust);
/*@
requires valid_attr: \valid(attr);
assigns \result, *attr \from indirect:type;
ensures success_or_error: \result == 0 || \result == EINVAL;
- */
+*/
extern int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type);
-extern int pthread_once(pthread_once_t *, void (*)(void));
-extern int pthread_rwlock_destroy(pthread_rwlock_t *);
-extern int pthread_rwlock_init(pthread_rwlock_t *restrict,
- const pthread_rwlockattr_t *restrict);
-extern int pthread_rwlock_rdlock(pthread_rwlock_t *);
-extern int pthread_rwlock_timedrdlock(pthread_rwlock_t *restrict,
- const struct timespec *restrict);
-extern int pthread_rwlock_timedwrlock(pthread_rwlock_t *restrict,
- const struct timespec *restrict);
-extern int pthread_rwlock_tryrdlock(pthread_rwlock_t *);
-extern int pthread_rwlock_trywrlock(pthread_rwlock_t *);
-extern int pthread_rwlock_unlock(pthread_rwlock_t *);
-extern int pthread_rwlock_wrlock(pthread_rwlock_t *);
-extern int pthread_rwlockattr_destroy(pthread_rwlockattr_t *);
-extern int pthread_rwlockattr_getpshared(const pthread_rwlockattr_t *restrict,
- int *restrict);
-extern int pthread_rwlockattr_init(pthread_rwlockattr_t *);
-extern int pthread_rwlockattr_setpshared(pthread_rwlockattr_t *, int);
+/*@
+ assigns \result, *pthread_once \from *pthread_once, indirect:init_routine;
+*/
+extern int pthread_once(pthread_once_t *pthread_once,
+ void (*init_routine)(void));
+
+/*@
+ assigns \result, *rwlock \from *rwlock;
+*/
+extern int pthread_rwlock_destroy(pthread_rwlock_t *rwlock);
+
+/*@
+ assigns \result, *rwlock \from *attr;
+*/
+extern int pthread_rwlock_init(pthread_rwlock_t *restrict rwlock,
+ const pthread_rwlockattr_t *restrict attr);
+
+/*@
+ assigns \result, *rwlock \from *rwlock;
+*/
+extern int pthread_rwlock_rdlock(pthread_rwlock_t *rwlock);
+
+/*@
+ assigns \result, *rwlock \from *rwlock, *abstime;
+*/
+extern int pthread_rwlock_timedrdlock(pthread_rwlock_t *restrict rwlock,
+ const struct timespec *restrict abstime);
+
+/*@
+ assigns \result, *rwlock \from *rwlock, *abstime;
+*/
+extern int pthread_rwlock_timedwrlock(pthread_rwlock_t *restrict rwlock,
+ const struct timespec *restrict abstime);
+
+/*@
+ assigns \result, *rwlock \from *rwlock;
+*/
+extern int pthread_rwlock_tryrdlock(pthread_rwlock_t *rwlock);
+
+/*@
+ assigns \result, *rwlock \from *rwlock;
+*/
+extern int pthread_rwlock_trywrlock(pthread_rwlock_t *rwlock);
+
+/*@
+ assigns \result, *rwlock \from *rwlock;
+*/
+extern int pthread_rwlock_unlock(pthread_rwlock_t *rwlock);
+
+/*@
+ assigns \result, *rwlock \from *rwlock;
+*/
+extern int pthread_rwlock_wrlock(pthread_rwlock_t *rwlock);
+
+/*@
+ assigns \result, *attr \from *attr;
+*/
+extern int pthread_rwlockattr_destroy(pthread_rwlockattr_t *attr);
+
+/*@
+ assigns \result, *pshared \from *attr;
+*/
+extern int pthread_rwlockattr_getpshared(const pthread_rwlockattr_t *restrict attr,
+ int *restrict pshared);
+
+/*@
+ assigns \result, *attr \from \nothing;
+*/
+extern int pthread_rwlockattr_init(pthread_rwlockattr_t *attr);
+
+/*@
+ assigns \result, *attr \from *attr, pshared;
+*/
+extern int pthread_rwlockattr_setpshared(pthread_rwlockattr_t *attr, int pshared);
+
+/*@
+ assigns \result \from \nothing; //missing: \from 'current thread'
+*/
extern pthread_t pthread_self(void);
-extern int pthread_setcancelstate(int, int *);
-extern int pthread_setcanceltype(int, int *);
-extern int pthread_setconcurrency(int);
-extern int pthread_setschedparam(pthread_t, int, const struct sched_param *);
-extern int pthread_setschedprio(pthread_t, int);
-extern int pthread_setspecific(pthread_key_t, const void *);
-extern int pthread_spin_destroy(pthread_spinlock_t *);
-extern int pthread_spin_init(pthread_spinlock_t *, int);
-extern int pthread_spin_lock(pthread_spinlock_t *);
-extern int pthread_spin_trylock(pthread_spinlock_t *);
-extern int pthread_spin_unlock(pthread_spinlock_t *);
+
+/*@
+ assigns \result, *oldstate \from state; //missing: \from 'current thread'
+*/
+extern int pthread_setcancelstate(int state, int *oldstate);
+
+/*@
+ assigns \result, *oldtype \from type; //missing: \from 'current thread'
+*/
+extern int pthread_setcanceltype(int type, int *oldtype);
+
+/*@
+ assigns \result \from indirect:new_level; //missing: assigns 'current thread'
+*/
+extern int pthread_setconcurrency(int new_level);
+
+/*@
+ assigns \result \from indirect:thread, indirect:policy, indirect:*param; //missing: assigns 'current thread'
+*/
+extern int pthread_setschedparam(pthread_t thread, int policy,
+ const struct sched_param *param);
+
+/*@
+ assigns \result \from indirect:thread, indirect:prio; //missing: assigns 'current thread'
+*/
+extern int pthread_setschedprio(pthread_t thread, int prio);
+
+/*@
+ assigns \result \from indirect:key, indirect:value; //missing: assigns 'current thread data'
+*/
+extern int pthread_setspecific(pthread_key_t key, const void *value);
+
+/*@
+ assigns \result, *lock \from *lock;
+*/
+extern int pthread_spin_destroy(pthread_spinlock_t *lock);
+
+/*@
+ assigns \result, *lock \from pshared;
+*/
+extern int pthread_spin_init(pthread_spinlock_t *lock, int pshared);
+
+/*@
+ assigns \result, *lock \from *lock;
+*/
+extern int pthread_spin_lock(pthread_spinlock_t *lock);
+
+/*@
+ assigns \result, *lock \from *lock;
+*/
+extern int pthread_spin_trylock(pthread_spinlock_t *lock);
+
+/*@
+ assigns \result, *lock \from *lock;
+*/
+extern int pthread_spin_unlock(pthread_spinlock_t *lock);
+
+/*@
+ assigns \nothing; //missing: assigns 'current thread'
+*/
extern void pthread_testcancel(void);
// GNU extensions
diff --git a/share/libc/pwd.h b/share/libc/pwd.h
index 101e35e3df1..e3dcb358014 100644
--- a/share/libc/pwd.h
+++ b/share/libc/pwd.h
@@ -113,8 +113,23 @@ extern int getpwnam_r(const char *name, struct passwd *pwd,
extern int getpwuid_r(uid_t uid, struct passwd *pwd,
char *buf, size_t buflen, struct passwd **result);
+// Represents the user database and its current entry
+struct passwd __fc_pwent;
+
+/*@
+ assigns __fc_pwent \from __fc_pwent;
+*/
extern void endpwent(void);
+
+/*@
+ assigns __fc_pwent \from __fc_pwent;
+ assigns \result \from &__fc_pwent;
+*/
extern struct passwd *getpwent(void);
+
+/*@
+ assigns __fc_pwent \from __fc_pwent;
+*/
extern void setpwent(void);
__END_DECLS
diff --git a/share/libc/semaphore.h b/share/libc/semaphore.h
index bae1236fcf3..5ad03082ad2 100644
--- a/share/libc/semaphore.h
+++ b/share/libc/semaphore.h
@@ -36,16 +36,58 @@ typedef union __fc_sem_t {
#define SEM_FAILED ((sem_t *) 0)
-extern int sem_close(sem_t *);
-extern int sem_destroy(sem_t *);
-extern int sem_getvalue(sem_t *restrict, int *restrict);
-extern int sem_init(sem_t *, int, unsigned);
-extern sem_t *sem_open(const char *, int, ...);
-extern int sem_post(sem_t *);
-extern int sem_timedwait(sem_t *restrict, const struct timespec *restrict);
-extern int sem_trywait(sem_t *);
-extern int sem_unlink(const char *);
-extern int sem_wait(sem_t *);
+/*@
+ frees sem;
+ assigns \result \from *sem;
+*/
+extern int sem_close(sem_t *sem);
+
+/*@
+ assigns \result, *sem \from *sem;
+*/
+extern int sem_destroy(sem_t *sem);
+
+/*@
+ assigns \result, *sval \from *sem;
+*/
+extern int sem_getvalue(sem_t *restrict sem, int *restrict sval);
+
+/*@
+ assigns \result, *sem \from *sem, pshared, value;
+*/
+extern int sem_init(sem_t *sem, int pshared, unsigned value);
+
+/*@
+ allocates \result;
+ assigns \result \from indirect:name[0..], oflag; //missing: \from variadic args
+*/
+extern sem_t *sem_open(const char *name, int oflag, ...);
+
+/*@
+ assigns \result, *sem \from *sem;
+*/
+extern int sem_post(sem_t *sem);
+
+/*@
+ assigns \result, *sem \from *sem, *abstime;
+*/
+extern int sem_timedwait(sem_t *restrict sem,
+ const struct timespec *restrict abstime);
+
+/*@
+ assigns \result, *sem \from *sem;
+*/
+extern int sem_trywait(sem_t *sem);
+
+/*@
+ assigns \result \from indirect:name[0..]; //missing: assigns 'named semaphore'
+*/
+extern int sem_unlink(const char *name);
+
+/*@
+ assigns \result, *sem \from *sem;
+*/
+extern int sem_wait(sem_t *sem);
__END_DECLS
__POP_FC_STDLIB
diff --git a/share/libc/signal.h b/share/libc/signal.h
index 94848b2e723..082f1e39dae 100644
--- a/share/libc/signal.h
+++ b/share/libc/signal.h
@@ -47,8 +47,13 @@ typedef void (*__fc_sighandler_t) (int);
/* for BSD 4.4 */
typedef __fc_sighandler_t sig_t;
+/*@ assigns \nothing; */
extern void __fc_sig_dfl(int);
+
+/*@ assigns \nothing; */
extern void __fc_sig_ign(int);
+
+/*@ assigns \nothing; */
extern void __fc_sig_err(int);
#define SIG_DFL (&__fc_sig_dfl) /* default signal handling */
diff --git a/share/libc/spawn.h b/share/libc/spawn.h
index 6dae29babee..51b21aa891d 100644
--- a/share/libc/spawn.h
+++ b/share/libc/spawn.h
@@ -46,73 +46,147 @@ typedef struct __fc_posix_posix_spawn_file_actions_t {
#define POSIX_SPAWN_SETSIGDEF 0x04
#define POSIX_SPAWN_SETSIGMASK 0x08
+/*@
+ assigns *pid, \result \from
+ indirect:path[0..],
+ indirect:*file_actions,
+ indirect:*attrp,
+ indirect:*argv[0..],
+ indirect:*envp[0..];
+*/
extern int posix_spawn(pid_t *restrict pid, const char *restrict path,
const posix_spawn_file_actions_t *file_actions,
const posix_spawnattr_t *restrict attrp,
char *const *restrict argv,
char *const *restrict envp);
+/*@
+ assigns \result, *file_actions \from fildes;
+*/
extern int posix_spawn_file_actions_addclose(posix_spawn_file_actions_t
*file_actions,
int fildes);
+/*@
+ assigns \result, *file_actions \from fildes, newfildes;
+*/
extern int posix_spawn_file_actions_adddup2(posix_spawn_file_actions_t
*file_actions,
int fildes, int newfildes);
+/*@
+ assigns \result, *file_actions
+ \from fildes, path[0..], oflag, mode;
+*/
extern int posix_spawn_file_actions_addopen(posix_spawn_file_actions_t
*restrict file_actions,
int fildes,
const char *restrict path,
int oflag, mode_t mode);
+/*@
+ assigns \result, *file_actions \from \nothing; // missing: \from 'filesystem'
+*/
extern int posix_spawn_file_actions_destroy(posix_spawn_file_actions_t
*file_actions);
+/*@
+ assigns \result, *file_actions \from \nothing; // missing: \from 'filesystem'
+*/
extern int posix_spawn_file_actions_init(posix_spawn_file_actions_t
*file_actions);
+/*@
+ assigns \result, *attr \from \nothing;
+*/
extern int posix_spawnattr_destroy(posix_spawnattr_t *attr);
+/*@
+ assigns \result, *flags \from *attr;
+*/
extern int posix_spawnattr_getflags(const posix_spawnattr_t *restrict attr,
short *restrict flags);
+/*@
+ assigns \result, *pgroup \from *attr;
+*/
extern int posix_spawnattr_getpgroup(const posix_spawnattr_t *restrict attr,
pid_t *restrict pgroup);
+/*@
+ assigns \result, *schedparam \from *attr;
+*/
extern int posix_spawnattr_getschedparam(const posix_spawnattr_t *restrict attr,
struct sched_param *restrict
schedparam);
+/*@
+ assigns \result, *schedpolicy \from *attr;
+*/
extern int posix_spawnattr_getschedpolicy(const posix_spawnattr_t *restrict
attr,
int *restrict schedpolicy);
+/*@
+ assigns \result, *sigdefault \from *attr;
+*/
extern int posix_spawnattr_getsigdefault(const posix_spawnattr_t *restrict attr,
sigset_t *restrict sigdefault);
+/*@
+ assigns \result, *sigmask \from *attr;
+*/
extern int posix_spawnattr_getsigmask(const posix_spawnattr_t *restrict attr,
- sigset_t *restrict);
+ sigset_t *restrict sigmask);
+/*@
+ assigns \result, *attr \from \nothing;
+*/
extern int posix_spawnattr_init(posix_spawnattr_t *attr);
+/*@
+ assigns \result, *attr \from flags;
+*/
extern int posix_spawnattr_setflags(posix_spawnattr_t *attr, short flags);
+/*@
+ assigns \result, *attr \from pgroup;
+*/
extern int posix_spawnattr_setpgroup(posix_spawnattr_t *attr, pid_t pgroup);
+/*@
+ assigns \result, *attr \from *schedparam;
+*/
extern int posix_spawnattr_setschedparam(posix_spawnattr_t *restrict attr,
const struct sched_param *restrict
schedparam);
+/*@
+ assigns \result, *attr \from schedpolicy;
+*/
extern int posix_spawnattr_setschedpolicy(posix_spawnattr_t *attr,
int schedpolicy);
+/*@
+ assigns \result, *attr \from *sigdefault;
+*/
extern int posix_spawnattr_setsigdefault(posix_spawnattr_t *restrict attr,
const sigset_t *restrict sigdefault);
+/*@
+ assigns \result, *attr \from *sigmask;
+*/
extern int posix_spawnattr_setsigmask(posix_spawnattr_t *restrict attr,
const sigset_t *restrict sigmask);
+/*@
+ assigns *pid, \result \from
+ indirect:file[0..], //missing: '\from PWD'
+ indirect:*file_actions,
+ indirect:*attrp,
+ indirect:*argv[0..],
+ indirect:*envp[0..];
+*/
extern int posix_spawnp(pid_t *restrict pid, const char *restrict file,
const posix_spawn_file_actions_t *file_actions,
const posix_spawnattr_t *restrict attrp,
diff --git a/share/libc/strings.h b/share/libc/strings.h
index 0bc801348bb..ee25b389858 100644
--- a/share/libc/strings.h
+++ b/share/libc/strings.h
@@ -29,32 +29,52 @@ __PUSH_FC_STDLIB
__BEGIN_DECLS
-extern int bcmp(const void *, const void *, size_t);
-extern void bcopy(const void *, void *, size_t);
+/*@
+ assigns \result \from indirect:((char*)s1)[0 .. n-1],
+ indirect:((char*)s2)[0 .. n-1];
+*/
+extern int bcmp(const void *s1, const void *s2, size_t n);
+
+/*@
+ assigns ((char*)dest)[0 .. n-1] \from ((char*)src)[0 .. n-1], indirect:n;
+*/
+extern void bcopy(const void *src, void *dest, size_t n);
/*@ requires valid_memory_area: \valid (((char*) s)+(0 .. n-1));
assigns ((char*) s)[0 .. n-1] \from \nothing;
ensures s_initialized:initialization:\initialized(((char*) s)+(0 .. n-1));
ensures zero_initialized: \subset(((char*) s)[0 .. n-1], {0}); */
-extern void bzero(void *s, size_t n);
-extern int ffs(int);
-extern char *index(const char *, int);
-extern char *rindex(const char *, int);
+extern void bzero(void *s, size_t n);
+
+/*@
+ assigns \result \from i;
+*/
+extern int ffs(int i);
+
+/*@
+ assigns \result \from s, indirect:s[0 .. strlen(s)], indirect:c;
+*/
+extern char *index(const char *s, int c);
+
+/*@
+ assigns \result \from s, indirect:s[0 .. strlen(s)], indirect:c;
+*/
+extern char *rindex(const char *s, int c);
/*@
requires valid_string_s1: valid_read_string(s1);
requires valid_string_s2: valid_read_string(s2);
assigns \result \from indirect:s1[0..], indirect:s2[0..];
*/
-extern int strcasecmp(const char *s1, const char *s2);
+extern int strcasecmp(const char *s1, const char *s2);
/*@
requires valid_string_s1: valid_read_nstring(s1, n);
requires valid_string_s2: valid_read_nstring(s2, n);
assigns \result \from indirect:n, indirect:s1[0..n-1], indirect:s2[0..n-1];
*/
-extern int strncasecmp(const char *s1, const char *s2, size_t n);
+extern int strncasecmp(const char *s1, const char *s2, size_t n);
__END_DECLS
diff --git a/share/libc/utmp.h b/share/libc/utmp.h
index 388073413a2..3f7894f0e62 100644
--- a/share/libc/utmp.h
+++ b/share/libc/utmp.h
@@ -28,22 +28,12 @@
__PUSH_FC_STDLIB
#include "__fc_define_pid_t.h"
+#include "__fc_utmp_constants.h"
#include "sys/time.h"
#include "stdint.h"
__BEGIN_DECLS
-#define _PATH_UTMP "/var/run/utmp"
-#define UTMP_FILE _PATH_UTMP
-#define UTMP_FILENAME _PATH_UTMP
-#define _PATH_WTMP "/var/log/wtmp"
-#define WTMP_FILE _PATH_WTMP
-#define WTMP_FILENAME _PATH_WTMP
-
-#define UT_LINESIZE 32
-#define UT_NAMESIZE 32
-#define UT_HOSTSIZE 256
-
struct lastlog
{
time_t ll_time;
@@ -72,36 +62,96 @@ struct utmp
char __glibc_reserved[20]; // used by who.c
};
-#define ut_name ut_user
-#define ut_time ut_tv.tv_sec
-
+/*@
+ assigns \result, __fc_fopen[fd] \from __fc_fopen[fd], fd;
+*/
extern int login_tty (int fd);
-extern void login (const struct utmp *entry);
+
+// static storage used by some getter functions
+extern struct utmp __fc_get;
+
+/*@
+ assigns __fc_utmp \from __fc_utmp, *ut;
+ assigns __fc_wtmp \from __fc_wtmp, *ut;
+*/
+extern void login (const struct utmp *ut);
+
+/*@
+ assigns __fc_utmp \from __fc_wtmp, *ut_line;
+ assigns \result \from indirect:__fc_wtmp, indirect:*ut_line;
+*/
extern int logout (const char *ut_line);
+
+/*@
+ assigns __fc_wtmp \from __fc_wtmp, ut_line[0..], ut_name[0..], ut_host[0..];
+*/
extern void logwtmp (const char *ut_line, const char *ut_name,
const char *ut_host);
+/*@
+ assigns \nothing; // missing: assigns 'file named wtmp_file in the filesystem' \from *utmp;
+*/
extern void updwtmp (const char *wtmp_file, const struct utmp *utmp);
+/*@
+ assigns \result \from file[0..]; // missing: assigns 'file named file in the filesystem';
+*/
extern int utmpname (const char *file);
+/*@
+ assigns \result \from &__fc_get, indirect:__fc_utmp;
+ assigns __fc_get \from __fc_get, indirect:__fc_utmp;
+*/
extern struct utmp *getutent (void);
+/*@
+ assigns __fc_utmp \from __fc_utmp;
+*/
extern void setutent (void);
+/*@
+ assigns __fc_utmp \from __fc_utmp;
+*/
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;
+*/
extern struct utmp *getutid (const struct utmp *id);
+/*@
+ assigns \result \from &__fc_get, indirect:__fc_utmp, indirect:*line;
+ assigns __fc_get \from __fc_get, indirect:__fc_utmp, indirect:*line;
+*/
extern struct utmp *getutline (const struct utmp *line);
+/*@
+ assigns __fc_utmp \from __fc_utmp, *utmp_ptr;
+ assigns \result \from utmp_ptr;
+*/
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;
+*/
extern int getutent_r (struct utmp *buffer, struct utmp **result);
+/*@
+ assigns \result \from indirect:*id, indirect:__fc_utmp;
+ assigns *buffer \from indirect:*id, __fc_utmp;
+ assigns *result \from indirect:*id, &__fc_utmp;
+*/
extern int getutid_r (const struct utmp *id, struct utmp *buffer,
struct utmp **result);
+/*@
+ assigns \result \from indirect:*line, indirect:__fc_utmp;
+ assigns *buffer \from indirect:*line, __fc_utmp;
+ assigns *result \from indirect:*line, &__fc_utmp;
+*/
extern int getutline_r (const struct utmp *line,
struct utmp *buffer, struct utmp **result);
diff --git a/share/libc/utmpx.h b/share/libc/utmpx.h
index 876076f94c2..0fd2bc7817b 100644
--- a/share/libc/utmpx.h
+++ b/share/libc/utmpx.h
@@ -26,6 +26,7 @@
__PUSH_FC_STDLIB
#include "__fc_define_pid_t.h"
+#include "__fc_utmp_constants.h"
#include "stdint.h"
#include "sys/time.h"
@@ -46,21 +47,42 @@ struct utmpx {
char __glibc_reserved[20]; // not POSIX, but allowed by it
};
-#define EMPTY 0
-#define BOOT_TIME 2
-#define OLD_TIME 4
-#define NEW_TIME 3
-#define USER_PROCESS 7
-#define INIT_PROCESS 5
-#define LOGIN_PROCESS 6
-#define DEAD_PROCESS 8
+// static storage used by some getter functions
+extern struct utmpx __fc_getx;
-extern void endutxent(void);
-extern struct utmpx *getutxent(void);
-extern struct utmpx *getutxid(const struct utmpx *);
-extern struct utmpx *getutxline(const struct utmpx *);
-extern struct utmpx *pututxline(const struct utmpx *);
-extern void setutxent(void);
+/*@
+ assigns \result \from &__fc_getx, indirect:__fc_utmp;
+ assigns __fc_getx \from __fc_getx, indirect:__fc_utmp;
+*/
+extern struct utmpx *getutxent (void);
+
+/*@
+ assigns __fc_utmp \from __fc_utmp;
+*/
+extern void setutxent (void);
+
+/*@
+ assigns __fc_utmp \from __fc_utmp;
+*/
+extern void endutxent (void);
+
+/*@
+ assigns \result \from &__fc_getx, indirect:__fc_utmp, indirect:*id;
+ assigns __fc_getx \from __fc_getx, indirect:__fc_utmp, indirect:*id;
+*/
+extern struct utmpx *getutxid (const struct utmpx *id);
+
+/*@
+ assigns \result \from &__fc_getx, indirect:__fc_utmp, indirect:*line;
+ assigns __fc_getx \from __fc_getx, indirect:__fc_utmp, indirect:*line;
+*/
+extern struct utmpx *getutxline (const struct utmpx *line);
+
+/*@
+ assigns __fc_utmp \from __fc_utmp, *utmp_ptr;
+ assigns \result \from utmp_ptr;
+*/
+extern struct utmpx *pututxline (const struct utmpx *utmp_ptr);
__END_DECLS
__POP_FC_STDLIB
diff --git a/tests/libc/fc_libc.c b/tests/libc/fc_libc.c
index 4d4ec0cf07d..30692f59a93 100644
--- a/tests/libc/fc_libc.c
+++ b/tests/libc/fc_libc.c
@@ -97,6 +97,7 @@
#include "fcntl.h"
#include "__fc_select.h"
#include "__fc_string_axiomatic.h"
+#include "__fc_utmp_constants.h"
#include "features.h"
#include "fenv.h"
#include "float.h"
--
GitLab