diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
index ff3377f7af83998145077713848304f591b5c218..fa452142c65806d3a2aa27294f056f66985e4693 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
@@ -15,25 +15,25 @@ int __gen_e_acsl_p1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
/*@ predicate p2(ℤ x, ℤ y) = x + y > 0;
*/
-int __gen_e_acsl_p2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
-
int __gen_e_acsl_p2_3(int __gen_e_acsl_x_arg, long __gen_e_acsl_y_arg);
+int __gen_e_acsl_p2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
+
int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg);
/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
*/
-void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_y_arg);
+long __gen_e_acsl_f1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
int __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg);
-long __gen_e_acsl_f1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
+void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg);
/*@ logic char h_char(char c) = c;
*/
@@ -283,11 +283,27 @@ char __gen_e_acsl_h_char(int __gen_e_acsl_c_arg)
return __retres;
}
-long __gen_e_acsl_f1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
+void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
{
- long __retres;
- __retres = __gen_e_acsl_x_arg + (long)__gen_e_acsl_y_arg;
- return __retres;
+ __e_acsl_mpz_t __gen_e_acsl_x_4;
+ __e_acsl_mpz_t __gen_e_acsl_y_4;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __gmpz_init_set(__gen_e_acsl_x_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_arg));
+ __gmpz_init_set(__gen_e_acsl_y_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
+ __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_4));
+ __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_4);
+ __gmpz_clear(__gen_e_acsl_add_4);
+ return;
}
void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
@@ -312,27 +328,11 @@ void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
return;
}
-void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
+long __gen_e_acsl_f1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
{
- __e_acsl_mpz_t __gen_e_acsl_x_4;
- __e_acsl_mpz_t __gen_e_acsl_y_4;
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- __gmpz_init_set(__gen_e_acsl_x_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_arg));
- __gmpz_init_set(__gen_e_acsl_y_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
- __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_4));
- __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_4);
- __gmpz_clear(__gen_e_acsl_add_4);
- return;
+ long __retres;
+ __retres = __gen_e_acsl_x_arg + (long)__gen_e_acsl_y_arg;
+ return __retres;
}
int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
@@ -361,6 +361,13 @@ int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
return __retres;
}
+int __gen_e_acsl_p2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
+{
+ int __retres;
+ __retres = __gen_e_acsl_x_arg + (long)__gen_e_acsl_y_arg > 0L;
+ return __retres;
+}
+
int __gen_e_acsl_p2_3(int __gen_e_acsl_x_arg, long __gen_e_acsl_y_arg)
{
int __retres;
@@ -386,13 +393,6 @@ int __gen_e_acsl_p2_3(int __gen_e_acsl_x_arg, long __gen_e_acsl_y_arg)
return __retres;
}
-int __gen_e_acsl_p2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
-{
- int __retres;
- __retres = __gen_e_acsl_x_arg + (long)__gen_e_acsl_y_arg > 0L;
- return __retres;
-}
-
int __gen_e_acsl_p1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
{
int __retres;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
index a06e1629b8c1f2bd11e05973dd83841c789b3e17..f742b5af9b1f4f310a24d50cf6083b93638113a6 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
@@ -23,10 +23,6 @@ int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
*/
-void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_y_arg);
-
void __gen_e_acsl_f1(__e_acsl_mpz_struct * __retres_arg,
int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
@@ -34,6 +30,10 @@ void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
int __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg);
+void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg);
+
/*@ logic char h_char(char c) = c;
*/
char __gen_e_acsl_h_char(int __gen_e_acsl_c_arg);
@@ -352,6 +352,29 @@ char __gen_e_acsl_h_char(int __gen_e_acsl_c_arg)
return __retres;
}
+void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_x_6;
+ __e_acsl_mpz_t __gen_e_acsl_y_6;
+ __e_acsl_mpz_t __gen_e_acsl_add_6;
+ __gmpz_init_set(__gen_e_acsl_x_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_arg));
+ __gmpz_init_set(__gen_e_acsl_y_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
+ __gmpz_init(__gen_e_acsl_add_6);
+ __gmpz_add(__gen_e_acsl_add_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_6));
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
+ __gmpz_clear(__gen_e_acsl_x_6);
+ __gmpz_clear(__gen_e_acsl_y_6);
+ __gmpz_clear(__gen_e_acsl_add_6);
+ return;
+}
+
void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
int __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg)
@@ -394,29 +417,6 @@ void __gen_e_acsl_f1(__e_acsl_mpz_struct * __retres_arg,
return;
}
-void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_x_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
-{
- __e_acsl_mpz_t __gen_e_acsl_x_6;
- __e_acsl_mpz_t __gen_e_acsl_y_6;
- __e_acsl_mpz_t __gen_e_acsl_add_6;
- __gmpz_init_set(__gen_e_acsl_x_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_arg));
- __gmpz_init_set(__gen_e_acsl_y_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
- __gmpz_init(__gen_e_acsl_add_6);
- __gmpz_add(__gen_e_acsl_add_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_6));
- __gmpz_init_set(__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_6));
- __gmpz_clear(__gen_e_acsl_x_6);
- __gmpz_clear(__gen_e_acsl_y_6);
- __gmpz_clear(__gen_e_acsl_add_6);
- return;
-}
-
int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg)
{
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
index b4ac4d23a38a3311fa9e082569097e0965709471..57ff6cf62739bee6687132cc3056b78fd10db0c5 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
@@ -4,40 +4,40 @@
/*@ logic ℤ f1(ℤ n) = n ≤ 0? 0: f1(n - 1) + n;
*/
-void __gen_e_acsl_f1(__e_acsl_mpz_struct * __retres_arg,
- int __gen_e_acsl_n_arg);
-
void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
long __gen_e_acsl_n_arg);
+void __gen_e_acsl_f1(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg);
+
void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
__e_acsl_mpz_struct * __gen_e_acsl_n_arg);
/*@ logic ℤ f2(ℤ n) = n < 0? 1: (f2(n - 1) * f2(n - 2)) / f2(n - 3);
*/
-int __gen_e_acsl_f2(int __gen_e_acsl_n_arg);
-
int __gen_e_acsl_f2_2(long __gen_e_acsl_n_arg);
+int __gen_e_acsl_f2(int __gen_e_acsl_n_arg);
+
int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg);
/*@ logic ℤ g(ℤ n) = 0;
*/
-int __gen_e_acsl_g(int __gen_e_acsl_n_arg);
-
int __gen_e_acsl_g_2(long __gen_e_acsl_n_arg);
+int __gen_e_acsl_g(int __gen_e_acsl_n_arg);
+
int __gen_e_acsl_g_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg);
/*@ logic ℤ f3(ℤ n) = n > 0? g(n) * f3(n - 1) - 5: g(n + 1);
*/
-int __gen_e_acsl_f3(int __gen_e_acsl_n_arg);
-
int __gen_e_acsl_f3_2(long __gen_e_acsl_n_arg);
+int __gen_e_acsl_f3(int __gen_e_acsl_n_arg);
+
int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg);
/*@
@@ -45,10 +45,10 @@ logic ℤ f4(ℤ n) =
n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
*/
-unsigned long __gen_e_acsl_f4(int __gen_e_acsl_n_arg);
-
unsigned long __gen_e_acsl_f4_2(long __gen_e_acsl_n_arg);
+unsigned long __gen_e_acsl_f4(int __gen_e_acsl_n_arg);
+
unsigned long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg);
int main(void)
@@ -173,6 +173,25 @@ unsigned long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
return __retres;
}
+unsigned long __gen_e_acsl_f4(int __gen_e_acsl_n_arg)
+{
+ unsigned long __retres;
+ unsigned long __gen_e_acsl_if_15;
+ if (__gen_e_acsl_n_arg < 100) {
+ unsigned long __gen_e_acsl_f4_tapp_2;
+ __gen_e_acsl_f4_tapp_2 = __gen_e_acsl_f4_2(__gen_e_acsl_n_arg + 1L);
+ __gen_e_acsl_if_15 = __gen_e_acsl_f4_tapp_2;
+ }
+ else {
+ unsigned long __gen_e_acsl_if_14;
+ if ((long)__gen_e_acsl_n_arg < 9223372036854775807L) __gen_e_acsl_if_14 = 9223372036854775807UL;
+ else __gen_e_acsl_if_14 = 6UL;
+ __gen_e_acsl_if_15 = __gen_e_acsl_if_14;
+ }
+ __retres = __gen_e_acsl_if_15;
+ return __retres;
+}
+
unsigned long __gen_e_acsl_f4_2(long __gen_e_acsl_n_arg)
{
unsigned long __retres;
@@ -204,25 +223,6 @@ unsigned long __gen_e_acsl_f4_2(long __gen_e_acsl_n_arg)
return __retres;
}
-unsigned long __gen_e_acsl_f4(int __gen_e_acsl_n_arg)
-{
- unsigned long __retres;
- unsigned long __gen_e_acsl_if_15;
- if (__gen_e_acsl_n_arg < 100) {
- unsigned long __gen_e_acsl_f4_tapp_2;
- __gen_e_acsl_f4_tapp_2 = __gen_e_acsl_f4_2(__gen_e_acsl_n_arg + 1L);
- __gen_e_acsl_if_15 = __gen_e_acsl_f4_tapp_2;
- }
- else {
- unsigned long __gen_e_acsl_if_14;
- if ((long)__gen_e_acsl_n_arg < 9223372036854775807L) __gen_e_acsl_if_14 = 9223372036854775807UL;
- else __gen_e_acsl_if_14 = 6UL;
- __gen_e_acsl_if_15 = __gen_e_acsl_if_14;
- }
- __retres = __gen_e_acsl_if_15;
- return __retres;
-}
-
int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
{
int __retres;
@@ -271,6 +271,26 @@ int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
return __retres;
}
+int __gen_e_acsl_f3(int __gen_e_acsl_n_arg)
+{
+ int __retres;
+ int __gen_e_acsl_if_9;
+ if (__gen_e_acsl_n_arg > 0) {
+ int __gen_e_acsl_g_tapp;
+ int __gen_e_acsl_f3_tapp_2;
+ __gen_e_acsl_g_tapp = __gen_e_acsl_g(__gen_e_acsl_n_arg);
+ __gen_e_acsl_f3_tapp_2 = __gen_e_acsl_f3_2(__gen_e_acsl_n_arg - 1L);
+ __gen_e_acsl_if_9 = __gen_e_acsl_g_tapp * __gen_e_acsl_f3_tapp_2 - 5;
+ }
+ else {
+ int __gen_e_acsl_g_tapp_6;
+ __gen_e_acsl_g_tapp_6 = __gen_e_acsl_g_2(__gen_e_acsl_n_arg + 1L);
+ __gen_e_acsl_if_9 = __gen_e_acsl_g_tapp_6;
+ }
+ __retres = __gen_e_acsl_if_9;
+ return __retres;
+}
+
int __gen_e_acsl_f3_2(long __gen_e_acsl_n_arg)
{
int __retres;
@@ -315,26 +335,6 @@ int __gen_e_acsl_f3_2(long __gen_e_acsl_n_arg)
return __retres;
}
-int __gen_e_acsl_f3(int __gen_e_acsl_n_arg)
-{
- int __retres;
- int __gen_e_acsl_if_9;
- if (__gen_e_acsl_n_arg > 0) {
- int __gen_e_acsl_g_tapp;
- int __gen_e_acsl_f3_tapp_2;
- __gen_e_acsl_g_tapp = __gen_e_acsl_g(__gen_e_acsl_n_arg);
- __gen_e_acsl_f3_tapp_2 = __gen_e_acsl_f3_2(__gen_e_acsl_n_arg - 1L);
- __gen_e_acsl_if_9 = __gen_e_acsl_g_tapp * __gen_e_acsl_f3_tapp_2 - 5;
- }
- else {
- int __gen_e_acsl_g_tapp_6;
- __gen_e_acsl_g_tapp_6 = __gen_e_acsl_g_2(__gen_e_acsl_n_arg + 1L);
- __gen_e_acsl_if_9 = __gen_e_acsl_g_tapp_6;
- }
- __retres = __gen_e_acsl_if_9;
- return __retres;
-}
-
int __gen_e_acsl_g_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
{
int __retres;
@@ -346,14 +346,14 @@ int __gen_e_acsl_g_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
return __retres;
}
-int __gen_e_acsl_g_2(long __gen_e_acsl_n_arg)
+int __gen_e_acsl_g(int __gen_e_acsl_n_arg)
{
int __retres;
__retres = 0;
return __retres;
}
-int __gen_e_acsl_g(int __gen_e_acsl_n_arg)
+int __gen_e_acsl_g_2(long __gen_e_acsl_n_arg)
{
int __retres;
__retres = 0;
@@ -418,6 +418,27 @@ int __gen_e_acsl_f2_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
return __retres;
}
+int __gen_e_acsl_f2(int __gen_e_acsl_n_arg)
+{
+ int __retres;
+ int __gen_e_acsl_if_6;
+ if (__gen_e_acsl_n_arg < 0) __gen_e_acsl_if_6 = 1;
+ else {
+ int __gen_e_acsl_f2_tapp_2;
+ int __gen_e_acsl_f2_tapp_9;
+ int __gen_e_acsl_f2_tapp_10;
+ __gen_e_acsl_f2_tapp_2 = __gen_e_acsl_f2_2(__gen_e_acsl_n_arg - 1L);
+ __gen_e_acsl_f2_tapp_9 = __gen_e_acsl_f2_2(__gen_e_acsl_n_arg - 2L);
+ __gen_e_acsl_f2_tapp_10 = __gen_e_acsl_f2_2(__gen_e_acsl_n_arg - 3L);
+ __e_acsl_assert(__gen_e_acsl_f2_tapp_10 != 0,(char *)"RTE",(char *)"f2",
+ (char *)"division_by_zero: __gen_e_acsl_f2_tapp_10 != 0",
+ 9);
+ __gen_e_acsl_if_6 = (__gen_e_acsl_f2_tapp_2 * __gen_e_acsl_f2_tapp_9) / __gen_e_acsl_f2_tapp_10;
+ }
+ __retres = __gen_e_acsl_if_6;
+ return __retres;
+}
+
int __gen_e_acsl_f2_2(long __gen_e_acsl_n_arg)
{
int __retres;
@@ -469,27 +490,6 @@ int __gen_e_acsl_f2_2(long __gen_e_acsl_n_arg)
return __retres;
}
-int __gen_e_acsl_f2(int __gen_e_acsl_n_arg)
-{
- int __retres;
- int __gen_e_acsl_if_6;
- if (__gen_e_acsl_n_arg < 0) __gen_e_acsl_if_6 = 1;
- else {
- int __gen_e_acsl_f2_tapp_2;
- int __gen_e_acsl_f2_tapp_9;
- int __gen_e_acsl_f2_tapp_10;
- __gen_e_acsl_f2_tapp_2 = __gen_e_acsl_f2_2(__gen_e_acsl_n_arg - 1L);
- __gen_e_acsl_f2_tapp_9 = __gen_e_acsl_f2_2(__gen_e_acsl_n_arg - 2L);
- __gen_e_acsl_f2_tapp_10 = __gen_e_acsl_f2_2(__gen_e_acsl_n_arg - 3L);
- __e_acsl_assert(__gen_e_acsl_f2_tapp_10 != 0,(char *)"RTE",(char *)"f2",
- (char *)"division_by_zero: __gen_e_acsl_f2_tapp_10 != 0",
- 9);
- __gen_e_acsl_if_6 = (__gen_e_acsl_f2_tapp_2 * __gen_e_acsl_f2_tapp_9) / __gen_e_acsl_f2_tapp_10;
- }
- __retres = __gen_e_acsl_if_6;
- return __retres;
-}
-
void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
{
@@ -541,6 +541,41 @@ void __gen_e_acsl_f1_3(__e_acsl_mpz_struct * __retres_arg,
return;
}
+void __gen_e_acsl_f1(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_if_3;
+ if (__gen_e_acsl_n_arg <= 0) {
+ __e_acsl_mpz_t __gen_e_acsl_;
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ __gmpz_clear(__gen_e_acsl_);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_f1_tapp_2;
+ __e_acsl_mpz_t __gen_e_acsl_n_3;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __gmpz_init(__gen_e_acsl_f1_tapp_2);
+ __gen_e_acsl_f1_2((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_2,
+ __gen_e_acsl_n_arg - 1L);
+ __gmpz_init_set_si(__gen_e_acsl_n_3,(long)__gen_e_acsl_n_arg);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3));
+ __gmpz_init_set(__gen_e_acsl_if_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
+ __gmpz_clear(__gen_e_acsl_f1_tapp_2);
+ __gmpz_clear(__gen_e_acsl_n_3);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ }
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_3));
+ __gmpz_clear(__gen_e_acsl_if_3);
+ return;
+}
+
void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
long __gen_e_acsl_n_arg)
{
@@ -585,39 +620,4 @@ void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
return;
}
-void __gen_e_acsl_f1(__e_acsl_mpz_struct * __retres_arg,
- int __gen_e_acsl_n_arg)
-{
- __e_acsl_mpz_t __gen_e_acsl_if_3;
- if (__gen_e_acsl_n_arg <= 0) {
- __e_acsl_mpz_t __gen_e_acsl_;
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gmpz_init_set(__gen_e_acsl_if_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- __gmpz_clear(__gen_e_acsl_);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_f1_tapp_2;
- __e_acsl_mpz_t __gen_e_acsl_n_3;
- __e_acsl_mpz_t __gen_e_acsl_add_3;
- __gmpz_init(__gen_e_acsl_f1_tapp_2);
- __gen_e_acsl_f1_2((__e_acsl_mpz_struct *)__gen_e_acsl_f1_tapp_2,
- __gen_e_acsl_n_arg - 1L);
- __gmpz_init_set_si(__gen_e_acsl_n_3,(long)__gen_e_acsl_n_arg);
- __gmpz_init(__gen_e_acsl_add_3);
- __gmpz_add(__gen_e_acsl_add_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_tapp_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3));
- __gmpz_init_set(__gen_e_acsl_if_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3));
- __gmpz_clear(__gen_e_acsl_f1_tapp_2);
- __gmpz_clear(__gen_e_acsl_n_3);
- __gmpz_clear(__gen_e_acsl_add_3);
- }
- __gmpz_init_set(__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_3));
- __gmpz_clear(__gen_e_acsl_if_3);
- return;
-}
-
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c
index fe7af1124fe838af0a4e417f92b2d00509013a15..114902cf4bcf17a3454aa703c089715dd22738c4 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c
@@ -42,12 +42,12 @@ logic ℤ f4(ℤ n) =
n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
*/
-void __gen_e_acsl_f4_2(__e_acsl_mpz_struct * __retres_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_n_arg);
-
void __gen_e_acsl_f4(__e_acsl_mpz_struct * __retres_arg,
int __gen_e_acsl_n_arg);
+void __gen_e_acsl_f4_2(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg);
+
int main(void)
{
int __retres;
@@ -155,6 +155,70 @@ int main(void)
return __retres;
}
+void __gen_e_acsl_f4_2(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n_14;
+ __e_acsl_mpz_t __gen_e_acsl__36;
+ int __gen_e_acsl_lt_4;
+ __e_acsl_mpz_t __gen_e_acsl_if_8;
+ __gmpz_init_set(__gen_e_acsl_n_14,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_arg));
+ __gmpz_init_set_si(__gen_e_acsl__36,100L);
+ __gen_e_acsl_lt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_14),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__36));
+ if (__gen_e_acsl_lt_4 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__37;
+ __e_acsl_mpz_t __gen_e_acsl_add_6;
+ __e_acsl_mpz_t __gen_e_acsl_f4_tapp_3;
+ __gmpz_init_set_si(__gen_e_acsl__37,1L);
+ __gmpz_init(__gen_e_acsl_add_6);
+ __gmpz_add(__gen_e_acsl_add_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_14),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__37));
+ __gmpz_init(__gen_e_acsl_f4_tapp_3);
+ __gen_e_acsl_f4_2((__e_acsl_mpz_struct *)__gen_e_acsl_f4_tapp_3,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_add_6);
+ __gmpz_init_set(__gen_e_acsl_if_8,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_tapp_3));
+ __gmpz_clear(__gen_e_acsl__37);
+ __gmpz_clear(__gen_e_acsl_add_6);
+ __gmpz_clear(__gen_e_acsl_f4_tapp_3);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__38;
+ int __gen_e_acsl_lt_5;
+ __e_acsl_mpz_t __gen_e_acsl_if_7;
+ __gmpz_init_set_ui(__gen_e_acsl__38,9223372036854775807UL);
+ __gen_e_acsl_lt_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_14),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__38));
+ if (__gen_e_acsl_lt_5 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__39;
+ __gmpz_init_set_ui(__gen_e_acsl__39,9223372036854775807UL);
+ __gmpz_init_set(__gen_e_acsl_if_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__39));
+ __gmpz_clear(__gen_e_acsl__39);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__40;
+ __gmpz_init_set_si(__gen_e_acsl__40,6L);
+ __gmpz_init_set(__gen_e_acsl_if_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__40));
+ __gmpz_clear(__gen_e_acsl__40);
+ }
+ __gmpz_init_set(__gen_e_acsl_if_8,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_7));
+ __gmpz_clear(__gen_e_acsl__38);
+ __gmpz_clear(__gen_e_acsl_if_7);
+ }
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_8));
+ __gmpz_clear(__gen_e_acsl_n_14);
+ __gmpz_clear(__gen_e_acsl__36);
+ __gmpz_clear(__gen_e_acsl_if_8);
+ return;
+}
+
void __gen_e_acsl_f4(__e_acsl_mpz_struct * __retres_arg,
int __gen_e_acsl_n_arg)
{
@@ -224,70 +288,6 @@ void __gen_e_acsl_f4(__e_acsl_mpz_struct * __retres_arg,
return;
}
-void __gen_e_acsl_f4_2(__e_acsl_mpz_struct * __retres_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_n_arg)
-{
- __e_acsl_mpz_t __gen_e_acsl_n_14;
- __e_acsl_mpz_t __gen_e_acsl__36;
- int __gen_e_acsl_lt_4;
- __e_acsl_mpz_t __gen_e_acsl_if_8;
- __gmpz_init_set(__gen_e_acsl_n_14,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_arg));
- __gmpz_init_set_si(__gen_e_acsl__36,100L);
- __gen_e_acsl_lt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_14),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__36));
- if (__gen_e_acsl_lt_4 < 0) {
- __e_acsl_mpz_t __gen_e_acsl__37;
- __e_acsl_mpz_t __gen_e_acsl_add_6;
- __e_acsl_mpz_t __gen_e_acsl_f4_tapp_3;
- __gmpz_init_set_si(__gen_e_acsl__37,1L);
- __gmpz_init(__gen_e_acsl_add_6);
- __gmpz_add(__gen_e_acsl_add_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_14),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__37));
- __gmpz_init(__gen_e_acsl_f4_tapp_3);
- __gen_e_acsl_f4_2((__e_acsl_mpz_struct *)__gen_e_acsl_f4_tapp_3,
- (__e_acsl_mpz_struct *)__gen_e_acsl_add_6);
- __gmpz_init_set(__gen_e_acsl_if_8,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_tapp_3));
- __gmpz_clear(__gen_e_acsl__37);
- __gmpz_clear(__gen_e_acsl_add_6);
- __gmpz_clear(__gen_e_acsl_f4_tapp_3);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__38;
- int __gen_e_acsl_lt_5;
- __e_acsl_mpz_t __gen_e_acsl_if_7;
- __gmpz_init_set_ui(__gen_e_acsl__38,9223372036854775807UL);
- __gen_e_acsl_lt_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_14),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__38));
- if (__gen_e_acsl_lt_5 < 0) {
- __e_acsl_mpz_t __gen_e_acsl__39;
- __gmpz_init_set_ui(__gen_e_acsl__39,9223372036854775807UL);
- __gmpz_init_set(__gen_e_acsl_if_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__39));
- __gmpz_clear(__gen_e_acsl__39);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__40;
- __gmpz_init_set_si(__gen_e_acsl__40,6L);
- __gmpz_init_set(__gen_e_acsl_if_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__40));
- __gmpz_clear(__gen_e_acsl__40);
- }
- __gmpz_init_set(__gen_e_acsl_if_8,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_7));
- __gmpz_clear(__gen_e_acsl__38);
- __gmpz_clear(__gen_e_acsl_if_7);
- }
- __gmpz_init_set(__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_8));
- __gmpz_clear(__gen_e_acsl_n_14);
- __gmpz_clear(__gen_e_acsl__36);
- __gmpz_clear(__gen_e_acsl_if_8);
- return;
-}
-
void __gen_e_acsl_f3_2(__e_acsl_mpz_struct * __retres_arg,
__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
{