diff --git a/src/plugins/e-acsl/real.ml b/src/plugins/e-acsl/real.ml
index 964f5913c0e111177eda0e084b8efff5da35e55a..5a530410a0cee366f60372a7fc70a5adb3d3014f 100644
--- a/src/plugins/e-acsl/real.ml
+++ b/src/plugins/e-acsl/real.ml
@@ -170,7 +170,7 @@ let add_cast ~loc ?name e env ty =
(* 1) Cast R to Z using cast_to_z
2) Extract ulong from Z
3) Potentially cast ulong to ty *)
- Error.not_yet "R to TInt"
+ Error.not_yet "R to Int"
| _ ->
Error.not_yet "R to <typ>"
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
index c735e13f00f0de2dadee0c103dcfacc4a5dffdcb..efbf831c0e626b5573f733d25e2ca2b6fa140bd0 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
@@ -140,26 +140,26 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
if (__gen_e_acsl_eq == 0) {
__e_acsl_mpq_t __gen_e_acsl__3;
__e_acsl_mpq_t __gen_e_acsl__4;
- __e_acsl_mpq_t __gen_e_acsl__5;
__e_acsl_mpq_t __gen_e_acsl_mul;
+ __e_acsl_mpq_t __gen_e_acsl__5;
int __gen_e_acsl_lt;
__gmpq_init(__gen_e_acsl__3);
- __gmpq_set_d(__gen_e_acsl__3,(double)*__gen_e_acsl_at_3);
+ __gmpq_set_str(__gen_e_acsl__3,"085/100",10);
__gmpq_init(__gen_e_acsl__4);
- __gmpq_set_str(__gen_e_acsl__4,"085/100",10);
- __gmpq_init(__gen_e_acsl__5);
- __gmpq_set_d(__gen_e_acsl__5,(double)*__gen_e_acsl_at_4);
+ __gmpq_set_d(__gen_e_acsl__4,(double)*__gen_e_acsl_at_4);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
- __gen_e_acsl_lt = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__3),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__3),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__4));
+ __gmpq_init(__gen_e_acsl__5);
+ __gmpq_set_d(__gen_e_acsl__5,(double)*__gen_e_acsl_at_3);
+ __gen_e_acsl_lt = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__5),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul));
__gen_e_acsl_and = __gen_e_acsl_lt < 0;
__gmpq_clear(__gen_e_acsl__3);
__gmpq_clear(__gen_e_acsl__4);
- __gmpq_clear(__gen_e_acsl__5);
__gmpq_clear(__gen_e_acsl_mul);
+ __gmpq_clear(__gen_e_acsl__5);
}
else __gen_e_acsl_and = 0;
if (__gen_e_acsl_and) {
@@ -167,11 +167,11 @@ void __gen_e_acsl_bar(float *Mtmin_in, float *Mwmin, float *Mtmin_out)
__e_acsl_mpq_t __gen_e_acsl__7;
int __gen_e_acsl_ne;
__gmpq_init(__gen_e_acsl__6);
- __gmpq_set_d(__gen_e_acsl__6,(double)*__gen_e_acsl_at_5);
+ __gmpq_set_str(__gen_e_acsl__6,"0/1",10);
__gmpq_init(__gen_e_acsl__7);
- __gmpq_set_str(__gen_e_acsl__7,"0/1",10);
- __gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__6),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__7));
+ __gmpq_set_d(__gen_e_acsl__7,(double)*__gen_e_acsl_at_5);
+ __gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__7),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__6));
__gen_e_acsl_if = __gen_e_acsl_ne != 0;
__gmpq_clear(__gen_e_acsl__6);
__gmpq_clear(__gen_e_acsl__7);
@@ -257,51 +257,50 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__e_acsl_mpq_t __gen_e_acsl_;
__e_acsl_mpq_t __gen_e_acsl__2;
__e_acsl_mpq_t __gen_e_acsl__3;
- __e_acsl_mpq_t __gen_e_acsl__4;
- __e_acsl_mpq_t __gen_e_acsl__5;
__e_acsl_mpq_t __gen_e_acsl_div;
- __e_acsl_mpq_t __gen_e_acsl__6;
+ __e_acsl_mpq_t __gen_e_acsl__4;
__e_acsl_mpq_t __gen_e_acsl_mul;
- __e_acsl_mpq_t __gen_e_acsl__7;
+ __e_acsl_mpq_t __gen_e_acsl__5;
__e_acsl_mpq_t __gen_e_acsl_mul_2;
__e_acsl_mpq_t __gen_e_acsl_sub;
+ __e_acsl_mpq_t __gen_e_acsl__6;
__e_acsl_mpq_t __gen_e_acsl_add;
+ __e_acsl_mpq_t __gen_e_acsl__7;
int __gen_e_acsl_ne;
__gmpq_init(__gen_e_acsl_);
- __gmpq_set_d(__gen_e_acsl_,(double)*__gen_e_acsl_at);
+ __gmpq_set_str(__gen_e_acsl_,"5",10);
__gmpq_init(__gen_e_acsl__2);
- __gmpq_set_d(__gen_e_acsl__2,(double)*__gen_e_acsl_at_2);
+ __gmpq_set_si(__gen_e_acsl__2,5L);
__gmpq_init(__gen_e_acsl__3);
- __gmpq_set_str(__gen_e_acsl__3,"5",10);
- __gmpq_init(__gen_e_acsl__4);
- __gmpq_set_si(__gen_e_acsl__4,5L);
- __gmpq_init(__gen_e_acsl__5);
- __gmpq_set_si(__gen_e_acsl__5,80L);
+ __gmpq_set_si(__gen_e_acsl__3,80L);
__gmpq_init(__gen_e_acsl_div);
__gmpq_div(__gen_e_acsl_div,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
- __gmpq_init(__gen_e_acsl__6);
- __gmpq_set_d(__gen_e_acsl__6,(double)*__gen_e_acsl_at_3);
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__2),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__3));
+ __gmpq_init(__gen_e_acsl__4);
+ __gmpq_set_d(__gen_e_acsl__4,(double)*__gen_e_acsl_at_3);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_div),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__6));
- __gmpq_init(__gen_e_acsl__7);
- __gmpq_set_str(__gen_e_acsl__7,"04/10",10);
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__4));
+ __gmpq_init(__gen_e_acsl__5);
+ __gmpq_set_str(__gen_e_acsl__5,"04/10",10);
__gmpq_init(__gen_e_acsl_mul_2);
__gmpq_mul(__gen_e_acsl_mul_2,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__7));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
__gmpq_init(__gen_e_acsl_sub);
- __gmpq_sub(__gen_e_acsl_sub,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__3),
+ __gmpq_sub(__gen_e_acsl_sub,(__e_acsl_mpq_struct const *)(__gen_e_acsl_),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul_2));
+ __gmpq_init(__gen_e_acsl__6);
+ __gmpq_set_d(__gen_e_acsl__6,(double)*__gen_e_acsl_at_2);
__gmpq_init(__gen_e_acsl_add);
__gmpq_add(__gen_e_acsl_add,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__2),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__6),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_sub));
- __gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_),
+ __gmpq_init(__gen_e_acsl__7);
+ __gmpq_set_d(__gen_e_acsl__7,(double)*__gen_e_acsl_at);
+ __gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__7),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add));
__e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Postcondition",
(char *)"foo",
@@ -313,15 +312,15 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
__gmpq_clear(__gen_e_acsl_);
__gmpq_clear(__gen_e_acsl__2);
__gmpq_clear(__gen_e_acsl__3);
- __gmpq_clear(__gen_e_acsl__4);
- __gmpq_clear(__gen_e_acsl__5);
__gmpq_clear(__gen_e_acsl_div);
- __gmpq_clear(__gen_e_acsl__6);
+ __gmpq_clear(__gen_e_acsl__4);
__gmpq_clear(__gen_e_acsl_mul);
- __gmpq_clear(__gen_e_acsl__7);
+ __gmpq_clear(__gen_e_acsl__5);
__gmpq_clear(__gen_e_acsl_mul_2);
__gmpq_clear(__gen_e_acsl_sub);
+ __gmpq_clear(__gen_e_acsl__6);
__gmpq_clear(__gen_e_acsl_add);
+ __gmpq_clear(__gen_e_acsl__7);
return;
}
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
index d8923c033f8550819d6c097b24f51053a69018ca..e7ac9d9dec4083d410b7ec698e1f64027c0cd3a8 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
@@ -1,7 +1,6 @@
[e-acsl] beginning translation.
-[e-acsl] Warning: R to float: double rounding might cause unsoundness
[e-acsl] tests/gmp/cast.i:23: Warning:
- E-ACSL construct `R to TInt' is not yet supported. Ignoring annotation.
+ E-ACSL construct `R to Int' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
index 57d1fdcd6fe691a345adc14c366123f4dd7b60ff..7ac62ea8423fbba17d74651d7e521c862099f2b8 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
@@ -1,7 +1,6 @@
[e-acsl] beginning translation.
-[e-acsl] Warning: R to float: double rounding might cause unsoundness
[e-acsl] tests/gmp/cast.i:23: Warning:
- E-ACSL construct `R to TInt' is not yet supported. Ignoring annotation.
+ E-ACSL construct `R to Int' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
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 b554b4b014ce358be8f65b0350a1f1539dcd227a..c71d46e5640378eaecb4deb5569439c41eb1c79e 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
@@ -244,19 +244,19 @@ mystruct __gen_e_acsl_t1(mystruct m)
int __gen_e_acsl_p1(int x, int y)
{
- int __retres = x + y > 0L;
+ int __retres = x + (long)y > 0L;
return __retres;
}
long __gen_e_acsl_t2(mystruct m)
{
- long __retres = m.k + m.l;
+ long __retres = m.k + (long)m.l;
return __retres;
}
int __gen_e_acsl_p2(int x, int y)
{
- int __retres = x + y > 0L;
+ int __retres = x + (long)y > 0L;
return __retres;
}
@@ -312,7 +312,7 @@ int __gen_e_acsl_k_pred(int x)
long __gen_e_acsl_f1(int x, int y)
{
- long __retres = x + y;
+ long __retres = x + (long)y;
return __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 0fa4a22a630c4d80f8f44b38a7c561a6b5e93f13..bc071fb5cb4836a10cef705c1d591faac6fec620 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
@@ -5,31 +5,31 @@
*/
/*@ logic ℤ f2(ℤ n) = n < 0? 1: (f2(n - 1) * f2(n - 2)) / f2(n - 3);
*/
-int __gen_e_acsl_f2_2(long n);
-
int __gen_e_acsl_f2(int n);
+int __gen_e_acsl_f2_2(long n);
+
/*@ logic ℤ g(ℤ n) = 0;
*/
-int __gen_e_acsl_g_5(long n);
-
int __gen_e_acsl_g(int n);
+int __gen_e_acsl_g_5(long n);
+
/*@ logic ℤ f3(ℤ n) = n > 0? g(n) * f3(n - 1) - 5: g(n + 1);
*/
-int __gen_e_acsl_f3_2(long n);
-
int __gen_e_acsl_f3(int n);
+int __gen_e_acsl_f3_2(long n);
+
/*@
logic ℤ f4(ℤ n) =
n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
*/
-unsigned long __gen_e_acsl_f4_2(long n);
-
unsigned long __gen_e_acsl_f4(int n);
+unsigned long __gen_e_acsl_f4_2(long n);
+
int main(void)
{
int __retres;
@@ -59,38 +59,36 @@ int main(void)
return __retres;
}
-unsigned long __gen_e_acsl_f4_2(long n)
-{
- unsigned long __gen_e_acsl_if_6;
- 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_6 = __gen_e_acsl_f4_4;
- }
- else {
- unsigned long __gen_e_acsl_if_5;
- if (n < 9223372036854775807L) __gen_e_acsl_if_5 = 9223372036854775807UL;
- else __gen_e_acsl_if_5 = 6UL;
- __gen_e_acsl_if_6 = __gen_e_acsl_if_5;
- }
- return __gen_e_acsl_if_6;
-}
-
-unsigned long __gen_e_acsl_f4(int n)
+int __gen_e_acsl_f2(int n)
{
- unsigned long __gen_e_acsl_if_8;
- 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_8 = __gen_e_acsl_f4_5;
- }
+ int __gen_e_acsl_if_2;
+ if (n < 0) __gen_e_acsl_if_2 = 1;
else {
- unsigned long __gen_e_acsl_if_7;
- if ((long)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;
+ int __gen_e_acsl_f2_9;
+ int __gen_e_acsl_f2_11;
+ int __gen_e_acsl_f2_13;
+ __gen_e_acsl_f2_9 = __gen_e_acsl_f2_2(n - 1L);
+ __gen_e_acsl_f2_11 = __gen_e_acsl_f2_2(n - 2L);
+ __gen_e_acsl_f2_13 = __gen_e_acsl_f2_2(n - 3L);
+ __e_acsl_assert(__gen_e_acsl_f2_13 != 0,(char *)"RTE",(char *)"f2",
+ (char *)"division_by_zero: __gen_e_acsl_f2_13 != 0",10);
+ /*@ assert Eva: division_by_zero: __gen_e_acsl_f2_13 ≢ 0; */
+ /*@ assert
+ Eva: signed_overflow:
+ -2147483648 ≤ __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11;
+ */
+ /*@ assert
+ Eva: signed_overflow:
+ __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11 ≤ 2147483647;
+ */
+ /*@ assert
+ Eva: signed_overflow:
+ (int)(__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13
+ ≤ 2147483647;
+ */
+ __gen_e_acsl_if_2 = (__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13;
}
- return __gen_e_acsl_if_8;
+ return __gen_e_acsl_if_2;
}
int __gen_e_acsl_f2_2(long n)
@@ -125,36 +123,10 @@ int __gen_e_acsl_f2_2(long n)
return __gen_e_acsl_if;
}
-int __gen_e_acsl_f2(int n)
+int __gen_e_acsl_g(int n)
{
- int __gen_e_acsl_if_2;
- if (n < 0) __gen_e_acsl_if_2 = 1;
- else {
- int __gen_e_acsl_f2_9;
- int __gen_e_acsl_f2_11;
- int __gen_e_acsl_f2_13;
- __gen_e_acsl_f2_9 = __gen_e_acsl_f2_2(n - 1L);
- __gen_e_acsl_f2_11 = __gen_e_acsl_f2_2(n - 2L);
- __gen_e_acsl_f2_13 = __gen_e_acsl_f2_2(n - 3L);
- __e_acsl_assert(__gen_e_acsl_f2_13 != 0,(char *)"RTE",(char *)"f2",
- (char *)"division_by_zero: __gen_e_acsl_f2_13 != 0",10);
- /*@ assert Eva: division_by_zero: __gen_e_acsl_f2_13 ≢ 0; */
- /*@ assert
- Eva: signed_overflow:
- -2147483648 ≤ __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11;
- */
- /*@ assert
- Eva: signed_overflow:
- __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11 ≤ 2147483647;
- */
- /*@ assert
- Eva: signed_overflow:
- (int)(__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13
- ≤ 2147483647;
- */
- __gen_e_acsl_if_2 = (__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13;
- }
- return __gen_e_acsl_if_2;
+ int __retres = 0;
+ return __retres;
}
int __gen_e_acsl_g_5(long n)
@@ -163,10 +135,22 @@ int __gen_e_acsl_g_5(long n)
return __retres;
}
-int __gen_e_acsl_g(int n)
+int __gen_e_acsl_f3(int n)
{
- int __retres = 0;
- return __retres;
+ int __gen_e_acsl_if_4;
+ 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_4 = __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_4 = __gen_e_acsl_g_8;
+ }
+ return __gen_e_acsl_if_4;
}
int __gen_e_acsl_f3_2(long n)
@@ -187,22 +171,38 @@ int __gen_e_acsl_f3_2(long n)
return __gen_e_acsl_if_3;
}
-int __gen_e_acsl_f3(int n)
+unsigned long __gen_e_acsl_f4(int n)
{
- int __gen_e_acsl_if_4;
- 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_4 = __gen_e_acsl_g_2 * __gen_e_acsl_f3_5 - 5;
+ unsigned long __gen_e_acsl_if_8;
+ 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_8 = __gen_e_acsl_f4_5;
}
else {
- int __gen_e_acsl_g_8;
- __gen_e_acsl_g_8 = __gen_e_acsl_g_5(n + 1L);
- __gen_e_acsl_if_4 = __gen_e_acsl_g_8;
+ unsigned long __gen_e_acsl_if_7;
+ if ((long)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_4;
+ return __gen_e_acsl_if_8;
+}
+
+unsigned long __gen_e_acsl_f4_2(long n)
+{
+ unsigned long __gen_e_acsl_if_6;
+ 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_6 = __gen_e_acsl_f4_4;
+ }
+ else {
+ unsigned long __gen_e_acsl_if_5;
+ if (n < 9223372036854775807L) __gen_e_acsl_if_5 = 9223372036854775807UL;
+ else __gen_e_acsl_if_5 = 6UL;
+ __gen_e_acsl_if_6 = __gen_e_acsl_if_5;
+ }
+ return __gen_e_acsl_if_6;
}
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 c13d6d1e49b1ef2fae4f1c8c5fb0922a23127c3f..9af269bd2db4bf590352f544990b3b31d0b32030 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
@@ -6,33 +6,33 @@
/*@ logic ℤ f2(ℤ n) = n < 0? 1: (f2(n - 1) * f2(n - 2)) / f2(n - 3);
*/
-void __gen_e_acsl_f2_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
-
void __gen_e_acsl_f2(__e_acsl_mpz_t *__retres_arg, int n);
+void __gen_e_acsl_f2_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
+
/*@ logic ℤ g(ℤ n) = 0;
*/
-void __gen_e_acsl_g_5(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
-
void __gen_e_acsl_g(__e_acsl_mpz_t *__retres_arg, int n);
+void __gen_e_acsl_g_5(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
+
/*@ logic ℤ f3(ℤ n) = n > 0? g(n) * f3(n - 1) - 5: g(n + 1);
*/
-void __gen_e_acsl_f3_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
-
void __gen_e_acsl_f3(__e_acsl_mpz_t *__retres_arg, int n);
+void __gen_e_acsl_f3_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
+
/*@
logic ℤ f4(ℤ n) =
n < 100? f4(n + 1): (n < 0x7fffffffffffffffL? 0x7fffffffffffffffL: 6);
*/
-void __gen_e_acsl_f4_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
-
void __gen_e_acsl_f4(__e_acsl_mpz_t *__retres_arg, int n);
+void __gen_e_acsl_f4_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n);
+
int main(void)
{
int __retres;
@@ -88,135 +88,107 @@ int main(void)
return __retres;
}
-void __gen_e_acsl_f4_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
+void __gen_e_acsl_f2(__e_acsl_mpz_t *__retres_arg, int n)
{
- __e_acsl_mpz_t __gen_e_acsl__26;
- int __gen_e_acsl_lt_4;
- __e_acsl_mpz_t __gen_e_acsl_if_6;
- __gmpz_init_set_si(__gen_e_acsl__26,100L);
- __gen_e_acsl_lt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__26));
- if (__gen_e_acsl_lt_4 < 0) {
- __e_acsl_mpz_t __gen_e_acsl__27;
- __e_acsl_mpz_t __gen_e_acsl_add_4;
- __e_acsl_mpz_t __gen_e_acsl_f4_4;
- __gmpz_init_set_si(__gen_e_acsl__27,1L);
- __gmpz_init(__gen_e_acsl_add_4);
- __gmpz_add(__gen_e_acsl_add_4,(__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__27));
+ __e_acsl_mpz_t __gen_e_acsl_n;
+ __e_acsl_mpz_t __gen_e_acsl_;
+ int __gen_e_acsl_lt;
+ __e_acsl_mpz_t __gen_e_acsl_if_2;
+ __gmpz_init_set_si(__gen_e_acsl_n,(long)n);
+ __gmpz_init_set_si(__gen_e_acsl_,0L);
+ __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+ if (__gen_e_acsl_lt < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__2;
+ __gmpz_init_set_si(__gen_e_acsl__2,1L);
+ __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+ __gmpz_clear(__gen_e_acsl__2);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n_2;
+ __e_acsl_mpz_t __gen_e_acsl__3;
+ __e_acsl_mpz_t __gen_e_acsl_sub;
+ __e_acsl_mpz_t __gen_e_acsl_f2_9;
+ __e_acsl_mpz_t __gen_e_acsl__10;
+ __e_acsl_mpz_t __gen_e_acsl_sub_5;
+ __e_acsl_mpz_t __gen_e_acsl_f2_11;
+ __e_acsl_mpz_t __gen_e_acsl_mul_2;
+ __e_acsl_mpz_t __gen_e_acsl__11;
+ __e_acsl_mpz_t __gen_e_acsl_sub_6;
+ __e_acsl_mpz_t __gen_e_acsl_f2_13;
+ __e_acsl_mpz_t __gen_e_acsl__12;
+ int __gen_e_acsl_div_guard_2;
+ __e_acsl_mpz_t __gen_e_acsl_div_2;
+ __gmpz_init_set_si(__gen_e_acsl_n_2,(long)n);
+ __gmpz_init_set_si(__gen_e_acsl__3,1L);
+ __gmpz_init(__gen_e_acsl_sub);
+ __gmpz_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
/*@ assert
Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
*/
- __gen_e_acsl_f4_2(& __gen_e_acsl_f4_4,
- (__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
- __gmpz_init_set(__gen_e_acsl_if_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_4));
- __gmpz_clear(__gen_e_acsl__27);
- __gmpz_clear(__gen_e_acsl_add_4);
- __gmpz_clear(__gen_e_acsl_f4_4);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__28;
- int __gen_e_acsl_lt_5;
- __e_acsl_mpz_t __gen_e_acsl_if_5;
- __gmpz_init_set_ui(__gen_e_acsl__28,9223372036854775807UL);
- __gen_e_acsl_lt_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__28));
- if (__gen_e_acsl_lt_5 < 0) {
- __e_acsl_mpz_t __gen_e_acsl__29;
- __gmpz_init_set_ui(__gen_e_acsl__29,9223372036854775807UL);
- __gmpz_init_set(__gen_e_acsl_if_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__29));
- __gmpz_clear(__gen_e_acsl__29);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__30;
- __gmpz_init_set_si(__gen_e_acsl__30,6L);
- __gmpz_init_set(__gen_e_acsl_if_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__30));
- __gmpz_clear(__gen_e_acsl__30);
- }
- __gmpz_init_set(__gen_e_acsl_if_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_5));
- __gmpz_clear(__gen_e_acsl__28);
- __gmpz_clear(__gen_e_acsl_if_5);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_6));
- __gmpz_clear(__gen_e_acsl__26);
- __gmpz_clear(__gen_e_acsl_if_6);
- return;
-}
-
-void __gen_e_acsl_f4(__e_acsl_mpz_t *__retres_arg, int n)
-{
- __e_acsl_mpz_t __gen_e_acsl_n_6;
- __e_acsl_mpz_t __gen_e_acsl__24;
- int __gen_e_acsl_lt_3;
- __e_acsl_mpz_t __gen_e_acsl_if_8;
- __gmpz_init_set_si(__gen_e_acsl_n_6,(long)n);
- __gmpz_init_set_si(__gen_e_acsl__24,100L);
- __gen_e_acsl_lt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_6),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
- if (__gen_e_acsl_lt_3 < 0) {
- __e_acsl_mpz_t __gen_e_acsl_n_7;
- __e_acsl_mpz_t __gen_e_acsl__25;
- __e_acsl_mpz_t __gen_e_acsl_add_3;
- __e_acsl_mpz_t __gen_e_acsl_f4_5;
- __gmpz_init_set_si(__gen_e_acsl_n_7,(long)n);
- __gmpz_init_set_si(__gen_e_acsl__25,1L);
- __gmpz_init(__gen_e_acsl_add_3);
- __gmpz_add(__gen_e_acsl_add_3,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_7),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
+ __gen_e_acsl_f2_2(& __gen_e_acsl_f2_9,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub);
+ __gmpz_init_set_si(__gen_e_acsl__10,2L);
+ __gmpz_init(__gen_e_acsl_sub_5);
+ __gmpz_sub(__gen_e_acsl_sub_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
/*@ assert
Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
*/
- __gen_e_acsl_f4_2(& __gen_e_acsl_f4_5,
- (__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
- __gmpz_init_set(__gen_e_acsl_if_8,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_5));
- __gmpz_clear(__gen_e_acsl_n_7);
- __gmpz_clear(__gen_e_acsl__25);
- __gmpz_clear(__gen_e_acsl_add_3);
- __gmpz_clear(__gen_e_acsl_f4_5);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_n_8;
- __e_acsl_mpz_t __gen_e_acsl__31;
- int __gen_e_acsl_lt_6;
- __e_acsl_mpz_t __gen_e_acsl_if_7;
- __gmpz_init_set_si(__gen_e_acsl_n_8,(long)n);
- __gmpz_init_set_ui(__gen_e_acsl__31,9223372036854775807UL);
- __gen_e_acsl_lt_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_8),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__31));
- if (__gen_e_acsl_lt_6 < 0) {
- __e_acsl_mpz_t __gen_e_acsl__32;
- __gmpz_init_set_ui(__gen_e_acsl__32,9223372036854775807UL);
- __gmpz_init_set(__gen_e_acsl_if_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__32));
- __gmpz_clear(__gen_e_acsl__32);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl__33;
- __gmpz_init_set_si(__gen_e_acsl__33,6L);
- __gmpz_init_set(__gen_e_acsl_if_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__33));
- __gmpz_clear(__gen_e_acsl__33);
- }
- __gmpz_init_set(__gen_e_acsl_if_8,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_7));
- __gmpz_clear(__gen_e_acsl_n_8);
- __gmpz_clear(__gen_e_acsl__31);
- __gmpz_clear(__gen_e_acsl_if_7);
+ __gen_e_acsl_f2_2(& __gen_e_acsl_f2_11,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
+ __gmpz_init(__gen_e_acsl_mul_2);
+ __gmpz_mul(__gen_e_acsl_mul_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_9),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_11));
+ __gmpz_init_set_si(__gen_e_acsl__11,3L);
+ __gmpz_init(__gen_e_acsl_sub_6);
+ __gmpz_sub(__gen_e_acsl_sub_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
+ */
+ __gen_e_acsl_f2_2(& __gen_e_acsl_f2_13,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
+ __gmpz_init_set_si(__gen_e_acsl__12,0L);
+ __gen_e_acsl_div_guard_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_13),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
+ __gmpz_init(__gen_e_acsl_div_2);
+ /*@ assert E_ACSL: f2(n - 3) ≢ 0; */
+ __e_acsl_assert(! (__gen_e_acsl_div_guard_2 == 0),(char *)"Assertion",
+ (char *)"f2",(char *)"f2(n - 3) == 0",10);
+ __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_13));
+ __gmpz_init_set(__gen_e_acsl_if_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_div_2));
+ __gmpz_clear(__gen_e_acsl_n_2);
+ __gmpz_clear(__gen_e_acsl__3);
+ __gmpz_clear(__gen_e_acsl_sub);
+ __gmpz_clear(__gen_e_acsl_f2_9);
+ __gmpz_clear(__gen_e_acsl__10);
+ __gmpz_clear(__gen_e_acsl_sub_5);
+ __gmpz_clear(__gen_e_acsl_f2_11);
+ __gmpz_clear(__gen_e_acsl_mul_2);
+ __gmpz_clear(__gen_e_acsl__11);
+ __gmpz_clear(__gen_e_acsl_sub_6);
+ __gmpz_clear(__gen_e_acsl_f2_13);
+ __gmpz_clear(__gen_e_acsl__12);
+ __gmpz_clear(__gen_e_acsl_div_2);
}
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_8));
- __gmpz_clear(__gen_e_acsl_n_6);
- __gmpz_clear(__gen_e_acsl__24);
- __gmpz_clear(__gen_e_acsl_if_8);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
+ __gmpz_clear(__gen_e_acsl_n);
+ __gmpz_clear(__gen_e_acsl_);
+ __gmpz_clear(__gen_e_acsl_if_2);
return;
}
@@ -315,107 +287,9 @@ void __gen_e_acsl_f2_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
return;
}
-void __gen_e_acsl_f2(__e_acsl_mpz_t *__retres_arg, int n)
+void __gen_e_acsl_g(__e_acsl_mpz_t *__retres_arg, int n)
{
- __e_acsl_mpz_t __gen_e_acsl_n;
- __e_acsl_mpz_t __gen_e_acsl_;
- int __gen_e_acsl_lt;
- __e_acsl_mpz_t __gen_e_acsl_if_2;
- __gmpz_init_set_si(__gen_e_acsl_n,(long)n);
- __gmpz_init_set_si(__gen_e_acsl_,0L);
- __gen_e_acsl_lt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
- if (__gen_e_acsl_lt < 0) {
- __e_acsl_mpz_t __gen_e_acsl__2;
- __gmpz_init_set_si(__gen_e_acsl__2,1L);
- __gmpz_init_set(__gen_e_acsl_if_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
- __gmpz_clear(__gen_e_acsl__2);
- }
- else {
- __e_acsl_mpz_t __gen_e_acsl_n_2;
- __e_acsl_mpz_t __gen_e_acsl__3;
- __e_acsl_mpz_t __gen_e_acsl_sub;
- __e_acsl_mpz_t __gen_e_acsl_f2_9;
- __e_acsl_mpz_t __gen_e_acsl__10;
- __e_acsl_mpz_t __gen_e_acsl_sub_5;
- __e_acsl_mpz_t __gen_e_acsl_f2_11;
- __e_acsl_mpz_t __gen_e_acsl_mul_2;
- __e_acsl_mpz_t __gen_e_acsl__11;
- __e_acsl_mpz_t __gen_e_acsl_sub_6;
- __e_acsl_mpz_t __gen_e_acsl_f2_13;
- __e_acsl_mpz_t __gen_e_acsl__12;
- int __gen_e_acsl_div_guard_2;
- __e_acsl_mpz_t __gen_e_acsl_div_2;
- __gmpz_init_set_si(__gen_e_acsl_n_2,(long)n);
- __gmpz_init_set_si(__gen_e_acsl__3,1L);
- __gmpz_init(__gen_e_acsl_sub);
- __gmpz_sub(__gen_e_acsl_sub,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__3));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub);
- */
- __gen_e_acsl_f2_2(& __gen_e_acsl_f2_9,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub);
- __gmpz_init_set_si(__gen_e_acsl__10,2L);
- __gmpz_init(__gen_e_acsl_sub_5);
- __gmpz_sub(__gen_e_acsl_sub_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
- */
- __gen_e_acsl_f2_2(& __gen_e_acsl_f2_11,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub_5);
- __gmpz_init(__gen_e_acsl_mul_2);
- __gmpz_mul(__gen_e_acsl_mul_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_9),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_11));
- __gmpz_init_set_si(__gen_e_acsl__11,3L);
- __gmpz_init(__gen_e_acsl_sub_6);
- __gmpz_sub(__gen_e_acsl_sub_6,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
- /*@ assert
- Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
- */
- __gen_e_acsl_f2_2(& __gen_e_acsl_f2_13,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub_6);
- __gmpz_init_set_si(__gen_e_acsl__12,0L);
- __gen_e_acsl_div_guard_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f2_13),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
- __gmpz_init(__gen_e_acsl_div_2);
- /*@ assert E_ACSL: f2(n - 3) ≢ 0; */
- __e_acsl_assert(! (__gen_e_acsl_div_guard_2 == 0),(char *)"Assertion",
- (char *)"f2",(char *)"f2(n - 3) == 0",10);
- __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_13));
- __gmpz_init_set(__gen_e_acsl_if_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_div_2));
- __gmpz_clear(__gen_e_acsl_n_2);
- __gmpz_clear(__gen_e_acsl__3);
- __gmpz_clear(__gen_e_acsl_sub);
- __gmpz_clear(__gen_e_acsl_f2_9);
- __gmpz_clear(__gen_e_acsl__10);
- __gmpz_clear(__gen_e_acsl_sub_5);
- __gmpz_clear(__gen_e_acsl_f2_11);
- __gmpz_clear(__gen_e_acsl_mul_2);
- __gmpz_clear(__gen_e_acsl__11);
- __gmpz_clear(__gen_e_acsl_sub_6);
- __gmpz_clear(__gen_e_acsl_f2_13);
- __gmpz_clear(__gen_e_acsl__12);
- __gmpz_clear(__gen_e_acsl_div_2);
- }
- __gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_2));
- __gmpz_clear(__gen_e_acsl_n);
- __gmpz_clear(__gen_e_acsl_);
- __gmpz_clear(__gen_e_acsl_if_2);
+ __gmpz_init_set_si(*__retres_arg,0L);
return;
}
@@ -425,9 +299,87 @@ void __gen_e_acsl_g_5(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
return;
}
-void __gen_e_acsl_g(__e_acsl_mpz_t *__retres_arg, int n)
+void __gen_e_acsl_f3(__e_acsl_mpz_t *__retres_arg, int n)
{
- __gmpz_init_set_si(*__retres_arg,0L);
+ __e_acsl_mpz_t __gen_e_acsl_n_3;
+ __e_acsl_mpz_t __gen_e_acsl__14;
+ int __gen_e_acsl_gt;
+ __e_acsl_mpz_t __gen_e_acsl_if_4;
+ __gmpz_init_set_si(__gen_e_acsl_n_3,(long)n);
+ __gmpz_init_set_si(__gen_e_acsl__14,0L);
+ __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
+ if (__gen_e_acsl_gt > 0) {
+ __e_acsl_mpz_t __gen_e_acsl_g_2;
+ __e_acsl_mpz_t __gen_e_acsl_n_4;
+ __e_acsl_mpz_t __gen_e_acsl__15;
+ __e_acsl_mpz_t __gen_e_acsl_sub_7;
+ __e_acsl_mpz_t __gen_e_acsl_f3_5;
+ __e_acsl_mpz_t __gen_e_acsl_mul_4;
+ __e_acsl_mpz_t __gen_e_acsl__21;
+ __e_acsl_mpz_t __gen_e_acsl_sub_10;
+ __gen_e_acsl_g(& __gen_e_acsl_g_2,n);
+ __gmpz_init_set_si(__gen_e_acsl_n_4,(long)n);
+ __gmpz_init_set_si(__gen_e_acsl__15,1L);
+ __gmpz_init(__gen_e_acsl_sub_7);
+ __gmpz_sub(__gen_e_acsl_sub_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
+ */
+ __gen_e_acsl_f3_2(& __gen_e_acsl_f3_5,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
+ __gmpz_init(__gen_e_acsl_mul_4);
+ __gmpz_mul(__gen_e_acsl_mul_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_2),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f3_5));
+ __gmpz_init_set_si(__gen_e_acsl__21,5L);
+ __gmpz_init(__gen_e_acsl_sub_10);
+ __gmpz_sub(__gen_e_acsl_sub_10,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_4),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
+ __gmpz_init_set(__gen_e_acsl_if_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_10));
+ __gmpz_clear(__gen_e_acsl_g_2);
+ __gmpz_clear(__gen_e_acsl_n_4);
+ __gmpz_clear(__gen_e_acsl__15);
+ __gmpz_clear(__gen_e_acsl_sub_7);
+ __gmpz_clear(__gen_e_acsl_f3_5);
+ __gmpz_clear(__gen_e_acsl_mul_4);
+ __gmpz_clear(__gen_e_acsl__21);
+ __gmpz_clear(__gen_e_acsl_sub_10);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl_n_5;
+ __e_acsl_mpz_t __gen_e_acsl__22;
+ __e_acsl_mpz_t __gen_e_acsl_add_2;
+ __e_acsl_mpz_t __gen_e_acsl_g_8;
+ __gmpz_init_set_si(__gen_e_acsl_n_5,(long)n);
+ __gmpz_init_set_si(__gen_e_acsl__22,1L);
+ __gmpz_init(__gen_e_acsl_add_2);
+ __gmpz_add(__gen_e_acsl_add_2,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__22));
+ /*@ assert
+ Eva: initialization:
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
+ */
+ __gen_e_acsl_g_5(& __gen_e_acsl_g_8,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
+ __gmpz_init_set(__gen_e_acsl_if_4,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_8));
+ __gmpz_clear(__gen_e_acsl_n_5);
+ __gmpz_clear(__gen_e_acsl__22);
+ __gmpz_clear(__gen_e_acsl_add_2);
+ __gmpz_clear(__gen_e_acsl_g_8);
+ }
+ __gmpz_init_set(*__retres_arg,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_4));
+ __gmpz_clear(__gen_e_acsl_n_3);
+ __gmpz_clear(__gen_e_acsl__14);
+ __gmpz_clear(__gen_e_acsl_if_4);
return;
}
@@ -506,87 +458,135 @@ void __gen_e_acsl_f3_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
return;
}
-void __gen_e_acsl_f3(__e_acsl_mpz_t *__retres_arg, int n)
+void __gen_e_acsl_f4(__e_acsl_mpz_t *__retres_arg, int n)
{
- __e_acsl_mpz_t __gen_e_acsl_n_3;
- __e_acsl_mpz_t __gen_e_acsl__14;
- int __gen_e_acsl_gt;
- __e_acsl_mpz_t __gen_e_acsl_if_4;
- __gmpz_init_set_si(__gen_e_acsl_n_3,(long)n);
- __gmpz_init_set_si(__gen_e_acsl__14,0L);
- __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_3),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
- if (__gen_e_acsl_gt > 0) {
- __e_acsl_mpz_t __gen_e_acsl_g_2;
- __e_acsl_mpz_t __gen_e_acsl_n_4;
- __e_acsl_mpz_t __gen_e_acsl__15;
- __e_acsl_mpz_t __gen_e_acsl_sub_7;
- __e_acsl_mpz_t __gen_e_acsl_f3_5;
- __e_acsl_mpz_t __gen_e_acsl_mul_4;
- __e_acsl_mpz_t __gen_e_acsl__21;
- __e_acsl_mpz_t __gen_e_acsl_sub_10;
- __gen_e_acsl_g(& __gen_e_acsl_g_2,n);
- __gmpz_init_set_si(__gen_e_acsl_n_4,(long)n);
- __gmpz_init_set_si(__gen_e_acsl__15,1L);
- __gmpz_init(__gen_e_acsl_sub_7);
- __gmpz_sub(__gen_e_acsl_sub_7,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__15));
+ __e_acsl_mpz_t __gen_e_acsl_n_6;
+ __e_acsl_mpz_t __gen_e_acsl__24;
+ int __gen_e_acsl_lt_3;
+ __e_acsl_mpz_t __gen_e_acsl_if_8;
+ __gmpz_init_set_si(__gen_e_acsl_n_6,(long)n);
+ __gmpz_init_set_si(__gen_e_acsl__24,100L);
+ __gen_e_acsl_lt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_6),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__24));
+ if (__gen_e_acsl_lt_3 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl_n_7;
+ __e_acsl_mpz_t __gen_e_acsl__25;
+ __e_acsl_mpz_t __gen_e_acsl_add_3;
+ __e_acsl_mpz_t __gen_e_acsl_f4_5;
+ __gmpz_init_set_si(__gen_e_acsl_n_7,(long)n);
+ __gmpz_init_set_si(__gen_e_acsl__25,1L);
+ __gmpz_init(__gen_e_acsl_add_3);
+ __gmpz_add(__gen_e_acsl_add_3,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_7),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__25));
/*@ assert
Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
*/
- __gen_e_acsl_f3_2(& __gen_e_acsl_f3_5,
- (__e_acsl_mpz_struct *)__gen_e_acsl_sub_7);
- __gmpz_init(__gen_e_acsl_mul_4);
- __gmpz_mul(__gen_e_acsl_mul_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_2),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_f3_5));
- __gmpz_init_set_si(__gen_e_acsl__21,5L);
- __gmpz_init(__gen_e_acsl_sub_10);
- __gmpz_sub(__gen_e_acsl_sub_10,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_mul_4),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__21));
- __gmpz_init_set(__gen_e_acsl_if_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_sub_10));
- __gmpz_clear(__gen_e_acsl_g_2);
- __gmpz_clear(__gen_e_acsl_n_4);
- __gmpz_clear(__gen_e_acsl__15);
- __gmpz_clear(__gen_e_acsl_sub_7);
- __gmpz_clear(__gen_e_acsl_f3_5);
- __gmpz_clear(__gen_e_acsl_mul_4);
- __gmpz_clear(__gen_e_acsl__21);
- __gmpz_clear(__gen_e_acsl_sub_10);
+ __gen_e_acsl_f4_2(& __gen_e_acsl_f4_5,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_add_3);
+ __gmpz_init_set(__gen_e_acsl_if_8,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_5));
+ __gmpz_clear(__gen_e_acsl_n_7);
+ __gmpz_clear(__gen_e_acsl__25);
+ __gmpz_clear(__gen_e_acsl_add_3);
+ __gmpz_clear(__gen_e_acsl_f4_5);
}
else {
- __e_acsl_mpz_t __gen_e_acsl_n_5;
- __e_acsl_mpz_t __gen_e_acsl__22;
- __e_acsl_mpz_t __gen_e_acsl_add_2;
- __e_acsl_mpz_t __gen_e_acsl_g_8;
- __gmpz_init_set_si(__gen_e_acsl_n_5,(long)n);
- __gmpz_init_set_si(__gen_e_acsl__22,1L);
- __gmpz_init(__gen_e_acsl_add_2);
- __gmpz_add(__gen_e_acsl_add_2,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_n_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__22));
+ __e_acsl_mpz_t __gen_e_acsl_n_8;
+ __e_acsl_mpz_t __gen_e_acsl__31;
+ int __gen_e_acsl_lt_6;
+ __e_acsl_mpz_t __gen_e_acsl_if_7;
+ __gmpz_init_set_si(__gen_e_acsl_n_8,(long)n);
+ __gmpz_init_set_ui(__gen_e_acsl__31,9223372036854775807UL);
+ __gen_e_acsl_lt_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_n_8),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__31));
+ if (__gen_e_acsl_lt_6 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__32;
+ __gmpz_init_set_ui(__gen_e_acsl__32,9223372036854775807UL);
+ __gmpz_init_set(__gen_e_acsl_if_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__32));
+ __gmpz_clear(__gen_e_acsl__32);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__33;
+ __gmpz_init_set_si(__gen_e_acsl__33,6L);
+ __gmpz_init_set(__gen_e_acsl_if_7,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__33));
+ __gmpz_clear(__gen_e_acsl__33);
+ }
+ __gmpz_init_set(__gen_e_acsl_if_8,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_7));
+ __gmpz_clear(__gen_e_acsl_n_8);
+ __gmpz_clear(__gen_e_acsl__31);
+ __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_6);
+ __gmpz_clear(__gen_e_acsl__24);
+ __gmpz_clear(__gen_e_acsl_if_8);
+ return;
+}
+
+void __gen_e_acsl_f4_2(__e_acsl_mpz_t *__retres_arg, __e_acsl_mpz_struct * n)
+{
+ __e_acsl_mpz_t __gen_e_acsl__26;
+ int __gen_e_acsl_lt_4;
+ __e_acsl_mpz_t __gen_e_acsl_if_6;
+ __gmpz_init_set_si(__gen_e_acsl__26,100L);
+ __gen_e_acsl_lt_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__26));
+ if (__gen_e_acsl_lt_4 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__27;
+ __e_acsl_mpz_t __gen_e_acsl_add_4;
+ __e_acsl_mpz_t __gen_e_acsl_f4_4;
+ __gmpz_init_set_si(__gen_e_acsl__27,1L);
+ __gmpz_init(__gen_e_acsl_add_4);
+ __gmpz_add(__gen_e_acsl_add_4,(__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__27));
/*@ assert
Eva: initialization:
- \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
+ \initialized((__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
*/
- __gen_e_acsl_g_5(& __gen_e_acsl_g_8,
- (__e_acsl_mpz_struct *)__gen_e_acsl_add_2);
- __gmpz_init_set(__gen_e_acsl_if_4,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_g_8));
- __gmpz_clear(__gen_e_acsl_n_5);
- __gmpz_clear(__gen_e_acsl__22);
- __gmpz_clear(__gen_e_acsl_add_2);
- __gmpz_clear(__gen_e_acsl_g_8);
+ __gen_e_acsl_f4_2(& __gen_e_acsl_f4_4,
+ (__e_acsl_mpz_struct *)__gen_e_acsl_add_4);
+ __gmpz_init_set(__gen_e_acsl_if_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_f4_4));
+ __gmpz_clear(__gen_e_acsl__27);
+ __gmpz_clear(__gen_e_acsl_add_4);
+ __gmpz_clear(__gen_e_acsl_f4_4);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__28;
+ int __gen_e_acsl_lt_5;
+ __e_acsl_mpz_t __gen_e_acsl_if_5;
+ __gmpz_init_set_ui(__gen_e_acsl__28,9223372036854775807UL);
+ __gen_e_acsl_lt_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(n),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__28));
+ if (__gen_e_acsl_lt_5 < 0) {
+ __e_acsl_mpz_t __gen_e_acsl__29;
+ __gmpz_init_set_ui(__gen_e_acsl__29,9223372036854775807UL);
+ __gmpz_init_set(__gen_e_acsl_if_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__29));
+ __gmpz_clear(__gen_e_acsl__29);
+ }
+ else {
+ __e_acsl_mpz_t __gen_e_acsl__30;
+ __gmpz_init_set_si(__gen_e_acsl__30,6L);
+ __gmpz_init_set(__gen_e_acsl_if_5,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__30));
+ __gmpz_clear(__gen_e_acsl__30);
+ }
+ __gmpz_init_set(__gen_e_acsl_if_6,
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_5));
+ __gmpz_clear(__gen_e_acsl__28);
+ __gmpz_clear(__gen_e_acsl_if_5);
}
__gmpz_init_set(*__retres_arg,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_4));
- __gmpz_clear(__gen_e_acsl_n_3);
- __gmpz_clear(__gen_e_acsl__14);
- __gmpz_clear(__gen_e_acsl_if_4);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl_if_6));
+ __gmpz_clear(__gen_e_acsl__26);
+ __gmpz_clear(__gen_e_acsl_if_6);
return;
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_let.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_let.c
index d5b5c352ae2a76d234a0c27079eddc65b310ebe8..09ec8b4b6a9d92bee0ab1394102ea70ad26b73e4 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_let.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_let.c
@@ -93,18 +93,18 @@ int main(void)
/*@ assert \let u = f; u ≡ f; */
{
__e_acsl_mpq_t __gen_e_acsl_u_10;
- __e_acsl_mpq_t __gen_e_acsl_f;
+ __e_acsl_mpq_t __gen_e_acsl_;
int __gen_e_acsl_eq;
__gmpq_init(__gen_e_acsl_u_10);
__gmpq_set_d(__gen_e_acsl_u_10,(double)f);
- __gmpq_init(__gen_e_acsl_f);
- __gmpq_set_d(__gen_e_acsl_f,(double)f);
+ __gmpq_init(__gen_e_acsl_);
+ __gmpq_set_d(__gen_e_acsl_,(double)f);
__gen_e_acsl_eq = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_u_10),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_f));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_));
__e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
(char *)"\\let u = f; u == f",27);
__gmpq_clear(__gen_e_acsl_u_10);
- __gmpq_clear(__gen_e_acsl_f);
+ __gmpq_clear(__gen_e_acsl_);
}
int t[4] = {1, 2, 3, 4};
/*@ assert \let u = &t[1]; 1 ≡ 1; */
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c
index bda19038bd3f45b7f817652d6b4c49db5439a41a..d2eb693da9f9d5ebca059faf87aad3622b79fd6d 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c
@@ -207,32 +207,32 @@ int main(void)
/*@ assert \let u = f; u ≡ f; */
{
__e_acsl_mpq_t __gen_e_acsl_u_14;
- __e_acsl_mpq_t __gen_e_acsl_f;
+ __e_acsl_mpq_t __gen_e_acsl__10;
int __gen_e_acsl_eq_4;
__gmpq_init(__gen_e_acsl_u_14);
__gmpq_set_d(__gen_e_acsl_u_14,(double)f);
- __gmpq_init(__gen_e_acsl_f);
- __gmpq_set_d(__gen_e_acsl_f,(double)f);
+ __gmpq_init(__gen_e_acsl__10);
+ __gmpq_set_d(__gen_e_acsl__10,(double)f);
__gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_u_14),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_f));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__10));
__e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
(char *)"main",(char *)"\\let u = f; u == f",27);
__gmpq_clear(__gen_e_acsl_u_14);
- __gmpq_clear(__gen_e_acsl_f);
+ __gmpq_clear(__gen_e_acsl__10);
}
int t[4] = {1, 2, 3, 4};
/*@ assert \let u = &t[1]; 1 ≡ 1; */
{
int * /*[4]*/ __gen_e_acsl_u_15;
- __e_acsl_mpz_t __gen_e_acsl__10;
+ __e_acsl_mpz_t __gen_e_acsl__11;
int __gen_e_acsl_eq_5;
__gen_e_acsl_u_15 = & t[1];
- __gmpz_init_set_si(__gen_e_acsl__10,1L);
- __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__10));
+ __gmpz_init_set_si(__gen_e_acsl__11,1L);
+ __gen_e_acsl_eq_5 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__11),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
__e_acsl_assert(__gen_e_acsl_eq_5 == 0,(char *)"Assertion",
(char *)"main",(char *)"\\let u = &t[1]; 1 == 1",30);
- __gmpz_clear(__gen_e_acsl__10);
+ __gmpz_clear(__gen_e_acsl__11);
}
/*@ assert (\let u = &t[1]; 1) ≡ 1; */
{
@@ -247,27 +247,27 @@ int main(void)
/*@ assert \let u = r; u.x + u.y ≡ 3; */
{
struct __anonstruct_r_1 __gen_e_acsl_u_17;
- __e_acsl_mpz_t __gen_e_acsl__11;
__e_acsl_mpz_t __gen_e_acsl__12;
- __e_acsl_mpz_t __gen_e_acsl_add_5;
__e_acsl_mpz_t __gen_e_acsl__13;
+ __e_acsl_mpz_t __gen_e_acsl_add_5;
+ __e_acsl_mpz_t __gen_e_acsl__14;
int __gen_e_acsl_eq_6;
__gen_e_acsl_u_17 = r;
- __gmpz_init_set_si(__gen_e_acsl__11,(long)__gen_e_acsl_u_17.x);
- __gmpz_init_set_si(__gen_e_acsl__12,(long)__gen_e_acsl_u_17.y);
+ __gmpz_init_set_si(__gen_e_acsl__12,(long)__gen_e_acsl_u_17.x);
+ __gmpz_init_set_si(__gen_e_acsl__13,(long)__gen_e_acsl_u_17.y);
__gmpz_init(__gen_e_acsl_add_5);
__gmpz_add(__gen_e_acsl_add_5,
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__11),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__12));
- __gmpz_init_set_si(__gen_e_acsl__13,3L);
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__12),
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
+ __gmpz_init_set_si(__gen_e_acsl__14,3L);
__gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_5),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl__13));
+ (__e_acsl_mpz_struct const *)(__gen_e_acsl__14));
__e_acsl_assert(__gen_e_acsl_eq_6 == 0,(char *)"Assertion",
(char *)"main",(char *)"\\let u = r; u.x + u.y == 3",35);
- __gmpz_clear(__gen_e_acsl__11);
__gmpz_clear(__gen_e_acsl__12);
- __gmpz_clear(__gen_e_acsl_add_5);
__gmpz_clear(__gen_e_acsl__13);
+ __gmpz_clear(__gen_e_acsl_add_5);
+ __gmpz_clear(__gen_e_acsl__14);
}
s.x = 5;
/*@ assert (\let u = s; u.x) > 0; */