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/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index dadf77c4d5acc057bceabae2c0f4b6e742c24198..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,8 +40,8 @@
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 (414)
==============================
@@ -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);
@@ -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 = 498
- 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 1115f88c003d98c273476f68cafe718e0ad4c209..fd785f066330f5aec494ac26657707f3754da401 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -6975,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/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;
}