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 249a2e3366637540cf22f0fbbc67c8468d49a72d..3431019cbc4f8793231f6b90f6ab869c3762ae82 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 b65d0e8fe7686a76b411ddaa1c26c7d331c15ce1..73ea4bf5ab15bfb8cdebf3895769ca0f0947ec9d 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 ee37178a854e61491d674d217859bdedbc1fa830..e6bc5c1484f8a7102929c7c731ffb0d2cee4cf7c 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 17dee7105453488b730f112a3de0e6c604b8eeae..205c4799a854078e9477b9ef4546492c0726ef6b 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 e96f4973e6c3c735ac875d125d378d469f0fd181..7d9adc9263454897905a9a96c35a0d6d3f8e8004 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 c5a5d0cce531b902d925bd9b435b23ff6b64d963..d2d3f52aea0b8a803f2c0951334bc238227309dd 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 08496d44c2396e09142e025ace2d5fe9aec84610..29e8ecabb565015063620d90d4e76d1ce3232cc4 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 812ba798a39afad86acd699e1379e8641718a5bf..5dbab6510d7dff48a8506e74fd5d2d0e7cc013cc 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 b9015c95933c865e01c9d365c7a3b2c73c8c4a4f..0bca2910d93fe3bc6c413c798d9a5a1a0dc27eb5 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 15a95e1655951a6ae8a649d80881877aff06af4b..ea0b303a88fe9578a4d1393ed1948681026723b4 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 85b41bb2972fe22862a0cba068ff0c8c60df0bdb..dcaaaa3d9e96f463f5e8d8d198990277b59dc088 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 0720b6503aa754f974b9df3eb49a3e708e503dd3..16cf4cd3b10ee8809887c59cb5cb0f660d0f38a0 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 4ba24ca0879edf6173547ef7665fe0dfd3b135de..31c03d939acfbede317521fa9a87e793951a0025 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 d5e965010d24862b584dee905bc13b35828388af..e13edd15d57a19cfe1693bf1d92e7f6f5d0ec0a2 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 ab25e5f5395d1d1648a723cd7583b42285a50201..859f23f30709869281a2f4317c2e74ed93bccee6 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 69cf275ad871e22adade1febee237d73a55be2b0..adb3c8e3ab1ae9a9e9923207ad1fb14605e331b1 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 7ecbe49081f97141b4826d44f36fe9f8ff8e1acd..33236edf86c22697136f4cbc4a78fa60a60cecac 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 c0a299e37edcf2fcbadc801ccd3b5d5fa45a8482..a0a428c6ea0988debf0aad02354d54c2e9f1bab4 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 315f754cee7e3ea352066552a50e7559e8dcf1ff..ed0e31eeef3722d85e285e8dea7b1d52f8c2b71a 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 b3d1e5df6a10a1ce8fb80e3003fc4f942cdff13b..8131e10a3bd632923d333eae81fc18b92ed19afe 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 0dd57437ec161e0e7621b04820c1ce9dbab3a169..058f7b605d8f8d53d6ce9381ff5d84428bc63a14 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 66f0d9080e4c01efc18f40664b68ffd58b5a5119..27c7fe2e2f55c67c6099adb6a3335993e2178674 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 8f4aa78a77722c4c1bc7163cc8680bf7cc800d3a..38075f91be9c362dc3751df207f631511135b0ae 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 2168cfcf29b80a91829c36d6eaf3f2811853f641..ec3cb262ed2fe6298f17ac2bb415ef2aa95dc129 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 6dddd2a40459ae418afc2b9a752964fe125984dc..93c920650cd3172b3813c8c37b94f6c06de89f98 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 7343c2d33895d60c6567598d3324905e16bd2c7a..d9d891542f630ba8bd2ec97ca42c921ec09d6183 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 decb020884bd9905b3b7585220261037c6239991..979cba719c40a53c167df4b7425345a65ff1dfad 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 a076c7789a3df7ff28f98fcd7749a198275c2bbf..e0dbf835f6d8beb792e774bbff50f2ee37565157 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 ee8220d206ce297f6049fabbac14c0083640be76..9c79509d1f7d27490d5dbd13b9f5b138b3ec1ff3 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 0c35a1254beda7c48905f510b8cd0b0ae4af49f9..bc80c8d28dca93ea1fbc338769c80432ac8be614 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 41b668706f86030c287a11992ef37b9fd3328d1c..ee4442c59fd67c3ed332ea822f1eb11d1825545f 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 a33b19b9e42be188eaabb80ce398cd9370323f9b..b8f3d27191812e698cc095efcd9f8ac24f29033a 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 e3887d10a705e41beb1f739df200ac7a574232ae..84abbc44f8308b525e2959d9eae37e99773823e3 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 989bcb1766bd17886c7cc66d06c696124849a70f..bbf7b668bdeb592b79c4c964bcaffffc11ab6bcd 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 55454d5d36b67f3bfc10e27db0a1244dc5b64ba7..634afea64aeca153816808a03ca37aa56f2d6fea 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 bcaacac3a1ea3e50b3528a9f355f040e4a9b7a69..3ae4f0709cfc864381f38ed4794f9feba91ce7d0 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 90b370c4f2cd506313c73d515bb600fe16deb609..0c331aeb3b66bc2c15a76c77b9373c2b0935d525 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 8ad1e10fa53fcb05e3e4ce4bc9b1fd53785a94fc..e6ab7d016e17c216d6c6a4937ed7a24dc9cdad63 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 14dd1ab575af5a0d4560ecc5a1ac7ae3bc49a5d3..33c2861770404d56bcb16081bf8189028ee28a47 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 44cfac328f8ff8637b0acf5384c359fa86b3ea1b..b49b9ee26da2e1fdbd108bc6dbd1390fe7e5dfc0 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 7c2dc5ed4699cd1b21b3a8a1a2b331de709d4da0..ed65d0c6f152703aa95225d8cb26588573cc0522 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 9e7f63becc8b260a7c45ea04dcb5d33350f77fdd..c1d683e5f6d17e3e7acd9762ac651218ce782be7 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 ab2bc7b703821eac9e38b82846f04b971497d3c5..89cee38a6d7bd88fdee0c4b405888bf0d7f15956 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 803e14a2914f164781f4cd2324420ffc2567e370..f662b924a1e3ff944d227867fab63649b277aa43 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 06a5de92573cd1f63bb730d2872ce69f3432a319..4e43bc9fabffbbf5663023222f137159cc599b87 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 b9ba06467be864939e8f22b5f52bfe826b1b814e..d21ef113d761fe2047214836277f8f3fde8b0f8c 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 879d1ee52a8ea1608999651843b866fc15f8f381..c1944d903d8b2b3d7492251900b5c76206f8d22f 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 252046ac3c885a76d1db75b9e766725b2a12340b..07c6bff2ea6b1420cfefc2f7e86cc515bc286ac8 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 6b0f6fcf6b200810222c7a03b36bd41a2d2b6526..dccbec78338d13c8cc8351af5f78cf4110fb24cd 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 b9942c443b734d7b8125e9eb9632e5a9e0a1cd03..e088e9e145e72e17c2e2febe71f962453dfbf2e0 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 243f60598a1d7058fdac1047fc7513c4dea1bc85..819a2b7a157a92588d7890015ab49a9ee329b1b9 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 92e02166357ca38676b0a54bdfe18e6b4a1015b6..8b62fcfca7246451c4e19c78ff282458a54e0704 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 47e55d3fc12d7dc4c433a4048dc6a87d3fe16138..84a91929a6160d6724e7ddbb1b25c723d7e60da7 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 6657c1ae8ee2ab44422f5fe7bf30ed3f45503d99..7e89333ec36d22ebdedfa96617458c5ea8bc0cd1 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 7f687e99ca53151fcccbd49e94c070fa184416b3..ff43a1afe080ae9d69fc234a872bed6bf18923b8 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 c93c673e181c678d2b5003c6087e2b55dbe56f3a..4a64f9d92fb70c755451b60949dcaafcf82036f6 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 19a711261f332841d4200b024597595a077882fc..02725ad71ef446f838288ef1823a61a035f231f1 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 29818eff2cf2dafc7083b67ccf5598d9293b70dd..3d27c36ba8de272b81fa91f56270861049922dad 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 9db467e05fce5f01652cb191a4ef603018c77832..63c374fc8804cf88e5fb2d94bffd59717e1bda95 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 471424de4c8f5c0fcfd49f295599f72c9e845734..ab3f589ceb417a3607be08c2f99a647058b0a67f 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 7b77f53af25192904b9c35d6dc15f56152a3874e..bd03357db5ad987191d7ee78d65e016f52fe791c 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 6a17c6b8426bb74077ff37e8e435e93293fccc46..ec52f8d8911d4cfa324a4f8888a504654232f7d4 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 9f45f3d678f16d88ce64d3a27351bafe295429bc..9927263df1e1fec8e896f400960815d7d4e1a612 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 4cbe891d458c6fac7738d2ce38d0b5fc3b5e6a98..70135545c5ca8b7ff92943720cac1f45dfa7c96a 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 3871a01e451cfe6dde011661ac2b0b4942854639..44cb0bfe5031c10ce9a505834988481998a85b6f 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 719d8c6de18244f8507738bb25d68335882a474a..b835f6982ff8fd9b8fe78fc63794973c10ae4223 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 2cdd52844f8b3dd1d6ea9f77b90be6a3ebeeb7cf..7b3be6015b98f0fe3c415fc1dee1e0105488f97e 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 a5c535378151910cf595a16301c5ac72aa331ff9..96bcfdbdcdf34552bad0243ce6717143c9ecc0d9 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 52d996bb0201a28fd51cfb82afb06d4714107121..2a3a6d2b1575bed6649e16d34d73779167cac8dc 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 4c5ab738c91ed7526114235000e4d9162b7f22b1..0f7c83a627ad0118bfe6d37c73e041a1e62b26bd 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 aaa3abefdbd4f3f2b6c3f3a0c98403cd4f8aa347..f107396adc8cfc9cdd40e0b34eb7a8626145cf44 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 6504639acc77d78fee02adba6c18807b8d3d0c27..06eabe4d9f0fe10af383b73f7f4a3f1019f0b296 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 dcd56fb12c71d3ca2e9cc8fa528992df29cc0cd0..e16ba064495c8f55c56d9c584c913cf85c3e4f38 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 d5c1542ac4f7e43c2a39612fd1f6f8b8205fc76c..4e033175d14ddbd54c706f56c571b3f131cde53e 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 ef47698bb6f64ba11fe048320b1996032ce0c34a..e3e8cd4ae773b5c4b6f5f0e3d795946667d2053b 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 e3a9201614e27d12a529b3bf3b659e3654f02192..c063f126339e5b511cd94963ae48f84f98c2a6e8 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 0233781eddc1f5da18be1c0812a3727ad744420a..6b4322952dc1b9a80766894a70789edfc7038604 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 026e4bbef144f7d8a119f8d9d5fee687fb3f4dd6..50566fb3407c6f21b57ddcd6cb35f96da4b686aa 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 74ba7f26de69c765049127433fb50106aa2b6dfd..8710dc8c59571250e10b104fbcb998b2d919b716 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 3d26e79512a996e7a619a62f0c495e06bb09a0ee..81bdec6072509915722c0d9d9a0c646508ea620a 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 1f7424a1ec1eae755ed5ec0b6ae0b5c396c36c94..508da20bd2bdfc7fe35da252a666b3f3a5dd159f 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 a7de0f8707ddc4ec1edc095ebf3689bf5eb99a11..7dd067ecaf93f58f6a4589f386616aedfa48f70a 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 86e9de278227b7ff043988d6464c7b6120e761ae..f55653212501766263d4bbe15d33cf5c235fcb0b 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 f0a98343e01d91146897001094205c0d8d01a50e..53c57ee917932634a7b3679989189b5acb02a2ca 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 afc1d47904c708484482355ef4be0aaf6fcd4c2b..134e80f8dafed2dc211d27d63cf0ed3076a9c401 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 02d31514dd514a5bfd5f727e2be47391a94815c2..3da46b127572f9f9ce95205ee72f90cd9cb2f21b 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 4ce316ea42cfb59cd90e1929990019505f16440e..a294b87c0249b45f73ddee723818982f93756dab 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 e6f639fa93586a5740844dada0ba1163d4c1fc34..367bdac518c2dcd8d514577f7ba79e0a7c76790c 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 dbe02ee97e287e9b51200658e62179c11806c705..d3e4601ad639de99914601753a91ff8aa6ce462f 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 e021ea6783c863b45d6d1911bf9f1b6ba0536757..7437d4c8785aee9fcf9a93441856365517afacf0 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 89bbf9a94b82384ac91ba5d41542435a548061a6..d34788a14e92d66e46d0a3a1a20c57184474b438 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 7920e6b98d14aa615660abce4145ecb3cb3ea401..aa3776502d022fb3e352cde9686ef4de5b07c548 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 75bddabfbe9edd97d7bff4bac71129cf540e7428..225763b343eb67778691e0351f5045a2cd513d96 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 38b803a26a325b0b7f87db4a9117ad74d7359762..133ae6895b7de3536fda0f7074a18a5b1f8e8bcf 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 c89b0e938c99a2943e4996d7c1664500b5b00a82..a747d91890334831c4de93c9807867ab21dea619 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 e26605a59360eb544df4097ff5dcca47545b1f6c..384a5a75de5fb66faa03dd8cbb4933b1c4c1cbd5 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 f3ef2cd1836fa72946c9c1d10fa29a89789f02f9..ac348fd03d07fe972e9e5538f9ad71fea4efd51e 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 d2039f2b5ee5f5dc7add5b7346d91dfabeb5e52a..73cabbcc28ec08211c73aa530d2c3f32b96bf86d 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 dcc566b58e8566c1d56d8ef15dbf2bd961ea6918..61b7ebb65cd4a2f8f480859232517080cf439499 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 26550ea8e34632be7655d310a94ce4ab60191d8a..f317d0df3bcefc001519a56a8c2a001604f0a30e 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 e3d9f21d1ef1d28f6ad8fc0fad2c7e32ae3899af..2ef9690828f51e9219104f370ff96285a510a3c8 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 bf53cbc448ca5002bcbb6cb8616d2642a0ed8511..1df7f9c88591481a05ac5957fbda8240e2a866ff 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 32bcce13609ed4208f028c8e73bca07ca82c2b18..ae17894128e01dbc6defcdf9c94589f425b62e21 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 3e24ef3f308c7f68f1fb6accf0ea4b6e604afe72..74e64a13210cbb7376a5e228d47c7359defd6eae 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 9716b9407fbea3d261b33f75a9297ec8ab1c7a2d..e6b8e00059815b8e65de3ba22b53eeed6b2a9635 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 6da6eec960c029d6148152240ba285080ce36e83..36ce1e3ab274fdb43433598954c5ae80b380d7b1 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 f2c564d40b49843100e080bb245424a1ef3e40e1..39664bb15a905d77a0a77b801a6851fd367fb13b 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 54917f1f76f4ed54fee8bb91fdd07ad1cd298508..17025a19ee81ea21d97060ed8bb5bb0b2ee72f77 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 6ce50be381f69a319c1fed912c25b458a733a14b..a1ab4f085fb127dcfb3a6af1403e05a688163bf6 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 33388accb3a583dcd836676cc3d80c87a1432a8d..fa0bd6646796fd980927fa0180001ce6ac37fbb1 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 43f3a37fa9f431f9d1c235a64910218094a2bdbb..7182f81e3d3d82a7c9f257404cc3817ce9efabd0 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 b574f1ebb23ff90ef20b247d80dc53950ba7cac1..f1daa120b06f0d4839dfb06037889756fb21fe82 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 1a223bf90f4bb66628d86a49641066fc554af8cc..bfb6fd16794df282bb6507aee3803eeeece3460d 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 a0229a5254addc2c7a74de23b0aa3c3121d77d29..a582605286fe4fd188a50c40f4241f7c19a5016e 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 89bdc1b2a15ac81de191637ff8a7166ea868c723..22d485e658bc051bdaf6f9158b2456e76fbaa649 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 007456238249612053c6ccc263073ada9d9840ba..e77ce2220c0e3669518cd8279a60ab09e441a171 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 08d4bb0a0ae5e99f210cb68c0d31d6be16a79d4b..670764770e98f63c776052e30aff421eee39a713 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 b58537e485ce8c45b8dc68dd97a571a1631a62a4..6e7fbc4aed230a66be52eab7df485f78ba7e881d 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 8a0fc1325ad2739c205d5f68f3c75da00e5f9f53..9b76adcf47e0bb33f3c35e7637517adc88f17534 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 76272a2c173eda3263af3b55e463cbcf37df88f2..05b096a580145808c2bfac87c0bfa277a2b31c5b 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 b63675cf0ac80af956653e6eecf3ea3e20c391c5..e44bc6c264050ba1442a65bf25ce1d89e6127b7c 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;