From c8704c5d961eb6aac3fa8577e0b13e99ff387b1f Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 9 Oct 2020 16:04:49 +0200
Subject: [PATCH] [eacsl] Update tests
---
.../tests/bts/oracle_ci/bts1398.res.oracle | 2 --
.../e-acsl/tests/bts/oracle_ci/gen_bts1398.c | 2 +-
.../memory/oracle_ci/constructor.res.oracle | 2 --
.../tests/memory/oracle_ci/gen_constructor.c | 4 +--
.../tests/memory/oracle_ci/gen_local_goto.c | 9 +++--
.../memory/oracle_ci/local_goto.res.oracle | 2 --
.../oracle_ci/e-acsl-instrument.res.oracle | 10 ------
.../special/oracle_ci/gen_e-acsl-instrument.c | 33 ++++++++++++-------
.../temporal/oracle_ci/gen_t_malloc-asan.c | 2 +-
9 files changed, 31 insertions(+), 35 deletions(-)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle
index 196be478e59..efd02631129 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle
@@ -1,4 +1,2 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/bts/bts1398.c:12: Warning:
- Neither code nor specification for function printf, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c
index 38075f91be9..b2502604424 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c
@@ -26,7 +26,7 @@ int main(void)
int i = 1;
t[0] = 1;
t[1] = 2;
- printf(__gen_e_acsl_literal_string,x,t[0],t[i]);
+ printf(__gen_e_acsl_literal_string,x,t[0],t[i]); /* printf_va_1 */
__retres = 0;
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle
index 850186d110a..efd02631129 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle
@@ -1,4 +1,2 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/memory/constructor.c:16: Warning:
- Neither code nor specification for function printf, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c
index 4e43d7e9cff..22920e30cf3 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c
@@ -7,7 +7,7 @@ char *__gen_e_acsl_literal_string;
void f(void) __attribute__((__constructor__));
void f(void)
{
- printf(__gen_e_acsl_literal_string);
+ printf(__gen_e_acsl_literal_string); /* printf_va_1 */
char *buf = malloc((unsigned long)10 * sizeof(char));
free((void *)buf);
return;
@@ -36,7 +36,7 @@ int main(void)
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_globals_init();
- printf(__gen_e_acsl_literal_string_2);
+ printf(__gen_e_acsl_literal_string_2); /* printf_va_2 */
__retres = 0;
__e_acsl_memory_clean();
return __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
index 81bdec60725..b21a6a07c3e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
@@ -40,7 +40,8 @@ int main(int argc, char const **argv)
int t = 0;
UP: ;
if (t == 2) {
- printf(__gen_e_acsl_literal_string_2,t,__gen_e_acsl_literal_string);
+ printf(__gen_e_acsl_literal_string_2,t,
+ (char *)__gen_e_acsl_literal_string); /* printf_va_1 */
goto RET;
}
AGAIN:
@@ -58,7 +59,8 @@ int main(int argc, char const **argv)
}
/*@ assert \valid(&a); */ ;
if (t == 2) {
- printf(__gen_e_acsl_literal_string_2,t,__gen_e_acsl_literal_string_3);
+ printf(__gen_e_acsl_literal_string_2,t,
+ (char *)__gen_e_acsl_literal_string_3); /* printf_va_2 */
__e_acsl_delete_block((void *)(& a));
goto UP;
}
@@ -74,7 +76,8 @@ int main(int argc, char const **argv)
"tests/memory/local_goto.c",36);
}
/*@ assert \valid(&b); */ ;
- printf(__gen_e_acsl_literal_string_2,t,__gen_e_acsl_literal_string_4);
+ printf(__gen_e_acsl_literal_string_2,t,
+ (char *)__gen_e_acsl_literal_string_4); /* printf_va_3 */
__e_acsl_delete_block((void *)(& a));
__e_acsl_delete_block((void *)(& b));
goto AGAIN;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle
index 142c3f2be01..efd02631129 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle
@@ -1,4 +1,2 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/memory/local_goto.c:37: Warning:
- Neither code nor specification for function printf, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-instrument.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-instrument.res.oracle
index 724a37c22bb..efd02631129 100644
--- a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-instrument.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-instrument.res.oracle
@@ -1,12 +1,2 @@
[e-acsl] beginning translation.
-[e-acsl] tests/special/e-acsl-instrument.c:58: Warning:
- ignoring effect of variadic function vol
[e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/special/e-acsl-instrument.c:43: Warning:
- Neither code nor specification for function __builtin_va_start, generating default assigns from the prototype
-[kernel:annot:missing-spec] tests/special/e-acsl-instrument.c:44: Warning:
- Neither code nor specification for function __builtin_va_arg, generating default assigns from the prototype
-[eva:alarm] tests/special/e-acsl-instrument.c:44: Warning:
- accessing uninitialized left-value.
- assert \initialized(&tmp);
- (tmp from vararg)
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-instrument.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-instrument.c
index 2ef9690828f..24fc369486b 100644
--- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-instrument.c
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-instrument.c
@@ -4,12 +4,6 @@
#include "stdio.h"
extern int __e_acsl_sound_verdict;
-/* compiler builtin:
- void __builtin_va_arg(__builtin_va_list, unsigned long, void *); */
-/* compiler builtin:
- void __builtin_va_end(__builtin_va_list); */
-/* compiler builtin:
- void __builtin_va_start(__builtin_va_list); */
int __gen_e_acsl_uninstrument1(int *p);
int uninstrument1(int *p)
@@ -68,17 +62,22 @@ int instrument2(int *p)
return __retres;
}
-int vol(int n , ...)
+int vol(int n, void * const *__va_params)
{
int __retres;
va_list vl;
int tmp;
- __builtin_va_start(vl,n);
- tmp = __builtin_va_arg (vl, int);
- /*@ assert Eva: initialization: \initialized(&tmp); */
+ __e_acsl_store_block((void *)(& vl),(size_t)8);
+ __e_acsl_store_block((void *)(& __va_params),(size_t)8);
+ __e_acsl_full_init((void *)(& vl));
+ vl = __va_params;
+ tmp = *((int *)*vl);
+ __e_acsl_full_init((void *)(& vl));
+ vl ++;
int r = tmp;
- __builtin_va_end(vl);
__retres = 0;
+ __e_acsl_delete_block((void *)(& __va_params));
+ __e_acsl_delete_block((void *)(& vl));
return __retres;
}
@@ -113,7 +112,17 @@ int main(void)
57);
}
/*@ assert \initialized(&y); */ ;
- tmp = vol(6,1);
+ {
+ int __va_arg0 = 1;
+ __e_acsl_store_block((void *)(& __va_arg0),(size_t)4);
+ __e_acsl_full_init((void *)(& __va_arg0));
+ void *__va_args[1] = {& __va_arg0};
+ __e_acsl_store_block((void *)(__va_args),(size_t)8);
+ __e_acsl_full_init((void *)(& __va_args));
+ tmp = vol(6,(void * const *)(__va_args));
+ __e_acsl_delete_block((void *)(& __va_arg0));
+ __e_acsl_delete_block((void *)(__va_args));
+ }
__e_acsl_delete_block((void *)(& y));
__e_acsl_delete_block((void *)(& x));
__e_acsl_memory_clean();
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc-asan.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc-asan.c
index 670764770e9..d718f3e61f8 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc-asan.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc-asan.c
@@ -58,7 +58,7 @@ int main(void)
__e_acsl_temporal_reset_parameters();
__e_acsl_temporal_reset_return();
__e_acsl_temporal_save_nreferent_parameter((void *)(& p),1U);
- printf(__gen_e_acsl_literal_string,p,counter);
+ printf(__gen_e_acsl_literal_string,(void *)p,counter); /* printf_va_1 */
break;
}
__e_acsl_full_init((void *)(& p));
--
GitLab