[e-acsl] refactor Gmp: add Z.cmp

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

@@ -46,6 +46,22 @@ module Z = struct
     in
     e,env
 
+  let cmp ~loc name t_opt bop env kf e1 e2 =
+    let _, e, env = Env.new_var
+        ~loc
+        env
+        kf
+        t_opt
+        ~name
+        Cil.intType
+        (fun v _ ->
+           [ Smart_stmt.rtl_call ~loc
+               ~result:(Cil.var v)
+               ~prefix:""
+               "__gmpz_cmp"
+               [ e1; e2 ] ])
+    in
+    Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
 end
 
 module Q = struct

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

@@ -15,9 +15,14 @@ module Z : sig
   val binop:
     loc:location -> term option -> binop -> Env.t -> kernel_function ->
     exp -> exp -> exp * Env.t
-    (** Applies [binop] to the given expressions. The optional term
-        indicates whether the comparison has a correspondance in the logic. *)
+  (** Applies [binop] to the given expressions. The optional term
+      indicates whether the comparison has a correspondance in the logic. *)
 
+  val cmp:
+    loc:location -> string -> term option -> binop ->  Env.t ->
+    kernel_function -> exp -> exp -> exp * Env.t
+    (** Compares two expressions according to the given [binop]. The optional term
+        indicates whether the comparison has a correspondance in the logic. *)
 
 end
 

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

@@ -205,22 +205,7 @@ let comparison_to_exp
         match ity with
         | C_integer _ | C_float _ | Nan ->
           Cil.mkBinOp ~loc bop e1 e2, env
-        | Gmpz ->
-          let _, e, env = Env.new_var
-              ~loc
-              env
-              kf
-              t_opt
-              ~name
-              Cil.intType
-              (fun v _ ->
-                 [ Smart_stmt.rtl_call ~loc
-                     ~result:(Cil.var v)
-                     ~prefix:""
-                     "__gmpz_cmp"
-                     [ e1; e2 ] ])
-          in
-          Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
+        | Gmpz -> Gmp_gen.Z.cmp ~loc name t_opt bop env kf e1 e2
         | Rational -> Gmp_gen.Q.cmp ~loc t_opt bop env kf e1 e2
         | Real -> Error.not_yet "comparison involving real numbers"
       end