[eacsl] Update mk_delete_stmt to support addresses parameters

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

@@ -147,11 +147,11 @@ let mk_store_stmt ?str_size vi =
 let mk_duplicate_store_stmt ?str_size vi =
   mk_named_store_stmt "store_block_duplicate" ?str_size vi
 
-let mk_delete_stmt vi =
+let mk_delete_stmt ?(is_addr=false) vi =
   let loc = vi.vdecl in
   let mk = mk_rtl_call ~loc "delete_block" in
-  match Cil.unrollType vi.vtype with
-  | TArray(_, Some _, _, _) -> mk [ Cil.evar ~loc vi ]
+  match is_addr, Cil.unrollType vi.vtype with
+  | _, TArray(_, Some _, _, _) | true, _ -> mk [ Cil.evar ~loc vi ]
   | _ -> mk [ Cil.mkAddrOfVi vi ]
 
 let mk_mark_readonly vi =

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

@@ -54,9 +54,10 @@ val mk_duplicate_store_stmt: ?str_size:exp -> varinfo -> stmt
 (** Same as [mk_store_stmt] for [__e_acsl_duplicate_store_block] that first
     checks for a previous allocation of the given varinfo. *)
 
-val mk_delete_stmt: varinfo -> stmt
+val mk_delete_stmt: ?is_addr:bool -> varinfo -> stmt
 (** Same as [mk_store_stmt] for [__e_acsl_delete_block] that observes the
-    de-allocation of the given varinfo. *)
+    de-allocation of the given varinfo.
+    If [is_addr] is false (default), take the address of varinfo. *)
 
 val mk_full_init_stmt: varinfo -> stmt
 (** Same as [mk_store_stmt] for [__e_acsl_full_init] that observes the