From 7bdf8d51dd822010e6736d8f5dd93bcf78bf15c9 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 18 Jun 2020 17:34:36 +0200
Subject: [PATCH] [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 | 7 ++-----
src/plugins/e-acsl/src/code_generator/constructor.mli | 5 +++--
src/plugins/e-acsl/src/code_generator/global_observer.ml | 2 +-
3 files changed, 6 insertions(+), 8 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/constructor.ml b/src/plugins/e-acsl/src/code_generator/constructor.ml
index 923affc32ce..4cebe7a2479 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 b286e62ca2e..c3eb194acd0 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 703b4a6f6f6..a89178c8993 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
--
GitLab