[tests] update oracles

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

@@ -617,8 +617,8 @@ int main(void)
   size_t z;
   ptrdiff_t t;
   char *string = (char *)"Hello world !\n";
-  wchar_t *wstring = L"H" "e" "l" "l" "o" " " "w" "o" "r" "l" "d" " " "!"
-    "\\n" ;
+  wchar_t *wstring = (wchar_t *)L"H" "e" "l" "l" "o" " " "w" "o" "r" "l" "d"
+    " " "!" "\\n" ;
   char c = (char)'4';
   unsigned char uhh = (unsigned char)42;
   unsigned short uh = (unsigned short)42;

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

@@ -139,7 +139,7 @@ int main(void)
   short tt;
   unsigned int ui = (unsigned int)42;
   char *string = (char *)"foo";
-  wchar_t *wstring = L"b" "a" "r" ;
+  wchar_t *wstring = (wchar_t *)L"b" "a" "r" ;
   int volatile nondet = 0;
   switch (nondet) {
     case 0: printf("%n",(int *)(& tt)); /* printf_va_1 */

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

@@ -105,11 +105,11 @@ int main(void)
   if (nondet) {
     size_t tmp;
     tmp = wcslen((wchar_t const *)(data));
-    swprintf(dest,tmp,(wchar_t const *)L"%" "l" "s" ,data); /* swprintf_va_1 */
+    swprintf(dest,tmp,L"%" "l" "s" ,data); /* swprintf_va_1 */
     /*@ assert \false; */ ;
   }
   tmp_0 = wcslen((wchar_t const *)(data));
-  swprintf(dest,tmp_0 / (size_t)2,(wchar_t const *)L"%" "l" "s" ,data); /* swprintf_va_2 */
+  swprintf(dest,tmp_0 / (size_t)2,L"%" "l" "s" ,data); /* swprintf_va_2 */
   __retres = 0;
   return __retres;
 }

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

@@ -256,21 +256,20 @@ int main(void)
   int j;
   wchar_t input[0x100] =
     {102, 111, 114, 116, 121, 45, 116, 119, 111, 32, 105, 115, 0};
-  wprintf((wchar_t const *)L"%" "d" " " "%" "l" "d" "\\n" ,42,42L); /* wprintf_va_1 */
-  wprintf((wchar_t const *)L"%" "1" "0" "d" " " "%" "0" "1" "0" "d" "\\n" ,
-          42,42); /* wprintf_va_2 */
-  wprintf((wchar_t const *)L"%" "d" " " "%" "x" " " "%" "o" " " "%" "#" "x"
-          " " "%" "#" "o" "\\n" ,42,42u,42u,42u,42u); /* wprintf_va_3 */
-  wprintf((wchar_t const *)L"%" "2" "." "1" "f" " " "%" "+" "." "0" "e" " "
-          "%" "E" "\\n" ,42.0,42.0,42.0); /* wprintf_va_4 */
-  wprintf((wchar_t const *)L"%" "*" "d" " " "\\n" ,4,2); /* wprintf_va_5 */
-  wprintf((wchar_t const *)L"%" "l" "s" " " "\\n" ,L"4" "2" ); /* wprintf_va_6 */
-  swprintf(wstring,(size_t)0x100,(wchar_t const *)L"%" "s" " " "=" " " "%"
-           "d" ,(char *)L"4" "2" " " "+" " " "4" "2" ,42 + 42); /* swprintf_va_1 */
-  wscanf((wchar_t const *)L"%" "l" "s" ,wstring); /* wscanf_va_1 */
-  wscanf((wchar_t const *)L"%" "d" " " "%" "d" ,& i,& j); /* wscanf_va_2 */
-  swscanf((wchar_t const *)(input),(wchar_t const *)L"%" "l" "s" " " "%" "*"
-          "s" " " "%" "d" ,wstring,& i); /* swscanf_va_1 */
+  wprintf(L"%" "d" " " "%" "l" "d" "\\n" ,42,42L); /* wprintf_va_1 */
+  wprintf(L"%" "1" "0" "d" " " "%" "0" "1" "0" "d" "\\n" ,42,42); /* wprintf_va_2 */
+  wprintf(L"%" "d" " " "%" "x" " " "%" "o" " " "%" "#" "x" " " "%" "#" "o"
+          "\\n" ,42,42u,42u,42u,42u); /* wprintf_va_3 */
+  wprintf(L"%" "2" "." "1" "f" " " "%" "+" "." "0" "e" " " "%" "E" "\\n" ,
+          42.0,42.0,42.0); /* wprintf_va_4 */
+  wprintf(L"%" "*" "d" " " "\\n" ,4,2); /* wprintf_va_5 */
+  wprintf(L"%" "l" "s" " " "\\n" ,(wchar_t *)L"4" "2" ); /* wprintf_va_6 */
+  swprintf(wstring,(size_t)0x100,L"%" "s" " " "=" " " "%" "d" ,(char *)L"4"
+           "2" " " "+" " " "4" "2" ,42 + 42); /* swprintf_va_1 */
+  wscanf(L"%" "l" "s" ,wstring); /* wscanf_va_1 */
+  wscanf(L"%" "d" " " "%" "d" ,& i,& j); /* wscanf_va_2 */
+  swscanf((wchar_t const *)(input),L"%" "l" "s" " " "%" "*" "s" " " "%" "d" ,
+          wstring,& i); /* swscanf_va_1 */
   __retres = 0;
   return __retres;
 }

tests/libc/oracle/fc_libc.1.res.oracle

 [kernel] Parsing fc_libc.c (with preprocessing)
 /* Generated by Frama-C */
 typedef unsigned int size_t;
-typedef int wchar_t;
+typedef long wchar_t;
 struct __fc_div_t {
    int quot ;
    int rem ;
@@ -773,7 +773,7 @@ axiomatic WMemChr {
   
   axiom wmemchr_def{L}:
     ∀ wchar_t *s;
-    ∀ int c;
+    ∀ long c;
     ∀ ℤ n;
       wmemchr(s, c, n) ≡ \true ⇔
       (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c);
@@ -8677,11 +8677,11 @@ wchar_t *wcscpy(wchar_t *dest, wchar_t const *src)
 {
   size_t i;
   i = (size_t)0;
-  while (*(src + i) != 0) {
+  while (*(src + i) != 0L) {
     *(dest + i) = *(src + i);
     i ++;
   }
-  *(dest + i) = 0;
+  *(dest + i) = 0L;
   return dest;
 }
 
@@ -8694,7 +8694,7 @@ size_t wcslen(wchar_t const *str)
 {
   size_t i;
   i = (size_t)0;
-  while (*(str + i) != 0) i ++;
+  while (*(str + i) != 0L) i ++;
   return i;
 }
 
@@ -8716,11 +8716,11 @@ wchar_t *wcsncpy(wchar_t *dest, wchar_t const *src, size_t n)
   i = (size_t)0;
   while (i < n) {
     *(dest + i) = *(src + i);
-    if (*(src + i) == 0) break;
+    if (*(src + i) == 0L) break;
     i ++;
   }
   while (i < n) {
-    *(dest + i) = 0;
+    *(dest + i) = 0L;
     i ++;
   }
   return dest;
@@ -8748,11 +8748,11 @@ wchar_t *wcscat(wchar_t *dest, wchar_t const *src)
   size_t i;
   size_t n = wcslen((wchar_t const *)dest);
   i = (size_t)0;
-  while (*(src + i) != 0) {
+  while (*(src + i) != 0L) {
     *(dest + (n + i)) = *(src + i);
     i ++;
   }
-  *(dest + (n + i)) = 0;
+  *(dest + (n + i)) = 0L;
   return dest;
 }
 
@@ -8780,13 +8780,13 @@ wchar_t *wcsncat(wchar_t *dest, wchar_t const *src, size_t n)
   i = (size_t)0;
   while (1) {
     if (i < n) {
-      if (! (*(src + i) != 0)) break;
+      if (! (*(src + i) != 0L)) break;
     }
     else break;
     *(dest + (dest_len + i)) = *(src + i);
     i ++;
   }
-  *(dest + (dest_len + i)) = 0;
+  *(dest + (dest_len + i)) = 0L;
   return dest;
 }