From 8d4812c8933b3b1bedc0f4519d55bb90b7175eb5 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 10 Jun 2020 13:07:43 +0200
Subject: [PATCH] [e-acsl] fix tests

---
 .../tests/arith/oracle_ci/gen_functions.c     | 102 ++++++-------
 .../tests/arith/oracle_ci/gen_functions_rec.c | 140 +++++++++---------
 .../tests/gmp-only/oracle_ci/gen_functions.c  | 128 ++++++++--------
 3 files changed, 185 insertions(+), 185 deletions(-)

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 cfdc4b4830a..80def032755 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
@@ -232,6 +232,57 @@ void __gen_e_acsl_k(int x)
   return;
 }
 
+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;
+}
+
+int __gen_e_acsl_h_short(int s)
+{
+  return s;
+}
+
+int __gen_e_acsl_g_hidden(int x)
+{
+  return x;
+}
+
 double __gen_e_acsl_f2(double x)
 {
   __e_acsl_mpq_t __gen_e_acsl__8;
@@ -333,55 +384,4 @@ int __gen_e_acsl_k_pred(int x)
   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;
-}
-
-int __gen_e_acsl_h_short(int s)
-{
-  return s;
-}
-
-int __gen_e_acsl_g_hidden(int x)
-{
-  return x;
-}
-
 
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
index b9015c95933..df6e9ac544b 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
@@ -105,6 +105,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;
@@ -247,74 +317,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;
-}
-
 
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 19175f48356..2692583c529 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
@@ -277,6 +277,70 @@ void __gen_e_acsl_k(int x)
   return;
 }
 
+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;
+}
+
+int __gen_e_acsl_h_short(int s)
+{
+  return s;
+}
+
+int __gen_e_acsl_g_hidden(int x)
+{
+  return x;
+}
+
 double __gen_e_acsl_f2(double x)
 {
   __e_acsl_mpq_t __gen_e_acsl__13;
@@ -413,68 +477,4 @@ int __gen_e_acsl_k_pred(int x)
   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;
-}
-
-int __gen_e_acsl_h_short(int s)
-{
-  return s;
-}
-
-int __gen_e_acsl_g_hidden(int x)
-{
-  return x;
-}
-
 
-- 
GitLab