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..dadf77c4d5acc057bceabae2c0f4b6e742c24198 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -43,7 +43,7 @@
    wcscpy (0 call); wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call);
    wmemcpy (0 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);
@@ -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)
   =======================================
@@ -195,7 +195,7 @@
   Goto = 97
   Assignment = 459
   Exit point = 83
-  Function = 497
+  Function = 498
   Function call = 93
   Pointer dereferencing = 159
   Cyclomatic complexity = 296
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index be0c42e75318b30374f12a8cf0c5bbd05ec53a3c..1115f88c003d98c273476f68cafe718e0ad4c209 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));
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_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;
 }