From 2d5063b61e2b0464445c9d7a1cc87da88026fd61 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 10 Dec 2020 15:52:40 +0100
Subject: [PATCH] [variadic] Update tests for new default machdep
---
.../defined/oracle/multiple-va_start.res.oracle | 2 +-
.../variadic/tests/defined/oracle/va_copy.res.oracle | 2 +-
.../variadic/tests/known/oracle/printf.res.oracle | 12 ++++++------
.../tests/known/oracle/printf_garbled_mix.res.oracle | 6 +++---
.../tests/known/oracle/printf_wrong_types.res.oracle | 8 ++++++++
.../variadic/tests/known/oracle/snprintf.res.oracle | 2 +-
.../variadic/tests/known/oracle/swprintf.res.oracle | 2 +-
.../variadic/tests/known/oracle/wchar.res.oracle | 2 +-
8 files changed, 22 insertions(+), 14 deletions(-)
diff --git a/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle b/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle
index 7369a68d0b2..8b7c3751760 100644
--- a/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/multiple-va_start.res.oracle
@@ -53,7 +53,7 @@ int *pack(int first, void * const *__va_params)
if (! tmp) break;
size ++;
}
- ret = (int *)malloc(sizeof(int) * (unsigned int)(size + 1));
+ ret = (int *)malloc(sizeof(int) * (unsigned long)(size + 1));
*(ret + 0) = first;
list = __va_params;
i = 0;
diff --git a/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle b/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle
index 83a0ba4f9cf..f67c309b1b9 100644
--- a/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/va_copy.res.oracle
@@ -54,7 +54,7 @@ int *pack(int first, void * const *__va_params)
if (! tmp) break;
size ++;
}
- ret = (int *)malloc(sizeof(int) * (unsigned int)(size + 1));
+ ret = (int *)malloc(sizeof(int) * (unsigned long)(size + 1));
*(ret + 0) = first;
i = 0;
while (i < size) {
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index 5dfc5110fbc..cac34c3b811 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -468,7 +468,7 @@ int printf_va_18(char const * __restrict format, size_t param0,
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_19(char const * __restrict format, unsigned long long param0);
+int printf_va_19(char const * __restrict format, unsigned long param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -494,7 +494,7 @@ int printf_va_20(char const * __restrict format, int param0);
__fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
param0;
*/
-int printf_va_21(char const * __restrict format, unsigned long long param0);
+int printf_va_21(char const * __restrict format, unsigned long param0);
/*@ requires valid_read_string(format);
assigns \result, __fc_stdout->__fc_FILE_data;
@@ -617,9 +617,9 @@ int main(void)
uintmax_t uj = (unsigned long long)42;
double f = (double)42.0f;
long double L = 42.0l;
- uint64_t u64 = (unsigned long long)42ul;
+ uint64_t u64 = 42ul;
int8_t i8 = (signed char)42;
- uint_least64_t uleast64 = (unsigned long long)42u;
+ uint_least64_t uleast64 = (unsigned long)42u;
int_fast32_t ifast32 = 42;
printf("Hello world !\n"); /* printf_va_1 */
printf("%s%n",string,& i); /* printf_va_2 */
@@ -639,9 +639,9 @@ int main(void)
printf("%llu ",ull); /* printf_va_16 */
printf("%jo ",uj); /* printf_va_17 */
printf("%zx %tX\n",z,t); /* printf_va_18 */
- printf("%llu",u64); /* printf_va_19 */
+ printf("%lu",u64); /* printf_va_19 */
printf("%hhi",(int)i8); /* printf_va_20 */
- printf("%llx",uleast64); /* printf_va_21 */
+ printf("%lx",uleast64); /* printf_va_21 */
printf("%d",ifast32); /* printf_va_22 */
printf("%f %Le\n",f,L); /* printf_va_23 */
printf("%c\n",(int)c); /* printf_va_24 */
diff --git a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
index 18e29885565..3cecd8f9b1e 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_garbled_mix.res.oracle
@@ -26,7 +26,7 @@
The imprecision originates from Arithmetic
{tests/known/printf_garbled_mix.c:6}
[eva:alarm] tests/known/printf_garbled_mix.c:7: Warning:
- pointer downcast. assert (unsigned int)b ≤ 2147483647;
+ pointer downcast. assert (unsigned long)b ≤ 2147483647;
[eva] using specification for function printf_va_1
[eva] tests/known/printf_garbled_mix.c:8:
Frama_C_show_each_nb_printed: [-2147483648..2147483647]
@@ -68,8 +68,8 @@ int printf_va_1(char const * __restrict format, int param0);
void main(void)
{
int a[2] = {1, 2};
- int *b = (int *)((unsigned int)(a) * (unsigned int)2);
- /*@ assert Eva: pointer_downcast: (unsigned int)b ≤ 2147483647; */
+ int *b = (int *)((unsigned long)(a) * (unsigned long)2);
+ /*@ assert Eva: pointer_downcast: (unsigned long)b ≤ 2147483647; */
int nb_printed = printf_va_1("%d",(int)b);
Frama_C_show_each_nb_printed(nb_printed);
b = (int *)0;
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
index e7804a787db..a9e71214ada 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
@@ -438,12 +438,20 @@ int main(void)
Incorrect type for argument 2. The argument will be cast from int to unsigned int.
[variadic] tests/known/printf_wrong_types.c:21:
Translating call to printf to a call to the specialized version printf_va_4.
+[variadic] tests/known/printf_wrong_types.c:21: Warning:
+ Incorrect type for argument 2. The argument will be cast from int to long.
[variadic] tests/known/printf_wrong_types.c:22:
Translating call to printf to a call to the specialized version printf_va_5.
+[variadic] tests/known/printf_wrong_types.c:22: Warning:
+ Incorrect type for argument 2. The argument will be cast from long to int.
[variadic] tests/known/printf_wrong_types.c:23:
Translating call to printf to a call to the specialized version printf_va_6.
+[variadic] tests/known/printf_wrong_types.c:23: Warning:
+ Incorrect type for argument 2. The argument will be cast from unsigned int to unsigned long.
[variadic] tests/known/printf_wrong_types.c:24:
Translating call to printf to a call to the specialized version printf_va_7.
+[variadic] tests/known/printf_wrong_types.c:24: Warning:
+ Incorrect type for argument 2. The argument will be cast from unsigned long to unsigned int.
[variadic] tests/known/printf_wrong_types.c:25:
Translating call to printf to a call to the specialized version printf_va_8.
[variadic] tests/known/printf_wrong_types.c:25: Warning:
diff --git a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
index e8e49846730..a55e9b9b905 100644
--- a/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/snprintf.res.oracle
@@ -84,7 +84,7 @@ int main(void)
int __retres;
char data[100];
size_t tmp_0;
- memset((void *)(data),'A',(unsigned int)99);
+ memset((void *)(data),'A',(unsigned long)99);
data[99] = (char)0;
char dest[50] = {(char)'\000'};
if (nondet) {
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index 338a605bafc..505fe9d8346 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -97,7 +97,7 @@ int main(void)
int __retres;
wchar_t data[100];
size_t tmp_0;
- wmemset(data,65,(unsigned int)99);
+ wmemset(data,65,(unsigned long)99);
data[99] = 0;
wchar_t dest[50] = {0};
if (nondet) {
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index 631396fece9..b0188cdf152 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -263,7 +263,7 @@ int main(void)
"%" "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" ,(wchar_t *)L"4" "2" ); /* wprintf_va_6 */
- swprintf(wstring,(unsigned int)0x100,(wchar_t const *)L"%" "s" " " "=" " "
+ swprintf(wstring,(unsigned long)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 */
--
GitLab