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

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

+module Z = struct
+  let create ~loc ?name t_opt env kf e =
+    let _, e, env =
+      Env.new_var
+        ~loc
+        ?name
+        env
+        kf
+        t_opt
+        (Gmp_types.Z.t ())
+        (fun lv v -> [ Gmp.init_set ~loc (Cil.var lv) v e ])
+    in
+    e, env
+end
+
+module Q = struct
+  let create ~loc ?name t_opt env kf e =
+    let ty = Cil.typeOf e in
+    if Gmp_types.Q.is_t ty then
+      e, env
+    else
+      let _, e, env =
+        Env.new_var
+          ~loc
+          ?name
+          env
+          kf
+          t_opt
+          (Gmp_types.Q.t ())
+          (fun vi vi_e ->
+             [ Gmp.init ~loc vi_e ;
+               Gmp.affect ~loc (Cil.var vi) vi_e e ])
+      in
+      e, env
+end

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

+open Cil_types
+
+module Z : sig
+  val create:
+    loc:location -> ?name:string -> term option ->  Env.t -> kernel_function ->
+    exp -> exp * Env.t
+    (** Create an integer *)
+end
+
+
+module Q : sig
+  val create:
+    loc:location -> ?name:string -> term option ->  Env.t -> kernel_function ->
+    exp -> exp * Env.t
+    (** Create a real *)
+end

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

@@ -22,25 +22,6 @@
 
 open Cil_types
 
-let create ~loc ?name e env kf t_opt =
-  let ty = Cil.typeOf e in
-  if Gmp_types.Q.is_t ty then
-    e, env
-  else
-    let _, e, env =
-      Env.new_var
-        ~loc
-        ?name
-        env
-        kf
-        t_opt
-        (Gmp_types.Q.t ())
-        (fun vi vi_e ->
-           [ Gmp.init ~loc vi_e ;
-             Gmp.affect ~loc (Cil.var vi) vi_e e ])
-    in
-    e, env
-
 exception Not_a_decimal of string
 exception Is_a_float
 
@@ -180,8 +161,8 @@ let cmp ~loc bop e1 e2 env kf t_opt =
   let name = Misc.name_of_binop bop in
   (* TODO: [t1_opt] and [t2_opt] could be provided when creating [e1] and
      [e2] *)
-  let e1, env = create ~loc e1 env kf None in
-  let e2, env = create ~loc e2 env kf None in
+  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 _, e, env =
     Env.new_var
       ~loc
@@ -222,8 +203,8 @@ let binop ~loc bop e1 e2 env kf t_opt =
   let name = name_arith_bop bop in
   (* TODO: [t1_opt] and [t2_opt] could be provided when creating [e1] and
      [e2] *)
-  let e1, env = create ~loc e1 env kf None in
-  let e2, env = create ~loc e2 env kf None in
+  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

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

@@ -26,13 +26,6 @@
 
 open Cil_types
 
-(* TODO: change the call convention *)
-val create:
-  loc:location -> ?name:string -> exp -> Env.t -> kernel_function ->
-  term option ->
-  exp * Env.t
-(** Create a real *)
-
 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/typed_number.ml

@@ -28,22 +28,9 @@ type strnum =
   | C_number      (* integers and floats included *)
 
 let add_cast ~loc ?name env kf ctx strnum t_opt e =
-  let mk_mpz e =
-    let _, e, env =
-      Env.new_var
-        ~loc
-        ?name
-        env
-        kf
-        t_opt
-        (Gmp_types.Z.t ())
-        (fun lv v -> [ Gmp.init_set ~loc (Cil.var lv) v e ])
-    in
-    e, env
-  in
   let e, env = match strnum with
-    | Str_Z -> mk_mpz e
-    | Str_R -> Rational.create ~loc ?name e env kf t_opt
+    | Str_Z -> Gmp_gen.Z.create ~loc ?name t_opt env kf e
+    | Str_R -> Gmp_gen.Q.create ~loc ?name t_opt env kf e
     | C_number -> e, env
   in
   match ctx with
@@ -71,13 +58,13 @@ let add_cast ~loc ?name env kf ctx strnum t_opt e =
           else
             e
         in
-        mk_mpz e
+        Gmp_gen.Z.create ~loc ?name t_opt env kf e
     | _, false ->
       if Gmp_types.Q.is_t ctx then
         if Gmp_types.Q.is_t (Cil.typeOf e) then (* R --> R *)
           e, env
         else (* C integer or Z --> R *)
-          Rational.create ~loc ?name e env kf t_opt
+          Gmp_gen.Q.create ~loc ?name t_opt env kf e
       else if Gmp_types.Z.is_t ty || strnum = Str_Z then
         (* Z --> C type or the integer is represented by a string:
            anyway, it fits into a C integer: convert it *)