diff --git a/src/plugins/e-acsl/src/code_generator/constructor.ml b/src/plugins/e-acsl/src/code_generator/constructor.ml index 923affc32ced8756a88b0bc9bab3e60f61e07f35..4cebe7a2479f09eeb6ce5a1f36ff54470130ee9c 100644 --- a/src/plugins/e-acsl/src/code_generator/constructor.ml +++ b/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 -> diff --git a/src/plugins/e-acsl/src/code_generator/constructor.mli b/src/plugins/e-acsl/src/code_generator/constructor.mli index b286e62ca2ea8184a86152dfae56312102c76a39..c3eb194acd00e8e2c1eec50fbae115a064ac0e3d 100644 --- a/src/plugins/e-acsl/src/code_generator/constructor.mli +++ b/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 diff --git a/src/plugins/e-acsl/src/code_generator/global_observer.ml b/src/plugins/e-acsl/src/code_generator/global_observer.ml index 703b4a6f6f60fca6d7f3333d31c43d3baed817b4..a89178c89937f87f01466e80690473f37d7f64e6 100644 --- a/src/plugins/e-acsl/src/code_generator/global_observer.ml +++ b/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