[eacsl] Update Constructor.mk_full_init_stmt

Remove unused labelled argument and simplify the function as a result.

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

@@ -105,12 +105,9 @@ let mk_rtl_call ~loc ?result fname args =
 (** {2 Handling the E-ACSL's C-libraries, part II} *)
 (* ************************************************************************** *)
 
-let mk_full_init_stmt ?(addr=true) vi =
+let mk_full_init_stmt vi =
   let loc = vi.vdecl in
-  let mk = mk_rtl_call ~loc "full_init" in
-  match addr, Cil.unrollType vi.vtype with
-  | _, TArray(_,Some _, _, _) | false, _ -> mk [ Cil.evar ~loc vi ]
-  | _ -> mk [ Cil.mkAddrOfVi vi ]
+  mk_rtl_call ~loc "full_init" [ Cil.evar ~loc vi ]
 
 let mk_initialize ~loc (host, offset as lv) = match host, offset with
   | Var _, NoOffset ->

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

@@ -58,9 +58,10 @@ val mk_delete_stmt: varinfo -> stmt
 (** Same as [mk_store_stmt] for [__e_acsl_delete_block] that observes the
     de-allocation of the given varinfo. *)
 
-val mk_full_init_stmt: ?addr:bool -> varinfo -> stmt
+val mk_full_init_stmt: varinfo -> stmt
 (** Same as [mk_store_stmt] for [__e_acsl_full_init] that observes the
-    initialization of the given varinfo. *)
+    initialization of the given varinfo. The varinfo is the address to fully
+    initialize, no [addrOf] is taken. *)
 
 val mk_initialize: loc:location -> lval -> stmt
 (** Same as [mk_store_stmt] for [__e_acsl_initialize] that observes the

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

@@ -138,7 +138,7 @@ let mk_init_function () =
          let str_size = Cil.new_exp loc (SizeOfStr s) in
          Cil.mkStmtOneInstr ~valid_sid:true (Set(Cil.var vi, e, loc))
          :: Constructor.mk_store_stmt ~str_size vi
-         :: Constructor.mk_full_init_stmt ~addr:false vi
+         :: Constructor.mk_full_init_stmt vi
          :: Constructor.mk_mark_readonly vi
          :: stmts)
       stmts