diff --git a/share/libc/argz.c b/share/libc/argz.c
index 61da9d43f1b6a48fc37cf45250a3f2ecf5c58bfc..fdf81545c9a8136127b9ea21e3584b963a0552d3 100644
--- a/share/libc/argz.c
+++ b/share/libc/argz.c
@@ -43,6 +43,7 @@ void argz_stringify (char *argz, size_t len, int sep) {
     }
 }
 
+/*@ assigns *to, *to_len \from buf[0 .. buf_len - 1]; */
 static void str_append (char **to, size_t *to_len, const char *buf,
                         const size_t buf_len) {
   size_t new_len = *to_len + buf_len;
diff --git a/share/libc/netdb.c b/share/libc/netdb.c
index 536053ca7680fac1289c5768b7d3ad6d237effdd..88682b5f91582b7c8fabf8fed66f6c3f3d93e3b8 100644
--- a/share/libc/netdb.c
+++ b/share/libc/netdb.c
@@ -93,6 +93,10 @@ struct __fc_gethostbyname {
 
 struct __fc_gethostbyname __fc_ghbn;
 
+/*@
+  assigns answer[0 .. anslen-1], \result
+    \from indirect:anslen, Frama_C_entropy_source;
+*/
 static int res_search(const char *dname, int rec_class, int type,
                char *answer, int anslen) {
   for (int i = 0; i < anslen-1; i++) {
diff --git a/share/libc/netdb.h b/share/libc/netdb.h
index a97dc179618b5d0e4bf962ddadbde6e728fedffa..412d06331a48163b7bc1c78fa9d7b4ef401fa49b 100644
--- a/share/libc/netdb.h
+++ b/share/libc/netdb.h
@@ -178,7 +178,12 @@ extern int getaddrinfo(
   struct addrinfo **restrict res);
 
 extern struct hostent *gethostbyaddr(const void *, socklen_t, int);
-extern struct hostent *gethostbyname(const char *);
+
+/*@
+  assigns \result, *\result \from name[0 .. strlen(name)];
+*/
+extern struct hostent *gethostbyname(const char *name);
+
 extern struct hostent *gethostent(void);
 extern int getnameinfo(const struct sockaddr *restrict, socklen_t,
  char *restrict, socklen_t, char *restrict,
diff --git a/share/libc/pwd.c b/share/libc/pwd.c
index 85cc012618cb9d449709aa82061292271ca727e0..92dcae6e47104ca72f11ac636a7a8af8fd9a83b0 100644
--- a/share/libc/pwd.c
+++ b/share/libc/pwd.c
@@ -48,6 +48,11 @@ static int __fc_getpw_init; // used to initialize the __fc_getpw* strings
   remaining -= len
 
 // Common code between getpwman_r and getpwuid_r
+/*@ assigns __fc_getpw_init, __fc_getpw_pw_name[0..63],
+            __fc_getpw_pw_passwd[0..63], __fc_getpw_pw_gecos[0..63],
+            __fc_getpw_pw_dir[0..63], __fc_getpw_pw_shell[0..63],
+            buf[0 .. buflen-1], *pwd, *result, \result
+      \from __fc_pwd; */
 static int __fc_getpw_r(struct passwd *pwd, char *buf,
                         size_t buflen, struct passwd **result) {
   // initialize global strings (only during first execution)
diff --git a/share/libc/stdatomic.c b/share/libc/stdatomic.c
index 28723c038b582e998df80c4dd33c57593dd745a6..30c975051b9451942b3d43b252c7d9a91f6f6174 100644
--- a/share/libc/stdatomic.c
+++ b/share/libc/stdatomic.c
@@ -26,6 +26,7 @@
 #include "string.h"
 __PUSH_FC_STDLIB
 
+/*@ assigns \nothing; */
 void __fc_atomic_init_marker(void *obj, unsigned long long value) {}
 
 void atomic_thread_fence(memory_order order) {}
diff --git a/share/libc/stdio.h b/share/libc/stdio.h
index 3b614812403ad6a3a39d9b5df548639cc6e8c4fc..0e82d078e0afb5771ac3c8fb814937f0bc0a122a 100644
--- a/share/libc/stdio.h
+++ b/share/libc/stdio.h
@@ -581,7 +581,7 @@ extern int pclose(FILE *stream);
 // This file may be included by non-POSIX machdeps, which do not define
 // ssize_t, so we must check it
 #ifdef __FC_POSIX_VERSION
-// No specification given; include "stdio.c" to use Frama-C's implementation
+/*@ assigns (*lineptr)[0 .. *n-1], *n, *stream, \result \from *stream; */
 ssize_t getline(char **lineptr, size_t *n, FILE *stream);
 #endif
 
diff --git a/share/libc/stdlib.c b/share/libc/stdlib.c
index 3eed8b8186295c65b44007a98fb9f968c4f611bf..ca6863450b7abe4d018ec8168fb6e8b033262ef4 100644
--- a/share/libc/stdlib.c
+++ b/share/libc/stdlib.c
@@ -80,6 +80,10 @@ char *__fc_env[ARG_MAX];
 #define __FC_INITENV_LEN 64
 static char __fc_env_strings[__FC_INITENV_LEN];
 
+/*@
+  assigns __fc_env_strings[0 .. __FC_INITENV_LEN-1], __fc_env[0 .. ARG_MAX - 1]
+    \from Frama_C_entropy_source;
+*/
 static void __fc_initenv() {
   static char init;
   if (!init) {
diff --git a/share/libc/string.c b/share/libc/string.c
index 1ab5d995df54441c322148db3a62d93206098c28..d546b236ceaf813e8204eb1f833a6d5a7a21a596 100644
--- a/share/libc/string.c
+++ b/share/libc/string.c
@@ -172,6 +172,9 @@ int memcmp(const void *s1, const void *s2, size_t n)
 
 // NOTE: strcasecmp is in POSIX's strings.h but not in C99
 // auxiliary function for strcasecmp
+/*@
+  assigns \result \from c1, c2;
+*/
 static int char_equal_ignore_case(char c1, char c2)
 {
   if (c1 >= 'A' && c1 <= 'Z') c1 -= ('A' - 'a');