diff --git a/share/libc/wchar.c b/share/libc/wchar.c
index 565670186d0b76f467493a536e37e8d950cde592..15d80f10324eb435887f55f3388dc7a8eb86796e 100644
--- a/share/libc/wchar.c
+++ b/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
diff --git a/share/libc/wchar.h b/share/libc/wchar.h
index 5ea6aa80e83353e559c1f2fec72ba6504d6ab0c5..bb8a4b6fd455aea9f79cfdf506026d5e00903d92 100644
--- a/share/libc/wchar.h
+++ b/share/libc/wchar.h
@@ -260,6 +260,13 @@ extern wchar_t *fgetws(wchar_t * restrict ws, int n, FILE * restrict stream);
   }
 */
 
+/*@
+  requires valid_wstring_ws1: valid_read_wstring(ws1);
+  requires valid_wstring_ws2: valid_read_wstring(ws2);
+  assigns \result \from indirect:ws1[0..], indirect:ws2[0..];
+*/
+extern int wcscasecmp(const wchar_t *ws1, const wchar_t *ws2);
+
 /* It is unclear whether these are more often in wchar.h or stdio.h */
 
 extern int fwprintf(FILE * stream, const wchar_t * format, ...);
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index cac34c3b81106e48fc46ce258937ba54cea5230e..b8b4149310dcfd70df60ca7b42a8bfa05e53588e 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:265: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:272: 
   Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:267: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:274: 
   Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:269: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:276: 
   Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:272: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:279: 
   Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:274: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:281: 
   Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:276: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:283: 
   Declaration of variadic function swscanf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index 505fe9d8346afc035f367aaf1005fad87644e19c..326508d6ec1331114c74ad831beef0dcf890958c 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:265: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:272: 
   Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:267: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:274: 
   Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:269: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:276: 
   Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:272: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:279: 
   Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:274: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:281: 
   Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:276: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:283: 
   Declaration of variadic function swscanf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index b0188cdf1525b78c8f76532497dad499c2bfd2ff..fb03056d82e92a3bd583652a7ce2d7835c903477 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:265: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:272: 
   Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:267: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:274: 
   Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:269: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:276: 
   Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:272: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:279: 
   Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:274: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:281: 
   Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:276: 
+[variadic] FRAMAC_SHARE/libc/wchar.h:283: 
   Declaration of variadic function swscanf.
 [variadic] FRAMAC_SHARE/libc/stdio.h:207: 
   Declaration of variadic function fprintf.
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 9cd8d6f3657ff4f090b9d78bd2d0916e9644b61e..5ba9d6cd179e271e66d7029f2bbe88fa4b466efe 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/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,10 +40,10 @@
    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 (413)
+  Specified-only functions (414)
   ==============================
    FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
    Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -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);
@@ -163,11 +163,11 @@
    ungetc (0 call); unlink (0 call); usleep (0 call); utimes (0 call);
    vfprintf (0 call); vfscanf (0 call); vprintf (0 call); vscanf (0 call);
    vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call); wait (0 call);
-   waitpid (0 call); wcschr (0 call); wcscmp (0 call); wcscspn (0 call);
-   wcslcat (0 call); wcslcpy (0 call); wcsncmp (0 call); wcspbrk (0 call);
-   wcsrchr (0 call); wcsspn (0 call); wcsstr (0 call); wcstombs (0 call);
-   wctomb (0 call); wmemchr (0 call); wmemcmp (0 call); wmemmove (0 call);
-   write (0 call); 
+   waitpid (0 call); wcscasecmp (0 call); wcschr (0 call); wcscmp (0 call);
+   wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call); wcsncmp (0 call);
+   wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call); wcsstr (0 call);
+   wcstombs (0 call); wctomb (0 call); wmemchr (0 call); wmemcmp (0 call);
+   wmemmove (0 call); write (0 call); 
   
   Undefined and unspecified functions (1)
   =======================================
@@ -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 = 497
-  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"
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index be0c42e75318b30374f12a8cf0c5bbd05ec53a3c..fd785f066330f5aec494ac26657707f3754da401 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -6789,6 +6789,14 @@ extern wchar_t *fgetws(wchar_t * __restrict ws, int n,
       }
 
 */
+/*@ requires valid_wstring_ws1: valid_read_wstring(ws1);
+    requires valid_wstring_ws2: valid_read_wstring(ws2);
+    assigns \result;
+    assigns \result
+      \from (indirect: *(ws1 + (0 ..))), (indirect: *(ws2 + (0 ..)));
+ */
+extern int wcscasecmp(wchar_t const *ws1, wchar_t const *ws2);
+
 /*@ requires
       valid_dest:
         valid_or_empty((void *)dest, (unsigned int)(sizeof(wchar_t) * n));
@@ -6967,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));
diff --git a/tests/libc/oracle/wchar_c_h.0.res.oracle b/tests/libc/oracle/wchar_c_h.0.res.oracle
index bf7be7856c70d4995356619b9b5d331ff8a39e68..c03089cbb4c3912c5900092bb203abd7919ae444 100644
--- a/tests/libc/oracle/wchar_c_h.0.res.oracle
+++ b/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}
diff --git a/tests/libc/oracle/wchar_h.res.oracle b/tests/libc/oracle/wchar_h.res.oracle
index bf863d20cc98ba05b724a972dbc48a76447e3120..e224ff4e25b18074e7af8fcc120c1760d9f16eb1 100644
--- a/tests/libc/oracle/wchar_h.res.oracle
+++ b/tests/libc/oracle/wchar_h.res.oracle
@@ -185,6 +185,21 @@
 [eva] tests/libc/wchar_h.c:66: 
   function wcsncat: no state left, precondition 'separation' got status valid.
 [eva] Done for function wcsncat
+[eva] computing for function wcscasecmp <- main.
+  Called from tests/libc/wchar_h.c:70.
+[eva] using specification for function wcscasecmp
+[eva] tests/libc/wchar_h.c:70: 
+  function wcscasecmp: precondition 'valid_wstring_ws1' got status valid.
+[eva] tests/libc/wchar_h.c:70: 
+  function wcscasecmp: precondition 'valid_wstring_ws2' got status valid.
+[eva] Done for function wcscasecmp
+[eva] computing for function wcscasecmp <- main.
+  Called from tests/libc/wchar_h.c:71.
+[eva] tests/libc/wchar_h.c:71: 
+  function wcscasecmp: precondition 'valid_wstring_ws1' got status valid.
+[eva] tests/libc/wchar_h.c:71: 
+  function wcscasecmp: precondition 'valid_wstring_ws2' got status valid.
+[eva] Done for function wcscasecmp
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -201,4 +216,5 @@
   wdst2[0..9] ∈ {65}
        [10] ∈ {0}
        [11..19] ∈ [--..--]
+  ir ∈ [--..--]
   __retres ∈ {0; 1}
diff --git a/tests/libc/wchar_c_h.c b/tests/libc/wchar_c_h.c
index 8dadb46e2f8bf6ed9d7b3339bb0b193e6a4a08b8..0baf530c850383431efbda23cdbb51e574f09d05 100644
--- a/tests/libc/wchar_c_h.c
+++ b/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;
 }
diff --git a/tests/libc/wchar_h.c b/tests/libc/wchar_h.c
index e7cb493fa75d8adf0b06af406ebdf64c38dd3463..3bde71c8dc721489453c79ddf683c6dbbba409c3 100644
--- a/tests/libc/wchar_h.c
+++ b/tests/libc/wchar_h.c
@@ -66,5 +66,8 @@ int main() {
     wcsncat(wdst2+10, wdst2, 10); // error: no separation
     //@ assert unreachable:\false;
   }
+
+  int ir = wcscasecmp(L"\0", L"\0");
+  ir = wcscasecmp(wsrc, L"\0");
   return 0;
 }