diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 2c4ace3aea337c3113b74e6f977b64824b33b8b9..562aa9e561d6017fbaa23d3676b9aec6b783a5b9 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -868,9 +868,11 @@ and predicate_content_to_exp ?name kf env p =
       call_valid t p
     end else begin
       match t.term_node, t.term_type with
-      | TLval tlv, Ctype ty ->
+      | TLval tlv, lty ->
         let init =
-          Logic_const.pinitialized ~loc (llabel, Misc.term_addr_of ~loc tlv ty)
+          Logic_const.pinitialized
+            ~loc
+            (llabel, Logic_utils.mk_logic_AddrOf ~loc tlv lty)
         in
         Typing.type_named_predicate ~must_clear:false init;
         let p = Logic_const.pand ~loc (init, p) in
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 95e8177eaab3ea44db06987a7c26de20c2d803c7..69a788246b64b72045d19274ffa853a55c0385e5 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -77,9 +77,6 @@ let rec add_casts tys e =
     let e = Cil.mkCast ~newt e in
     add_casts tl e
 
-let term_addr_of ~loc tlv ty =
-  Logic_const.taddrof ~loc tlv (Ctype (TPtr(ty, [])))
-
 let cty = function
   | Ctype ty -> ty
   | lty -> Options.fatal "Expecting a C type. Got %a" Printer.pp_logic_type lty
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index 60c4934e4951628512da4010fb60a44787d60560..daddb3fee0821e40d2420494dd0254f1d8f40e66 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -44,8 +44,6 @@ val is_fc_stdlib_generated: varinfo -> bool
 (** Returns true if the [varinfo] is a generated stdlib function. (For instance
     generated function by the Variadic plug-in. *)
 
-val term_addr_of: loc:location -> term_lval -> typ -> term
-
 val cty: logic_type -> typ
 (** Assume that the logic type is indeed a C type. Just return it. *)