[e-acsl] refactor Gmp: move Gmp.name_of_mpz_arith_bop

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

@@ -37,23 +37,6 @@ let apply_on_var ~loc funname e =
   in
   Smart_stmt.rtl_call ~loc ~prefix funname [ e ]
 
-let name_of_mpz_arith_bop = function
-  | PlusA -> "__gmpz_add"
-  | MinusA -> "__gmpz_sub"
-  | Mult -> "__gmpz_mul"
-  | Div -> "__gmpz_tdiv_q"
-  | Mod -> "__gmpz_tdiv_r"
-  | BAnd -> "__gmpz_and"
-  | BOr -> "__gmpz_ior"
-  | BXor -> "__gmpz_xor"
-  | Shiftlt -> "__gmpz_mul_2exp"
-  | Shiftrt -> "__gmpz_tdiv_q_2exp"
-  | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr | PlusPI | MinusPI
-  | MinusPP as bop ->
-    Options.fatal
-      "Operation '%a' either not arithmetic or not supported on GMP integers"
-      Printer.pp_binop bop
-
 let init ~loc e = apply_on_var "init" ~loc e
 let clear ~loc e = apply_on_var "clear" ~loc e
 
@@ -154,6 +137,26 @@ let init_set ~loc lv ev e =
   else
     mpz_init_set ""
 
+module Z = struct
+
+  let name_arith_bop = function
+    | PlusA -> "__gmpz_add"
+    | MinusA -> "__gmpz_sub"
+    | Mult -> "__gmpz_mul"
+    | Div -> "__gmpz_tdiv_q"
+    | Mod -> "__gmpz_tdiv_r"
+    | BAnd -> "__gmpz_and"
+    | BOr -> "__gmpz_ior"
+    | BXor -> "__gmpz_xor"
+    | Shiftlt -> "__gmpz_mul_2exp"
+    | Shiftrt -> "__gmpz_tdiv_q_2exp"
+    | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr | PlusPI | MinusPI
+    | MinusPP as bop ->
+      Options.fatal
+        "Operation '%a' either not arithmetic or not supported on GMP integers"
+        Printer.pp_binop bop
+
+end
 
 module Q = struct
   exception Not_a_decimal of string

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

@@ -24,10 +24,6 @@
 
 open Cil_types
 
-val name_of_mpz_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. *)
-
 val init: loc:location -> exp -> stmt
 (** build stmt [mpz_init(v)] or [mpq_init(v)] depending on typ of [v] *)
 
@@ -44,6 +40,14 @@ val affect: loc:location -> lval -> exp -> exp -> stmt
     or [mpq_set*(e)] with the good function 'set'
     according to the type of [e] *)
 
+module Z : 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/translate_terms.ml

@@ -115,7 +115,7 @@ let affect_binop ~loc var_as_varinfo var_as_exp binop exp_type exp1 exp2 =
          "__gmpz_cmp"
          [exp1; exp2]
      | Some e ->
-       let name = Gmp.name_of_mpz_arith_bop binop in
+       let name = Gmp.Z.name_arith_bop binop in
        Smart_stmt.rtl_call
          ~loc ~prefix:"" name [e; exp1; exp2])
   else if Gmp_types.Q.is_t exp_type then
@@ -350,7 +350,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
     let e1, adata, env = to_exp ~adata kf env t1 in
     let e2, adata, env = to_exp ~adata kf env t2 in
     if Gmp_types.Z.is_t ty then
-      let name = Gmp.name_of_mpz_arith_bop bop in
+      let name = Gmp.Z.name_arith_bop bop in
       let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc
                              ~prefix:""
                              name
@@ -384,7 +384,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
          RTE should do this automatically. *)
       let ctx = Typing.get_number_ty ~logic_env t in
       let t = Some t in
-      let name = Gmp.name_of_mpz_arith_bop bop in
+      let name = Gmp.Z.name_arith_bop bop in
       (* [TODO] can now do better since the type system got some info about
          possible values of [t2] *)
       (* guarding divisions and modulos *)
@@ -560,7 +560,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
 
       (* Create the shift instruction *)
       let mk_shift_instr result_e =
-        let name = Gmp.name_of_mpz_arith_bop bop in
+        let name = Gmp.Z.name_arith_bop bop in
         Smart_stmt.rtl_call ~loc
           ~prefix:""
           name
@@ -691,7 +691,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
     let e2, adata, env = to_exp ~adata kf env t2 in
     if Gmp_types.Z.is_t ty then
       let mk_stmts _v e =
-        let name = Gmp.name_of_mpz_arith_bop bop in
+        let name = Gmp.Z.name_arith_bop bop in
         let instr = Smart_stmt.rtl_call ~loc ~prefix:"" name [ e; e1; e2 ] in
         [ instr ]
       in