[eacsl] Create a function in Env to call an RTL function and store the result in a new variable

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

@@ -246,6 +246,21 @@ let new_var_and_mpz_init ~loc ?scope ?name env kf t mk_stmts =
     (Gmp_types.Z.t ())
     (fun v e -> Gmp.init ~loc e :: mk_stmts v e)
 
+let rtl_call_to_new_var ~loc ?scope ?name env kf t ty func_name args =
+  let _, exp, env =
+    new_var
+      ~loc
+      ?scope
+      ?name
+      env
+      kf
+      t
+      ty
+      (fun v _ ->
+         [ Constructor.mk_rtl_call ~loc ~result:(Cil.var v) func_name args ])
+  in
+  exp, env
+
 module Logic_binding = struct
 
   let add_binding env logic_v vi =

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

@@ -59,6 +59,15 @@ val new_var_and_mpz_init:
 (** Same as [new_var], but dedicated to mpz_t variables initialized by
     {!Mpz.init}. *)
 
+val rtl_call_to_new_var:
+  loc:location -> ?scope:Varname.scope -> ?name:string ->
+  t -> kernel_function -> term option -> typ ->
+  string -> exp list ->
+  exp * t
+(** [rtl_call_to_new_var env t ty name args] Same as [new_var] but initialize
+    the variable with a call to the RTL function [name] with the given [args].
+*)
+
 module Logic_binding: sig
   val add: ?ty:typ -> t -> kernel_function -> logic_var -> varinfo * exp * t
   (* Add a new C binding to the list of bindings for the logic variable. *)

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

@@ -116,19 +116,15 @@ let call ~loc kf name ctx env t =
   assert (name = "base_addr" || name = "block_length"
           || name = "offset" || name ="freeable");
   let e, env = !term_to_exp_ref kf (Env.rte env true) t in
-  let _, res, env =
-    Env.new_var
-      ~loc
-      ~name
-      env
-      kf
-      None
-      ctx
-      (fun v _ ->
-         let name = Functions.RTL.mk_api_name name in
-         [ Constructor.mk_lib_call ~loc ~result:(Cil.var v) name [ e ] ])
-  in
-  res, env
+  Env.rtl_call_to_new_var
+    ~loc
+    ~name
+    env
+    kf
+    None
+    ctx
+    name
+    [ e ]
 
 (*****************************************************************************)
 (************************* Calls with Range Elimination **********************)
@@ -234,24 +230,20 @@ let call_memory_block ~loc kf name ctx env ptr r p =
     | _ -> assert false
   in
   (* generating env *)
-  let _, e, env =
-    Env.new_var
-      ~loc
-      ~name
-      env
-      kf
-      None
-      ctx
-      (fun v _ ->
-         let fname = Functions.RTL.mk_api_name name in
-         let args = match name with
-           | "valid" | "valid_read" -> [ ptr; size; base; base_addr ]
-           | "initialized" -> [ ptr; size ]
-           | _ -> Error.not_yet ("builtin " ^ name)
-         in
-         [ Constructor.mk_lib_call ~loc ~result:(Cil.var v) fname args ])
+  let args = match name with
+    | "valid" | "valid_read" -> [ ptr; size; base; base_addr ]
+    | "initialized" -> [ ptr; size ]
+    | _ -> Error.not_yet ("builtin " ^ name)
   in
-  e, env
+  Env.rtl_call_to_new_var
+    ~loc
+    ~name
+    env
+    kf
+    None
+    ctx
+    name
+    args
 
 (* [call_with_ranges] handles ranges in [t] when calling builtin [name].
    It only supports the following cases for the time being:
@@ -342,23 +334,17 @@ let call_with_size ~loc kf name ctx env t p =
   let call_for_unsupported_constructs ~loc kf name ctx env t =
     let term_to_exp = !term_to_exp_ref in
     let e, env = term_to_exp kf (Env.rte env true) t in
-    let _, res, env =
-      Env.new_var
-        ~loc
-        ~name
-        env
-        kf
-        None
-        ctx
-        (fun v _ ->
-           let ty = Misc.cty t.term_type in
-           let sizeof = Misc.mk_ptr_sizeof ty loc in
-           [ Constructor.mk_rtl_call ~loc
-               ~result:(Cil.var v)
-               name
-               [ e; sizeof ] ])
-    in
-    res, env
+    let ty = Misc.cty t.term_type in
+    let sizeof = Misc.mk_ptr_sizeof ty loc in
+    Env.rtl_call_to_new_var
+      ~loc
+      ~name
+      env
+      kf
+      None
+      ctx
+      name
+      [ e; sizeof ]
   in
   call_with_ranges
     ~loc
@@ -382,21 +368,18 @@ let call_valid ~loc kf name ctx env t p =
       | Lval lv | StartOf lv -> Cil.mkAddrOrStartOf ~loc lv
       | _ -> assert false
     in
-    let _, res, env =
-      Env.new_var
-        ~loc
-        ~name
-        env
-        kf
-        None
-        ctx
-        (fun v _ ->
-           let ty = Misc.cty t.term_type in
-           let sizeof = Misc.mk_ptr_sizeof ty loc in
-           let args = [ e; sizeof; base; base_addr ] in
-           [ Constructor.mk_rtl_call ~loc ~result:(Cil.var v) name args ])
-    in
-    res, env
+    let ty = Misc.cty t.term_type in
+    let sizeof = Misc.mk_ptr_sizeof ty loc in
+    let args = [ e; sizeof; base; base_addr ] in
+    Env.rtl_call_to_new_var
+      ~loc
+      ~name
+      env
+      kf
+      None
+      ctx
+      name
+      args
   in
   call_with_ranges
     ~loc