diff --git a/share/libc/wchar.h b/share/libc/wchar.h
index 2a263e502a834526b56fe23340f29346ffc8c9de..645abea737132a24d40e31d66af9f8b5bd3f5263 100644
--- a/share/libc/wchar.h
+++ b/share/libc/wchar.h
@@ -267,6 +267,25 @@ extern wchar_t *fgetws(wchar_t * restrict ws, int n, FILE * restrict stream);
 */
 extern int wcscasecmp(const wchar_t *ws1, const wchar_t *ws2);
 
+/*@
+  requires valid_wstring: valid_read_wstring(ws);
+  allocates \result;
+  assigns \result \from indirect:ws[0..wcslen(ws)], indirect:__fc_heap_status;
+  behavior allocation:
+    assumes can_allocate: is_allocable(wcslen(ws));
+    assigns __fc_heap_status \from indirect:ws, __fc_heap_status;
+    assigns \result \from indirect:ws[0..wcslen(ws)], indirect:__fc_heap_status;
+    ensures allocation: \fresh(\result,wcslen(ws) * sizeof(wchar_t));
+    ensures result_valid_string_and_same_contents:
+      valid_wstring(\result) && wcscmp(\result,ws) == 0;
+  behavior no_allocation:
+    assumes cannot_allocate: !is_allocable(wcslen(ws));
+    assigns \result \from \nothing;
+    allocates \nothing;
+    ensures result_null: \result == \null;
+*/
+extern wchar_t *wcsdup(const wchar_t *ws);
+
 /* 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/eva/utils/library_functions.ml b/src/plugins/eva/utils/library_functions.ml
index f0772345006d14cfb4d73e05130cc94ce3a31aea..6f019013f462ebfd00c5aa00bcebdd5f74de1419 100644
--- a/src/plugins/eva/utils/library_functions.ml
+++ b/src/plugins/eva/utils/library_functions.ml
@@ -90,6 +90,7 @@ let unsupported_specifications =
     "strerror", "string.c";
     "strndup", "string.c";
     "unsetenv", "stdlib.c";
+    "wcsdup", "wchar.c";
   ]
 
 let unsupported_specs_tbl =
diff --git a/tests/libc/oracle/wchar_h.res.oracle b/tests/libc/oracle/wchar_h.res.oracle
index 57c7ffada801b0c69bad2cf9b86f6757a672241e..b11bedc26e32b1bd658d42c38a85bc2ad45daa82 100644
--- a/tests/libc/oracle/wchar_h.res.oracle
+++ b/tests/libc/oracle/wchar_h.res.oracle
@@ -192,6 +192,19 @@
 [eva] wchar_h.c:71: 
   function wcscasecmp: precondition 'valid_wstring_ws2' got status valid.
 [eva] Done for function wcscasecmp
+[eva] computing for function wcsdup <- main.
+  Called from wchar_h.c:73.
+[eva] using specification for function wcsdup
+[eva:libc:unsupported-spec] wchar_h.c:73: Warning: 
+  The specification of function 'wcsdup' is currently not supported by Eva.
+  Consider adding 'FRAMAC_SHARE/libc/wchar.c' to the analyzed source files.
+[eva] wchar_h.c:73: Warning: ignoring unsupported allocates clause
+[eva] wchar_h.c:73: 
+  function wcsdup: precondition 'valid_wstring' got status valid.
+[eva] Done for function wcsdup
+[eva] wchar_h.c:74: 
+  cannot evaluate ACSL term, unsupported ACSL construct: wide constant strings
+[eva:alarm] wchar_h.c:74: Warning: check got status unknown.
 [eva] Recording results for main
 [eva] Done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -209,4 +222,5 @@
        [10] ∈ {0} or UNINITIALIZED
        [11..19] ∈ [--..--] or UNINITIALIZED
   ir ∈ [--..--] or UNINITIALIZED
+  ws ∈ [--..--] or UNINITIALIZED
   __retres ∈ {0; 1}
diff --git a/tests/libc/wchar_h.c b/tests/libc/wchar_h.c
index c0780e750592fb13d44b882251214dd8d1a7a096..20c963ecb30d8d627980e7188515bcc730ec4f3f 100644
--- a/tests/libc/wchar_h.c
+++ b/tests/libc/wchar_h.c
@@ -69,5 +69,8 @@ int main() {
 
   int ir = wcscasecmp(L"\0", L"\0");
   ir = wcscasecmp(wsrc, L"\0");
+
+  wchar_t *ws = wcsdup(L"Wide thing"); // imprecise: allocates unsupported
+  //@ check wcslen(ws) == wcslen(L"Wide thing");
   return 0;
 }