[eacsl] Update code with calls to Constructor module

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

@@ -295,14 +295,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 =
-        Cil.mkStmtOneInstr ~valid_sid:true (Set(lval, e, loc))
+        Constructor.mk_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. *)
-      [ Cil.mkStmt ~valid_sid:true (Block block) ], env
+      [ Constructor.mk_block_stmt block ], env
     | Misc.PoT_term t ->
       begin match Typing.get_number_ty t with
       | Typing.(C_integer _ | C_float _ | Nan) ->
@@ -311,14 +311,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 =
-          Cil.mkStmtOneInstr ~valid_sid:true (Set(lval, e, loc))
+         Constructor.mk_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. *)
-        [ Cil.mkStmt ~valid_sid:true (Block block) ], env
+        [ Constructor.mk_block_stmt block ], env
       | Typing.(Rational | Real) ->
         Error.not_yet "\\at on purely logic variables and over real type"
       | Typing.Gmpz ->
@@ -334,7 +334,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
-    (Cil.mkStmt ~valid_sid:true (Block storing_loops_block))
+    (Constructor.mk_block_stmt storing_loops_block)
     ~global_clear:false
     Env.After
   in
@@ -342,7 +342,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 = Cil.new_exp ~loc (Lval lval_at_index) in
+  let e = Constructor.mk_lval ~loc lval_at_index in
   e, env
 
 (*

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

@@ -336,9 +336,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 = Cil.mkStmt ~valid_sid:true (Block block) in
+  let new_stmt = Constructor.mk_block_stmt block in
   let sk = stmt.skind in
-  stmt.skind <- Block (Cil.mkBlock [ new_stmt; Cil.mkStmt ~valid_sid:true sk ]);
+  stmt.skind <- Block (Cil.mkBlock [ new_stmt; Constructor.mk_stmt sk ]);
   let pre = match label with
     | BuiltinLabel(Here | Post) -> true
     | BuiltinLabel(Old | Pre | LoopEntry | LoopCurrent | Init)
@@ -432,7 +432,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 = Cil.mkStmt ~valid_sid:true (Block b) in
+      let sblock = Constructor.mk_block_stmt b in
       Cil.transient_block (Cil.mkBlock [ sblock; stmt ])
     else
       b

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

@@ -136,7 +136,7 @@ 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
-         Cil.mkStmtOneInstr ~valid_sid:true (Set(Cil.var vi, e, loc))
+         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
@@ -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 = Cil.mkStmt ~valid_sid:true (Block b) :: stmts in
+  let stmts = Constructor.mk_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,18 @@ let mk_init_function () =
       (Local_init (vi_already_run, init, loc))
   in
   let already_run =
-    Cil.mkStmtOneInstr ~valid_sid:true
-      (Set (Cil.var vi_already_run, Cil.one ~loc, loc))
+    Constructor.mk_assigns
+      ~loc
+      ~result:(Cil.var vi_already_run)
+      (Cil.one ~loc)
   in
   let stmts = already_run :: stmts in
   let guard =
-    Cil.mkStmt
-      ~valid_sid:true
-      (If (Cil.evar vi_already_run, Cil.mkBlock [], Cil.mkBlock stmts, loc))
+    Constructor.mk_if
+      ~loc
+      ~cond:(Cil.evar vi_already_run)
+      (Cil.mkBlock [])
+      ~else_blk:(Cil.mkBlock stmts)
   in
   let return = Cil.mkStmt ~valid_sid:true (Return (None, loc)) in
   let stmts = [ init_stmt; guard; return ] in

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

@@ -92,7 +92,7 @@ let generic_affect ~loc fname lv ev e =
     let suf, args = get_set_suffix_and_arg ty e in
     Constructor.mk_lib_call ~loc (fname ^ suf) (ev :: args)
   end else
-    Cil.mkStmtOneInstr ~valid_sid:true (Set(lv, e, e.eloc))
+    Constructor.mk_assigns ~loc:e.eloc ~result:lv e
 
 let init_set ~loc lv ev e =
   let fname =
@@ -121,7 +121,7 @@ let init_set ~loc lv ev e =
              Cil.zero ~loc;
              Cil.mkAddrOf ~loc elv ]
        in
-       Cil.mkStmt ~valid_sid:true (Block (Cil.mkBlock [ init ~loc ev; call ]))
+       Constructor.mk_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/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 = Cil.new_exp ~loc (Lval lv_star_ret) in
+      let star_ret = Constructor.mk_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

@@ -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 = mkStmt ~valid_sid:true (Block b) in
+    let block_to_stmt b = Constructor.mk_block_stmt b in
     let tlv = Logic_const.tvar ~loc logic_x in
     let guard =
       (* must copy [t2] to force being typed again *)
@@ -221,16 +221,14 @@ 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 = mkStmt ~valid_sid:true (Break guard_exp.eloc) in
+    let break_stmt = Constructor.mk_break ~loc:guard_exp.eloc in
     let guard_blk, env = Env.pop_and_get
         env
-        (mkStmt
-           ~valid_sid:true
-           (If(
-               guard_exp,
-               mkBlock [ mkEmptyStmt ~loc () ],
-               mkBlock [ break_stmt ],
-               guard_exp.eloc)))
+        (Constructor.mk_if
+           ~loc:guard_exp.eloc
+           ~cond:guard_exp
+           (mkBlock [ mkEmptyStmt ~loc () ])
+           ~else_blk:(mkBlock [ break_stmt ]))
         ~global_clear:false
         Env.Middle
     in
@@ -256,7 +254,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
           Constructor.mk_runtime_check Constructor.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 = Cil.mkStmt ~valid_sid:true (Block b) in
+        let guard_for_small_type = Constructor.mk_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/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
-             [ mkStmtOneInstr ~valid_sid:true (Set(lv, init_val, loc)) ])
+             [ Constructor.mk_assigns ~loc ~result:lv init_val ])
       in
       let end_loop_ref = ref dummyStmt in
       (* innermost block *)
@@ -183,29 +183,28 @@ let convert kf env loc is_forall p bounded_vars hyps goal =
            to evaluation of the goal *)
         let named_predicate_to_exp = !predicate_to_exp_ref in
         let test, env = named_predicate_to_exp kf (Env.push env) goal in
-        let then_block = mkBlock [ mkEmptyStmt ~loc () ] in
-        let else_block =
+        let then_blk = mkBlock [ mkEmptyStmt ~loc () ] in
+        let else_blk =
           (* use a 'goto', not a simple 'break' in order to handle 'forall' with
              multiple binders (leading to imbricated loops) *)
           mkBlock
-            [ mkStmtOneInstr ~valid_sid:true (Set(var var_res, found_val, loc));
+            [ Constructor.mk_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
-            (mkStmt ~valid_sid:true
-               (If(mk_guard test, then_block, else_block, loc)))
+            (Constructor.mk_if ~loc ~cond:(mk_guard test) then_blk ~else_blk)
             ~global_clear:false
             Env.After
         in
         let blk = Cil.flatten_transient_sub_blocks blk in
-        [ mkStmt ~valid_sid:true (Block blk) ], env
+        [ Constructor.mk_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 (mkStmt ~valid_sid:true (Block (mkBlock stmts)))
+        Env.add_stmt env kf (Constructor.mk_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,11 +24,10 @@ open Cil_types
 
 (* No init_set for GMPQ: init then set separately *)
 let init_set ~loc lval vi_e e =
-  Cil.mkStmt
-    ~valid_sid:true
-    (Block (Cil.mkBlock
-              [ Gmp.init ~loc vi_e ;
-                Gmp.affect ~loc lval vi_e e ]))
+  Constructor.mk_block_stmt
+    (Cil.mkBlock
+       [ Gmp.init ~loc vi_e ;
+         Gmp.affect ~loc lval vi_e e ])
 
 let create ~loc ?name e env kf t_opt =
   let ty = Cil.typeOf e in

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

@@ -262,7 +262,7 @@ end = struct
   (* Update local environment with a statement tracking temporal metadata
      associated with assignment [ret] = [func(args)]. *)
   let call_with_ret ?(alloc=false) current_stmt loc ret env kf =
-    let rhs = Cil.new_exp ~loc (Lval ret) in
+    let rhs = Constructor.mk_lval ~loc ret in
     let vals = assign ret rhs loc in
     (* Track referent numbers of assignments via function calls.
        Library functions (i.e., with no source code available) that return

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

@@ -221,15 +221,15 @@ let conditional_to_exp ?(name="if") loc kf t_opt e1 (e2, env2) (e3, env3) =
              Gmp.init_set
            in
            let affect e = init_set ~loc lv ev e in
-           let then_block, _ =
+           let then_blk, _ =
              let s = affect e2 in
              Env.pop_and_get env2 s ~global_clear:false Env.Middle
            in
-           let else_block, _ =
+           let else_blk, _ =
              let s = affect e3 in
              Env.pop_and_get env3 s ~global_clear:false Env.Middle
            in
-           [ Cil.mkStmt ~valid_sid:true (If(e1, then_block, else_block, loc)) ])
+           [ Constructor.mk_if ~loc ~cond:e1 then_blk ~else_blk ])
     in
     e, env
 
@@ -276,7 +276,7 @@ and context_insensitive_term_to_exp kf env t =
     c, env, strnum, ""
   | TLval lv ->
     let lv, env, name = tlval_to_lval kf env lv in
-    Cil.new_exp ~loc (Lval lv), env, C_number, name
+    Constructor.mk_lval ~loc lv, env, C_number, name
   | TSizeOf ty -> Cil.sizeOf ~loc ty, env, C_number, "sizeof"
   | TSizeOfE t ->
     let e, env = term_to_exp kf env t in
@@ -838,7 +838,7 @@ and env_of_li li kf env loc =
   let e, env = term_to_exp kf env t in
   let stmt = match Typing.get_number_ty t with
     | Typing.(C_integer _ | C_float _ | Nan) ->
-      Cil.mkStmtOneInstr ~valid_sid:true (Set (Cil.var vi, e, loc))
+      Constructor.mk_assigns ~loc ~result:(Cil.var vi) e
     | Typing.Gmpz ->
       Gmp.init_set ~loc (Cil.var vi) vi_e e
     | Typing.Rational ->