[Libc] add stub for wcsdup

share/libc/wchar.c

@@ -91,4 +91,18 @@ wchar_t* wcsncat(wchar_t *dest, const wchar_t *src, size_t n)
   return dest;
 }
 
+/* Warning: read considerations about malloc() in Frama-C */
+#include "stdlib.h"
+wchar_t *wcsdup(const wchar_t *ws)
+{
+  size_t l = wcslen(ws) + 1;
+  wchar_t *p = malloc(sizeof(wchar_t) * l);
+  if (!p) {
+    errno = ENOMEM;
+    return 0;
+  }
+  wmemcpy(p, ws, l);
+  return p;
+}
+
 __POP_FC_STDLIB

tests/libc/oracle/fc_libc.0.res.oracle

@@ -15,7 +15,7 @@
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
   
-[metrics] Defined functions (83)
+[metrics] Defined functions (84)
   ======================
    Frama_C_abort (1 call); Frama_C_char_interval (1 call);
    Frama_C_double_interval (0 call); Frama_C_float_interval (0 call);
@@ -40,8 +40,8 @@
    strncat (0 call); strncmp (0 call); strncpy (2 calls); strndup (0 call);
    strnlen (0 call); strrchr (0 call); strsignal (0 call); strstr (0 call);
    tolower (0 call); toupper (0 call); unsetenv (0 call); wcscat (0 call);
-   wcscpy (0 call); wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call);
-   wmemcpy (0 call); wmemset (0 call); 
+   wcscpy (0 call); wcsdup (0 call); wcslen (3 calls); wcsncat (0 call);
+   wcsncpy (0 call); wmemcpy (1 call); wmemset (0 call); 
   
   Specified-only functions (414)
   ==============================
@@ -118,7 +118,7 @@
    log10f (0 call); log10l (0 call); log2 (0 call); log2f (0 call);
    log2l (0 call); logf (0 call); logl (0 call); longjmp (0 call);
    lrand48 (0 call); lseek (0 call); lstat (0 call); makedev (0 call);
-   malloc (8 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
+   malloc (9 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
    mkdir (0 call); mkfifo (0 call); mknod (0 call); mkstemp (0 call);
    mktime (0 call); mrand48 (0 call); nan (0 call); nanf (0 call);
    nanl (0 call); nanosleep (0 call); nrand48 (0 call); ntohl (0 call);
@@ -187,18 +187,18 @@
   
   Global metrics
   ============== 
-  Sloc = 1127
-  Decision point = 213
+  Sloc = 1138
+  Decision point = 214
   Global variables = 85
-  If = 198
+  If = 199
   Loop = 43
-  Goto = 97
-  Assignment = 459
-  Exit point = 83
-  Function = 498
-  Function call = 93
+  Goto = 98
+  Assignment = 465
+  Exit point = 84
+  Function = 499
+  Function call = 96
   Pointer dereferencing = 159
-  Cyclomatic complexity = 296
+  Cyclomatic complexity = 298
 /* Generated by Frama-C */
 #include "__fc_builtin.c"
 #include "__fc_builtin.h"

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

@@ -6975,6 +6975,23 @@ wchar_t *wcsncat(wchar_t *dest, wchar_t const *src, size_t n)
   return dest;
 }
 
+wchar_t *wcsdup(wchar_t const *ws)
+{
+  wchar_t *__retres;
+  size_t tmp;
+  tmp = wcslen(ws);
+  size_t l = tmp + (size_t)1;
+  wchar_t *p = malloc(sizeof(wchar_t) * l);
+  if (! p) {
+    __fc_errno = 12;
+    __retres = (wchar_t *)0;
+    goto return_label;
+  }
+  wmemcpy(p,ws,l);
+  __retres = p;
+  return_label: return __retres;
+}
+
 /*@ ghost extern int __fc_stack_status; */
 
 /*@ ensures allocation: \fresh{Old, Here}(\result,\old(size));

tests/libc/oracle/wchar_c_h.0.res.oracle

@@ -185,6 +185,33 @@
   function wmemchr: precondition 'initialization' got status valid.
 [eva] tests/libc/wchar_c_h.c:70: 
   function wmemchr: precondition 'danglingness' got status valid.
+[eva] computing for function wcsdup <- main.
+  Called from tests/libc/wchar_c_h.c:73.
+[eva] share/libc/wchar.c:98: Call to builtin wcslen
+[eva] share/libc/wchar.c:98: 
+  function wcslen: precondition 'valid_string_s' got status valid.
+[eva] share/libc/wchar.c:99: Call to builtin malloc
+[eva] share/libc/wchar.c:99: allocating variable __malloc_wcsdup_l99
+[eva] computing for function wmemcpy <- wcsdup <- main.
+  Called from share/libc/wchar.c:104.
+[eva] Recording results for wmemcpy
+[eva] Done for function wmemcpy
+[eva] Recording results for wcsdup
+[eva] Done for function wcsdup
+[eva] computing for function wcsdup <- main.
+  Called from tests/libc/wchar_c_h.c:75.
+[eva] share/libc/wchar.c:98: Call to builtin wcslen
+[eva] share/libc/wchar.c:99: Call to builtin malloc
+[eva] share/libc/wchar.c:99: allocating variable __malloc_wcsdup_l99_0
+[eva] computing for function wmemcpy <- wcsdup <- main.
+  Called from share/libc/wchar.c:104.
+[eva] Recording results for wmemcpy
+[eva] Done for function wmemcpy
+[eva] Recording results for wcsdup
+[eva] Done for function wcsdup
+[eva] tests/libc/wchar_c_h.c:76: Call to builtin free
+[eva] tests/libc/wchar_c_h.c:76: 
+  function free: precondition 'freeable' got status valid.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -234,16 +261,38 @@
      [4] ∈ {116}
      [5..19] ∈ UNINITIALIZED
 [eva:final-states] Values at end of function wmemcpy:
-  buf[0] ∈ {72}
-     [1] ∈ {97}
-     [2] ∈ {121}
-     [3] ∈ {115}
-     [4] ∈ {116}
-     [5..19] ∈ UNINITIALIZED
+  buf[0..4] ∈ [--..--]
+     [5] ∈ {0} or UNINITIALIZED
+     [6..19] ∈ UNINITIALIZED
+  __malloc_wcsdup_l99[0] ∈ {65}
+                     [1] ∈ {66}
+                     [2] ∈ {67}
+                     [3] ∈ {0}
+  __malloc_wcsdup_l99_0[0] ∈ {65}
+                       [1] ∈ {66}
+                       [2] ∈ {67}
+                       [3] ∈ {0}
+[eva:final-states] Values at end of function wcsdup:
+  __fc_errno ∈ [--..--]
+  __fc_heap_status ∈ [--..--]
+  l ∈ {4}
+  p ∈ {{ NULL ; &__malloc_wcsdup_l99[0] ; &__malloc_wcsdup_l99_0[0] }}
+  __retres ∈
+          {{ NULL ; &__malloc_wcsdup_l99[0] ; &__malloc_wcsdup_l99_0[0] }}
+  __malloc_wcsdup_l99[0] ∈ {65}
+                     [1] ∈ {66}
+                     [2] ∈ {67}
+                     [3] ∈ {0}
+  __malloc_wcsdup_l99_0[0] ∈ {65}
+                       [1] ∈ {66}
+                       [2] ∈ {67}
+                       [3] ∈ {0}
 [eva:final-states] Values at end of function wmemset:
   buf[0..4] ∈ [--..--]
      [5..19] ∈ UNINITIALIZED
 [eva:final-states] Values at end of function main:
+  __fc_errno ∈ [--..--]
+  __fc_heap_status ∈ [--..--]
   sc1 ∈ {{ L"Needle" }}
   sc2 ∈ {{ L"Haystack" }}
   buf[0..4] ∈ [--..--] or UNINITIALIZED
@@ -267,4 +316,13 @@
   wcr ∈ {{ L"ABC" + {8} }}
   wmr1 ∈ {0}
   wmr2 ∈ {{ L"ABC" + {8} }}
+  dupbuf ∈ {{ NULL ; &__malloc_wcsdup_l99_0[0] }} or ESCAPINGADDR
   __retres ∈ {0}
+  __malloc_wcsdup_l99[0] ∈ {65}
+                     [1] ∈ {66}
+                     [2] ∈ {67}
+                     [3] ∈ {0}
+  __malloc_wcsdup_l99_0[0] ∈ {65}
+                       [1] ∈ {66}
+                       [2] ∈ {67}
+                       [3] ∈ {0}

tests/libc/wchar_c_h.c

@@ -69,6 +69,13 @@ int main() {
   wchar_t *wmr1 = wmemchr(wc, L'C', 2); // not found
   wchar_t *wmr2 = wmemchr(p, L'C', 2); // found
 
+#ifdef TEST_IMPLEMENTATION
+  wchar_t *dupbuf = wcsdup(wc);
+  if (!dupbuf) goto exit;
+  dupbuf = wcsdup(dupbuf); // memory leak
+  free(dupbuf);
+#endif
+
 exit:
   return 0;
 }