From d3a6265c1f168cc8631eea74ceb90a89dd851e88 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 3 Sep 2020 15:39:13 +0200
Subject: [PATCH] [eacsl] Update tests

---
 .../e-acsl/tests/arith/oracle_ci/gen_arith.c  |   2 +-
 .../e-acsl/tests/arith/oracle_ci/gen_array.c  |   2 +-
 .../e-acsl/tests/arith/oracle_ci/gen_at.c     |   2 +-
 .../gen_at_on-purely-logic-variables.c        |   2 +-
 .../tests/arith/oracle_ci/gen_bitwise.c       |   2 +-
 .../e-acsl/tests/arith/oracle_ci/gen_cast.c   |   2 +-
 .../tests/arith/oracle_ci/gen_comparison.c    |   2 +-
 .../tests/arith/oracle_ci/gen_functions.c     |   2 +-
 .../tests/arith/oracle_ci/gen_functions_rec.c |   2 +-
 .../arith/oracle_ci/gen_integer_constant.c    |   2 +-
 .../e-acsl/tests/arith/oracle_ci/gen_let.c    |   2 +-
 .../tests/arith/oracle_ci/gen_longlong.c      |   2 +-
 .../e-acsl/tests/arith/oracle_ci/gen_not.c    |   2 +-
 .../tests/arith/oracle_ci/gen_quantif.c       |   2 +-
 .../tests/arith/oracle_ci/gen_rationals.c     |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_bts1304.c  |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_bts1307.c  |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_bts1324.c  |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_bts1326.c  |   2 +-
 .../oracle_ci/gen_bts1386_complex_flowgraph.c |   1 -
 .../e-acsl/tests/bts/oracle_ci/gen_bts1390.c  |   1 +
 .../e-acsl/tests/bts/oracle_ci/gen_bts1395.c  |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_bts1398.c  |   1 -
 .../e-acsl/tests/bts/oracle_ci/gen_bts1399.c  |   1 +
 .../e-acsl/tests/bts/oracle_ci/gen_bts1478.c  |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_bts1700.c  |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_bts1717.c  |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_bts1718.c  |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_bts1740.c  |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_bts1837.c  |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_bts2191.c  |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_bts2192.c  |   1 +
 .../e-acsl/tests/bts/oracle_ci/gen_bts2231.c  |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_bts2252.c  |   1 +
 .../e-acsl/tests/bts/oracle_ci/gen_bts2305.c  |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_bts2386.c  |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_bts2406.c  |   2 +-
 .../tests/bts/oracle_ci/gen_issue-eacsl-105.c |   2 +-
 .../tests/bts/oracle_ci/gen_issue-eacsl-91.c  |   2 +-
 .../e-acsl/tests/bts/oracle_ci/gen_issue69.c  |   2 +-
 .../tests/constructs/oracle_ci/gen_false.c    |   2 +-
 .../oracle_ci/gen_function_contract.c         |   2 +-
 .../tests/constructs/oracle_ci/gen_ghost.c    |   2 +-
 .../constructs/oracle_ci/gen_invariant.c      |   2 +-
 .../constructs/oracle_ci/gen_labeled_stmt.c   |   2 +-
 .../tests/constructs/oracle_ci/gen_lazy.c     |   2 +-
 .../tests/constructs/oracle_ci/gen_loop.c     |   2 +-
 .../oracle_ci/gen_nested_code_annot.c         |   2 +-
 .../tests/constructs/oracle_ci/gen_result.c   |   2 +-
 .../constructs/oracle_ci/gen_stmt_contract.c  |   2 +-
 .../tests/constructs/oracle_ci/gen_true.c     |   2 +-
 .../tests/constructs/oracle_ci/gen_typedef.c  |   2 +-
 .../oracle_ci/gen_functions_contiki.c         |   1 +
 .../examples/oracle_ci/gen_linear_search.c    |   2 +-
 .../tests/format/oracle_ci/fprintf.res.oracle |  15 +-
 .../tests/format/oracle_ci/gen_fprintf.c      |   1 +
 .../format/oracle_dev/printf.e-acsl.err.log   | 255 ++++++------------
 .../full-mtracking/oracle_ci/gen_addrOf.c     |   2 +-
 .../tests/gmp-only/oracle_ci/gen_arith.c      |   2 +-
 .../tests/gmp-only/oracle_ci/gen_functions.c  |   2 +-
 .../tests/memory/oracle_ci/gen_addrOf.c       |   2 +-
 .../e-acsl/tests/memory/oracle_ci/gen_alias.c |   2 +-
 .../tests/memory/oracle_ci/gen_base_addr.c    |   1 +
 .../tests/memory/oracle_ci/gen_block_length.c |   1 +
 .../tests/memory/oracle_ci/gen_block_valid.c  |   1 +
 .../tests/memory/oracle_ci/gen_bypassed_var.c |   2 +-
 .../e-acsl/tests/memory/oracle_ci/gen_call.c  |   1 +
 .../oracle_ci/gen_compound_initializers.c     |   2 +-
 .../tests/memory/oracle_ci/gen_ctype_macros.c |   2 +-
 .../memory/oracle_ci/gen_decl_in_switch.c     |   2 +-
 .../tests/memory/oracle_ci/gen_early_exit.c   |   2 +-
 .../tests/memory/oracle_ci/gen_freeable.c     |   1 +
 .../memory/oracle_ci/gen_ghost_parameters.c   |   2 +-
 .../e-acsl/tests/memory/oracle_ci/gen_goto.c  |   2 +-
 .../memory/oracle_ci/gen_hidden_malloc.c      |   1 +
 .../e-acsl/tests/memory/oracle_ci/gen_init.c  |   2 +-
 .../memory/oracle_ci/gen_init_function.c      |   1 +
 .../tests/memory/oracle_ci/gen_initialized.c  |   1 +
 .../memory/oracle_ci/gen_literal_string.c     |   2 +-
 .../tests/memory/oracle_ci/gen_local_goto.c   |   1 -
 .../tests/memory/oracle_ci/gen_local_init.c   |   2 +-
 .../tests/memory/oracle_ci/gen_local_var.c    |   1 +
 .../tests/memory/oracle_ci/gen_mainargs.c     |   1 -
 .../tests/memory/oracle_ci/gen_memalign.c     |   1 +
 .../tests/memory/oracle_ci/gen_memsize.c      |   1 +
 .../e-acsl/tests/memory/oracle_ci/gen_null.c  |   2 +-
 .../tests/memory/oracle_ci/gen_offset.c       |   1 +
 .../memory/oracle_ci/gen_other_constants.c    |   2 +-
 .../e-acsl/tests/memory/oracle_ci/gen_ptr.c   |   2 +-
 .../tests/memory/oracle_ci/gen_ptr_init.c     |   1 +
 .../memory/oracle_ci/gen_ranges_in_builtins.c |   1 +
 .../tests/memory/oracle_ci/gen_sizeof.c       |   2 +-
 .../tests/memory/oracle_ci/gen_stdout.c       |   1 -
 .../e-acsl/tests/memory/oracle_ci/gen_valid.c |   1 +
 .../tests/memory/oracle_ci/gen_valid_alias.c  |   1 +
 .../memory/oracle_ci/gen_valid_in_contract.c  |   1 +
 .../tests/memory/oracle_ci/gen_vector.c       |   1 +
 .../e-acsl/tests/memory/oracle_ci/gen_vla.c   |   2 +-
 .../tests/special/oracle_ci/gen_builtin.c     |   2 +-
 .../special/oracle_ci/gen_e-acsl-functions.c  |   2 +-
 .../special/oracle_ci/gen_e-acsl-instrument.c |   2 +-
 .../special/oracle_ci/gen_e-acsl-valid.c      |   1 +
 .../temporal/oracle_ci/gen_t_addr-by-val.c    |   2 +-
 .../tests/temporal/oracle_ci/gen_t_args.c     |   1 -
 .../tests/temporal/oracle_ci/gen_t_array.c    |   2 +-
 .../tests/temporal/oracle_ci/gen_t_char.c     |   2 +-
 .../tests/temporal/oracle_ci/gen_t_darray.c   |   2 +-
 .../tests/temporal/oracle_ci/gen_t_dpointer.c |   1 +
 .../tests/temporal/oracle_ci/gen_t_fptr.c     |   2 +-
 .../tests/temporal/oracle_ci/gen_t_fun_lib.c  |   1 +
 .../tests/temporal/oracle_ci/gen_t_fun_ptr.c  |   1 +
 .../tests/temporal/oracle_ci/gen_t_getenv.c   |   1 +
 .../temporal/oracle_ci/gen_t_global_init.c    |   2 +-
 .../tests/temporal/oracle_ci/gen_t_labels.c   |   2 +-
 .../temporal/oracle_ci/gen_t_lit_string.c     |   2 +-
 .../temporal/oracle_ci/gen_t_local_init.c     |   1 -
 .../temporal/oracle_ci/gen_t_malloc-asan.c    |   1 +
 .../tests/temporal/oracle_ci/gen_t_malloc.c   |   1 +
 .../tests/temporal/oracle_ci/gen_t_scope.c    |   2 +-
 .../tests/temporal/oracle_ci/gen_t_struct.c   |   1 +
 .../tests/temporal/oracle_ci/gen_t_while.c    |   2 +-
 121 files changed, 207 insertions(+), 262 deletions(-)

diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
index 249a2e33666..3431019cbc4 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
index b65d0e8fe76..73ea4bf5ab1 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int T1[3];
 int T2[4];
 void arrays(void)
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at.c
index ee37178a854..e6bc5c1484f 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 int A = 0;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
index 17dee710545..205c4799a85 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 /*@ ensures
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_bitwise.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_bitwise.c
index e96f4973e6c..7d9adc92634 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_bitwise.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_bitwise.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 void f_signed(int a, int b)
 {
   int c = a << 2;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
index c5a5d0cce53..d2d3f52aea0 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
index 08496d44c23..29e8ecabb56 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
index 812ba798a39..5dbab6510d7 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 struct mystruct {
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
index b9015c95933..0bca2910d93 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 /*@ logic ℤ f1(ℤ n) = n ≤ 0? 0: f1(n - 1) + n;
 
 */
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
index 15a95e16559..ea0b303a88f 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_let.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_let.c
index 85b41bb2972..dcaaaa3d9e9 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_let.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_let.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 struct __anonstruct_r_1 {
    int x ;
    int y ;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
index 0720b6503aa..16cf4cd3b10 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 unsigned long long my_pow(unsigned int x, unsigned int n)
 {
   unsigned long long __retres;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
index 4ba24ca0879..31c03d939ac 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c
index d5e965010d2..e13edd15d57 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
index ab25e5f5395..859f23f3070 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 /*@ ensures \let delta = 1;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1304.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1304.c
index 69cf275ad87..adb3c8e3ab1 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1304.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1304.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 struct msgA {
    int type ;
    int a[2] ;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c
index 7ecbe49081f..33236edf86c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 /*@ requires \valid(Mtmax_in);
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1324.c
index c0a299e37ed..a0a428c6ea0 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1324.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 /*@ behavior yes:
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1326.c
index 315f754cee7..ed0e31eeef3 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1326.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1326.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 typedef int ArrayInt[5];
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c
index b3d1e5df6a1..8131e10a3bd 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c
@@ -1,7 +1,6 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 void duffcopy(char *to, char *from, int count)
 {
   __e_acsl_store_block((void *)(& from),(size_t)8);
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1390.c
index 0dd57437ec1..058f7b605d8 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1390.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
index 66f0d9080e4..27c7fe2e2f5 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 /*@ requires n > 0; */
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 8f4aa78a777..38075f91be9 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
@@ -1,7 +1,6 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 char *__gen_e_acsl_literal_string;
 void __e_acsl_globals_init(void)
 {
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1399.c
index 2168cfcf29b..ec3cb262ed2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1399.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 struct spongeStateStruct {
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
index 6dddd2a4045..93c920650cd 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 int global_i;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1700.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1700.c
index 7343c2d3389..d9d891542f6 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1700.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1700.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 struct toto {
    
 };
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1717.c
index decb020884b..979cba719c4 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1717.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1717.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1718.c
index a076c7789a3..e0dbf835f6d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1718.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1718.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1740.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1740.c
index ee8220d206c..9c79509d1f7 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1740.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1740.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
index 0c35a1254be..bc80c8d28dc 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 char *__gen_e_acsl_literal_string_3;
 char *__gen_e_acsl_literal_string;
 char *__gen_e_acsl_literal_string_2;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
index 41b668706f8..ee4442c59fd 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 char *__gen_e_acsl_literal_string;
 char *__gen_e_acsl_literal_string_2;
 struct ST {
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
index a33b19b9e42..b8f3d271918 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
index e3887d10a70..84abbc44f83 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 long A = (long)0;
 int main(void)
 {
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
index 989bcb1766b..bbf7b668bde 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 #include "string.h"
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
index 55454d5d36b..634afea64ae 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 struct bitfields {
    int i : 2 ;
    _Bool j : 1 ;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2386.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2386.c
index bcaacac3a1e..3ae4f0709cf 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2386.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2386.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 char *__gen_e_acsl_literal_string;
 void f(void const *s, int c, unsigned long n)
 {
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
index 90b370c4f2c..0c331aeb3b6 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 char const tab[];
 char t[10];
 void __e_acsl_globals_init(void)
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-105.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-105.c
index 8ad1e10fa53..e6ab7d016e1 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-105.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-105.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int f(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c
index 14dd1ab575a..33c28617704 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 short a;
 char b(void)
 {
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
index 44cfac328f8..b49b9ee26da 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c
index 7c2dc5ed469..ed65d0c6f15 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c
index 9e7f63becc8..c1d683e5f6d 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 int X = 0;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c
index ab2bc7b7038..89cee38a6d7 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int G = 0;
 int *P;
 void __e_acsl_globals_init(void)
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c
index 803e14a2914..f662b924a1e 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c
index 06a5de92573..4e43bc9fabf 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 int X = 0;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c
index b9ba06467be..d21ef113d76 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c
index 879d1ee52a8..c1944d903d8 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 void simple_loop(void)
 {
   int sum = 0;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c
index 252046ac3c8..07c6bff2ea6 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c
index 6b0f6fcf6b2..dccbec78338 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 /*@ ensures \result ≡ (int)(\old(x) - \old(x)); */
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c
index b9942c443b7..e088e9e145e 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c
index 243f60598a1..819a2b7a157 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c
index 92e02166357..8b62fcfca72 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c
+++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 typedef unsigned char uint8;
 int main(void)
 {
diff --git a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c
index 47e55d3fc12..84a91929a61 100644
--- a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c
+++ b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 struct list {
diff --git a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
index 6657c1ae8ee..7e89333ec36 100644
--- a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
+++ b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 int A[10];
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
index 7f687e99ca5..ff43a1afe08 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
@@ -82,11 +82,13 @@
 [eva:alarm] tests/format/fprintf.c:36: Warning: 
   accessing uninitialized left-value. assert \initialized(&process_status_8);
 [eva:invalid-assigns] tests/format/fprintf.c:37: 
-  Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
+  Completely invalid destination for assigns clause *(buffer + (0 ..)).
+  Ignoring.
 [eva:alarm] tests/format/fprintf.c:37: Warning: 
   accessing uninitialized left-value. assert \initialized(&process_status_9);
 [eva:invalid-assigns] tests/format/fprintf.c:38: 
-  Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
+  Completely invalid destination for assigns clause *(buffer + (0 ..)).
+  Ignoring.
 [eva:alarm] tests/format/fprintf.c:38: Warning: 
   accessing uninitialized left-value. assert \initialized(&process_status_10);
 [kernel:annot:missing-spec] tests/format/fprintf.c:41: Warning: 
@@ -96,16 +98,19 @@
 [eva:alarm] tests/format/fprintf.c:42: Warning: 
   accessing uninitialized left-value. assert \initialized(&process_status_12);
 [eva:invalid-assigns] tests/format/fprintf.c:43: 
-  Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
+  Completely invalid destination for assigns clause *(buffer + (0 ..)).
+  Ignoring.
 [eva:alarm] tests/format/fprintf.c:43: Warning: 
   accessing uninitialized left-value. assert \initialized(&process_status_13);
 [eva:alarm] tests/format/fprintf.c:44: Warning: 
   accessing uninitialized left-value. assert \initialized(&process_status_14);
 [eva:invalid-assigns] tests/format/fprintf.c:45: 
-  Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
+  Completely invalid destination for assigns clause *(buffer + (0 ..)).
+  Ignoring.
 [eva:alarm] tests/format/fprintf.c:45: Warning: 
   accessing uninitialized left-value. assert \initialized(&process_status_15);
 [eva:invalid-assigns] tests/format/fprintf.c:46: 
-  Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
+  Completely invalid destination for assigns clause *(buffer + (0 ..)).
+  Ignoring.
 [eva:alarm] tests/format/fprintf.c:46: Warning: 
   accessing uninitialized left-value. assert \initialized(&process_status_16);
diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
index c93c673e181..4a64f9d92fb 100644
--- a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
@@ -1,5 +1,6 @@
 /* Generated by Frama-C */
 #include "signal.h"
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 #include "sys/select.h"
diff --git a/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log b/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log
index 19a711261f3..02725ad71ef 100644
--- a/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log
@@ -29,25 +29,19 @@ TEST 20: OK: Expected execution at tests/format/printf.c:209
 TEST 21: OK: Expected execution at tests/format/printf.c:209
 TEST 22: OK: Expected execution at tests/format/printf.c:209
 TEST 23: OK: Expected execution at tests/format/printf.c:209
-Format error: wrong application of precision [.] to format specifier [c]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of precision [.] to format specifier [c]
 TEST 24: OK: Expected signal at tests/format/printf.c:209
 TEST 25: OK: Expected execution at tests/format/printf.c:209
-Format error: wrong application of precision [.] to format specifier [p]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of precision [.] to format specifier [p]
 TEST 26: OK: Expected signal at tests/format/printf.c:209
-Format error: wrong application of precision [.] to format specifier [n]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of precision [.] to format specifier [n]
 TEST 27: OK: Expected signal at tests/format/printf.c:209
-Format error: wrong application of flag [#] to format specifier [d]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [d]
 TEST 28: OK: Expected signal at tests/format/printf.c:215
-Format error: wrong application of flag [#] to format specifier [i]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [i]
 TEST 29: OK: Expected signal at tests/format/printf.c:215
 TEST 30: OK: Expected execution at tests/format/printf.c:215
-Format error: wrong application of flag [#] to format specifier [u]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [u]
 TEST 31: OK: Expected signal at tests/format/printf.c:215
 TEST 32: OK: Expected execution at tests/format/printf.c:215
 TEST 33: OK: Expected execution at tests/format/printf.c:215
@@ -58,17 +52,13 @@ TEST 37: OK: Expected execution at tests/format/printf.c:215
 TEST 38: OK: Expected execution at tests/format/printf.c:215
 TEST 39: OK: Expected execution at tests/format/printf.c:215
 TEST 40: OK: Expected execution at tests/format/printf.c:215
-Format error: wrong application of flag [#] to format specifier [c]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [c]
 TEST 41: OK: Expected signal at tests/format/printf.c:215
-Format error: wrong application of flag [#] to format specifier [s]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [s]
 TEST 42: OK: Expected signal at tests/format/printf.c:215
-Format error: wrong application of flag [#] to format specifier [p]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [p]
 TEST 43: OK: Expected signal at tests/format/printf.c:215
-Format error: wrong application of flag [#] to format specifier [n]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [n]
 TEST 44: OK: Expected signal at tests/format/printf.c:215
 TEST 45: OK: Expected execution at tests/format/printf.c:218
 TEST 46: OK: Expected execution at tests/format/printf.c:218
@@ -83,54 +73,39 @@ TEST 54: OK: Expected execution at tests/format/printf.c:218
 TEST 55: OK: Expected execution at tests/format/printf.c:218
 TEST 56: OK: Expected execution at tests/format/printf.c:218
 TEST 57: OK: Expected execution at tests/format/printf.c:218
-Format error: wrong application of flag [0] to format specifier [c]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [0] to format specifier [c]
 TEST 58: OK: Expected signal at tests/format/printf.c:218
-Format error: wrong application of flag [0] to format specifier [s]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [0] to format specifier [s]
 TEST 59: OK: Expected signal at tests/format/printf.c:218
-Format error: wrong application of flag [0] to format specifier [p]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [0] to format specifier [p]
 TEST 60: OK: Expected signal at tests/format/printf.c:218
-Format error: wrong application of flag [0] to format specifier [n]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [0] to format specifier [n]
 TEST 61: OK: Expected signal at tests/format/printf.c:218
 TEST 62: OK: Expected execution at tests/format/printf.c:224
 TEST 63: OK: Expected execution at tests/format/printf.c:225
 Format error: illegal format specifier 'l'
 TEST 64: OK: Expected signal at tests/format/printf.c:226
-Format error: wrong application of length modifier [hh] to format specifier [f]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [f]
 TEST 65: OK: Expected signal at tests/format/printf.c:232
-Format error: wrong application of length modifier [hh] to format specifier [F]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [F]
 TEST 66: OK: Expected signal at tests/format/printf.c:232
-Format error: wrong application of length modifier [hh] to format specifier [e]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [e]
 TEST 67: OK: Expected signal at tests/format/printf.c:232
-Format error: wrong application of length modifier [hh] to format specifier [E]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [E]
 TEST 68: OK: Expected signal at tests/format/printf.c:232
-Format error: wrong application of length modifier [hh] to format specifier [g]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [g]
 TEST 69: OK: Expected signal at tests/format/printf.c:232
-Format error: wrong application of length modifier [hh] to format specifier [G]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [G]
 TEST 70: OK: Expected signal at tests/format/printf.c:232
-Format error: wrong application of length modifier [hh] to format specifier [a]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [a]
 TEST 71: OK: Expected signal at tests/format/printf.c:232
-Format error: wrong application of length modifier [hh] to format specifier [A]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [A]
 TEST 72: OK: Expected signal at tests/format/printf.c:232
-Format error: wrong application of length modifier [hh] to format specifier [c]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [c]
 TEST 73: OK: Expected signal at tests/format/printf.c:232
-Format error: wrong application of length modifier [hh] to format specifier [s]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [s]
 TEST 74: OK: Expected signal at tests/format/printf.c:232
-Format error: wrong application of length modifier [hh] to format specifier [p]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [hh] to format specifier [p]
 TEST 75: OK: Expected signal at tests/format/printf.c:232
 TEST 76: OK: Expected execution at tests/format/printf.c:233
 TEST 77: OK: Expected execution at tests/format/printf.c:233
@@ -139,38 +114,27 @@ TEST 79: OK: Expected execution at tests/format/printf.c:234
 TEST 80: OK: Expected execution at tests/format/printf.c:235
 TEST 81: OK: Expected execution at tests/format/printf.c:235
 TEST 82: OK: Expected execution at tests/format/printf.c:235
-Format error: wrong application of length modifier [h] to format specifier [f]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [f]
 TEST 83: OK: Expected signal at tests/format/printf.c:238
-Format error: wrong application of length modifier [h] to format specifier [F]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [F]
 TEST 84: OK: Expected signal at tests/format/printf.c:238
-Format error: wrong application of length modifier [h] to format specifier [e]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [e]
 TEST 85: OK: Expected signal at tests/format/printf.c:238
-Format error: wrong application of length modifier [h] to format specifier [E]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [E]
 TEST 86: OK: Expected signal at tests/format/printf.c:238
-Format error: wrong application of length modifier [h] to format specifier [g]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [g]
 TEST 87: OK: Expected signal at tests/format/printf.c:238
-Format error: wrong application of length modifier [h] to format specifier [G]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [G]
 TEST 88: OK: Expected signal at tests/format/printf.c:238
-Format error: wrong application of length modifier [h] to format specifier [a]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [a]
 TEST 89: OK: Expected signal at tests/format/printf.c:238
-Format error: wrong application of length modifier [h] to format specifier [A]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [A]
 TEST 90: OK: Expected signal at tests/format/printf.c:238
-Format error: wrong application of length modifier [h] to format specifier [c]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [c]
 TEST 91: OK: Expected signal at tests/format/printf.c:238
-Format error: wrong application of length modifier [h] to format specifier [s]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [s]
 TEST 92: OK: Expected signal at tests/format/printf.c:238
-Format error: wrong application of length modifier [h] to format specifier [p]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [h] to format specifier [p]
 TEST 93: OK: Expected signal at tests/format/printf.c:238
 TEST 94: OK: Expected execution at tests/format/printf.c:239
 TEST 95: OK: Expected execution at tests/format/printf.c:239
@@ -179,8 +143,7 @@ TEST 97: OK: Expected execution at tests/format/printf.c:240
 TEST 98: OK: Expected execution at tests/format/printf.c:241
 TEST 99: OK: Expected execution at tests/format/printf.c:241
 TEST 100: OK: Expected execution at tests/format/printf.c:241
-Format error: wrong application of length modifier [l] to format specifier [p]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [l] to format specifier [p]
 TEST 101: OK: Expected signal at tests/format/printf.c:244
 TEST 102: OK: Expected execution at tests/format/printf.c:245
 TEST 103: OK: Expected execution at tests/format/printf.c:245
@@ -205,38 +168,27 @@ TEST 121: OK: Expected execution at tests/format/printf.c:262
 TEST 122: OK: Expected execution at tests/format/printf.c:263
 TEST 123: OK: Expected execution at tests/format/printf.c:263
 TEST 124: OK: Expected execution at tests/format/printf.c:263
-Format error: wrong application of length modifier [j] to format specifier [f]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [f]
 TEST 125: OK: Expected signal at tests/format/printf.c:266
-Format error: wrong application of length modifier [j] to format specifier [F]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [F]
 TEST 126: OK: Expected signal at tests/format/printf.c:266
-Format error: wrong application of length modifier [j] to format specifier [e]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [e]
 TEST 127: OK: Expected signal at tests/format/printf.c:266
-Format error: wrong application of length modifier [j] to format specifier [E]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [E]
 TEST 128: OK: Expected signal at tests/format/printf.c:266
-Format error: wrong application of length modifier [j] to format specifier [g]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [g]
 TEST 129: OK: Expected signal at tests/format/printf.c:266
-Format error: wrong application of length modifier [j] to format specifier [G]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [G]
 TEST 130: OK: Expected signal at tests/format/printf.c:266
-Format error: wrong application of length modifier [j] to format specifier [a]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [a]
 TEST 131: OK: Expected signal at tests/format/printf.c:266
-Format error: wrong application of length modifier [j] to format specifier [A]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [A]
 TEST 132: OK: Expected signal at tests/format/printf.c:266
-Format error: wrong application of length modifier [j] to format specifier [c]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [c]
 TEST 133: OK: Expected signal at tests/format/printf.c:266
-Format error: wrong application of length modifier [j] to format specifier [s]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [s]
 TEST 134: OK: Expected signal at tests/format/printf.c:266
-Format error: wrong application of length modifier [j] to format specifier [p]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [j] to format specifier [p]
 TEST 135: OK: Expected signal at tests/format/printf.c:266
 TEST 136: OK: Expected execution at tests/format/printf.c:267
 TEST 137: OK: Expected execution at tests/format/printf.c:267
@@ -245,38 +197,27 @@ TEST 139: OK: Expected execution at tests/format/printf.c:268
 TEST 140: OK: Expected execution at tests/format/printf.c:269
 TEST 141: OK: Expected execution at tests/format/printf.c:269
 TEST 142: OK: Expected execution at tests/format/printf.c:269
-Format error: wrong application of length modifier [z] to format specifier [f]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [f]
 TEST 143: OK: Expected signal at tests/format/printf.c:272
-Format error: wrong application of length modifier [z] to format specifier [F]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [F]
 TEST 144: OK: Expected signal at tests/format/printf.c:272
-Format error: wrong application of length modifier [z] to format specifier [e]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [e]
 TEST 145: OK: Expected signal at tests/format/printf.c:272
-Format error: wrong application of length modifier [z] to format specifier [E]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [E]
 TEST 146: OK: Expected signal at tests/format/printf.c:272
-Format error: wrong application of length modifier [z] to format specifier [g]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [g]
 TEST 147: OK: Expected signal at tests/format/printf.c:272
-Format error: wrong application of length modifier [z] to format specifier [G]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [G]
 TEST 148: OK: Expected signal at tests/format/printf.c:272
-Format error: wrong application of length modifier [z] to format specifier [a]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [a]
 TEST 149: OK: Expected signal at tests/format/printf.c:272
-Format error: wrong application of length modifier [z] to format specifier [A]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [A]
 TEST 150: OK: Expected signal at tests/format/printf.c:272
-Format error: wrong application of length modifier [z] to format specifier [c]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [c]
 TEST 151: OK: Expected signal at tests/format/printf.c:272
-Format error: wrong application of length modifier [z] to format specifier [s]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [s]
 TEST 152: OK: Expected signal at tests/format/printf.c:272
-Format error: wrong application of length modifier [z] to format specifier [p]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [z] to format specifier [p]
 TEST 153: OK: Expected signal at tests/format/printf.c:272
 TEST 154: OK: Expected execution at tests/format/printf.c:277
 TEST 155: OK: Expected execution at tests/format/printf.c:277
@@ -285,38 +226,27 @@ TEST 157: OK: Expected execution at tests/format/printf.c:281
 TEST 158: OK: Expected execution at tests/format/printf.c:282
 TEST 159: OK: Expected execution at tests/format/printf.c:282
 TEST 160: OK: Expected execution at tests/format/printf.c:282
-Format error: wrong application of length modifier [t] to format specifier [f]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [f]
 TEST 161: OK: Expected signal at tests/format/printf.c:287
-Format error: wrong application of length modifier [t] to format specifier [F]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [F]
 TEST 162: OK: Expected signal at tests/format/printf.c:287
-Format error: wrong application of length modifier [t] to format specifier [e]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [e]
 TEST 163: OK: Expected signal at tests/format/printf.c:287
-Format error: wrong application of length modifier [t] to format specifier [E]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [E]
 TEST 164: OK: Expected signal at tests/format/printf.c:287
-Format error: wrong application of length modifier [t] to format specifier [g]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [g]
 TEST 165: OK: Expected signal at tests/format/printf.c:287
-Format error: wrong application of length modifier [t] to format specifier [G]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [G]
 TEST 166: OK: Expected signal at tests/format/printf.c:287
-Format error: wrong application of length modifier [t] to format specifier [a]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [a]
 TEST 167: OK: Expected signal at tests/format/printf.c:287
-Format error: wrong application of length modifier [t] to format specifier [A]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [A]
 TEST 168: OK: Expected signal at tests/format/printf.c:287
-Format error: wrong application of length modifier [t] to format specifier [c]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [c]
 TEST 169: OK: Expected signal at tests/format/printf.c:287
-Format error: wrong application of length modifier [t] to format specifier [s]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [s]
 TEST 170: OK: Expected signal at tests/format/printf.c:287
-Format error: wrong application of length modifier [t] to format specifier [p]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [t] to format specifier [p]
 TEST 171: OK: Expected signal at tests/format/printf.c:287
 TEST 172: OK: Expected execution at tests/format/printf.c:289
 TEST 173: OK: Expected execution at tests/format/printf.c:289
@@ -325,32 +255,23 @@ TEST 175: OK: Expected execution at tests/format/printf.c:290
 TEST 176: OK: Expected execution at tests/format/printf.c:295
 TEST 177: OK: Expected execution at tests/format/printf.c:295
 TEST 178: OK: Expected execution at tests/format/printf.c:296
-Format error: wrong application of length modifier [L] to format specifier [d]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [d]
 TEST 179: OK: Expected signal at tests/format/printf.c:299
-Format error: wrong application of length modifier [L] to format specifier [i]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [i]
 TEST 180: OK: Expected signal at tests/format/printf.c:299
-Format error: wrong application of length modifier [L] to format specifier [o]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [o]
 TEST 181: OK: Expected signal at tests/format/printf.c:299
-Format error: wrong application of length modifier [L] to format specifier [u]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [u]
 TEST 182: OK: Expected signal at tests/format/printf.c:299
-Format error: wrong application of length modifier [L] to format specifier [x]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [x]
 TEST 183: OK: Expected signal at tests/format/printf.c:299
-Format error: wrong application of length modifier [L] to format specifier [c]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [c]
 TEST 184: OK: Expected signal at tests/format/printf.c:299
-Format error: wrong application of length modifier [L] to format specifier [s]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [s]
 TEST 185: OK: Expected signal at tests/format/printf.c:299
-Format error: wrong application of length modifier [L] to format specifier [p]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [p]
 TEST 186: OK: Expected signal at tests/format/printf.c:299
-Format error: wrong application of length modifier [L] to format specifier [n]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of length modifier [L] to format specifier [n]
 TEST 187: OK: Expected signal at tests/format/printf.c:299
 TEST 188: OK: Expected execution at tests/format/printf.c:300
 TEST 189: OK: Expected execution at tests/format/printf.c:300
@@ -629,14 +550,11 @@ printf: directive 1 ('%n') expects argument of type 'int*' but the corresponding
 TEST 368: OK: Expected signal at tests/format/printf.c:460
 printf: argument 0 of directive %n not allocated or writeable
 TEST 369: OK: Expected signal at tests/format/printf.c:461
-Format error: wrong application of flag ['] to format specifier [n]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag ['] to format specifier [n]
 TEST 370: OK: Expected signal at tests/format/printf.c:464
-Format error: wrong application of flag [0] to format specifier [n]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [0] to format specifier [n]
 TEST 371: OK: Expected signal at tests/format/printf.c:465
-Format error: wrong application of flag [#] to format specifier [n]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of flag [#] to format specifier [n]
 TEST 372: OK: Expected signal at tests/format/printf.c:466
 Format error: one of more flags with [n] specifier
 TEST 373: OK: Expected signal at tests/format/printf.c:467
@@ -644,14 +562,11 @@ Format error: one of more flags with [n] specifier
 TEST 374: OK: Expected signal at tests/format/printf.c:468
 Format error: one of more flags with [n] specifier
 TEST 375: OK: Expected signal at tests/format/printf.c:469
-Format error: wrong application of precision [.] to format specifier [n]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of precision [.] to format specifier [n]
 TEST 376: OK: Expected signal at tests/format/printf.c:470
-Format error: wrong application of precision [.] to format specifier [n]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of precision [.] to format specifier [n]
 TEST 377: OK: Expected signal at tests/format/printf.c:471
-Format error: wrong application of precision [.] to format specifier [n]
- at FRAMAC_SHARE/e-acsl/e_acsl_format.h:593
+FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:541: Format error: wrong application of precision [.] to format specifier [n]
 TEST 378: OK: Expected signal at tests/format/printf.c:472
 Format error: field width used with [n] specifier
 TEST 379: OK: Expected signal at tests/format/printf.c:473
diff --git a/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c
index 29818eff2cf..3d27c36ba8d 100644
--- a/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 void f(void)
 {
   int m;
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
index 9db467e05fc..63c374fc880 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
index 471424de4c8..ab3f589ceb4 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 struct mystruct {
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_addrOf.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_addrOf.c
index 7b77f53af25..bd03357db5a 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_addrOf.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_addrOf.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 void f(void)
 {
   int m;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_alias.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_alias.c
index 6a17c6b8426..ec52f8d8911 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_alias.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_alias.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 void f(int *dest, int val)
 {
   __e_acsl_store_block((void *)(& dest),(size_t)8);
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
index 9f45f3d678f..9927263df1e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 int A[4] = {1, 2, 3, 4};
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
index 4cbe891d458..70135545c5c 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 struct Zero {
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
index 3871a01e451..44cb0bfe503 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 int A = 1;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_bypassed_var.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_bypassed_var.c
index 719d8c6de18..b835f6982ff 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_bypassed_var.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_bypassed_var.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(int argc, char const **argv)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_call.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_call.c
index 2cdd52844f8..7b3be6015b9 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_call.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_call.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 extern int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
index a5c53537815..96bcfdbdcdf 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 char *__gen_e_acsl_literal_string_3;
 char *__gen_e_acsl_literal_string;
 char *__gen_e_acsl_literal_string_2;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c
index 52d996bb020..2a3a6d2b157 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "ctype.h"
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 /*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c
index 4c5ab738c91..0f7c83a627a 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 void decl_in_switch(int value)
 {
   __e_acsl_store_block((void *)(& value),(size_t)4);
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_early_exit.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_early_exit.c
index aaa3abefdbd..f107396adc8 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_early_exit.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_early_exit.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int goto_bts(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
index 6504639acc7..06eabe4d9f0 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 char array[1024];
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
index dcd56fb12c7..e16ba064495 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 void function(int a, int b, int c, int d)
 {
   return;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
index d5c1542ac4f..4e033175d14 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 char a;
 void __e_acsl_globals_init(void)
 {
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_hidden_malloc.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_hidden_malloc.c
index ef47698bb6f..e3e8cd4ae77 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_hidden_malloc.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_hidden_malloc.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
index e3a9201614e..c063f126339 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int a = 0;
 int b;
 void __e_acsl_globals_init(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init_function.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init_function.c
index 0233781eddc..6b4322952dc 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init_function.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init_function.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
index 026e4bbef14..50566fb3407 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 int A = 0;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
index 74ba7f26de6..8710dc8c595 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 char *__gen_e_acsl_literal_string_6;
 char *__gen_e_acsl_literal_string_5;
 char *__gen_e_acsl_literal_string;
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 3d26e79512a..81bdec60725 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
@@ -1,7 +1,6 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 char *__gen_e_acsl_literal_string_2;
 char *__gen_e_acsl_literal_string_3;
 char *__gen_e_acsl_literal_string;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
index 1f7424a1ec1..508da20bd2b 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int X = 0;
 int *p = & X;
 int f(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_var.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_var.c
index a7de0f8707d..7dd067ecaf9 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_var.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_var.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 struct list {
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
index 86e9de27822..f5565321250 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
@@ -1,7 +1,6 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 #include "string.h"
 extern int __e_acsl_sound_verdict;
 
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
index f0a98343e01..53c57ee9179 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 extern int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
index afc1d47904c..134e80f8daf 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 extern size_t __e_acsl_heap_allocation_size;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
index 02d31514dd5..3da46b12757 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
index 4ce316ea42c..a294b87c024 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 int A[4] = {1, 2, 3, 4};
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
index e6f639fa935..367bdac518c 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 enum bool {
     false = 0,
     true = 1
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr.c
index dbe02ee97e2..d3e4601ad63 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
index e021ea6783c..7437d4c8785 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 int *A;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
index 89bbf9a94b8..d34788a14e9 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 extern int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
index 7920e6b98d1..aa3776502d0 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
index 75bddabfbe9..225763b343e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
@@ -1,7 +1,6 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 void __e_acsl_globals_init(void)
 {
   static char __e_acsl_already_run = 0;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
index 38b803a26a3..133ae6895b7 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 extern int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_alias.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_alias.c
index c89b0e938c9..a747d918903 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_alias.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 int main(void)
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_in_contract.c
index e26605a5936..384a5a75de5 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_in_contract.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 extern int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vector.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vector.c
index f3ef2cd1836..ac348fd03d0 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vector.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vector.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 int LAST;
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
index d2039f2b5ee..73cabbcc28e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int LEN = 10;
 int main(int argc, char **argv)
 {
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
index dcc566b58e8..61b7ebb65cd 100644
--- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 int incr(int x);
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c
index 26550ea8e34..f317d0df3bc 100644
--- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 /*@ requires \initialized(p);
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 e3d9f21d1ef..2ef9690828f 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
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
 #include "stdarg.h"
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 extern int __e_acsl_sound_verdict;
 
 /* compiler builtin: 
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
index bf53cbc448c..1df7f9c8859 100644
--- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 extern int __e_acsl_sound_verdict;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_addr-by-val.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_addr-by-val.c
index 32bcce13609..ae17894128e 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_addr-by-val.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_addr-by-val.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdint.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(int argc, char **argv)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c
index 3e24ef3f308..74e64a13210 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c
@@ -1,7 +1,6 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(int argc, char const **argv)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_array.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_array.c
index 9716b9407fb..e6b8e000598 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_array.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_array.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_char.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_char.c
index 6da6eec960c..36ce1e3ab27 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_char.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_char.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(int argc, char const **argv)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
index f2c564d40b4..39664bb15a9 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 void area_triangle(double (*vertices)[4])
 {
   {
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_dpointer.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_dpointer.c
index 54917f1f76f..17025a19ee8 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_dpointer.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_dpointer.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 int main(void)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
index 6ce50be381f..a1ab4f085fb 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int *foo(int *p)
 {
   int *q = p;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_lib.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_lib.c
index 33388accb3a..fa0bd664679 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_lib.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_lib.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_ptr.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_ptr.c
index 43f3a37fa9f..7182f81e3d3 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_ptr.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_ptr.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdint.h"
 #include "stdio.h"
 #include "stdlib.h"
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c
index b574f1ebb23..f1daa120b06 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string_2;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
index 1a223bf90f4..bfb6fd16794 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 char *__gen_e_acsl_literal_string;
 char *__gen_e_acsl_literal_string_2;
 char *__gen_e_acsl_literal_string_4;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_labels.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_labels.c
index a0229a5254a..a582605286f 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_labels.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_labels.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 void foo(int *a, int *b)
 {
   __e_acsl_store_block((void *)(& b),(size_t)8);
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_lit_string.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_lit_string.c
index 89bdc1b2a15..22d485e658b 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_lit_string.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_lit_string.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 char *__gen_e_acsl_literal_string_2;
 char *__gen_e_acsl_literal_string;
 void __e_acsl_globals_init(void)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
index 00745623824..e77ce2220c0 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
@@ -1,7 +1,6 @@
 /* Generated by Frama-C */
 #include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 char *__gen_e_acsl_literal_string_4;
 char *__gen_e_acsl_literal_string_3;
 char *__gen_e_acsl_literal_string;
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 08d4bb0a0ae..670764770e9 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
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 char *__gen_e_acsl_literal_string;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc.c
index b58537e485c..6e7fbc4aed2 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 int main(void)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_scope.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_scope.c
index 8a0fc1325ad..9b76adcf47e 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_scope.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_scope.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_struct.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_struct.c
index 76272a2c173..05b096a5801 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_struct.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_struct.c
@@ -1,4 +1,5 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
 #include "stdlib.h"
 struct temporal_t {
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_while.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_while.c
index b63675cf0ac..e44bc6c2640 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_while.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_while.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
+#include "stddef.h"
 #include "stdio.h"
-#include "stdlib.h"
 int main(void)
 {
   int __retres;
-- 
GitLab