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

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

@@ -108,4 +108,29 @@ module Q = struct
     | _ ->
       Error.not_yet "R to <typ>"
 
+  let new_var_and_init ~loc ?scope ?name env kf t_opt mk_stmts =
+    Env.new_var
+      ~loc
+      ?scope
+      ?name
+      env
+      kf
+      t_opt
+      (Gmp_types.Q.t ())
+      (fun v e -> Gmp.init ~loc e :: mk_stmts v e)
+
+  let binop ~loc t_opt bop env kf e1 e2 =
+    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 = create ~loc None env kf e1 in
+    let e2, env = create ~loc None env kf e2 in
+    let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc
+                           ~prefix:""
+                           name
+                           [ e; e1; e2 ] ] in
+    let name = Misc.name_of_binop bop in
+    let _, e, env = new_var_and_init ~loc ~name env kf t_opt mk_stmts in
+    e, env
+
 end

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

@@ -27,7 +27,14 @@ module Q : sig
   val add_cast:
     loc:location -> ?name:string -> Env.t -> kernel_function -> typ -> exp ->
     exp * Env.t
-    (** Assumes that the given exp is of real type and casts it into
-        the given typ *)
+  (** Assumes that the given exp is of real type and casts it into
+      the given typ *)
+
+  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. *)
+
 
 end

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

@@ -47,30 +47,6 @@ let cmp ~loc bop e1 e2 env kf t_opt =
   in
   Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
 
-let new_var_and_init ~loc ?scope ?name env kf t_opt mk_stmts =
-  Env.new_var
-    ~loc
-    ?scope
-    ?name
-    env
-    kf
-    t_opt
-    (Gmp_types.Q.t ())
-    (fun v e -> Gmp.init ~loc e :: mk_stmts v e)
-
-let binop ~loc bop e1 e2 env kf t_opt =
-  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
-  let e2, env = Gmp_gen.Q.create ~loc None env kf e2 in
-  let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc
-                         ~prefix:""
-                         name
-                         [ e; e1; e2 ] ] in
-  let name = Misc.name_of_binop bop in
-  let _, e, env = new_var_and_init ~loc ~name env kf t_opt mk_stmts in
-  e, env
 
 (*
 Local Variables:

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

@@ -27,14 +27,6 @@
 open Cil_types
 
 
-(* TODO: change the call convention --> exp at the end *)
-val binop:
-  loc:location -> binop -> exp -> exp -> Env.t -> kernel_function ->
-  term option ->
-  exp * Env.t
-(** Applies [binop] to the given expressions. The optional term
-    indicates whether the comparison has a correspondance in the logic. *)
-
 (* TODO: change the call convention --> exp at the end *)
 val cmp:
   loc:location -> binop -> exp -> exp -> Env.t -> kernel_function ->

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

@@ -361,7 +361,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
       in
       e, adata, env, Typed_number.C_number, ""
     else if Gmp_types.Q.is_t ty then
-      let e, env = Rational.binop ~loc bop e1 e2 env kf (Some t) in
+      let e, env = Gmp_gen.Q.binop ~loc (Some t) bop env kf e1 e2 in
       e, adata, env, Typed_number.C_number, ""
     else begin
       assert (Logic_typing.is_integral_type t.term_type);
@@ -428,7 +428,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
       e, adata, env, Typed_number.C_number, ""
     else if Gmp_types.Q.is_t ty then
       let e2, adata, env = t2_to_exp adata env in
-      let e, env = Rational.binop ~loc bop e1 e2 env kf (Some t) in
+      let e, env = Gmp_gen.Q.binop ~loc (Some t) bop env kf e1 e2 in
       e, adata, env, Typed_number.C_number, ""
     else begin
       assert (Logic_typing.is_integral_type t.term_type);