Merge branch 'bugfix/julien/e-acsl/init_rationals_from_integers' into 'stable/scandium'

Fix a soundness bug when initializing rationals from integers

See merge request frama-c/frama-c!2699

src/plugins/e-acsl/doc/Changelog

@@ -27,6 +27,8 @@ Plugin E-ACSL 21.0 (Scandium)
 
 -* E-ACSL       [2020-06-10] Fix ##13: bug when mixing integers and floats in
                 annotations while -e-acsl-gmp-only is activated.
+-* E-ACSL       [2020-06-10] Fix a soundness bug (##14) when initializing
+                rationals from integers.
 -* E-ACSL       [2020-03-24] Fix automatic deactivation of plug-in Variadic when
                 E-ACSL is directly called from Frama-C without using
                 e-acsl-gcc.sh.

src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h

@@ -145,8 +145,13 @@ extern void __gmpq_set_d(mpq_t q, double d)
   __attribute__((FC_BUILTIN));
 
 /*@ requires \valid(q);
-  @ assigns *q \from n; */
-extern void __gmpq_set_si(mpq_t q, signed long int n)
+  @ assigns *q \from n,d; */
+extern void __gmpq_set_ui(mpq_t q, unsigned long int n, unsigned long int d)
+  __attribute__((FC_BUILTIN));
+
+/*@ requires \valid(q);
+  @ assigns *q \from n,d; */
+extern void __gmpq_set_si(mpq_t q, signed long int n, unsigned long int d)
   __attribute__((FC_BUILTIN));
 
 /*@ allocates q;
@@ -158,7 +163,6 @@ extern int __gmpq_set_str(mpq_t q, const char *str, int base)
   __attribute__((FC_BUILTIN));
 
 /*@ requires \valid(z);
-//  @ ensures z->n == n;
   @ assigns *z \from n; */
 extern void __gmpz_set_ui(mpz_t z, unsigned long int n)
   __attribute__((FC_BUILTIN));

src/plugins/e-acsl/src/code_generator/gmp.ml

@@ -40,18 +40,25 @@ let clear ~loc e = apply_on_var "clear" ~loc e
 
 exception Longlong of ikind
 
-let get_set_suffix_and_arg e =
+let get_set_suffix_and_arg res_ty e =
   let ty = Cil.typeOf e in
   if Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty then "", [ e ]
   else
+    let args_uisi e =
+      if Gmp_types.Z.is_t res_ty then [ e ]
+      else begin
+        assert (Gmp_types.Q.is_t res_ty);
+        [ e; Cil.one ~loc:e.eloc ]
+      end
+    in
     match Cil.unrollType ty with
     | TInt(IChar, _) ->
       (if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui"
        else "_si"),
-      [ e ]
+      args_uisi e
     | TInt((IBool | IUChar | IUInt | IUShort | IULong), _) ->
-      "_ui", [ e ]
-    | TInt((ISChar | IShort | IInt | ILong), _) -> "_si", [ e ]
+      "_ui", args_uisi e
+    | TInt((ISChar | IShort | IInt | ILong), _) -> "_si", args_uisi e
     | TInt((ILongLong | IULongLong as ikind), _) -> raise (Longlong ikind)
     | TPtr(TInt(IChar, _), _) ->
       "_str",
@@ -71,7 +78,7 @@ let get_set_suffix_and_arg e =
 let generic_affect ~loc fname lv ev e =
   let ty = Cil.typeOf ev in
   if Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty then begin
-    let suf, args = get_set_suffix_and_arg e in
+    let suf, args = get_set_suffix_and_arg ty e in
     Constructor.mk_lib_call ~loc (fname ^ suf) (ev :: args)
   end else
     Cil.mkStmtOneInstr ~valid_sid:true (Set(lv, e, e.eloc))
@@ -122,6 +129,6 @@ let affect ~loc lv ev e =
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)

src/plugins/e-acsl/src/code_generator/gmp.mli

@@ -42,6 +42,6 @@ val affect: loc:location -> lval -> exp -> exp -> stmt
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)

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

@@ -232,62 +232,6 @@ void __gen_e_acsl_k(int x)
   return;
 }
 
-int __gen_e_acsl_p2(int x, int y)
-{
-  int __retres = x + (long)y > 0L;
-  return __retres;
-}
-
-int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * 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_si(__gen_e_acsl_x,(long)x);
-  __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 *)(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));
-  int __retres = __gen_e_acsl_gt > 0;
-  __gmpz_clear(__gen_e_acsl_x);
-  __gmpz_clear(__gen_e_acsl_add);
-  __gmpz_clear(__gen_e_acsl__2);
-  return __retres;
-}
-
-int __gen_e_acsl_p2_5(int x, long y)
-{
-  __e_acsl_mpz_t __gen_e_acsl_x_2;
-  __e_acsl_mpz_t __gen_e_acsl_y;
-  __e_acsl_mpz_t __gen_e_acsl_add_2;
-  __e_acsl_mpz_t __gen_e_acsl__3;
-  int __gen_e_acsl_gt_2;
-  __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
-  __gmpz_init_set_si(__gen_e_acsl_y,y);
-  __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));
-  __gmpz_init_set_si(__gen_e_acsl__3,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__3));
-  int __retres = __gen_e_acsl_gt_2 > 0;
-  __gmpz_clear(__gen_e_acsl_x_2);
-  __gmpz_clear(__gen_e_acsl_y);
-  __gmpz_clear(__gen_e_acsl_add_2);
-  __gmpz_clear(__gen_e_acsl__3);
-  return __retres;
-}
-
-int __gen_e_acsl_k_pred(int x)
-{
-  int __retres = x > 0;
-  return __retres;
-}
-
 long __gen_e_acsl_f1(int x, int y)
 {
   long __retres = x + (long)y;
@@ -384,4 +328,60 @@ long __gen_e_acsl_t2(mystruct m)
   return __retres;
 }
 
+int __gen_e_acsl_p2(int x, int y)
+{
+  int __retres = x + (long)y > 0L;
+  return __retres;
+}
+
+int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * 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_si(__gen_e_acsl_x,(long)x);
+  __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 *)(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));
+  int __retres = __gen_e_acsl_gt > 0;
+  __gmpz_clear(__gen_e_acsl_x);
+  __gmpz_clear(__gen_e_acsl_add);
+  __gmpz_clear(__gen_e_acsl__2);
+  return __retres;
+}
+
+int __gen_e_acsl_p2_5(int x, long y)
+{
+  __e_acsl_mpz_t __gen_e_acsl_x_2;
+  __e_acsl_mpz_t __gen_e_acsl_y;
+  __e_acsl_mpz_t __gen_e_acsl_add_2;
+  __e_acsl_mpz_t __gen_e_acsl__3;
+  int __gen_e_acsl_gt_2;
+  __gmpz_init_set_si(__gen_e_acsl_x_2,(long)x);
+  __gmpz_init_set_si(__gen_e_acsl_y,y);
+  __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));
+  __gmpz_init_set_si(__gen_e_acsl__3,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__3));
+  int __retres = __gen_e_acsl_gt_2 > 0;
+  __gmpz_clear(__gen_e_acsl_x_2);
+  __gmpz_clear(__gen_e_acsl_y);
+  __gmpz_clear(__gen_e_acsl_add_2);
+  __gmpz_clear(__gen_e_acsl__3);
+  return __retres;
+}
+
+int __gen_e_acsl_k_pred(int x)
+{
+  int __retres = x > 0;
+  return __retres;
+}
+
 

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

@@ -105,18 +105,6 @@ int main(void)
   return __retres;
 }
 
-int __gen_e_acsl_g(int n)
-{
-  int __retres = 0;
-  return __retres;
-}
-
-int __gen_e_acsl_g_5(long n)
-{
-  int __retres = 0;
-  return __retres;
-}
-
 int __gen_e_acsl_f3(int n)
 {
   int __gen_e_acsl_if_6;
@@ -317,4 +305,16 @@ int __gen_e_acsl_f2_2(long n)
   return __gen_e_acsl_if_3;
 }
 
+int __gen_e_acsl_g(int n)
+{
+  int __retres = 0;
+  return __retres;
+}
+
+int __gen_e_acsl_g_5(long n)
+{
+  int __retres = 0;
+  return __retres;
+}
+
 

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

@@ -223,6 +223,44 @@ int main(void)
     __gmpq_clear(__gen_e_acsl__24);
   }
   /*@ assert 1.1d ≢ 1 + 0.1; */ ;
+  short a = (short)1;
+  short b = (short)1;
+  {
+    __e_acsl_mpq_t __gen_e_acsl__25;
+    __e_acsl_mpq_t __gen_e_acsl__26;
+    __e_acsl_mpq_t __gen_e_acsl_add_5;
+    __e_acsl_mpq_t __gen_e_acsl__27;
+    __e_acsl_mpq_t __gen_e_acsl__28;
+    __e_acsl_mpq_t __gen_e_acsl_sub_2;
+    int __gen_e_acsl_gt;
+    __gmpq_init(__gen_e_acsl__25);
+    __gmpq_set_si(__gen_e_acsl__25,(long)a,1UL);
+    __gmpq_init(__gen_e_acsl__26);
+    __gmpq_set_si(__gen_e_acsl__26,(long)((int)b),1UL);
+    __gmpq_init(__gen_e_acsl_add_5);
+    __gmpq_add(__gen_e_acsl_add_5,
+               (__e_acsl_mpq_struct const *)(__gen_e_acsl__25),
+               (__e_acsl_mpq_struct const *)(__gen_e_acsl__26));
+    __gmpq_init(__gen_e_acsl__27);
+    __gmpq_set_d(__gen_e_acsl__27,2.);
+    __gmpq_init(__gen_e_acsl__28);
+    __gmpq_set_d(__gen_e_acsl__28,1.);
+    __gmpq_init(__gen_e_acsl_sub_2);
+    __gmpq_sub(__gen_e_acsl_sub_2,
+               (__e_acsl_mpq_struct const *)(__gen_e_acsl__27),
+               (__e_acsl_mpq_struct const *)(__gen_e_acsl__28));
+    __gen_e_acsl_gt = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_add_5),
+                                 (__e_acsl_mpq_struct const *)(__gen_e_acsl_sub_2));
+    __e_acsl_assert(__gen_e_acsl_gt > 0,"Assertion","main","a + b > 2. - 1.",
+                    "tests/arith/rationals.c",32);
+    __gmpq_clear(__gen_e_acsl__25);
+    __gmpq_clear(__gen_e_acsl__26);
+    __gmpq_clear(__gen_e_acsl_add_5);
+    __gmpq_clear(__gen_e_acsl__27);
+    __gmpq_clear(__gen_e_acsl__28);
+    __gmpq_clear(__gen_e_acsl_sub_2);
+  }
+  /*@ assert a + b > 2. - 1.; */ ;
   __retres = 0;
   return __retres;
 }
@@ -275,7 +313,7 @@ double __gen_e_acsl_avg(double a, double b)
     __gmpq_set(__gen_e_acsl_avg_real,
                (__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
     __gmpq_init(__gen_e_acsl_delta_2);
-    __gmpq_set_si(__gen_e_acsl_delta_2,(long)__gen_e_acsl_delta);
+    __gmpq_set_si(__gen_e_acsl_delta_2,(long)__gen_e_acsl_delta,1UL);
     __gmpq_init(__gen_e_acsl_sub);
     __gmpq_sub(__gen_e_acsl_sub,
                (__e_acsl_mpq_struct const *)(__gen_e_acsl_avg_real),
@@ -290,7 +328,7 @@ double __gen_e_acsl_avg(double a, double b)
       __e_acsl_mpq_t __gen_e_acsl__4;
       int __gen_e_acsl_lt_2;
       __gmpq_init(__gen_e_acsl_delta_3);
-      __gmpq_set_si(__gen_e_acsl_delta_3,(long)__gen_e_acsl_delta);
+      __gmpq_set_si(__gen_e_acsl_delta_3,(long)__gen_e_acsl_delta,1UL);
       __gmpq_init(__gen_e_acsl_add_2);
       __gmpq_add(__gen_e_acsl_add_2,
                  (__e_acsl_mpq_struct const *)(__gen_e_acsl_avg_real),

src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle

@@ -43,3 +43,5 @@
 [eva:alarm] tests/arith/rationals.c:29: Warning: 
   function __e_acsl_assert: precondition got status unknown.
 [eva:alarm] tests/arith/rationals.c:29: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:32: Warning: 
+  function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/arith/rationals.c

@@ -28,6 +28,9 @@ int main(void) {
 
   /*@ assert 1.1d != 1 + 0.1; */ ;
 
+  short a = 1, b = 1;
+  //@ assert a+b > 2.  - 1.; // gitlab public issue #14
+
   // Not yet:
   // long double ld = 0.1l;
   // /*@ assert d + 1 != ld + 1; */ ; // long double

src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c

@@ -272,9 +272,9 @@ void __gen_e_acsl_foo(float *Mtmax_in, float *Mwmax, float *Mtmax_out)
     __gmpq_init(__gen_e_acsl_);
     __gmpq_set_str(__gen_e_acsl_,"5",10);
     __gmpq_init(__gen_e_acsl__2);
-    __gmpq_set_si(__gen_e_acsl__2,5L);
+    __gmpq_set_si(__gen_e_acsl__2,5L,1UL);
     __gmpq_init(__gen_e_acsl__3);
-    __gmpq_set_si(__gen_e_acsl__3,80L);
+    __gmpq_set_si(__gen_e_acsl__3,80L,1UL);
     __gmpq_init(__gen_e_acsl_div);
     __gmpq_div(__gen_e_acsl_div,
                (__e_acsl_mpq_struct const *)(__gen_e_acsl__2),

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

@@ -288,66 +288,6 @@ void __gen_e_acsl_k(int x)
   return;
 }
 
-int __gen_e_acsl_p2(int x, int y)
-{
-  __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)x);
-  __gmpz_init_set_si(__gen_e_acsl_y_2,(long)y);
-  __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));
-  int __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_3(int x, __e_acsl_mpz_struct * y)
-{
-  __e_acsl_mpz_t __gen_e_acsl_x_3;
-  __e_acsl_mpz_t __gen_e_acsl_add_3;
-  __e_acsl_mpz_t __gen_e_acsl__4;
-  int __gen_e_acsl_gt_3;
-  __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
-  __gmpz_init(__gen_e_acsl_add_3);
-  __gmpz_add(__gen_e_acsl_add_3,
-             (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
-             (__e_acsl_mpz_struct const *)(y));
-  __gmpz_init_set_si(__gen_e_acsl__4,0L);
-  __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3),
-                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
-  int __retres = __gen_e_acsl_gt_3 > 0;
-  __gmpz_clear(__gen_e_acsl_x_3);
-  __gmpz_clear(__gen_e_acsl_add_3);
-  __gmpz_clear(__gen_e_acsl__4);
-  return __retres;
-}
-
-int __gen_e_acsl_k_pred(int x)
-{
-  __e_acsl_mpz_t __gen_e_acsl_x;
-  __e_acsl_mpz_t __gen_e_acsl_;
-  int __gen_e_acsl_gt;
-  __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
-  __gmpz_init_set_si(__gen_e_acsl_,0L);
-  __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
-                               (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
-  int __retres = __gen_e_acsl_gt > 0;
-  __gmpz_clear(__gen_e_acsl_x);
-  __gmpz_clear(__gen_e_acsl_);
-  return __retres;
-}
-
 void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
 {
   __e_acsl_mpz_t __gen_e_acsl_x_4;
@@ -488,4 +428,64 @@ void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
   return;
 }
 
+int __gen_e_acsl_p2(int x, int y)
+{
+  __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)x);
+  __gmpz_init_set_si(__gen_e_acsl_y_2,(long)y);
+  __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));
+  int __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_3(int x, __e_acsl_mpz_struct * y)
+{
+  __e_acsl_mpz_t __gen_e_acsl_x_3;
+  __e_acsl_mpz_t __gen_e_acsl_add_3;
+  __e_acsl_mpz_t __gen_e_acsl__4;
+  int __gen_e_acsl_gt_3;
+  __gmpz_init_set_si(__gen_e_acsl_x_3,(long)x);
+  __gmpz_init(__gen_e_acsl_add_3);
+  __gmpz_add(__gen_e_acsl_add_3,
+             (__e_acsl_mpz_struct const *)(__gen_e_acsl_x_3),
+             (__e_acsl_mpz_struct const *)(y));
+  __gmpz_init_set_si(__gen_e_acsl__4,0L);
+  __gen_e_acsl_gt_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_3),
+                                 (__e_acsl_mpz_struct const *)(__gen_e_acsl__4));
+  int __retres = __gen_e_acsl_gt_3 > 0;
+  __gmpz_clear(__gen_e_acsl_x_3);
+  __gmpz_clear(__gen_e_acsl_add_3);
+  __gmpz_clear(__gen_e_acsl__4);
+  return __retres;
+}
+
+int __gen_e_acsl_k_pred(int x)
+{
+  __e_acsl_mpz_t __gen_e_acsl_x;
+  __e_acsl_mpz_t __gen_e_acsl_;
+  int __gen_e_acsl_gt;
+  __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
+  __gmpz_init_set_si(__gen_e_acsl_,0L);
+  __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+                               (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+  int __retres = __gen_e_acsl_gt > 0;
+  __gmpz_clear(__gen_e_acsl_x);
+  __gmpz_clear(__gen_e_acsl_);
+  return __retres;
+}
+