From dddbdb00aa640bb28856899da23b23aa856f66cb Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 13 May 2024 15:41:27 +0200
Subject: [PATCH] [libc] fixes and test oracle updates after review

---
 share/libc/netdb.h                     |   4 +-
 share/libc/stdatomic.h                 |   2 +-
 tests/libc/oracle/fc_libc.1.res.oracle |   8 +-
 tests/libc/oracle/netdb_c.res.oracle   |   6 +-
 tests/libc/oracle/string_c.res.oracle  | 816 ++++++++++++++++++++++---
 tests/libc/string_c.c                  |  11 +-
 6 files changed, 738 insertions(+), 109 deletions(-)

diff --git a/share/libc/netdb.h b/share/libc/netdb.h
index 6e1c2515915..7a5457ec2b3 100644
--- a/share/libc/netdb.h
+++ b/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);
 
diff --git a/share/libc/stdatomic.h b/share/libc/stdatomic.h
index f02aee8016e..8f0674cbc62 100644
--- a/share/libc/stdatomic.h
+++ b/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))
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index bb27675e27a..3b045dfc981 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/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)
 {
diff --git a/tests/libc/oracle/netdb_c.res.oracle b/tests/libc/oracle/netdb_c.res.oracle
index 03e05636c29..0b6e3dc71d5 100644
--- a/tests/libc/oracle/netdb_c.res.oracle
+++ b/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
diff --git a/tests/libc/oracle/string_c.res.oracle b/tests/libc/oracle/string_c.res.oracle
index f183d490be9..67ca8f2a247 100644
--- a/tests/libc/oracle/string_c.res.oracle
+++ b/tests/libc/oracle/string_c.res.oracle
@@ -5,7 +5,7 @@
 [eva:initial-state] Values of globals at initialization
   v ∈ [--..--]
 [eva] computing for function test_memcpy <- main.
-  Called from string_c.c:294.
+  Called from string_c.c:293.
 [eva] computing for function memcpy <- test_memcpy <- main.
   Called from string_c.c:10.
 [eva] string_c.c:10: 
@@ -71,7 +71,7 @@
 [eva] Recording results for test_memcpy
 [eva] Done for function test_memcpy
 [eva] computing for function test_memmove <- main.
-  Called from string_c.c:295.
+  Called from string_c.c:294.
 [eva] string_c.c:34: Frama_C_show_each_s0: {1}
 [eva] string_c.c:35: Frama_C_show_each_s0: {2}
 [eva] string_c.c:36: Frama_C_show_each_s0: {3}
@@ -148,7 +148,7 @@
 [eva] Recording results for test_memmove
 [eva] Done for function test_memmove
 [eva] computing for function test_strlen <- main.
-  Called from string_c.c:296.
+  Called from string_c.c:295.
 [eva] computing for function strlen <- test_strlen <- main.
   Called from string_c.c:64.
 [eva] string_c.c:64: 
@@ -175,7 +175,7 @@
 [eva] Recording results for test_strlen
 [eva] Done for function test_strlen
 [eva] computing for function test_strnlen <- main.
-  Called from string_c.c:297.
+  Called from string_c.c:296.
 [eva] computing for function strnlen <- test_strnlen <- main.
   Called from string_c.c:75.
 [eva] string_c.c:75: 
@@ -223,7 +223,7 @@
 [eva] Recording results for test_strnlen
 [eva] Done for function test_strnlen
 [eva] computing for function test_memset <- main.
-  Called from string_c.c:298.
+  Called from string_c.c:297.
 [eva] computing for function memset <- test_memset <- main.
   Called from string_c.c:92.
 [eva] string_c.c:92: function memset: precondition 'valid_s' got status valid.
@@ -247,7 +247,7 @@
 [eva] Recording results for test_memset
 [eva] Done for function test_memset
 [eva] computing for function test_strcmp <- main.
-  Called from string_c.c:299.
+  Called from string_c.c:298.
 [eva] computing for function strcmp <- test_strcmp <- main.
   Called from string_c.c:104.
 [eva] string_c.c:104: 
@@ -318,12 +318,12 @@
 [eva] Recording results for test_strcmp
 [eva] Done for function test_strcmp
 [eva] computing for function test_strncmp <- main.
-  Called from string_c.c:300.
+  Called from string_c.c:299.
 [eva] computing for function strncmp <- test_strncmp <- main.
-  Called from string_c.c:167.
-[eva] string_c.c:167: 
+  Called from string_c.c:166.
+[eva] string_c.c:166: 
   function strncmp: precondition 'valid_string_s1' got status valid.
-[eva] string_c.c:167: 
+[eva] string_c.c:166: 
   function strncmp: precondition 'valid_string_s2' got status valid.
 [eva] FRAMAC_SHARE/libc/string.h:181: 
   cannot evaluate ACSL term, unsupported ACSL construct: logic function strncmp
@@ -331,85 +331,85 @@
   function strncmp: postcondition 'acsl_c_equiv' got status unknown.
 [eva] Recording results for strncmp
 [eva] Done for function strncmp
-[eva] string_c.c:168: assertion got status valid.
+[eva] string_c.c:167: assertion got status valid.
 [eva] computing for function strncmp <- test_strncmp <- main.
-  Called from string_c.c:169.
-[eva] string_c.c:169: 
+  Called from string_c.c:168.
+[eva] string_c.c:168: 
   function strncmp: precondition 'valid_string_s1' got status valid.
-[eva] string_c.c:169: 
+[eva] string_c.c:168: 
   function strncmp: precondition 'valid_string_s2' got status valid.
 [eva] Recording results for strncmp
 [eva] Done for function strncmp
-[eva] string_c.c:170: assertion got status valid.
+[eva] string_c.c:169: assertion got status valid.
 [eva] computing for function strncmp <- test_strncmp <- main.
-  Called from string_c.c:172.
-[eva] string_c.c:172: 
+  Called from string_c.c:171.
+[eva] string_c.c:171: 
   function strncmp: precondition 'valid_string_s1' got status valid.
-[eva] string_c.c:172: 
+[eva] string_c.c:171: 
   function strncmp: precondition 'valid_string_s2' got status valid.
 [eva] Recording results for strncmp
 [eva] Done for function strncmp
-[eva] string_c.c:173: assertion got status valid.
+[eva] string_c.c:172: assertion got status valid.
 [eva] computing for function strncmp <- test_strncmp <- main.
-  Called from string_c.c:174.
-[eva] string_c.c:174: 
+  Called from string_c.c:173.
+[eva] string_c.c:173: 
   function strncmp: precondition 'valid_string_s1' got status valid.
-[eva] string_c.c:174: 
+[eva] string_c.c:173: 
   function strncmp: precondition 'valid_string_s2' got status valid.
 [eva] Recording results for strncmp
 [eva] Done for function strncmp
-[eva] string_c.c:175: assertion got status valid.
+[eva] string_c.c:174: assertion got status valid.
 [eva] computing for function strncmp <- test_strncmp <- main.
-  Called from string_c.c:176.
-[eva] string_c.c:176: 
+  Called from string_c.c:175.
+[eva] string_c.c:175: 
   function strncmp: precondition 'valid_string_s1' got status valid.
-[eva] string_c.c:176: 
+[eva] string_c.c:175: 
   function strncmp: precondition 'valid_string_s2' got status valid.
 [eva] Recording results for strncmp
 [eva] Done for function strncmp
-[eva] string_c.c:177: assertion got status valid.
+[eva] string_c.c:176: assertion got status valid.
 [eva] computing for function strncmp <- test_strncmp <- main.
-  Called from string_c.c:178.
-[eva] string_c.c:178: 
+  Called from string_c.c:177.
+[eva] string_c.c:177: 
   function strncmp: precondition 'valid_string_s1' got status valid.
-[eva] string_c.c:178: 
+[eva] string_c.c:177: 
   function strncmp: precondition 'valid_string_s2' got status valid.
 [eva] Recording results for strncmp
 [eva] Done for function strncmp
-[eva] string_c.c:179: assertion got status valid.
+[eva] string_c.c:178: assertion got status valid.
 [eva] computing for function strncmp <- test_strncmp <- main.
-  Called from string_c.c:180.
-[eva] string_c.c:180: 
+  Called from string_c.c:179.
+[eva] string_c.c:179: 
   function strncmp: precondition 'valid_string_s1' got status valid.
-[eva] string_c.c:180: 
+[eva] string_c.c:179: 
   function strncmp: precondition 'valid_string_s2' got status valid.
 [eva] Recording results for strncmp
 [eva] Done for function strncmp
-[eva] string_c.c:181: assertion got status valid.
+[eva] string_c.c:180: assertion got status valid.
 [eva] computing for function strncmp <- test_strncmp <- main.
-  Called from string_c.c:182.
-[eva] string_c.c:182: 
+  Called from string_c.c:181.
+[eva] string_c.c:181: 
   function strncmp: precondition 'valid_string_s1' got status valid.
-[eva] string_c.c:182: 
+[eva] string_c.c:181: 
   function strncmp: precondition 'valid_string_s2' got status valid.
 [eva] Recording results for strncmp
 [eva] Done for function strncmp
-[eva] string_c.c:183: assertion got status valid.
+[eva] string_c.c:182: assertion got status valid.
 [eva] Recording results for test_strncmp
 [eva] Done for function test_strncmp
 [eva] computing for function test_memcmp <- main.
-  Called from string_c.c:301.
+  Called from string_c.c:300.
 [eva] computing for function memcmp <- test_memcmp <- main.
-  Called from string_c.c:188.
-[eva] string_c.c:188: function memcmp: precondition 'valid_s1' got status valid.
-[eva] string_c.c:188: function memcmp: precondition 'valid_s2' got status valid.
-[eva] string_c.c:188: 
+  Called from string_c.c:187.
+[eva] string_c.c:187: function memcmp: precondition 'valid_s1' got status valid.
+[eva] string_c.c:187: function memcmp: precondition 'valid_s2' got status valid.
+[eva] string_c.c:187: 
   function memcmp: precondition 'initialization,s1' got status valid.
-[eva] string_c.c:188: 
+[eva] string_c.c:187: 
   function memcmp: precondition 'initialization,s2' got status valid.
-[eva] string_c.c:188: 
+[eva] string_c.c:187: 
   function memcmp: precondition 'danglingness,s1' got status valid.
-[eva] string_c.c:188: 
+[eva] string_c.c:187: 
   function memcmp: precondition 'danglingness,s2' got status valid.
 [eva] FRAMAC_SHARE/libc/string.h:63: 
   cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
@@ -417,56 +417,56 @@
   function memcmp: postcondition 'logic_spec' got status unknown.
 [eva] Recording results for memcmp
 [eva] Done for function memcmp
-[eva] string_c.c:189: assertion got status valid.
+[eva] string_c.c:188: assertion got status valid.
 [eva] computing for function memcmp <- test_memcmp <- main.
-  Called from string_c.c:190.
-[eva] string_c.c:190: function memcmp: precondition 'valid_s1' got status valid.
-[eva] string_c.c:190: function memcmp: precondition 'valid_s2' got status valid.
-[eva] string_c.c:190: 
+  Called from string_c.c:189.
+[eva] string_c.c:189: function memcmp: precondition 'valid_s1' got status valid.
+[eva] string_c.c:189: function memcmp: precondition 'valid_s2' got status valid.
+[eva] string_c.c:189: 
   function memcmp: precondition 'initialization,s1' got status valid.
-[eva] string_c.c:190: 
+[eva] string_c.c:189: 
   function memcmp: precondition 'initialization,s2' got status valid.
-[eva] string_c.c:190: 
+[eva] string_c.c:189: 
   function memcmp: precondition 'danglingness,s1' got status valid.
-[eva] string_c.c:190: 
+[eva] string_c.c:189: 
   function memcmp: precondition 'danglingness,s2' got status valid.
 [eva] Recording results for memcmp
 [eva] Done for function memcmp
-[eva] string_c.c:191: assertion got status valid.
+[eva] string_c.c:190: assertion got status valid.
 [eva] computing for function memcmp <- test_memcmp <- main.
-  Called from string_c.c:192.
-[eva] string_c.c:192: function memcmp: precondition 'valid_s1' got status valid.
-[eva] string_c.c:192: function memcmp: precondition 'valid_s2' got status valid.
-[eva] string_c.c:192: 
+  Called from string_c.c:191.
+[eva] string_c.c:191: function memcmp: precondition 'valid_s1' got status valid.
+[eva] string_c.c:191: function memcmp: precondition 'valid_s2' got status valid.
+[eva] string_c.c:191: 
   function memcmp: precondition 'initialization,s1' got status valid.
-[eva] string_c.c:192: 
+[eva] string_c.c:191: 
   function memcmp: precondition 'initialization,s2' got status valid.
-[eva] string_c.c:192: 
+[eva] string_c.c:191: 
   function memcmp: precondition 'danglingness,s1' got status valid.
-[eva] string_c.c:192: 
+[eva] string_c.c:191: 
   function memcmp: precondition 'danglingness,s2' got status valid.
 [eva] Recording results for memcmp
 [eva] Done for function memcmp
-[eva] string_c.c:193: assertion got status valid.
+[eva] string_c.c:192: assertion got status valid.
 [eva] computing for function memcmp <- test_memcmp <- main.
-  Called from string_c.c:194.
-[eva] string_c.c:194: function memcmp: precondition 'valid_s1' got status valid.
-[eva] string_c.c:194: function memcmp: precondition 'valid_s2' got status valid.
-[eva] string_c.c:194: 
+  Called from string_c.c:193.
+[eva] string_c.c:193: function memcmp: precondition 'valid_s1' got status valid.
+[eva] string_c.c:193: function memcmp: precondition 'valid_s2' got status valid.
+[eva] string_c.c:193: 
   function memcmp: precondition 'initialization,s1' got status valid.
-[eva] string_c.c:194: 
+[eva] string_c.c:193: 
   function memcmp: precondition 'initialization,s2' got status valid.
-[eva] string_c.c:194: 
+[eva] string_c.c:193: 
   function memcmp: precondition 'danglingness,s1' got status valid.
-[eva] string_c.c:194: 
+[eva] string_c.c:193: 
   function memcmp: precondition 'danglingness,s2' got status valid.
 [eva] Recording results for memcmp
 [eva] Done for function memcmp
-[eva] string_c.c:195: assertion got status valid.
+[eva] string_c.c:194: assertion got status valid.
 [eva] Recording results for test_memcmp
 [eva] Done for function test_memcmp
 [eva] computing for function test_strcat <- main.
-  Called from string_c.c:302.
+  Called from string_c.c:301.
 [eva] computing for function strcat <- test_strcat <- main.
   Called from string_c.c:124.
 [eva] string_c.c:124: 
@@ -496,30 +496,550 @@
 [eva] string_c.c:125: assertion got status valid.
 [eva] string_c.c:126: assertion got status valid.
 [eva] computing for function strcat <- test_strcat <- main.
-  Called from string_c.c:132.
-[eva] string_c.c:132: 
+  Called from string_c.c:131.
+[eva] string_c.c:131: 
   function strcat: precondition 'valid_string_src' got status valid.
-[eva] string_c.c:132: 
+[eva] string_c.c:131: 
   function strcat: precondition 'valid_string_dest' got status valid.
-[eva] string_c.c:132: 
+[eva] string_c.c:131: 
   function strcat: precondition 'room_string' got status valid.
-[eva:alarm] string_c.c:132: Warning: 
-  function strcat: precondition 'separation' got status invalid.
-[eva] FRAMAC_SHARE/libc/string.h:483: 
-  function strcat: no state left, postcondition 'sum_of_lengths' got status valid.
-[eva] FRAMAC_SHARE/libc/string.h:486: 
-  function strcat: no state left, postcondition 'initialization,dest' got status valid.
-[eva] FRAMAC_SHARE/libc/string.h:487: 
-  function strcat: no state left, postcondition 'dest_null_terminated' got status valid.
-[eva] FRAMAC_SHARE/libc/string.h:488: 
-  function strcat: no state left, postcondition 'result_ptr' got status valid.
+[eva] string_c.c:131: 
+  function strcat: precondition 'separation' got status valid.
+[eva] computing for function strlen <- strcat <- test_strcat <- main.
+  Called from FRAMAC_SHARE/libc/string.c:201.
+[eva] Recording results for strlen
+[eva] Done for function strlen
+[eva] Recording results for strcat
+[eva] Done for function strcat
+[eva] string_c.c:132: assertion got status valid.
+[eva] computing for function strcat <- test_strcat <- main.
+  Called from string_c.c:133.
+[eva] string_c.c:133: 
+  function strcat: precondition 'valid_string_src' got status valid.
+[eva] string_c.c:133: 
+  function strcat: precondition 'valid_string_dest' got status valid.
+[eva] string_c.c:133: 
+  function strcat: precondition 'room_string' got status valid.
+[eva] string_c.c:133: 
+  function strcat: precondition 'separation' got status valid.
+[eva] computing for function strlen <- strcat <- test_strcat <- main.
+  Called from FRAMAC_SHARE/libc/string.c:201.
+[eva] Recording results for strlen
+[eva] Done for function strlen
 [eva] Recording results for strcat
 [eva] Done for function strcat
+[eva] computing for function strcat <- test_strcat <- main.
+  Called from string_c.c:134.
+[eva] string_c.c:134: 
+  function strcat: precondition 'valid_string_src' got status valid.
+[eva] string_c.c:134: 
+  function strcat: precondition 'valid_string_dest' got status valid.
+[eva] string_c.c:134: 
+  function strcat: precondition 'room_string' got status valid.
+[eva] string_c.c:134: 
+  function strcat: precondition 'separation' got status valid.
+[eva] FRAMAC_SHARE/libc/string.c:201: Reusing old results for call to strlen
+[eva] Recording results for strcat
+[eva] Done for function strcat
+[eva] string_c.c:135: assertion got status valid.
 [eva] Recording results for test_strcat
 [eva] Done for function test_strcat
+[eva] computing for function test_strcpy <- main.
+  Called from string_c.c:303.
+[eva] computing for function strcpy <- test_strcpy <- main.
+  Called from string_c.c:141.
+[eva] string_c.c:141: 
+  function strcpy: precondition 'valid_string_src' got status valid.
+[eva] string_c.c:141: 
+  function strcpy: precondition 'room_string' got status valid.
+[eva] string_c.c:141: 
+  function strcpy: precondition 'separation' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:425: 
+  cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
+[eva:alarm] FRAMAC_SHARE/libc/string.h:425: Warning: 
+  function strcpy: postcondition 'equal_contents' got status unknown.
+[eva] FRAMAC_SHARE/libc/string.h:426: 
+  function strcpy: postcondition 'result_ptr' got status valid.
+[eva] Recording results for strcpy
+[eva] Done for function strcpy
+[eva] string_c.c:142: assertion got status valid.
+[eva] string_c.c:143: assertion got status valid.
+[eva] computing for function strcpy <- test_strcpy <- main.
+  Called from string_c.c:144.
+[eva] string_c.c:144: 
+  function strcpy: precondition 'valid_string_src' got status valid.
+[eva] string_c.c:144: 
+  function strcpy: precondition 'room_string' got status valid.
+[eva] string_c.c:144: 
+  function strcpy: precondition 'separation' got status valid.
+[eva] Recording results for strcpy
+[eva] Done for function strcpy
+[eva] string_c.c:145: assertion got status valid.
+[eva] computing for function strcpy <- test_strcpy <- main.
+  Called from string_c.c:146.
+[eva] string_c.c:146: 
+  function strcpy: precondition 'valid_string_src' got status valid.
+[eva] string_c.c:146: 
+  function strcpy: precondition 'room_string' got status valid.
+[eva] string_c.c:146: 
+  function strcpy: precondition 'separation' got status valid.
+[eva] Recording results for strcpy
+[eva] Done for function strcpy
+[eva] string_c.c:147: assertion got status valid.
+[eva] Recording results for test_strcpy
+[eva] Done for function test_strcpy
+[eva] computing for function test_strncpy <- main.
+  Called from string_c.c:304.
+[eva] computing for function strncpy <- test_strncpy <- main.
+  Called from string_c.c:153.
+[eva] string_c.c:153: 
+  function strncpy: precondition 'valid_nstring_src' got status valid.
+[eva] string_c.c:153: 
+  function strncpy: precondition 'room_nstring' got status valid.
+[eva] string_c.c:153: 
+  function strncpy: precondition 'separation' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:437: 
+  function strncpy: postcondition 'result_ptr' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:438: 
+  function strncpy: postcondition 'initialization' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:441: 
+  cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp
+[eva:alarm] FRAMAC_SHARE/libc/string.h:441: Warning: 
+  function strncpy, behavior complete: postcondition 'equal_after_copy' got status unknown.
+[eva] Recording results for strncpy
+[eva] Done for function strncpy
+[eva] string_c.c:154: assertion got status valid.
+[eva] string_c.c:155: assertion got status valid.
+[eva] computing for function strncpy <- test_strncpy <- main.
+  Called from string_c.c:156.
+[eva] string_c.c:156: 
+  function strncpy: precondition 'valid_nstring_src' got status valid.
+[eva] string_c.c:156: 
+  function strncpy: precondition 'room_nstring' got status valid.
+[eva] string_c.c:156: 
+  function strncpy: precondition 'separation' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:444: 
+  cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
+[eva:alarm] FRAMAC_SHARE/libc/string.h:444: Warning: 
+  function strncpy, behavior partial: postcondition 'equal_prefix' got status unknown.
+[eva] Recording results for strncpy
+[eva] Done for function strncpy
+[eva] string_c.c:157: assertion got status valid.
+[eva] computing for function strncpy <- test_strncpy <- main.
+  Called from string_c.c:158.
+[eva] string_c.c:158: 
+  function strncpy: precondition 'valid_nstring_src' got status valid.
+[eva] string_c.c:158: 
+  function strncpy: precondition 'room_nstring' got status valid.
+[eva] string_c.c:158: 
+  function strncpy: precondition 'separation' got status valid.
+[eva] Recording results for strncpy
+[eva] Done for function strncpy
+[eva] string_c.c:159: assertion got status valid.
+[eva] computing for function strncpy <- test_strncpy <- main.
+  Called from string_c.c:160.
+[eva] string_c.c:160: 
+  function strncpy: precondition 'valid_nstring_src' got status valid.
+[eva] string_c.c:160: 
+  function strncpy: precondition 'room_nstring' got status valid.
+[eva] string_c.c:160: 
+  function strncpy: precondition 'separation' got status valid.
+[eva] Recording results for strncpy
+[eva] Done for function strncpy
+[eva] string_c.c:161: assertion got status valid.
+[eva] Recording results for test_strncpy
+[eva] Done for function test_strncpy
+[eva] computing for function test_strchr <- main.
+  Called from string_c.c:305.
+[eva] computing for function strchr <- test_strchr <- main.
+  Called from string_c.c:200.
+[eva] string_c.c:200: 
+  function strchr: precondition 'valid_string_s' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:197: 
+  function strchr, behavior found: postcondition 'result_valid_string' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:198: 
+  function strchr, behavior found: postcondition 'result_char' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:199: 
+  function strchr, behavior found: postcondition 'result_same_base' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:200: 
+  function strchr, behavior found: postcondition 'result_in_length' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:202: 
+  cannot evaluate ACSL term, unsupported logic var p
+[eva:alarm] FRAMAC_SHARE/libc/string.h:202: Warning: 
+  function strchr, behavior found: postcondition 'result_first_occurrence' got status unknown.
+[eva] Recording results for strchr
+[eva] Done for function strchr
+[eva] string_c.c:201: assertion got status valid.
+[eva] computing for function strchr <- test_strchr <- main.
+  Called from string_c.c:202.
+[eva] string_c.c:202: 
+  function strchr: precondition 'valid_string_s' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:205: 
+  function strchr, behavior not_found: postcondition 'result_null' got status valid.
+[eva] Recording results for strchr
+[eva] Done for function strchr
+[eva] string_c.c:203: assertion got status valid.
+[eva] computing for function strchr <- test_strchr <- main.
+  Called from string_c.c:204.
+[eva] string_c.c:204: 
+  function strchr: precondition 'valid_string_s' got status valid.
+[eva] Recording results for strchr
+[eva] Done for function strchr
+[eva] string_c.c:205: assertion got status valid.
+[eva] computing for function strchr <- test_strchr <- main.
+  Called from string_c.c:206.
+[eva] string_c.c:206: 
+  function strchr: precondition 'valid_string_s' got status valid.
+[eva] Recording results for strchr
+[eva] Done for function strchr
+[eva] string_c.c:207: assertion got status valid.
+[eva] Recording results for test_strchr
+[eva] Done for function test_strchr
+[eva] computing for function test_strrchr <- main.
+  Called from string_c.c:306.
+[eva] computing for function strrchr <- test_strrchr <- main.
+  Called from string_c.c:213.
+[eva] string_c.c:213: 
+  function strrchr: precondition 'valid_string_s' got status valid.
+[eva] computing for function strlen <- strrchr <- test_strrchr <- main.
+  Called from FRAMAC_SHARE/libc/string.c:266.
+[eva] FRAMAC_SHARE/libc/string.c:266: 
+  function strlen: precondition 'valid_string_s' got status valid.
+[eva] Recording results for strlen
+[eva] Done for function strlen
+[eva] FRAMAC_SHARE/libc/string.h:223: 
+  function strrchr: postcondition 'result_null_or_same_base' got status valid.
+[eva] Recording results for strrchr
+[eva] Done for function strrchr
+[eva] string_c.c:214: assertion got status valid.
+[eva] computing for function strrchr <- test_strrchr <- main.
+  Called from string_c.c:215.
+[eva] string_c.c:215: 
+  function strrchr: precondition 'valid_string_s' got status valid.
+[eva] FRAMAC_SHARE/libc/string.c:266: Reusing old results for call to strlen
+[eva] Recording results for strrchr
+[eva] Done for function strrchr
+[eva] string_c.c:216: assertion got status valid.
+[eva] computing for function strrchr <- test_strrchr <- main.
+  Called from string_c.c:217.
+[eva] string_c.c:217: 
+  function strrchr: precondition 'valid_string_s' got status valid.
+[eva] FRAMAC_SHARE/libc/string.c:266: Reusing old results for call to strlen
+[eva] Recording results for strrchr
+[eva] Done for function strrchr
+[eva] string_c.c:218: assertion got status valid.
+[eva] computing for function strrchr <- test_strrchr <- main.
+  Called from string_c.c:219.
+[eva] string_c.c:219: 
+  function strrchr: precondition 'valid_string_s' got status valid.
+[eva] FRAMAC_SHARE/libc/string.c:266: Reusing old results for call to strlen
+[eva] Recording results for strrchr
+[eva] Done for function strrchr
+[eva] string_c.c:220: assertion got status valid.
+[eva] Recording results for test_strrchr
+[eva] Done for function test_strrchr
+[eva] computing for function test_memchr <- main.
+  Called from string_c.c:307.
+[eva] computing for function memchr <- test_memchr <- main.
+  Called from string_c.c:226.
+[eva] string_c.c:226: function memchr: precondition 'valid' got status valid.
+[eva] string_c.c:226: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] string_c.c:226: 
+  function memchr: precondition 'danglingness' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:78: 
+  cannot evaluate ACSL term, unsupported ACSL construct: logic function memchr
+[eva] FRAMAC_SHARE/libc/string.h:86: 
+  cannot evaluate ACSL term, unsupported ACSL construct: logic function memchr
+[eva] FRAMAC_SHARE/libc/string.h:79: 
+  function memchr, behavior found: postcondition 'result_valid_read' got status valid. (Behavior may be inactive, no reduction performed.)
+[eva] FRAMAC_SHARE/libc/string.h:80: 
+  function memchr, behavior found: postcondition 'result_same_base' got status valid. (Behavior may be inactive, no reduction performed.)
+[eva] FRAMAC_SHARE/libc/string.h:81: 
+  function memchr, behavior found: postcondition 'result_char' got status valid. (Behavior may be inactive, no reduction performed.)
+[eva] FRAMAC_SHARE/libc/string.h:82: 
+  function memchr, behavior found: postcondition 'result_in_str' got status valid. (Behavior may be inactive, no reduction performed.)
+[eva:alarm] FRAMAC_SHARE/libc/string.h:87: Warning: 
+  function memchr, behavior not_found: postcondition 'result_null' got status invalid. (Behavior may be inactive, no reduction performed.)
+[eva] Recording results for memchr
+[eva] Done for function memchr
+[eva] string_c.c:227: assertion got status valid.
+[eva] computing for function memchr <- test_memchr <- main.
+  Called from string_c.c:228.
+[eva] string_c.c:228: function memchr: precondition 'valid' got status valid.
+[eva] string_c.c:228: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] string_c.c:228: 
+  function memchr: precondition 'danglingness' got status valid.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:79: Warning: 
+  function memchr, behavior found: postcondition 'result_valid_read' got status invalid. (Behavior may be inactive, no reduction performed.)
+[eva:alarm] FRAMAC_SHARE/libc/string.h:80: Warning: 
+  function memchr, behavior found: postcondition 'result_same_base' got status invalid. (Behavior may be inactive, no reduction performed.)
+[eva:alarm] FRAMAC_SHARE/libc/string.h:81: Warning: 
+  function memchr, behavior found: postcondition 'result_char' got status unknown. (Behavior may be inactive, no reduction performed.)
+[eva] FRAMAC_SHARE/libc/string.h:87: 
+  function memchr, behavior not_found: postcondition 'result_null' got status valid. (Behavior may be inactive, no reduction performed.)
+[eva] Recording results for memchr
+[eva] Done for function memchr
+[eva] string_c.c:229: assertion got status valid.
+[eva] computing for function memchr <- test_memchr <- main.
+  Called from string_c.c:230.
+[eva] string_c.c:230: function memchr: precondition 'valid' got status valid.
+[eva] string_c.c:230: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] string_c.c:230: 
+  function memchr: precondition 'danglingness' got status valid.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:82: Warning: 
+  function memchr, behavior found: postcondition 'result_in_str' got status unknown. (Behavior may be inactive, no reduction performed.)
+[eva] Recording results for memchr
+[eva] Done for function memchr
+[eva] string_c.c:231: assertion got status valid.
+[eva] computing for function memchr <- test_memchr <- main.
+  Called from string_c.c:232.
+[eva] string_c.c:232: function memchr: precondition 'valid' got status valid.
+[eva] string_c.c:232: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] string_c.c:232: 
+  function memchr: precondition 'danglingness' got status valid.
+[eva] Recording results for memchr
+[eva] Done for function memchr
+[eva] string_c.c:233: assertion got status valid.
+[eva] computing for function memchr <- test_memchr <- main.
+  Called from string_c.c:234.
+[eva] string_c.c:234: function memchr: precondition 'valid' got status valid.
+[eva] string_c.c:234: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] string_c.c:234: 
+  function memchr: precondition 'danglingness' got status valid.
+[eva] Recording results for memchr
+[eva] Done for function memchr
+[eva] string_c.c:235: assertion got status valid.
+[eva] computing for function memchr <- test_memchr <- main.
+  Called from string_c.c:236.
+[eva] string_c.c:236: function memchr: precondition 'valid' got status valid.
+[eva] string_c.c:236: 
+  function memchr: precondition 'initialization' got status valid.
+[eva] string_c.c:236: 
+  function memchr: precondition 'danglingness' got status valid.
+[eva] Recording results for memchr
+[eva] Done for function memchr
+[eva] string_c.c:237: assertion got status valid.
+[eva] Recording results for test_memchr
+[eva] Done for function test_memchr
+[eva] computing for function test_memrchr <- main.
+  Called from string_c.c:308.
+[eva] computing for function memrchr <- test_memrchr <- main.
+  Called from string_c.c:243.
+[eva] string_c.c:243: function memrchr: precondition 'valid' got status valid.
+[eva] string_c.c:243: 
+  function memrchr: precondition 'initialization' got status valid.
+[eva] string_c.c:243: 
+  function memrchr: precondition 'danglingness' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:99: 
+  cannot evaluate ACSL term, unsupported ACSL construct: logic function memchr
+[eva] FRAMAC_SHARE/libc/string.h:103: 
+  cannot evaluate ACSL term, unsupported ACSL construct: logic function memchr
+[eva] FRAMAC_SHARE/libc/string.h:100: 
+  function memrchr, behavior found: postcondition 'result_valid_read' got status valid. (Behavior may be inactive, no reduction performed.)
+[eva] FRAMAC_SHARE/libc/string.h:101: 
+  function memrchr, behavior found: postcondition 'result_same_base' got status valid. (Behavior may be inactive, no reduction performed.)
+[eva:alarm] FRAMAC_SHARE/libc/string.h:104: Warning: 
+  function memrchr, behavior not_found: postcondition 'result_null' got status invalid. (Behavior may be inactive, no reduction performed.)
+[eva] Recording results for memrchr
+[eva] Done for function memrchr
+[eva] string_c.c:244: assertion got status valid.
+[eva] computing for function memrchr <- test_memrchr <- main.
+  Called from string_c.c:245.
+[eva] string_c.c:245: function memrchr: precondition 'valid' got status valid.
+[eva] string_c.c:245: 
+  function memrchr: precondition 'initialization' got status valid.
+[eva] string_c.c:245: 
+  function memrchr: precondition 'danglingness' got status valid.
+[eva:alarm] FRAMAC_SHARE/libc/string.h:100: Warning: 
+  function memrchr, behavior found: postcondition 'result_valid_read' got status invalid. (Behavior may be inactive, no reduction performed.)
+[eva:alarm] FRAMAC_SHARE/libc/string.h:101: Warning: 
+  function memrchr, behavior found: postcondition 'result_same_base' got status invalid. (Behavior may be inactive, no reduction performed.)
+[eva] FRAMAC_SHARE/libc/string.h:104: 
+  function memrchr, behavior not_found: postcondition 'result_null' got status valid. (Behavior may be inactive, no reduction performed.)
+[eva] Recording results for memrchr
+[eva] Done for function memrchr
+[eva] string_c.c:246: assertion got status valid.
+[eva] computing for function memrchr <- test_memrchr <- main.
+  Called from string_c.c:247.
+[eva] string_c.c:247: function memrchr: precondition 'valid' got status valid.
+[eva] string_c.c:247: 
+  function memrchr: precondition 'initialization' got status valid.
+[eva] string_c.c:247: 
+  function memrchr: precondition 'danglingness' got status valid.
+[eva] Recording results for memrchr
+[eva] Done for function memrchr
+[eva] string_c.c:248: assertion got status valid.
+[eva] computing for function memrchr <- test_memrchr <- main.
+  Called from string_c.c:249.
+[eva] string_c.c:249: function memrchr: precondition 'valid' got status valid.
+[eva] string_c.c:249: 
+  function memrchr: precondition 'initialization' got status valid.
+[eva] string_c.c:249: 
+  function memrchr: precondition 'danglingness' got status valid.
+[eva] Recording results for memrchr
+[eva] Done for function memrchr
+[eva] string_c.c:250: assertion got status valid.
+[eva] computing for function memrchr <- test_memrchr <- main.
+  Called from string_c.c:251.
+[eva] string_c.c:251: function memrchr: precondition 'valid' got status valid.
+[eva] string_c.c:251: 
+  function memrchr: precondition 'initialization' got status valid.
+[eva] string_c.c:251: 
+  function memrchr: precondition 'danglingness' got status valid.
+[eva] Recording results for memrchr
+[eva] Done for function memrchr
+[eva] string_c.c:252: assertion got status valid.
+[eva] computing for function memrchr <- test_memrchr <- main.
+  Called from string_c.c:253.
+[eva] string_c.c:253: function memrchr: precondition 'valid' got status valid.
+[eva] string_c.c:253: 
+  function memrchr: precondition 'initialization' got status valid.
+[eva] string_c.c:253: 
+  function memrchr: precondition 'danglingness' got status valid.
+[eva] Recording results for memrchr
+[eva] Done for function memrchr
+[eva] string_c.c:254: assertion got status valid.
+[eva] Recording results for test_memrchr
+[eva] Done for function test_memrchr
+[eva] computing for function test_strstr <- main.
+  Called from string_c.c:309.
+[eva] computing for function strstr <- test_strstr <- main.
+  Called from string_c.c:260.
+[eva] string_c.c:260: 
+  function strstr: precondition 'valid_string_haystack' got status valid.
+[eva] string_c.c:260: 
+  function strstr: precondition 'valid_string_needle' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:266: 
+  cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
+[eva:alarm] FRAMAC_SHARE/libc/string.h:263: Warning: 
+  function strstr: postcondition 'result_null_or_in_haystack' got status unknown.
+[eva] Recording results for strstr
+[eva] Done for function strstr
+[eva] string_c.c:261: assertion got status valid.
+[eva] computing for function strstr <- test_strstr <- main.
+  Called from string_c.c:262.
+[eva] string_c.c:262: 
+  function strstr: precondition 'valid_string_haystack' got status valid.
+[eva] string_c.c:262: 
+  function strstr: precondition 'valid_string_needle' got status valid.
+[eva] Recording results for strstr
+[eva] Done for function strstr
+[eva] string_c.c:263: assertion got status valid.
+[eva] computing for function strstr <- test_strstr <- main.
+  Called from string_c.c:264.
+[eva] string_c.c:264: 
+  function strstr: precondition 'valid_string_haystack' got status valid.
+[eva] string_c.c:264: 
+  function strstr: precondition 'valid_string_needle' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:263: 
+  function strstr: postcondition 'result_null_or_in_haystack' got status valid.
+[eva] Recording results for strstr
+[eva] Done for function strstr
+[eva] string_c.c:265: assertion got status valid.
+[eva] computing for function strstr <- test_strstr <- main.
+  Called from string_c.c:266.
+[eva] string_c.c:266: 
+  function strstr: precondition 'valid_string_haystack' got status valid.
+[eva] string_c.c:266: 
+  function strstr: precondition 'valid_string_needle' got status valid.
+[eva] Recording results for strstr
+[eva] Done for function strstr
+[eva] string_c.c:267: assertion got status valid.
+[eva] computing for function strstr <- test_strstr <- main.
+  Called from string_c.c:268.
+[eva] string_c.c:268: 
+  function strstr: precondition 'valid_string_haystack' got status valid.
+[eva] string_c.c:268: 
+  function strstr: precondition 'valid_string_needle' got status valid.
+[eva] Recording results for strstr
+[eva] Done for function strstr
+[eva] string_c.c:269: assertion got status valid.
+[eva] computing for function strstr <- test_strstr <- main.
+  Called from string_c.c:270.
+[eva] string_c.c:270: 
+  function strstr: precondition 'valid_string_haystack' got status valid.
+[eva] string_c.c:270: 
+  function strstr: precondition 'valid_string_needle' got status valid.
+[eva] Recording results for strstr
+[eva] Done for function strstr
+[eva] string_c.c:271: assertion got status valid.
+[eva] computing for function strstr <- test_strstr <- main.
+  Called from string_c.c:272.
+[eva] string_c.c:272: 
+  function strstr: precondition 'valid_string_haystack' got status valid.
+[eva] string_c.c:272: 
+  function strstr: precondition 'valid_string_needle' got status valid.
+[eva] Recording results for strstr
+[eva] Done for function strstr
+[eva] string_c.c:273: assertion got status valid.
+[eva] computing for function strstr <- test_strstr <- main.
+  Called from string_c.c:274.
+[eva] string_c.c:274: 
+  function strstr: precondition 'valid_string_haystack' got status valid.
+[eva] string_c.c:274: 
+  function strstr: precondition 'valid_string_needle' got status valid.
+[eva] Recording results for strstr
+[eva] Done for function strstr
+[eva] string_c.c:275: assertion got status valid.
+[eva] Recording results for test_strstr
+[eva] Done for function test_strstr
+[eva] computing for function test_mempcpy <- main.
+  Called from string_c.c:313.
+[eva] computing for function mempcpy <- test_mempcpy <- main.
+  Called from string_c.c:281.
+[eva] string_c.c:281: 
+  function mempcpy: precondition 'valid_dest' got status valid.
+[eva] string_c.c:281: 
+  function mempcpy: precondition 'valid_src' got status valid.
+[eva] string_c.c:281: 
+  function mempcpy: precondition 'separation' got status valid.
+[eva] FRAMAC_SHARE/libc/string.h:131: 
+  cannot evaluate ACSL term, unsupported ACSL construct: logic function memcmp
+[eva:alarm] FRAMAC_SHARE/libc/string.h:131: Warning: 
+  function mempcpy: postcondition 'copied_contents' got status unknown.
+[kernel] FRAMAC_SHARE/libc/string.c:57: Warning: using size of 'void'
+[eva:alarm] FRAMAC_SHARE/libc/string.h:132: Warning: 
+  function mempcpy: postcondition 'result_next_byte' got status unknown.
+[eva] Recording results for mempcpy
+[eva] Done for function mempcpy
+[eva] string_c.c:282: assertion got status valid.
+[eva] string_c.c:283: assertion got status valid.
+[eva] computing for function mempcpy <- test_mempcpy <- main.
+  Called from string_c.c:285.
+[eva] string_c.c:285: 
+  function mempcpy: precondition 'valid_dest' got status valid.
+[eva] string_c.c:285: 
+  function mempcpy: precondition 'valid_src' got status valid.
+[eva] string_c.c:285: 
+  function mempcpy: precondition 'separation' got status valid.
+[eva] Recording results for mempcpy
+[eva] Done for function mempcpy
+[eva] string_c.c:286: assertion got status valid.
+[eva] computing for function mempcpy <- test_mempcpy <- main.
+  Called from string_c.c:287.
+[eva] string_c.c:287: 
+  function mempcpy: precondition 'valid_dest' got status valid.
+[eva] string_c.c:287: 
+  function mempcpy: precondition 'valid_src' got status valid.
+[eva] string_c.c:287: 
+  function mempcpy: precondition 'separation' got status valid.
+[eva] Recording results for mempcpy
+[eva] Done for function mempcpy
+[eva] string_c.c:288: assertion got status valid.
+[eva] Recording results for test_mempcpy
+[eva] Done for function test_mempcpy
 [eva] Recording results for main
 [eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function memchr:
+  ch ∈ {1; 2; 5}
+  ss ∈ {{ (unsigned char const *)&s }}
+  __retres ∈ {{ NULL ; (void *)&s{[0], [1]} }}
 [eva:final-states] Values at end of function memcmp:
   p1 ∈ {{ "hallo" ; "hallo" ; "a\000b" ; "a\000b" }}
   p2 ∈ {{ (unsigned char const *)&hello ; "a\000c" ; "a\000c" }}
@@ -547,28 +1067,78 @@
      [4] ∈ {3; 4; 5}
      [5] ∈ {4; 5; 6}
   __retres ∈ {{ (void *)&buf{[0], [2], [3]} }}
+[eva:final-states] Values at end of function mempcpy:
+  i ∈ {0; 3; 6}
+  dest[0] ∈ {97; 104}
+      [1] ∈ {0; 101}
+      [2] ∈ {98; 108}
+      [3] ∈ {108}
+      [4] ∈ {111}
+      [5] ∈ {0}
+  __retres ∈ {{ (void *)&dest{[0], [3], [6]} }}
+[eva:final-states] Values at end of function memrchr:
+  ch ∈ {1; 2; 5}
+  ss ∈ {{ (unsigned char const *)&s }}
+  __retres ∈ {{ NULL ; (void *)&s{[0], [3], [4]} }}
 [eva:final-states] Values at end of function memset:
   p ∈ {{ (unsigned char *)&dest }}
   dest[0..2] ∈ {42}
       [3] ∈ {0}
+[eva:final-states] Values at end of function strchr:
+  ch ∈ {0; 72; 104; 108}
+  i ∈ {0; 2; 5}
+  __retres ∈ {{ NULL ; "hello" + {0; 2; 5} }}
 [eva:final-states] Values at end of function strcmp:
   i ∈ {0; 1; 4; 5}
   __retres ∈ {-111; -104; -32; 0; 111}
+[eva:final-states] Values at end of function strcpy:
+  i ∈ {0; 5; 6}
+  s[0] ∈ {0; 54; 104}
+   [1] ∈ {53; 101}
+   [2] ∈ {52; 108}
+   [3] ∈ {51; 108}
+   [4] ∈ {50; 111}
+   [5] ∈ {0; 49}
+   [6] ∈ {0} or UNINITIALIZED
 [eva:final-states] Values at end of function strlen:
-  i ∈ {0; 2; 5}
+  i ∈ {0; 2; 4; 5; 6}
 [eva:final-states] Values at end of function strcat:
-  i ∈ {5}
-  n ∈ {0}
+  i ∈ {0; 1; 2; 5}
+  n ∈ {0; 4; 6}
   s[0] ∈ {104}
    [1] ∈ {101}
    [2..3] ∈ {108}
-   [4] ∈ {111}
-   [5] ∈ {0}
-   [6..9] ∈ UNINITIALIZED
+   [4] ∈ {108; 111}
+   [5] ∈ {0; 111}
+   [6] ∈ {0; 120} or UNINITIALIZED
+   [7] ∈ {0; 108} or UNINITIALIZED
+   [8] ∈ {111} or UNINITIALIZED
+   [9] ∈ {0} or UNINITIALIZED
 [eva:final-states] Values at end of function strncmp:
   __retres ∈ {-104; -4; 0; 111}
+[eva:final-states] Values at end of function strncpy:
+  i ∈ {0; 3; 5; 7}
+  s[0] ∈ {97; 98; 104}
+   [1] ∈ {98; 101; 121}
+   [2] ∈ {0; 101; 108}
+   [3] ∈ {0; 108}
+   [4] ∈ {0; 111}
+   [5..6] ∈ {0}
 [eva:final-states] Values at end of function strnlen:
   i ∈ {0; 2; 4; 5}
+[eva:final-states] Values at end of function strrchr:
+  ch ∈ {0; 72; 104; 108}
+  __retres ∈ {{ NULL ; "hello" + {0; 3; 5} }}
+[eva:final-states] Values at end of function strstr:
+  __retres ∈ {{ NULL ; "hello" + {0; 2; 3} }}
+[eva:final-states] Values at end of function test_memchr:
+  s[0] ∈ {1}
+   [1] ∈ {2}
+   [2] ∈ {3}
+   [3] ∈ {1}
+   [4] ∈ {2}
+   [5] ∈ {4}
+  p ∈ {{ &s[0] }}
 [eva:final-states] Values at end of function test_memcmp:
   hello[0] ∈ {104}
        [1] ∈ {101}
@@ -606,12 +1176,48 @@
   s ∈ {{ &buf[0] }}
   d ∈ {{ &buf[3] }}
   p ∈ {{ &buf[2] }}
+[eva:final-states] Values at end of function test_mempcpy:
+  dest[0] ∈ {97}
+      [1] ∈ {0}
+      [2] ∈ {98}
+      [3] ∈ {108}
+      [4] ∈ {111}
+      [5] ∈ {0}
+  src[0] ∈ {104}
+     [1] ∈ {101}
+     [2..3] ∈ {108}
+     [4] ∈ {111}
+     [5] ∈ {0}
+  p ∈ {{ &dest[0] }}
+  src2[0] ∈ {97}
+      [1] ∈ {0}
+      [2] ∈ {98}
+      [3..4] ∈ {0}
+[eva:final-states] Values at end of function test_memrchr:
+  s[0] ∈ {1}
+   [1] ∈ {2}
+   [2] ∈ {3}
+   [3] ∈ {1}
+   [4] ∈ {2}
+   [5] ∈ {4}
+  p ∈ {{ &s[0] }}
 [eva:final-states] Values at end of function test_memset:
   dest[0..2] ∈ {42}
       [3] ∈ {0}
   p ∈ {{ &dest[0] }}
 [eva:final-states] Values at end of function test_strcat:
-  NON TERMINATING FUNCTION
+  s[0] ∈ {104}
+   [1] ∈ {101}
+   [2..4] ∈ {108}
+   [5] ∈ {111}
+   [6] ∈ {120}
+   [7] ∈ {0}
+   [8] ∈ {111}
+   [9] ∈ {0}
+  p ∈ {{ &s[0] }}
+[eva:final-states] Values at end of function test_strchr:
+  s ∈ {{ "hello" }}
+  p ∈ {{ "hello" + {5} }}
 [eva:final-states] Values at end of function test_strcmp:
   hello[0] ∈ {104}
        [1] ∈ {97}
@@ -625,6 +1231,15 @@
   res5 ∈ {-104}
   res6 ∈ {0}
   res7 ∈ {0}
+[eva:final-states] Values at end of function test_strcpy:
+  s[0] ∈ {0}
+   [1] ∈ {53}
+   [2] ∈ {52}
+   [3] ∈ {51}
+   [4] ∈ {50}
+   [5] ∈ {49}
+   [6] ∈ {0}
+  p ∈ {{ &s[0] }}
 [eva:final-states] Values at end of function test_strlen:
   s ∈ {{ "hello" }}
   n ∈ {0}
@@ -642,8 +1257,19 @@
   res6 ∈ {-104}
   res7 ∈ {0}
   res8 ∈ {0}
+[eva:final-states] Values at end of function test_strncpy:
+  s[0] ∈ {97}
+   [1] ∈ {98}
+   [2..6] ∈ {0}
+  p ∈ {{ &s[0] }}
 [eva:final-states] Values at end of function test_strnlen:
   s ∈ {{ "hello" }}
   n ∈ {0}
+[eva:final-states] Values at end of function test_strrchr:
+  s ∈ {{ "hello" }}
+  p ∈ {{ "hello" + {5} }}
+[eva:final-states] Values at end of function test_strstr:
+  s ∈ {{ "hello" }}
+  p ∈ {{ "hello" }}
 [eva:final-states] Values at end of function main:
-  NON TERMINATING FUNCTION
+  __retres ∈ {0}
diff --git a/tests/libc/string_c.c b/tests/libc/string_c.c
index 3fb1d5a8056..56b7a8ad133 100644
--- a/tests/libc/string_c.c
+++ b/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)
-- 
GitLab