sync with frama-c!2347

src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c

@@ -230,6 +230,48 @@ void __gen_e_acsl_k(int x)
   return;
 }
 
+int __gen_e_acsl_k_pred(int x)
+{
+  int __retres = x > 0;
+  return __retres;
+}
+
+long __gen_e_acsl_f1(int x, int y)
+{
+  long __retres = x + (long)y;
+  return __retres;
+}
+
+void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
+                       __e_acsl_mpz_struct * y)
+{
+  __e_acsl_mpz_t __gen_e_acsl_x_3;
+  __e_acsl_mpz_t __gen_e_acsl_add_3;
+  __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
+  __gmpz_init(__gen_e_acsl_add_3);
+  __gmpz_add(__gen_e_acsl_add_3,
+             (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
+             (__e_acsl_mpz_struct const *)(y));
+  __gmpz_init_set(*__retres_arg,
+                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+  __gmpz_clear(__gen_e_acsl_x_3);
+  __gmpz_clear(__gen_e_acsl_add_3);
+  return;
+}
+
+void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+                       __e_acsl_mpz_struct * y)
+{
+  __e_acsl_mpz_t __gen_e_acsl_add_4;
+  __gmpz_init(__gen_e_acsl_add_4);
+  __gmpz_add(__gen_e_acsl_add_4,(__e_acsl_mpz_struct const *)(x),
+             (__e_acsl_mpz_struct const *)(y));
+  __gmpz_init_set(*__retres_arg,
+                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+  __gmpz_clear(__gen_e_acsl_add_4);
+  return;
+}
+
 int __gen_e_acsl_h_char(int c)
 {
   return c;
@@ -340,46 +382,4 @@ int __gen_e_acsl_p2_5(int x, long y)
   return __retres;
 }
 
-int __gen_e_acsl_k_pred(int x)
-{
-  int __retres = x > 0;
-  return __retres;
-}
-
-long __gen_e_acsl_f1(int x, int y)
-{
-  long __retres = x + (long)y;
-  return __retres;
-}
-
-void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
-                       __e_acsl_mpz_struct * y)
-{
-  __e_acsl_mpz_t __gen_e_acsl_x_3;
-  __e_acsl_mpz_t __gen_e_acsl_add_3;
-  __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
-  __gmpz_init(__gen_e_acsl_add_3);
-  __gmpz_add(__gen_e_acsl_add_3,
-             (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
-             (__e_acsl_mpz_struct const *)(y));
-  __gmpz_init_set(*__retres_arg,
-                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
-  __gmpz_clear(__gen_e_acsl_x_3);
-  __gmpz_clear(__gen_e_acsl_add_3);
-  return;
-}
-
-void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
-                       __e_acsl_mpz_struct * y)
-{
-  __e_acsl_mpz_t __gen_e_acsl_add_4;
-  __gmpz_init(__gen_e_acsl_add_4);
-  __gmpz_add(__gen_e_acsl_add_4,(__e_acsl_mpz_struct const *)(x),
-             (__e_acsl_mpz_struct const *)(y));
-  __gmpz_init_set(*__retres_arg,
-                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
-  __gmpz_clear(__gen_e_acsl_add_4);
-  return;
-}
-
 

src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c

@@ -106,6 +106,76 @@ int main(void)
   return __retres;
 }
 
+int __gen_e_acsl_f3(int n)
+{
+  int __gen_e_acsl_if_6;
+  if (n > 0) {
+    int __gen_e_acsl_g_2;
+    int __gen_e_acsl_f3_5;
+    __gen_e_acsl_g_2 = __gen_e_acsl_g(n);
+    __gen_e_acsl_f3_5 = __gen_e_acsl_f3_2(n - 1L);
+    __gen_e_acsl_if_6 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_5 - 5;
+  }
+  else {
+    int __gen_e_acsl_g_8;
+    __gen_e_acsl_g_8 = __gen_e_acsl_g_5(n + 1L);
+    __gen_e_acsl_if_6 = __gen_e_acsl_g_8;
+  }
+  return __gen_e_acsl_if_6;
+}
+
+int __gen_e_acsl_f3_2(long n)
+{
+  int __gen_e_acsl_if_5;
+  if (n > 0L) {
+    int __gen_e_acsl_g_4;
+    int __gen_e_acsl_f3_4;
+    __gen_e_acsl_g_4 = __gen_e_acsl_g((int)n);
+    __gen_e_acsl_f3_4 = __gen_e_acsl_f3_2(n - 1L);
+    __gen_e_acsl_if_5 = __gen_e_acsl_g_4 * __gen_e_acsl_f3_4 - 5;
+  }
+  else {
+    int __gen_e_acsl_g_6;
+    __gen_e_acsl_g_6 = __gen_e_acsl_g_5(n + 1L);
+    __gen_e_acsl_if_5 = __gen_e_acsl_g_6;
+  }
+  return __gen_e_acsl_if_5;
+}
+
+unsigned long __gen_e_acsl_f4(int n)
+{
+  unsigned long __gen_e_acsl_if_10;
+  if (n < 100) {
+    unsigned long __gen_e_acsl_f4_5;
+    __gen_e_acsl_f4_5 = __gen_e_acsl_f4_2(n + 1L);
+    __gen_e_acsl_if_10 = __gen_e_acsl_f4_5;
+  }
+  else {
+    unsigned long __gen_e_acsl_if_9;
+    if ((long)n < 9223372036854775807L) __gen_e_acsl_if_9 = 9223372036854775807UL;
+    else __gen_e_acsl_if_9 = 6UL;
+    __gen_e_acsl_if_10 = __gen_e_acsl_if_9;
+  }
+  return __gen_e_acsl_if_10;
+}
+
+unsigned long __gen_e_acsl_f4_2(long n)
+{
+  unsigned long __gen_e_acsl_if_8;
+  if (n < 100L) {
+    unsigned long __gen_e_acsl_f4_4;
+    __gen_e_acsl_f4_4 = __gen_e_acsl_f4_2(n + 1L);
+    __gen_e_acsl_if_8 = __gen_e_acsl_f4_4;
+  }
+  else {
+    unsigned long __gen_e_acsl_if_7;
+    if (n < 9223372036854775807L) __gen_e_acsl_if_7 = 9223372036854775807UL;
+    else __gen_e_acsl_if_7 = 6UL;
+    __gen_e_acsl_if_8 = __gen_e_acsl_if_7;
+  }
+  return __gen_e_acsl_if_8;
+}
+
 void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int n)
 {
   __e_acsl_mpz_t __gen_e_acsl_if_2;
@@ -246,74 +316,4 @@ int __gen_e_acsl_g_5(long n)
   return __retres;
 }
 
-int __gen_e_acsl_f3(int n)
-{
-  int __gen_e_acsl_if_6;
-  if (n > 0) {
-    int __gen_e_acsl_g_2;
-    int __gen_e_acsl_f3_5;
-    __gen_e_acsl_g_2 = __gen_e_acsl_g(n);
-    __gen_e_acsl_f3_5 = __gen_e_acsl_f3_2(n - 1L);
-    __gen_e_acsl_if_6 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_5 - 5;
-  }
-  else {
-    int __gen_e_acsl_g_8;
-    __gen_e_acsl_g_8 = __gen_e_acsl_g_5(n + 1L);
-    __gen_e_acsl_if_6 = __gen_e_acsl_g_8;
-  }
-  return __gen_e_acsl_if_6;
-}
-
-int __gen_e_acsl_f3_2(long n)
-{
-  int __gen_e_acsl_if_5;
-  if (n > 0L) {
-    int __gen_e_acsl_g_4;
-    int __gen_e_acsl_f3_4;
-    __gen_e_acsl_g_4 = __gen_e_acsl_g((int)n);
-    __gen_e_acsl_f3_4 = __gen_e_acsl_f3_2(n - 1L);
-    __gen_e_acsl_if_5 = __gen_e_acsl_g_4 * __gen_e_acsl_f3_4 - 5;
-  }
-  else {
-    int __gen_e_acsl_g_6;
-    __gen_e_acsl_g_6 = __gen_e_acsl_g_5(n + 1L);
-    __gen_e_acsl_if_5 = __gen_e_acsl_g_6;
-  }
-  return __gen_e_acsl_if_5;
-}
-
-unsigned long __gen_e_acsl_f4(int n)
-{
-  unsigned long __gen_e_acsl_if_10;
-  if (n < 100) {
-    unsigned long __gen_e_acsl_f4_5;
-    __gen_e_acsl_f4_5 = __gen_e_acsl_f4_2(n + 1L);
-    __gen_e_acsl_if_10 = __gen_e_acsl_f4_5;
-  }
-  else {
-    unsigned long __gen_e_acsl_if_9;
-    if ((long)n < 9223372036854775807L) __gen_e_acsl_if_9 = 9223372036854775807UL;
-    else __gen_e_acsl_if_9 = 6UL;
-    __gen_e_acsl_if_10 = __gen_e_acsl_if_9;
-  }
-  return __gen_e_acsl_if_10;
-}
-
-unsigned long __gen_e_acsl_f4_2(long n)
-{
-  unsigned long __gen_e_acsl_if_8;
-  if (n < 100L) {
-    unsigned long __gen_e_acsl_f4_4;
-    __gen_e_acsl_f4_4 = __gen_e_acsl_f4_2(n + 1L);
-    __gen_e_acsl_if_8 = __gen_e_acsl_f4_4;
-  }
-  else {
-    unsigned long __gen_e_acsl_if_7;
-    if (n < 9223372036854775807L) __gen_e_acsl_if_7 = 9223372036854775807UL;
-    else __gen_e_acsl_if_7 = 6UL;
-    __gen_e_acsl_if_8 = __gen_e_acsl_if_7;
-  }
-  return __gen_e_acsl_if_8;
-}
-
 

src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle

 [e-acsl] beginning translation.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:169: Warning: 
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:211: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
 [e-acsl] translation done in project "e-acsl".

src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle

@@ -15,15 +15,15 @@
 [e-acsl] Warning: annotating undefined function `waitpid':
   the generated program may miss memory instrumentation
   if there are memory-related annotations.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:165: Warning: 
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:207: Warning: 
   Neither code nor specification for function fprintf, generating default assigns from the prototype
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:169: Warning: 
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:211: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:171: Warning: 
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:213: Warning: 
   Neither code nor specification for function snprintf, generating default assigns from the prototype
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:173: Warning: 
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:215: Warning: 
   Neither code nor specification for function sprintf, generating default assigns from the prototype
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:369: Warning: 
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:521: Warning: 
   Neither code nor specification for function dprintf, generating default assigns from the prototype
 [kernel:annot:missing-spec] tests/format/fprintf.c:16: Warning: 
   Neither code nor specification for function fork, generating default assigns from the prototype
@@ -33,20 +33,20 @@
 [e-acsl] FRAMAC_SHARE/libc/sys/wait.h:86: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:94: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:120: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:96: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:122: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:82: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:97: Warning: 
   E-ACSL construct `predicate with no definition nor reads clause'
   is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:82: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:97: Warning: 
   E-ACSL construct `assigns clause in behavior' is not yet supported.
   Ignoring annotation.
-[e-acsl] FRAMAC_SHARE/libc/stdio.h:82: Warning: 
+[e-acsl] FRAMAC_SHARE/libc/stdio.h:97: Warning: 
   E-ACSL construct `abnormal termination case in behavior'
   is not yet supported.
   Ignoring annotation.
@@ -67,7 +67,7 @@
   accessing uninitialized left-value. assert \initialized(&process_status_0);
 [eva:alarm] tests/format/fprintf.c:20: Warning: 
   accessing uninitialized left-value. assert \initialized(&process_status_1);
-[eva:alarm] FRAMAC_SHARE/libc/stdio.h:94: Warning: 
+[eva:alarm] FRAMAC_SHARE/libc/stdio.h:120: Warning: 
   function __e_acsl_assert: precondition got status unknown.
 [eva:alarm] tests/format/fprintf.c:22: Warning: 
   accessing uninitialized left-value. assert \initialized(&process_status_2);

src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c

@@ -35,10 +35,16 @@ void __e_acsl_globals_init(void)
     __e_acsl_already_run = 1;
     __e_acsl_store_block((void *)(& f),(size_t)1);
     __e_acsl_full_init((void *)(& f));
+    __e_acsl_store_block((void *)(& __fc_p_tmpnam),(size_t)8);
+    __e_acsl_full_init((void *)(& __fc_p_tmpnam));
+    __e_acsl_store_block((void *)(__fc_tmpnam),(size_t)2048);
+    __e_acsl_full_init((void *)(& __fc_tmpnam));
     __e_acsl_store_block((void *)(& __fc_p_fopen),(size_t)8);
     __e_acsl_full_init((void *)(& __fc_p_fopen));
     __e_acsl_store_block((void *)(__fc_fopen),(size_t)128);
     __e_acsl_full_init((void *)(& __fc_fopen));
+    __e_acsl_store_block((void *)(& stdin),(size_t)8);
+    __e_acsl_full_init((void *)(& stdin));
     __e_acsl_store_block((void *)(& __fc_p_random48_counter),(size_t)8);
     __e_acsl_full_init((void *)(& __fc_p_random48_counter));
     __e_acsl_store_block((void *)(random48_counter),(size_t)6);
@@ -67,8 +73,11 @@ int main(void)
   __e_acsl_full_init((void *)(& __retres));
   __retres = 0;
   __e_acsl_delete_block((void *)(& f));
+  __e_acsl_delete_block((void *)(& __fc_p_tmpnam));
+  __e_acsl_delete_block((void *)(__fc_tmpnam));
   __e_acsl_delete_block((void *)(& __fc_p_fopen));
   __e_acsl_delete_block((void *)(__fc_fopen));
+  __e_acsl_delete_block((void *)(& stdin));
   __e_acsl_delete_block((void *)(& __fc_p_random48_counter));
   __e_acsl_delete_block((void *)(random48_counter));
   __e_acsl_delete_block((void *)(& __fc_random48_init));

src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c

@@ -276,6 +276,70 @@ void __gen_e_acsl_k(int x)
   return;
 }
 
+int __gen_e_acsl_k_pred(int x)
+{
+  __e_acsl_mpz_t __gen_e_acsl_x;
+  __e_acsl_mpz_t __gen_e_acsl_;
+  int __gen_e_acsl_gt;
+  __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
+  __gmpz_init_set_si(__gen_e_acsl_,0L);
+  __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+                               (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+  int __retres = __gen_e_acsl_gt > 0;
+  __gmpz_clear(__gen_e_acsl_x);
+  __gmpz_clear(__gen_e_acsl_);
+  return __retres;
+}
+
+void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
+{
+  __e_acsl_mpz_t __gen_e_acsl_x_4;
+  __e_acsl_mpz_t __gen_e_acsl_y_3;
+  __e_acsl_mpz_t __gen_e_acsl_add_4;
+  __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
+  __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
+  __gmpz_init(__gen_e_acsl_add_4);
+  __gmpz_add(__gen_e_acsl_add_4,
+             (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
+             (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3));
+  __gmpz_init_set(*__retres_arg,
+                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
+  __gmpz_clear(__gen_e_acsl_x_4);
+  __gmpz_clear(__gen_e_acsl_y_3);
+  __gmpz_clear(__gen_e_acsl_add_4);
+  return;
+}
+
+void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
+                       __e_acsl_mpz_struct * y)
+{
+  __e_acsl_mpz_t __gen_e_acsl_x_5;
+  __e_acsl_mpz_t __gen_e_acsl_add_5;
+  __gmpz_init_set_si(__gen_e_acsl_x_5,(long)x);
+  __gmpz_init(__gen_e_acsl_add_5);
+  __gmpz_add(__gen_e_acsl_add_5,
+             (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
+             (__e_acsl_mpz_struct const *)(y));
+  __gmpz_init_set(*__retres_arg,
+                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
+  __gmpz_clear(__gen_e_acsl_x_5);
+  __gmpz_clear(__gen_e_acsl_add_5);
+  return;
+}
+
+void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
+                       __e_acsl_mpz_struct * y)
+{
+  __e_acsl_mpz_t __gen_e_acsl_add_6;
+  __gmpz_init(__gen_e_acsl_add_6);
+  __gmpz_add(__gen_e_acsl_add_6,(__e_acsl_mpz_struct const *)(x),
+             (__e_acsl_mpz_struct const *)(y));
+  __gmpz_init_set(*__retres_arg,
+                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
+  __gmpz_clear(__gen_e_acsl_add_6);
+  return;
+}
+
 int __gen_e_acsl_h_char(int c)
 {
   return c;
@@ -412,68 +476,4 @@ int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
   return __retres;
 }
 
-int __gen_e_acsl_k_pred(int x)
-{
-  __e_acsl_mpz_t __gen_e_acsl_x;
-  __e_acsl_mpz_t __gen_e_acsl_;
-  int __gen_e_acsl_gt;
-  __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
-  __gmpz_init_set_si(__gen_e_acsl_,0L);
-  __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
-                               (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
-  int __retres = __gen_e_acsl_gt > 0;
-  __gmpz_clear(__gen_e_acsl_x);
-  __gmpz_clear(__gen_e_acsl_);
-  return __retres;
-}
-
-void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
-{
-  __e_acsl_mpz_t __gen_e_acsl_x_4;
-  __e_acsl_mpz_t __gen_e_acsl_y_3;
-  __e_acsl_mpz_t __gen_e_acsl_add_4;
-  __gmpz_init_set_si(__gen_e_acsl_x_4,(long)x);
-  __gmpz_init_set_si(__gen_e_acsl_y_3,(long)y);
-  __gmpz_init(__gen_e_acsl_add_4);
-  __gmpz_add(__gen_e_acsl_add_4,
-             (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_4),
-             (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_3));
-  __gmpz_init_set(*__retres_arg,
-                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_4));
-  __gmpz_clear(__gen_e_acsl_x_4);
-  __gmpz_clear(__gen_e_acsl_y_3);
-  __gmpz_clear(__gen_e_acsl_add_4);
-  return;
-}
-
-void __gen_e_acsl_f1_5(__e_acsl_mpz_t *__retres_arg, int x,
-                       __e_acsl_mpz_struct * y)
-{
-  __e_acsl_mpz_t __gen_e_acsl_x_5;
-  __e_acsl_mpz_t __gen_e_acsl_add_5;
-  __gmpz_init_set_si(__gen_e_acsl_x_5,(long)x);
-  __gmpz_init(__gen_e_acsl_add_5);
-  __gmpz_add(__gen_e_acsl_add_5,
-             (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_5),
-             (__e_acsl_mpz_struct const *)(y));
-  __gmpz_init_set(*__retres_arg,
-                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
-  __gmpz_clear(__gen_e_acsl_x_5);
-  __gmpz_clear(__gen_e_acsl_add_5);
-  return;
-}
-
-void __gen_e_acsl_f1_7(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * x,
-                       __e_acsl_mpz_struct * y)
-{
-  __e_acsl_mpz_t __gen_e_acsl_add_6;
-  __gmpz_init(__gen_e_acsl_add_6);
-  __gmpz_add(__gen_e_acsl_add_6,(__e_acsl_mpz_struct const *)(x),
-             (__e_acsl_mpz_struct const *)(y));
-  __gmpz_init_set(*__retres_arg,
-                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
-  __gmpz_clear(__gen_e_acsl_add_6);
-  return;
-}
-
 

src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle

 [e-acsl] beginning translation.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:169: Warning: 
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:211: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
 [e-acsl] translation done in project "e-acsl".

src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle

 [e-acsl] beginning translation.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:169: Warning: 
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:211: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
 [e-acsl] translation done in project "e-acsl".

src/plugins/e-acsl/tests/temporal/oracle_ci/t_malloc-asan.res.oracle

 [e-acsl] beginning translation.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:169: Warning: 
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:211: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
 [e-acsl] translation done in project "e-acsl".
 [eva:alarm] tests/temporal/t_malloc-asan.c:28: Warning: