[Libc] add spec for wcscasecmp

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, ...);

src/plugins/variadic/tests/known/oracle/printf.res.oracle

-[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.

src/plugins/variadic/tests/known/oracle/swprintf.res.oracle

-[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.

src/plugins/variadic/tests/known/oracle/wchar.res.oracle

-[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.

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

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));

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}

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;
 }