[libc] fixes and test oracle updates after review

share/libc/netdb.h

@@ -28,6 +28,7 @@ __PUSH_FC_STDLIB
 #include "netinet/in.h"
 #include "sys/socket.h"
 #include "inttypes.h"
+#include "__fc_builtin.h"
 #include "__fc_string_axiomatic.h"
 
 __BEGIN_DECLS
@@ -181,7 +182,8 @@ extern struct hostent *gethostbyaddr(const void *, socklen_t, int);
 
 /*@
   allocates \result;
-  assigns *\result \from name[0 .. strlen(name)];
+  assigns *\result \from name[0 .. strlen(name)], Frama_C_entropy_source;
+  assigns Frama_C_entropy_source \from Frama_C_entropy_source;
 */
 extern struct hostent *gethostbyname(const char *name);
 

share/libc/stdatomic.h

@@ -119,7 +119,7 @@ extern void atomic_thread_fence(memory_order order);
 extern void atomic_signal_fence(memory_order order);
 
 /*@
-  assigns \result \from indirect:((char*)obj)[0 .. obj_size-1];
+  assigns \result \from indirect:obj, indirect:obj_size; // in reality, should be '\from typeof(obj)'
 */
 _Bool __fc_atomic_is_lock_free(void *obj, size_t obj_size);
 #define atomic_is_lock_free(obj) __fc_atomic_is_lock_free(obj, sizeof(obj))

tests/libc/oracle/fc_libc.1.res.oracle

@@ -5254,8 +5254,10 @@ static int res_search(char const *dname, int rec_class, int type,
   return tmp;
 }
 
-/*@ assigns *\result;
-    assigns *\result \from *(name + (0 .. strlen{Old}(name)));
+/*@ assigns *\result, Frama_C_entropy_source;
+    assigns *\result
+      \from *(name + (0 .. strlen{Old}(name))), Frama_C_entropy_source;
+    assigns Frama_C_entropy_source \from Frama_C_entropy_source;
     allocates \result;
  */
 struct hostent *gethostbyname(char const *name)
@@ -6314,7 +6316,7 @@ void atomic_signal_fence(memory_order order)
 }
 
 /*@ assigns \result;
-    assigns \result \from (indirect: *((char *)obj + (0 .. obj_size - 1)));
+    assigns \result \from (indirect: obj), (indirect: obj_size);
  */
 _Bool __fc_atomic_is_lock_free(void *obj, size_t obj_size)
 {

tests/libc/oracle/netdb_c.res.oracle

@@ -52,12 +52,12 @@
   \return(inet_addr) == 4294967295 (auto)
   \return(inet_ntoa) == 0 (auto)
   \return(inet_ntop) == 0 (auto)
-  \return(gai_strerror) == 0 (auto)
-  \return(getaddrinfo) == 0 (auto)
-  \return(gethostbyname) == 0 (auto)
   \return(Frama_C_nondet) == 0 (auto)
   \return(Frama_C_nondet_ptr) == 0 (auto)
   \return(Frama_C_malloc_fresh) == 0 (auto)
+  \return(gai_strerror) == 0 (auto)
+  \return(getaddrinfo) == 0 (auto)
+  \return(gethostbyname) == 0 (auto)
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed

tests/libc/string_c.c

@@ -125,15 +125,14 @@ void test_strcat(void)
   //@assert p == s;
   //@assert s[0] == 'h' && s[4] == 'o' && s[5] == 0;
   s[4] = 0;
-  s[5] = 'h';
-  s[6] = 'e';
   s[7] = 'l';
-  s[8] = 0;
-  strcat(s, s+5);
-  //@assert s[3] == 'l' && s[4] == 'h' && s[6] == 'l' && s[7] == 0;
+  s[8] = 'o';
+  s[9] = 0;
+  strcat(s, s+7);
+  //@assert s[3] == 'l' && s[4] == 'l' && s[5] == 'o' && s[6] == 0;
   strcat(s, "");
   strcat(s, "x");
-  //@assert s[7] == 'x' && s[8] == 0;
+  //@assert s[6] == 'x' && s[7] == 0;
 }
 
 void test_strcpy(void)