[e-acsl] simplify signature in Gmp module

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

@@ -154,15 +154,18 @@ module Z = struct
         Printer.pp_binop bop
 
   let new_var ~loc ?scope ?name env kf t mk_stmts =
-    Env.new_var
-      ~loc
-      ?scope
-      ?name
-      env
-      kf
-      t
-      (Gmp_types.Z.t ())
-      (fun v e -> init ~loc e :: mk_stmts v e)
+    let _, e, env =
+      Env.new_var
+        ~loc
+        ?scope
+        ?name
+        env
+        kf
+        t
+        (Gmp_types.Z.t ())
+        (fun v e -> init ~loc e :: mk_stmts v e)
+    in
+    e, env
 
   let create ~loc ?name t_opt env kf e =
     let _, e, env =
@@ -206,7 +209,7 @@ module Z = struct
                            name
                            [ e; e1; e2 ] ] in
     let name = Misc.name_of_binop bop in
-    let _, e, env = new_var ~loc ~name env kf t_opt mk_stmts in
+    let e, env = new_var ~loc ~name env kf t_opt mk_stmts in
     e,env
 
   let cmp ~loc name t_opt bop env kf e1 e2 =
@@ -395,15 +398,17 @@ module Q = struct
       Error.not_yet "R to <typ>"
 
   let new_var ~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 -> init ~loc e :: mk_stmts v e)
+    let _, e, env = Env.new_var
+        ~loc
+        ?scope
+        ?name
+        env
+        kf
+        t_opt
+        (Gmp_types.Q.t ())
+        (fun v e -> init ~loc e :: mk_stmts v e)
+    in
+    e, env
 
   let binop ~loc t_opt bop env kf e1 e2 =
     let name = name_arith_bop bop in
@@ -414,7 +419,7 @@ module Q = struct
                            name
                            [ e; e1; e2 ] ] in
     let name = Misc.name_of_binop bop in
-    let _, e, env = new_var ~loc ~name env kf t_opt mk_stmts in
+    let e, env = new_var ~loc ~name env kf t_opt mk_stmts in
     e, env
 
   let cmp ~loc name t_opt bop env kf e1 e2 =

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

@@ -50,7 +50,7 @@ module Z : sig
     loc:location -> ?scope:Varname.scope -> ?name:string ->
     Env.t -> kernel_function -> term option ->
     (varinfo -> exp (* the var as exp *) -> stmt list) ->
-    varinfo * exp * Env.t
+    exp * Env.t
   (** Same as [Env.new_var], but dedicated to mpz_t variables initialized by
       {!Mpz.init}. *)
 

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

@@ -306,7 +306,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
         | BNot -> "__gmpz_com", "bnot"
         | LNot -> assert false
       in
-      let _, e, env =
+      let e, env =
         Gmp.Z.new_var
           ~loc
           env
@@ -419,7 +419,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
         [ cond; instr ]
       in
       let name = Misc.name_of_binop bop in
-      let _, e, env = Gmp.Z.new_var ~loc ~name env kf t mk_stmts in
+      let e, env = Gmp.Z.new_var ~loc ~name env kf t mk_stmts in
       e, adata, env, Analyses_types.C_number, ""
     else if Gmp_types.Q.is_t ty then
       let e2, adata, env = t2_to_exp adata env in
@@ -627,7 +627,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
         | Some e1_guard -> [ e1_guard; shift_instr ]
       in
       let name = bop_name in
-      let _, e, env = Gmp.Z.new_var ~loc ~name env kf t mk_stmts in
+      let e, env = Gmp.Z.new_var ~loc ~name env kf t mk_stmts in
       e, adata, env, Analyses_types.C_number, ""
     else begin
       assert (Logic_typing.is_integral_type t.term_type);
@@ -691,7 +691,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
       in
       let name = Misc.name_of_binop bop in
       let t = Some t in
-      let _, e, env = Gmp.Z.new_var ~loc ~name env kf t mk_stmts in
+      let e, env = Gmp.Z.new_var ~loc ~name env kf t mk_stmts in
       e, adata, env, Analyses_types.C_number, ""
     else begin
       assert (Logic_typing.is_integral_type t.term_type);