From fbe9945958fbef010991e712c90096b767a1bfa0 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 1 Mar 2019 09:37:56 +0100
Subject: [PATCH] [tests] update oracles
---
.../tests/gmp/oracle/functions.0.res.oracle | 1 +
.../tests/gmp/oracle/functions.1.res.oracle | 1 +
.../e-acsl/tests/gmp/oracle/gen_functions.c | 114 +++---
.../e-acsl/tests/gmp/oracle/gen_functions2.c | 126 +++----
.../tests/gmp/oracle/gen_functions_rec.c | 92 ++---
.../tests/gmp/oracle/gen_functions_rec2.c | 348 +++++++++---------
6 files changed, 344 insertions(+), 338 deletions(-)
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
index 8784a09a0db..c60cf271f5f 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
@@ -20,6 +20,7 @@
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
glob ∈ {5}
+ __e_acsl_sound_verdict ∈ [--..--]
[eva] using specification for function __e_acsl_memory_init
[eva] using specification for function __e_acsl_assert
[eva] using specification for function __gmpz_init_set_str
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle
index 46f1bb7194a..70b854b31ac 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle
@@ -20,6 +20,7 @@
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
glob ∈ {5}
+ __e_acsl_sound_verdict ∈ [--..--]
[eva] using specification for function __e_acsl_memory_init
[eva] using specification for function __gmpz_init_set_si
[eva] using specification for function __gmpz_init
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 0c716f6c8bb..9e926f5e7cf 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
@@ -1,6 +1,8 @@
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
+extern int __e_acsl_sound_verdict;
+
struct mystruct {
int k ;
int l ;
@@ -13,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_2(int __gen_e_acsl_x_arg,
- __e_acsl_mpz_struct * __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_3(int __gen_e_acsl_x_arg, long __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;
*/
-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);
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);
+long __gen_e_acsl_f1(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
/*@ logic char h_char(char c) = c;
*/
@@ -300,27 +302,11 @@ 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)
+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;
}
void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
@@ -345,10 +331,52 @@ void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
return;
}
-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;
+ __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;
+}
+
+int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
+{
+ int __retres;
+ __e_acsl_mpz_t __gen_e_acsl_y;
+ __e_acsl_mpz_t __gen_e_acsl_x;
+ __e_acsl_mpz_t __gen_e_acsl_add;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ int __gen_e_acsl_gt;
+ __gmpz_init_set(__gen_e_acsl_y,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
+ __gmpz_init_set_si(__gen_e_acsl_x,(long)__gen_e_acsl_x_arg);
+ __gmpz_init(__gen_e_acsl_add);
+ __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __retres = __gen_e_acsl_gt > 0;
+ __gmpz_clear(__gen_e_acsl_y);
+ __gmpz_clear(__gen_e_acsl_x);
+ __gmpz_clear(__gen_e_acsl_add);
+ __gmpz_clear(__gen_e_acsl__2);
return __retres;
}
@@ -384,32 +412,6 @@ int __gen_e_acsl_p2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
return __retres;
}
-int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_y_arg)
-{
- int __retres;
- __e_acsl_mpz_t __gen_e_acsl_y;
- __e_acsl_mpz_t __gen_e_acsl_x;
- __e_acsl_mpz_t __gen_e_acsl_add;
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_gt;
- __gmpz_init_set(__gen_e_acsl_y,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_arg));
- __gmpz_init_set_si(__gen_e_acsl_x,(long)__gen_e_acsl_x_arg);
- __gmpz_init(__gen_e_acsl_add);
- __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y));
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
- __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __retres = __gen_e_acsl_gt > 0;
- __gmpz_clear(__gen_e_acsl_y);
- __gmpz_clear(__gen_e_acsl_x);
- __gmpz_clear(__gen_e_acsl_add);
- __gmpz_clear(__gen_e_acsl__2);
- 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 890ef4bf2c6..bbf29e6ab39 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
@@ -1,6 +1,8 @@
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
+extern int __e_acsl_sound_verdict;
+
struct mystruct {
int k ;
int l ;
@@ -13,23 +15,23 @@ 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_2(int __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg);
-int __gen_e_acsl_p2(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg);
-
/*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
*/
-void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
- int __gen_e_acsl_x_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);
void __gen_e_acsl_f1(__e_acsl_mpz_struct * __retres_arg,
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,
+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);
/*@ logic char h_char(char c) = c;
@@ -369,26 +371,25 @@ 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,
+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)
{
- __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_t __gen_e_acsl_y_5;
+ __e_acsl_mpz_t __gen_e_acsl_x_5;
+ __e_acsl_mpz_t __gen_e_acsl_add_5;
+ __gmpz_init_set(__gen_e_acsl_y_5,
(__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_si(__gen_e_acsl_x_5,(long)__gen_e_acsl_x_arg);
+ __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 *)(__gen_e_acsl_y_5));
__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);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5));
+ __gmpz_clear(__gen_e_acsl_y_5);
+ __gmpz_clear(__gen_e_acsl_x_5);
+ __gmpz_clear(__gen_e_acsl_add_5);
return;
}
@@ -412,53 +413,29 @@ void __gen_e_acsl_f1(__e_acsl_mpz_struct * __retres_arg,
return;
}
-void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
- int __gen_e_acsl_x_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)
{
- __e_acsl_mpz_t __gen_e_acsl_y_5;
- __e_acsl_mpz_t __gen_e_acsl_x_5;
- __e_acsl_mpz_t __gen_e_acsl_add_5;
- __gmpz_init_set(__gen_e_acsl_y_5,
+ __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_set_si(__gen_e_acsl_x_5,(long)__gen_e_acsl_x_arg);
- __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 *)(__gen_e_acsl_y_5));
+ __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_5));
- __gmpz_clear(__gen_e_acsl_y_5);
- __gmpz_clear(__gen_e_acsl_x_5);
- __gmpz_clear(__gen_e_acsl_add_5);
+ (__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(int __gen_e_acsl_x_arg, int __gen_e_acsl_y_arg)
-{
- int __retres;
- __e_acsl_mpz_t __gen_e_acsl_x_2;
- __e_acsl_mpz_t __gen_e_acsl_y_2;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- __e_acsl_mpz_t __gen_e_acsl__2;
- int __gen_e_acsl_gt_2;
- __gmpz_init_set_si(__gen_e_acsl_x_2,(long)__gen_e_acsl_x_arg);
- __gmpz_init_set_si(__gen_e_acsl_y_2,(long)__gen_e_acsl_y_arg);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
- __gmpz_init_set_si(__gen_e_acsl__2,0L);
- __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __retres = __gen_e_acsl_gt_2 > 0;
- __gmpz_clear(__gen_e_acsl_x_2);
- __gmpz_clear(__gen_e_acsl_y_2);
- __gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl__2);
- return __retres;
-}
-
int __gen_e_acsl_p2_2(int __gen_e_acsl_x_arg,
__e_acsl_mpz_struct * __gen_e_acsl_y_arg)
{
@@ -486,6 +463,31 @@ 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;
+ __e_acsl_mpz_t __gen_e_acsl_x_2;
+ __e_acsl_mpz_t __gen_e_acsl_y_2;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ int __gen_e_acsl_gt_2;
+ __gmpz_init_set_si(__gen_e_acsl_x_2,(long)__gen_e_acsl_x_arg);
+ __gmpz_init_set_si(__gen_e_acsl_y_2,(long)__gen_e_acsl_y_arg);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_y_2));
+ __gmpz_init_set_si(__gen_e_acsl__2,0L);
+ __gen_e_acsl_gt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __retres = __gen_e_acsl_gt_2 > 0;
+ __gmpz_clear(__gen_e_acsl_x_2);
+ __gmpz_clear(__gen_e_acsl_y_2);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl__2);
+ 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_functions_rec.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
index c747ce87540..10ad7f46881 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
@@ -45,12 +45,12 @@ logic ℤ f4(ℤ n) =
n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
*/
-long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg);
-
long __gen_e_acsl_f4(int __gen_e_acsl_n_arg);
long __gen_e_acsl_f4_2(long __gen_e_acsl_n_arg);
+long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg);
+
int main(void)
{
int __retres;
@@ -129,6 +129,50 @@ int main(void)
return __retres;
}
+long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
+{
+ long __retres;
+ __e_acsl_mpz_t __gen_e_acsl_n_11;
+ __e_acsl_mpz_t __gen_e_acsl__23;
+ int __gen_e_acsl_lt_2;
+ long __gen_e_acsl_if_11;
+ __gmpz_init_set(__gen_e_acsl_n_11,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_arg));
+ __gmpz_init_set_si(__gen_e_acsl__23,100L);
+ __gen_e_acsl_lt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_11),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__23));
+ if (__gen_e_acsl_lt_2 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__24;
+ __e_acsl_mpz_t __gen_e_acsl_add_7;
+ long __gen_e_acsl_f4_tapp_4;
+ __gmpz_init_set_si(__gen_e_acsl__24,1L);
+ __gmpz_init(__gen_e_acsl_add_7);
+ __gmpz_add(__gen_e_acsl_add_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_11),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
+ __gen_e_acsl_f4_tapp_4 = __gen_e_acsl_f4_3((__e_acsl_mpz_struct *)__gen_e_acsl_add_7);
+ __gen_e_acsl_if_11 = __gen_e_acsl_f4_tapp_4;
+ __gmpz_clear(__gen_e_acsl__24);
+ __gmpz_clear(__gen_e_acsl_add_7);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__25;
+ int __gen_e_acsl_lt_3;
+ unsigned long __gen_e_acsl_if_10;
+ __gmpz_init_set_ui(__gen_e_acsl__25,9223372036854775807UL);
+ __gen_e_acsl_lt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_11),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
+ if (__gen_e_acsl_lt_3 < 0) __gen_e_acsl_if_10 = 9223372036854775807UL;
+ else __gen_e_acsl_if_10 = 6UL;
+ __gen_e_acsl_if_11 = (long)__gen_e_acsl_if_10;
+ __gmpz_clear(__gen_e_acsl__25);
+ }
+ __retres = __gen_e_acsl_if_11;
+ __gmpz_clear(__gen_e_acsl_n_11);
+ __gmpz_clear(__gen_e_acsl__23);
+ return __retres;
+}
+
long __gen_e_acsl_f4_2(long __gen_e_acsl_n_arg)
{
long __retres;
@@ -179,50 +223,6 @@ long __gen_e_acsl_f4(int __gen_e_acsl_n_arg)
return __retres;
}
-long __gen_e_acsl_f4_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
-{
- long __retres;
- __e_acsl_mpz_t __gen_e_acsl_n_11;
- __e_acsl_mpz_t __gen_e_acsl__23;
- int __gen_e_acsl_lt_2;
- long __gen_e_acsl_if_11;
- __gmpz_init_set(__gen_e_acsl_n_11,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_arg));
- __gmpz_init_set_si(__gen_e_acsl__23,100L);
- __gen_e_acsl_lt_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_11),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__23));
- if (__gen_e_acsl_lt_2 < 0) {
- __e_acsl_mpz_t __gen_e_acsl__24;
- __e_acsl_mpz_t __gen_e_acsl_add_7;
- long __gen_e_acsl_f4_tapp_4;
- __gmpz_init_set_si(__gen_e_acsl__24,1L);
- __gmpz_init(__gen_e_acsl_add_7);
- __gmpz_add(__gen_e_acsl_add_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_11),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
- __gen_e_acsl_f4_tapp_4 = __gen_e_acsl_f4_3((__e_acsl_mpz_struct *)__gen_e_acsl_add_7);
- __gen_e_acsl_if_11 = __gen_e_acsl_f4_tapp_4;
- __gmpz_clear(__gen_e_acsl__24);
- __gmpz_clear(__gen_e_acsl_add_7);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__25;
- int __gen_e_acsl_lt_3;
- unsigned long __gen_e_acsl_if_10;
- __gmpz_init_set_ui(__gen_e_acsl__25,9223372036854775807UL);
- __gen_e_acsl_lt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_11),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
- if (__gen_e_acsl_lt_3 < 0) __gen_e_acsl_if_10 = 9223372036854775807UL;
- else __gen_e_acsl_if_10 = 6UL;
- __gen_e_acsl_if_11 = (long)__gen_e_acsl_if_10;
- __gmpz_clear(__gen_e_acsl__25);
- }
- __retres = __gen_e_acsl_if_11;
- __gmpz_clear(__gen_e_acsl_n_11);
- __gmpz_clear(__gen_e_acsl__23);
- return __retres;
-}
-
int __gen_e_acsl_f3_3(__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
{
int __retres;
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 35f5f695298..fe7af1124fe 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
@@ -13,21 +13,21 @@ void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
/*@ logic ℤ f2(ℤ n) = n < 0? 1: (f2(n - 1) * f2(n - 2)) / f2(n - 3);
*/
-void __gen_e_acsl_f2_2(__e_acsl_mpz_struct * __retres_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_n_arg);
-
void __gen_e_acsl_f2(__e_acsl_mpz_struct * __retres_arg,
int __gen_e_acsl_n_arg);
+void __gen_e_acsl_f2_2(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg);
+
/*@ logic ℤ g(ℤ n) = 0;
*/
-void __gen_e_acsl_g_2(__e_acsl_mpz_struct * __retres_arg,
- __e_acsl_mpz_struct * __gen_e_acsl_n_arg);
-
void __gen_e_acsl_g(__e_acsl_mpz_struct * __retres_arg,
int __gen_e_acsl_n_arg);
+void __gen_e_acsl_g_2(__e_acsl_mpz_struct * __retres_arg,
+ __e_acsl_mpz_struct * __gen_e_acsl_n_arg);
+
/*@ logic ℤ f3(ℤ n) = n > 0? g(n) * f3(n - 1) - 5: g(n + 1);
*/
@@ -42,12 +42,12 @@ logic ℤ f4(ℤ n) =
n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
*/
-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);
+void __gen_e_acsl_f4(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg);
+
int main(void)
{
int __retres;
@@ -155,70 +155,6 @@ 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)
{
@@ -288,6 +224,70 @@ 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)
{
@@ -445,17 +445,6 @@ void __gen_e_acsl_f3(__e_acsl_mpz_struct * __retres_arg,
return;
}
-void __gen_e_acsl_g(__e_acsl_mpz_struct * __retres_arg,
- int __gen_e_acsl_n_arg)
-{
- __e_acsl_mpz_t __gen_e_acsl__24;
- __gmpz_init_set_si(__gen_e_acsl__24,0L);
- __gmpz_init_set(__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
- __gmpz_clear(__gen_e_acsl__24);
- return;
-}
-
void __gen_e_acsl_g_2(__e_acsl_mpz_struct * __retres_arg,
__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
{
@@ -471,98 +460,14 @@ void __gen_e_acsl_g_2(__e_acsl_mpz_struct * __retres_arg,
return;
}
-void __gen_e_acsl_f2(__e_acsl_mpz_struct * __retres_arg,
- int __gen_e_acsl_n_arg)
+void __gen_e_acsl_g(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg)
{
- __e_acsl_mpz_t __gen_e_acsl_n_4;
- __e_acsl_mpz_t __gen_e_acsl__10;
- int __gen_e_acsl_lt;
- __e_acsl_mpz_t __gen_e_acsl_if_4;
- __gmpz_init_set_si(__gen_e_acsl_n_4,(long)__gen_e_acsl_n_arg);
- __gmpz_init_set_si(__gen_e_acsl__10,0L);
- __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
- if (__gen_e_acsl_lt < 0) {
- __e_acsl_mpz_t __gen_e_acsl__11;
- __gmpz_init_set_si(__gen_e_acsl__11,1L);
- __gmpz_init_set(__gen_e_acsl_if_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
- __gmpz_clear(__gen_e_acsl__11);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_n_5;
- __e_acsl_mpz_t __gen_e_acsl__12;
- __e_acsl_mpz_t __gen_e_acsl_sub_3;
- __e_acsl_mpz_t __gen_e_acsl_f2_tapp_2;
- __e_acsl_mpz_t __gen_e_acsl__19;
- __e_acsl_mpz_t __gen_e_acsl_sub_7;
- __e_acsl_mpz_t __gen_e_acsl_f2_tapp_6;
- __e_acsl_mpz_t __gen_e_acsl_mul_2;
- __e_acsl_mpz_t __gen_e_acsl__20;
- __e_acsl_mpz_t __gen_e_acsl_sub_8;
- __e_acsl_mpz_t __gen_e_acsl_f2_tapp_7;
- __e_acsl_mpz_t __gen_e_acsl__21;
- int __gen_e_acsl_div_guard_2;
- __e_acsl_mpz_t __gen_e_acsl_div_2;
- __gmpz_init_set_si(__gen_e_acsl_n_5,(long)__gen_e_acsl_n_arg);
- __gmpz_init_set_si(__gen_e_acsl__12,1L);
- __gmpz_init(__gen_e_acsl_sub_3);
- __gmpz_sub(__gen_e_acsl_sub_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
- __gmpz_init(__gen_e_acsl_f2_tapp_2);
- __gen_e_acsl_f2_2((__e_acsl_mpz_struct *)__gen_e_acsl_f2_tapp_2,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub_3);
- __gmpz_init_set_si(__gen_e_acsl__19,2L);
- __gmpz_init(__gen_e_acsl_sub_7);
- __gmpz_sub(__gen_e_acsl_sub_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__19));
- __gmpz_init(__gen_e_acsl_f2_tapp_6);
- __gen_e_acsl_f2_2((__e_acsl_mpz_struct *)__gen_e_acsl_f2_tapp_6,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
- __gmpz_init(__gen_e_acsl_mul_2);
- __gmpz_mul(__gen_e_acsl_mul_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_6));
- __gmpz_init_set_si(__gen_e_acsl__20,3L);
- __gmpz_init(__gen_e_acsl_sub_8);
- __gmpz_sub(__gen_e_acsl_sub_8,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__20));
- __gmpz_init(__gen_e_acsl_f2_tapp_7);
- __gen_e_acsl_f2_2((__e_acsl_mpz_struct *)__gen_e_acsl_f2_tapp_7,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
- __gmpz_init_set_si(__gen_e_acsl__21,0L);
- __gen_e_acsl_div_guard_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
- __gmpz_init(__gen_e_acsl_div_2);
- __e_acsl_assert(! (__gen_e_acsl_div_guard_2 == 0),(char *)"Assertion",
- (char *)"f2_2",(char *)"f2(n - 3) == 0",9);
- __gmpz_tdiv_q(__gen_e_acsl_div_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_7));
- __gmpz_init_set(__gen_e_acsl_if_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_div_2));
- __gmpz_clear(__gen_e_acsl_n_5);
- __gmpz_clear(__gen_e_acsl__12);
- __gmpz_clear(__gen_e_acsl_sub_3);
- __gmpz_clear(__gen_e_acsl_f2_tapp_2);
- __gmpz_clear(__gen_e_acsl__19);
- __gmpz_clear(__gen_e_acsl_sub_7);
- __gmpz_clear(__gen_e_acsl_f2_tapp_6);
- __gmpz_clear(__gen_e_acsl_mul_2);
- __gmpz_clear(__gen_e_acsl__20);
- __gmpz_clear(__gen_e_acsl_sub_8);
- __gmpz_clear(__gen_e_acsl_f2_tapp_7);
- __gmpz_clear(__gen_e_acsl__21);
- __gmpz_clear(__gen_e_acsl_div_2);
- }
+ __e_acsl_mpz_t __gen_e_acsl__24;
+ __gmpz_init_set_si(__gen_e_acsl__24,0L);
__gmpz_init_set(__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_4));
- __gmpz_clear(__gen_e_acsl_n_4);
- __gmpz_clear(__gen_e_acsl__10);
- __gmpz_clear(__gen_e_acsl_if_4);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
+ __gmpz_clear(__gen_e_acsl__24);
return;
}
@@ -659,6 +564,101 @@ void __gen_e_acsl_f2_2(__e_acsl_mpz_struct * __retres_arg,
return;
}
+void __gen_e_acsl_f2(__e_acsl_mpz_struct * __retres_arg,
+ int __gen_e_acsl_n_arg)
+{
+ __e_acsl_mpz_t __gen_e_acsl_n_4;
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ int __gen_e_acsl_lt;
+ __e_acsl_mpz_t __gen_e_acsl_if_4;
+ __gmpz_init_set_si(__gen_e_acsl_n_4,(long)__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl__10,0L);
+ __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+ if (__gen_e_acsl_lt < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ __gmpz_init_set_si(__gen_e_acsl__11,1L);
+ __gmpz_init_set(__gen_e_acsl_if_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ __gmpz_clear(__gen_e_acsl__11);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n_5;
+ __e_acsl_mpz_t __gen_e_acsl__12;
+ __e_acsl_mpz_t __gen_e_acsl_sub_3;
+ __e_acsl_mpz_t __gen_e_acsl_f2_tapp_2;
+ __e_acsl_mpz_t __gen_e_acsl__19;
+ __e_acsl_mpz_t __gen_e_acsl_sub_7;
+ __e_acsl_mpz_t __gen_e_acsl_f2_tapp_6;
+ __e_acsl_mpz_t __gen_e_acsl_mul_2;
+ __e_acsl_mpz_t __gen_e_acsl__20;
+ __e_acsl_mpz_t __gen_e_acsl_sub_8;
+ __e_acsl_mpz_t __gen_e_acsl_f2_tapp_7;
+ __e_acsl_mpz_t __gen_e_acsl__21;
+ int __gen_e_acsl_div_guard_2;
+ __e_acsl_mpz_t __gen_e_acsl_div_2;
+ __gmpz_init_set_si(__gen_e_acsl_n_5,(long)__gen_e_acsl_n_arg);
+ __gmpz_init_set_si(__gen_e_acsl__12,1L);
+ __gmpz_init(__gen_e_acsl_sub_3);
+ __gmpz_sub(__gen_e_acsl_sub_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
+ __gmpz_init(__gen_e_acsl_f2_tapp_2);
+ __gen_e_acsl_f2_2((__e_acsl_mpz_struct *)__gen_e_acsl_f2_tapp_2,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_3);
+ __gmpz_init_set_si(__gen_e_acsl__19,2L);
+ __gmpz_init(__gen_e_acsl_sub_7);
+ __gmpz_sub(__gen_e_acsl_sub_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__19));
+ __gmpz_init(__gen_e_acsl_f2_tapp_6);
+ __gen_e_acsl_f2_2((__e_acsl_mpz_struct *)__gen_e_acsl_f2_tapp_6,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
+ __gmpz_init(__gen_e_acsl_mul_2);
+ __gmpz_mul(__gen_e_acsl_mul_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_6));
+ __gmpz_init_set_si(__gen_e_acsl__20,3L);
+ __gmpz_init(__gen_e_acsl_sub_8);
+ __gmpz_sub(__gen_e_acsl_sub_8,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__20));
+ __gmpz_init(__gen_e_acsl_f2_tapp_7);
+ __gen_e_acsl_f2_2((__e_acsl_mpz_struct *)__gen_e_acsl_f2_tapp_7,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_8);
+ __gmpz_init_set_si(__gen_e_acsl__21,0L);
+ __gen_e_acsl_div_guard_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
+ __gmpz_init(__gen_e_acsl_div_2);
+ __e_acsl_assert(! (__gen_e_acsl_div_guard_2 == 0),(char *)"Assertion",
+ (char *)"f2_2",(char *)"f2(n - 3) == 0",9);
+ __gmpz_tdiv_q(__gen_e_acsl_div_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_tapp_7));
+ __gmpz_init_set(__gen_e_acsl_if_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_div_2));
+ __gmpz_clear(__gen_e_acsl_n_5);
+ __gmpz_clear(__gen_e_acsl__12);
+ __gmpz_clear(__gen_e_acsl_sub_3);
+ __gmpz_clear(__gen_e_acsl_f2_tapp_2);
+ __gmpz_clear(__gen_e_acsl__19);
+ __gmpz_clear(__gen_e_acsl_sub_7);
+ __gmpz_clear(__gen_e_acsl_f2_tapp_6);
+ __gmpz_clear(__gen_e_acsl_mul_2);
+ __gmpz_clear(__gen_e_acsl__20);
+ __gmpz_clear(__gen_e_acsl_sub_8);
+ __gmpz_clear(__gen_e_acsl_f2_tapp_7);
+ __gmpz_clear(__gen_e_acsl__21);
+ __gmpz_clear(__gen_e_acsl_div_2);
+ }
+ __gmpz_init_set(__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_4));
+ __gmpz_clear(__gen_e_acsl_n_4);
+ __gmpz_clear(__gen_e_acsl__10);
+ __gmpz_clear(__gen_e_acsl_if_4);
+ return;
+}
+
void __gen_e_acsl_f1_2(__e_acsl_mpz_struct * __retres_arg,
__e_acsl_mpz_struct * __gen_e_acsl_n_arg)
{
--
GitLab