[e-acsl] refactor Gmp: remove Rational.name_arith_bop

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

@@ -159,6 +159,14 @@ module Z = struct
 end
 
 module Q = struct
+  let name_arith_bop = function
+    | PlusA -> "__gmpq_add"
+    | MinusA -> "__gmpq_sub"
+    | Mult -> "__gmpq_mul"
+    | Div -> "__gmpq_div"
+    | Mod | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr
+    | Shiftlt | Shiftrt | PlusPI | MinusPI | MinusPP -> assert false
+
   exception Not_a_decimal of string
   exception Is_a_float
 

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

@@ -48,6 +48,14 @@ module Z : sig
 
 end
 
+module Q : sig
+
+  val name_arith_bop: binop -> string
+  (** [name_of_mpz_arith_bop bop] returns the name of the GMP function on integer
+      corresponding to the [bop] arithmetic operation. *)
+
+end
+
 val normalize_str: string -> string
 (** Normalize the string so that it fits the representation used by the
     underlying real library. For example, "0.1" is a real number in ACSL

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

@@ -111,16 +111,8 @@ let new_var_and_init ~loc ?scope ?name env kf t_opt mk_stmts =
     (Gmp_types.Q.t ())
     (fun v e -> Gmp.init ~loc e :: mk_stmts v e)
 
-let name_arith_bop = function
-  | PlusA -> "__gmpq_add"
-  | MinusA -> "__gmpq_sub"
-  | Mult -> "__gmpq_mul"
-  | Div -> "__gmpq_div"
-  | Mod | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr
-  | Shiftlt | Shiftrt | PlusPI | MinusPI | MinusPP -> assert false
-
 let binop ~loc bop e1 e2 env kf t_opt =
-  let name = name_arith_bop bop in
+  let name = Gmp.Q.name_arith_bop bop in
   (* TODO: [t1_opt] and [t2_opt] could be provided when creating [e1] and
      [e2] *)
   let e1, env = Gmp_gen.Q.create ~loc None env kf e1 in