[libc] add specification for wcsdup

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

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 =

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}

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