[libc] add assigns for several functions

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;

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++) {

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,

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)

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) {}

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
 

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) {

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');