[eacsl] Update call sites of Constructor to use the new functions

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

@@ -260,7 +260,7 @@ let to_exp ~loc kf env pot label =
              let e_size, _ = term_to_exp kf env t_size in
              let e_size = Cil.constFold false e_size in
              let malloc_stmt =
-               Constructor.mk_lib_call ~loc
+               Smart_stmt.lib_call ~loc
                  ~result:(Cil.var vi)
                  "malloc"
                  [ e_size ]
@@ -273,7 +273,7 @@ let to_exp ~loc kf env pot label =
            | Typing.(Rational | Real | Nan) ->
              Error.not_yet "quantification over non-integer type"
          in
-         let free_stmt = Constructor.mk_lib_call ~loc "free" [e] in
+         let free_stmt = Smart_stmt.lib_call ~loc "free" [e] in
          (* The list of stmts returned by the current closure are inserted
             LOCALLY to the block where the new var is FIRST used, whatever scope
             is indicated to [Env.new_var].
@@ -296,14 +296,14 @@ let to_exp ~loc kf env pot label =
       let e, env = named_predicate_to_exp kf env p in
       let e = Cil.constFold false e in
       let storing_stmt =
-        Constructor.mk_assigns ~loc ~result:lval e
+        Smart_stmt.assigns ~loc ~result:lval e
       in
       let block, env =
         Env.pop_and_get env storing_stmt ~global_clear:false Env.After
       in
       (* We CANNOT return [block.bstmts] because it does NOT contain
          variable declarations. *)
-      [ Constructor.mk_block_stmt block ], env
+      [ Smart_stmt.block_stmt block ], env
     | Lscope.PoT_term t ->
       begin match Typing.get_number_ty t with
         | Typing.(C_integer _ | C_float _ | Nan) ->
@@ -312,14 +312,14 @@ let to_exp ~loc kf env pot label =
           let e, env = term_to_exp kf env t in
           let e = Cil.constFold false e in
           let storing_stmt =
-            Constructor.mk_assigns ~loc ~result:lval e
+            Smart_stmt.assigns ~loc ~result:lval e
           in
           let block, env =
             Env.pop_and_get env storing_stmt ~global_clear:false Env.After
           in
           (* We CANNOT return [block.bstmts] because it does NOT contain
              variable declarations. *)
-          [ Constructor.mk_block_stmt block ], env
+          [ Smart_stmt.block_stmt block ], env
         | Typing.(Rational | Real) ->
           Error.not_yet "\\at on purely logic variables and over real type"
         | Typing.Gmpz ->
@@ -335,7 +335,7 @@ let to_exp ~loc kf env pot label =
   let storing_loops_block = Cil.mkBlock storing_loops_stmts in
   let storing_loops_block, env = Env.pop_and_get
       env
-      (Constructor.mk_block_stmt storing_loops_block)
+      (Smart_stmt.block_stmt storing_loops_block)
       ~global_clear:false
       Env.After
   in
@@ -343,7 +343,7 @@ let to_exp ~loc kf env pot label =
   let env = put_block_at_label env kf storing_loops_block label in
   (* Returning *)
   let lval_at_index, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
-  let e = Constructor.mk_lval ~loc lval_at_index in
+  let e = Smart_exp.lval ~loc lval_at_index in
   e, env
 
 (*

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

@@ -56,7 +56,7 @@ type local_env = {
 type t = {
   lscope: Lscope.t;
   lscope_reset: bool;
-  annotation_kind: Constructor.annotation_kind;
+  annotation_kind: Smart_stmt.annotation_kind;
   new_global_vars: (varinfo * localized_scope) list;
   (* generated variables. The scope indicates the level where the variable
      should be added. *)
@@ -88,7 +88,7 @@ let empty_local_env =
 let empty =
   { lscope = Lscope.empty;
     lscope_reset = true;
-    annotation_kind = Constructor.Assertion;
+    annotation_kind = Smart_stmt.Assertion;
     new_global_vars = [];
     global_mp_tbl = empty_mp_tbl;
     env_stack = [];
@@ -257,7 +257,7 @@ let rtl_call_to_new_var ~loc ?scope ?name env kf t ty func_name args =
       t
       ty
       (fun v _ ->
-         [ Constructor.mk_rtl_call ~loc ~result:(Cil.var v) func_name args ])
+         [ Smart_stmt.rtl_call ~loc ~result:(Cil.var v) func_name args ])
   in
   exp, env
 
@@ -351,9 +351,9 @@ let add_stmt ?(post=false) ?before env kf stmt =
   { env with env_stack = local_env :: tl }
 
 let extend_stmt_in_place env stmt ~label block =
-  let new_stmt = Constructor.mk_block_stmt block in
+  let new_stmt = Smart_stmt.block_stmt block in
   let sk = stmt.skind in
-  stmt.skind <- Block (Cil.mkBlock [ new_stmt; Constructor.mk_stmt sk ]);
+  stmt.skind <- Block (Cil.mkBlock [ new_stmt; Smart_stmt.stmt sk ]);
   let pre = match label with
     | BuiltinLabel(Here | Post) -> true
     | BuiltinLabel(Old | Pre | LoopEntry | LoopCurrent | Init)
@@ -447,7 +447,7 @@ let pop_and_get ?(split=false) env stmt ~global_clear where =
        add the given [stmt] afterwards. This way, we have the guarantee that
        the final block does not contain any local, so may be transient. *)
     if split then
-      let sblock = Constructor.mk_block_stmt b in
+      let sblock = Smart_stmt.block_stmt b in
       Cil.transient_block (Cil.mkBlock [ sblock; stmt ])
     else
       b

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

@@ -148,8 +148,8 @@ end
 (** {2 Current annotation kind} *)
 (* ************************************************************************** *)
 
-val annotation_kind: t -> Constructor.annotation_kind
-val set_annotation_kind: t -> Constructor.annotation_kind -> t
+val annotation_kind: t -> Smart_stmt.annotation_kind
+val set_annotation_kind: t -> Smart_stmt.annotation_kind -> t
 
 (* ************************************************************************** *)
 (** {2 Loop invariants} *)

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

@@ -123,8 +123,8 @@ let mk_init_function () =
          if Misc.is_fc_or_compiler_builtin vi then stmts
          else
            (* a global is both allocated and initialized *)
-           Constructor.mk_store_stmt vi
-           :: Constructor.mk_initialize ~loc:Location.unknown (Cil.var vi)
+           Smart_stmt.store_stmt vi
+           :: Smart_stmt.initialize ~loc:Location.unknown (Cil.var vi)
            :: stmts)
       tbl
       stmts
@@ -136,10 +136,10 @@ let mk_init_function () =
          let loc = Location.unknown in
          let e = Cil.new_exp ~loc:loc (Const (CStr s)) in
          let str_size = Cil.new_exp loc (SizeOfStr s) in
-         Constructor.mk_assigns ~loc ~result:(Cil.var vi) e
-         :: Constructor.mk_store_stmt ~str_size vi
-         :: Constructor.mk_full_init_stmt vi
-         :: Constructor.mk_mark_readonly vi
+         Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
+         :: Smart_stmt.store_stmt ~str_size vi
+         :: Smart_stmt.full_init_stmt vi
+         :: Smart_stmt.mark_readonly vi
          :: stmts)
       stmts
   in
@@ -150,7 +150,7 @@ let mk_init_function () =
       let b, _env = Env.pop_and_get env stmt ~global_clear:true Env.Before in
       b, stmts
   in
-  let stmts = Constructor.mk_block_stmt b :: stmts in
+  let stmts = Smart_stmt.block_stmt b :: stmts in
   (* prevent multiple calls to [__e_acsl_globals_init] *)
   let loc = Location.unknown in
   let vi_already_run =
@@ -168,14 +168,14 @@ let mk_init_function () =
       (Local_init (vi_already_run, init, loc))
   in
   let already_run =
-    Constructor.mk_assigns
+    Smart_stmt.assigns
       ~loc
       ~result:(Cil.var vi_already_run)
       (Cil.one ~loc)
   in
   let stmts = already_run :: stmts in
   let guard =
-    Constructor.mk_if
+    Smart_stmt.if_stmt
       ~loc
       ~cond:(Cil.evar vi_already_run)
       (Cil.mkBlock [])
@@ -195,7 +195,7 @@ let mk_delete_function () =
     Varinfo.Hashtbl.fold_sorted
       (fun vi _l acc ->
          if Misc.is_fc_or_compiler_builtin vi then acc
-         else Constructor.mk_delete_stmt vi :: acc)
+         else Smart_stmt.delete_stmt vi :: acc)
       tbl
       []
   in

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

@@ -33,7 +33,7 @@ let apply_on_var ~loc funname e =
     else if Gmp_types.Q.is_t ty then "__gmpq_"
     else assert false
   in
-  Constructor.mk_lib_call ~loc (prefix ^ funname) [ e ]
+  Smart_stmt.lib_call ~loc (prefix ^ funname) [ e ]
 
 let init ~loc e = apply_on_var "init" ~loc e
 let clear ~loc e = apply_on_var "clear" ~loc e
@@ -90,9 +90,9 @@ let generic_affect ~loc fname lv ev e =
   let ty = Cil.typeOf ev in
   if Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty then begin
     let suf, args = get_set_suffix_and_arg ty e in
-    Constructor.mk_lib_call ~loc (fname ^ suf) (ev :: args)
+    Smart_stmt.lib_call ~loc (fname ^ suf) (ev :: args)
   end else
-    Constructor.mk_assigns ~loc:e.eloc ~result:lv e
+    Smart_stmt.assigns ~loc:e.eloc ~result:lv e
 
 let init_set ~loc lv ev e =
   let fname =
@@ -111,7 +111,7 @@ let init_set ~loc lv ev e =
      | Lval elv ->
        assert (Gmp_types.Z.is_t (Cil.typeOf ev));
        let call =
-         Constructor.mk_lib_call ~loc
+         Smart_stmt.lib_call ~loc
            "__gmpz_import"
            [ ev;
              Cil.one ~loc;
@@ -121,7 +121,7 @@ let init_set ~loc lv ev e =
              Cil.zero ~loc;
              Cil.mkAddrOf ~loc elv ]
        in
-       Constructor.mk_block_stmt (Cil.mkBlock [ init ~loc ev; call ])
+       Smart_stmt.block_stmt (Cil.mkBlock [ init ~loc ev; call ])
      | _ ->
        Error.not_yet "unsigned long long expression requiring GMP")
   | Longlong ILongLong ->

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

@@ -60,7 +60,7 @@ let inject_in_local_init loc env kf vi = function
   | ConsInit (fvi, sz :: _, _) as init
     when Functions.Libc.is_vla_alloc_name fvi.vname ->
     (* add a store statement when creating a variable length array *)
-    let store = Constructor.mk_store_stmt ~str_size:sz vi in
+    let store = Smart_stmt.store_stmt ~str_size:sz vi in
     let env = Env.add_stmt ~post:true env kf store in
     init, env
 
@@ -145,13 +145,13 @@ let add_initializer loc ?vi lv ?(post=false) stmt env kf =
         (* bitfields are not yet supported ==> no initializer.
            a [not_yet] will be raised in [Translate]. *)
         if Cil.isBitfield lv then Cil.mkEmptyStmt ()
-        else Constructor.mk_initialize ~loc lv
+        else Smart_stmt.initialize ~loc lv
       in
       let env = Env.add_stmt ~post ~before env kf new_stmt in
       let env = match vi with
         | None -> env
         | Some vi ->
-          let new_stmt = Constructor.mk_store_stmt vi in
+          let new_stmt = Smart_stmt.store_stmt vi in
           Env.add_stmt ~post ~before env kf new_stmt
       in
       env
@@ -189,7 +189,7 @@ let inject_in_instr env kf stmt = function
       if Functions.Libc.is_vla_free caller then
         match args with
         | [ { enode = CastE (_, { enode = Lval (Var vi, NoOffset) }) } ] ->
-          let delete_block = Constructor.mk_delete_stmt ~is_addr:true vi in
+          let delete_block = Smart_stmt.delete_stmt ~is_addr:true vi in
           Env.add_stmt env kf delete_block
         | _ -> Options.fatal "The normalization of __fc_vla_free() has changed"
       else
@@ -263,7 +263,7 @@ let add_new_block_in_stmt env kf stmt =
       let b, env =
         Env.pop_and_get env new_stmt ~global_clear:true Env.After
       in
-      let new_stmt = Constructor.mk_block stmt b in
+      let new_stmt = Smart_stmt.block stmt b in
       if not (Cil_datatype.Stmt.equal stmt new_stmt) then begin
         (* move the labels of the return to the new block in order to
            evaluate the postcondition when jumping to them. *)
@@ -293,7 +293,7 @@ let add_new_block_in_stmt env kf stmt =
       let post_block, env =
         Env.pop_and_get
           env
-          (Constructor.mk_block new_stmt pre_block)
+          (Smart_stmt.block new_stmt pre_block)
           ~global_clear:false
           Env.Before
       in
@@ -302,7 +302,7 @@ let add_new_block_in_stmt env kf stmt =
         then Cil.transient_block post_block
         else post_block
       in
-      let res = Constructor.mk_block new_stmt post_block in
+      let res = Smart_stmt.block new_stmt post_block in
       if not (Cil_datatype.Stmt.equal new_stmt res) then
         E_acsl_label.move kf new_stmt res;
       res, env
@@ -337,7 +337,7 @@ let insert_as_last_stmts_in_innermost_block ~last_stmts kf outer_block =
     match return_stmt with
     | Some return_stmt ->
       let b = Cil.mkBlock new_stmts in
-      let new_stmt = Constructor.mk_block return_stmt b in
+      let new_stmt = Smart_stmt.block return_stmt b in
       E_acsl_label.move kf return_stmt new_stmt;
       [ new_stmt ]
     | None -> new_stmts
@@ -516,7 +516,7 @@ and inject_in_block (env: Env.t) kf blk =
         List.fold_left
           (fun acc vi ->
              if Mmodel_analysis.must_model_vi ~kf vi
-             then Constructor.mk_delete_stmt vi :: acc
+             then Smart_stmt.delete_stmt vi :: acc
              else acc)
           stmts
           blk.blocals
@@ -531,7 +531,7 @@ and inject_in_block (env: Env.t) kf blk =
         List.fold_left
           (fun acc vi ->
              if Mmodel_analysis.must_model_vi vi && not vi.vdefined
-             then Constructor.mk_store_stmt vi :: acc
+             then Smart_stmt.store_stmt vi :: acc
              else acc)
           blk.bstmts
           blk.blocals;
@@ -821,8 +821,8 @@ let inject_mmodel_handler main =
       in
       let ptr_size = Cil.sizeOf loc Cil.voidPtrType in
       let args = args @ [ ptr_size ] in
-      let init = Constructor.mk_rtl_call loc "memory_init" args in
-      let clean = Constructor.mk_rtl_call loc "memory_clean" [] in
+      let init = Smart_stmt.rtl_call loc "memory_init" args in
+      let clean = Smart_stmt.rtl_call loc "memory_clean" [] in
       surround_function_with main fundec init (Some clean)
     in
     Extlib.may handle_main main

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

@@ -95,7 +95,7 @@ let length_exp ~loc kf env ~name array =
         ~name
         Cil.theMachine.typeOfSizeOf
         (fun v _ -> [
-             Constructor.mk_assigns
+             Smart_stmt.assigns
                ~loc
                ~result:(Cil.var v)
                (Cil.mkBinOp
@@ -168,7 +168,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
       None
       ~name
       Cil.intType
-      (fun v _ -> [ Constructor.mk_assigns ~loc ~result:(Cil.var v) (res_value ()) ])
+      (fun v _ -> [ Smart_stmt.assigns ~loc ~result:(Cil.var v) (res_value ()) ])
   in
 
   (* Retrieve the length of the arrays *)
@@ -193,8 +193,8 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
      arrays. This env will enable us to also check RTEs *)
   let env = Env.push env in
   (* Create the access to the arrays *)
-  let array1_iter_e = Constructor.mk_subscript ~loc array1 iter_e in
-  let array2_iter_e = Constructor.mk_subscript ~loc array2 iter_e in
+  let array1_iter_e = Smart_exp.subscript ~loc array1 iter_e in
+  let array2_iter_e = Smart_exp.subscript ~loc array2 iter_e in
   (* Check RTE on the arrays, filtering out bounding checks since the accesses
      are built already in bounds *)
   let filter a =
@@ -212,12 +212,12 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
   let cond = Cil.mkBinOp ~loc Ne array1_iter_e array2_iter_e in
   (* Create the statement representing the body of the for loop *)
   let body =
-    Constructor.mk_if
+    Smart_stmt.if_stmt
       ~loc
       ~cond
       (Cil.mkBlock [
-          Constructor.mk_assigns ~loc ~result:(Cil.var comparison_vi) (res_value ~flip:true ());
-          Constructor.mk_break ~loc
+          Smart_stmt.assigns ~loc ~result:(Cil.var comparison_vi) (res_value ~flip:true ());
+          Smart_stmt.break ~loc
         ])
   in
   (* Pop the env to build the body of the for loop *)
@@ -225,14 +225,14 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
 
   (* Create the statement representing the full for loop *)
   let for_loop =
-    (Constructor.mk_block_stmt
+    (Smart_stmt.block_stmt
        (Cil.mkBlock
           (Cil.mkForIncr
              ~iter
              ~first:(Cil.zero ~loc)
              ~stopat:len1_exp
              ~incr:(Cil.one ~loc)
-             ~body:[ Constructor.mk_block_stmt body_blk ]
+             ~body:[ Smart_stmt.block_stmt body_blk ]
           )
        )
     )
@@ -244,7 +244,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
 
   (* Add the check for the length before the for loop *)
   let prepend_coercion_check ~name env stmts array len =
-    let array_orig = Option.get (Constructor.extract_uncoerced_lval array) in
+    let array_orig = Option.get (Misc.extract_uncoerced_lval array) in
     if array_orig == array then
       stmts, env
     else
@@ -259,7 +259,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
       in
       let p = { p with pred_name = "array_coercion" :: p.pred_name } in
       let stmt =
-        Constructor.mk_runtime_check Constructor.RTE kf e p
+        Smart_stmt.runtime_check Smart_stmt.RTE kf e p
       in
       stmt :: stmts, env
   in
@@ -272,17 +272,17 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
 
   (* Pop the env to build the full then block *)
   let then_blk, env =
-    pop_and_get_env env (Constructor.mk_block_stmt (Cil.mkBlock then_stmts))
+    pop_and_get_env env (Smart_stmt.block_stmt (Cil.mkBlock then_stmts))
   in
 
   (* Create the statement representing the whole generated code *)
   let stmt =
-    Constructor.mk_if
+    Smart_stmt.if_stmt
       ~loc
       ~cond:(Cil.mkBinOp ~loc Eq len1_exp len2_exp)
       then_blk
       ~else_blk:(Cil.mkBlock
-                   [ Constructor.mk_assigns
+                   [ Smart_stmt.assigns
                        ~loc
                        ~result:(Cil.var comparison_vi)
                        (res_value ~flip:true ()) ])

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

@@ -98,7 +98,7 @@ let term_to_block ~loc kf env ret_ty ret_vi t =
        function (by reference). *)
     let set =
       let lv_star_ret = Cil.mkMem ~addr:(Cil.evar ~loc ret_vi) ~off:NoOffset in
-      let star_ret = Constructor.mk_lval ~loc lv_star_ret in
+      let star_ret = Smart_exp.lval ~loc lv_star_ret in
       Gmp.init_set ~loc lv_star_ret star_ret e
     in
     let return_void = Cil.mkStmt ~valid_sid:true (Return (None, loc)) in

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

@@ -59,11 +59,11 @@ let preserve_invariant env kf stmt = match stmt.skind with
         let blk, env =
           Env.pop_and_get env last ~global_clear:false Env.Before
         in
-        Constructor.mk_block last blk :: stmts, env
+        Smart_stmt.block last blk :: stmts, env
       | s :: tl ->
         handle_invariants (s :: stmts, env) tl
     in
-    let env = Env.set_annotation_kind env Constructor.Invariant in
+    let env = Env.set_annotation_kind env Smart_stmt.Invariant in
     let stmts, env = handle_invariants ([], env) stmts in
     let new_blk = { blk with bstmts = List.rev stmts } in
     { stmt with skind = Loop([], new_blk, loc, cont, break) },
@@ -212,7 +212,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
         Env.Middle
     in
     (* generate the guard [x bop t2] *)
-    let block_to_stmt b = Constructor.mk_block_stmt b in
+    let block_to_stmt b = Smart_stmt.block_stmt b in
     let tlv = Logic_const.tvar ~loc logic_x in
     let guard =
       (* must copy [t2] to force being typed again *)
@@ -221,10 +221,10 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
     in
     Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int guard;
     let guard_exp, env = term_to_exp kf (Env.push env) guard in
-    let break_stmt = Constructor.mk_break ~loc:guard_exp.eloc in
+    let break_stmt = Smart_stmt.break ~loc:guard_exp.eloc in
     let guard_blk, env = Env.pop_and_get
         env
-        (Constructor.mk_if
+        (Smart_stmt.if_stmt
            ~loc:guard_exp.eloc
            ~cond:guard_exp
            (mkBlock [ mkEmptyStmt ~loc () ])
@@ -251,10 +251,10 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
       | Some p ->
         let e, env = !named_predicate_ref kf (Env.push env) p in
         let stmt, env =
-          Constructor.mk_runtime_check Constructor.RTE kf e p, env
+          Smart_stmt.runtime_check Smart_stmt.RTE kf e p, env
         in
         let b, env = Env.pop_and_get env stmt ~global_clear:false Env.After in
-        let guard_for_small_type = Constructor.mk_block_stmt b in
+        let guard_for_small_type = Smart_stmt.block_stmt b in
         guard_for_small_type :: guard :: body @ [ next ], env
     in
     let start = block_to_stmt init_blk in

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

@@ -39,7 +39,7 @@ let store ?before env kf vars =
   tracking_stmt
     ?before
     List.fold_right (* small list *)
-    Constructor.mk_store_stmt
+    Smart_stmt.store_stmt
     env
     kf
     vars
@@ -48,7 +48,7 @@ let duplicate_store ?before env kf vars =
   tracking_stmt
     ?before
     Varinfo.Set.fold
-    Constructor.mk_duplicate_store_stmt
+    Smart_stmt.duplicate_store_stmt
     env
     kf
     vars
@@ -57,7 +57,7 @@ let delete_from_list ?before env kf vars =
   tracking_stmt
     ?before
     List.fold_right (* small list *)
-    Constructor.mk_delete_stmt
+    Smart_stmt.delete_stmt
     env
     kf
     vars
@@ -66,7 +66,7 @@ let delete_from_set ?before env kf vars =
   tracking_stmt
     ?before
     Varinfo.Set.fold
-    Constructor.mk_delete_stmt
+    Smart_stmt.delete_stmt
     env
     kf
     vars

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

@@ -155,8 +155,8 @@ let gmp_to_sizet ~loc kf env size p =
       None
       sizet
       (fun vi _ ->
-         [ Constructor.mk_runtime_check Constructor.RTE kf guard p;
-           Constructor.mk_lib_call ~loc
+         [ Smart_stmt.runtime_check Smart_stmt.RTE kf guard p;
+           Smart_stmt.lib_call ~loc
              ~result:(Cil.var vi)
              "__gmpz_get_ui"
              [ size ] ])

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

@@ -174,7 +174,7 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
           intType
           (fun v _ ->
              let lv = var v in
-             [ Constructor.mk_assigns ~loc ~result:lv init_val ])
+             [ Smart_stmt.assigns ~loc ~result:lv init_val ])
       in
       let end_loop_ref = ref dummyStmt in
       (* innermost block *)
@@ -188,23 +188,23 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
           (* use a 'goto', not a simple 'break' in order to handle 'forall' with
              multiple binders (leading to imbricated loops) *)
           mkBlock
-            [ Constructor.mk_assigns ~loc ~result:(var var_res) found_val;
+            [ Smart_stmt.assigns ~loc ~result:(var var_res) found_val;
               mkStmt ~valid_sid:true (Goto(end_loop_ref, loc)) ]
         in
         let blk, env = Env.pop_and_get
             env
-            (Constructor.mk_if ~loc ~cond:(mk_guard test) then_blk ~else_blk)
+            (Smart_stmt.if_stmt ~loc ~cond:(mk_guard test) then_blk ~else_blk)
             ~global_clear:false
             Env.After
         in
         let blk = Cil.flatten_transient_sub_blocks blk in
-        [ Constructor.mk_block_stmt blk ], env
+        [ Smart_stmt.block_stmt blk ], env
       in
       let stmts, env =
         Loops.mk_nested_loops ~loc mk_innermost_block kf env lvs_guards
       in
       let env =
-        Env.add_stmt env kf (Constructor.mk_block_stmt (mkBlock stmts))
+        Env.add_stmt env kf (Smart_stmt.block_stmt (mkBlock stmts))
       in
       (* where to jump to go out of the loop *)
       let end_loop = mkEmptyStmt ~loc () in

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

@@ -24,7 +24,7 @@ open Cil_types
 
 (* No init_set for GMPQ: init then set separately *)
 let init_set ~loc lval vi_e e =
-  Constructor.mk_block_stmt
+  Smart_stmt.block_stmt
     (Cil.mkBlock
        [ Gmp.init ~loc vi_e ;
          Gmp.affect ~loc lval vi_e e ])
@@ -148,7 +148,7 @@ let add_cast ~loc ?name e env kf ty =
         None
         Cil.doubleType
         (fun v _ ->
-           [ Constructor.mk_lib_call ~loc
+           [ Smart_stmt.lib_call ~loc
                ~result:(Cil.var v)
                "__gmpq_get_d"
                [ e ] ])
@@ -197,7 +197,7 @@ let cmp ~loc bop e1 e2 env kf t_opt =
       ~name
       Cil.intType
       (fun v _ ->
-         [ Constructor.mk_lib_call ~loc ~result:(Cil.var v) fname [ e1; e2 ] ])
+         [ Smart_stmt.lib_call ~loc ~result:(Cil.var v) fname [ e1; e2 ] ])
   in
   Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env