diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle index 7ee761f24d504c42269186b8ff7fffa29191c376..00c76b71477fdad6d9d4d065bb46b1cb38d82ea7 100644 --- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle +++ b/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; diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle index 61261c69b7f3e3af3676c8f2ecadcda889a2b9fa..9a98767e77768581ae88fd9ab8c72c787968a65c 100644 --- a/src/plugins/variadic/tests/known/oracle/printf_wrong_pointers.res.oracle +++ b/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 */ diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle index c31c436e505d57cd2728188cdb8bad388f31249d..8af3312245852398624861dd9ce724d859bdcd50 100644 --- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle +++ b/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; } diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle index f1a366040cbd837b60f664d8e632a2e5128fd36d..2a071e17fd01fd098b3e9d9afa7497d698bf87a0 100644 --- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle +++ b/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; } diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle index c06fe39d324009a48386b8d03101495e7bc319c6..6e0aac24eebd8a40cde965a90339724619618942 100644 --- a/tests/libc/oracle/fc_libc.1.res.oracle +++ b/tests/libc/oracle/fc_libc.1.res.oracle @@ -1,7 +1,7 @@ [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; }