diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index 78fcbdb2cb8319794ccf435ec231bfba949dd8dd..8b0030707084d570c0765af217a5a9fe898789a8 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -268,11 +268,6 @@ let term ?(loc=Cil_datatype.Location.unknown) term typ =
     term_name = [];
     term_loc = loc }
 
-let taddrof ?(loc=Cil_datatype.Location.unknown) lv typ =
-  match lv with
-  | TMem h, TNoOffset -> h
-  | _ -> term ~loc (TAddrOf lv) typ
-
 (** range of integers *)
 let trange ?(loc=Cil_datatype.Location.unknown) (low,high) =
   term ~loc (Trange(low,high))
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index adf4ec86d568b6826bf9b6e2148feb3d1a81c360..608071816f2bdcb3c97b7754d4736dbcb1746f13 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -296,10 +296,6 @@ val boolean_type: logic_type
 (** returns a anonymous term of the given type. *)
 val term : ?loc:Location.t -> term_node -> logic_type -> term
 
-(** &
-    @deprecated Neon-20130301 {!Logic_utils.mk_AddrOf} is easier to use.*)
-val taddrof: ?loc:Location.t -> term_lval -> logic_type -> term
-
 (** [..] of integers *)
 val trange: ?loc:Location.t -> term option * term option -> term
 
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 96f4b22d28ff03e4d2913087d47212a6109d2fa9..2fb166151250623148259f3b087a508891f3ef4c 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -823,14 +823,14 @@ let type_expr metaenv env ?tr ?current e =
           "Invalid operand for bitwise not: unexpected %a" Printer.pp_term t
     | PUnop(Logic_ptree.Uamp,e) ->
       let env, t, cond = aux env cond e in
-      let ptr =
-        try Ctype (TPtr (Logic_utils.logicCType t.term_type,[]))
-        with Failure _ ->
-          Aorai_option.abort "Cannot take address: not a C type(%a): %a"
-            Printer.pp_logic_type t.term_type Printer.pp_term t
-      in
       (match t.term_node with
-       | TLval v | TStartOf v -> env, Logic_const.taddrof v ptr, cond
+       | TLval v | TStartOf v ->
+         begin try
+             env, Logic_utils.mk_logic_AddrOf v t.term_type, cond
+           with Failure _ ->
+             Aorai_option.abort "Cannot take address: not a C type(%a): %a"
+               Printer.pp_logic_type t.term_type Printer.pp_term t
+         end
        | _ ->
          Aorai_option.abort "Cannot take address: not an lvalue %a"
            Printer.pp_term t
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index 28c79c7a0fd5a49a619817597983744a2cf08252..5e7c6b27d43866895b1a93aad79263d56a319013 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -367,13 +367,14 @@ let extract_quantifiers ~loc args =
                  eliminate_ranges_from_index_of_toffset ~loc toffset quantifiers
                in
                let lty_noset =
+                 Logic_typing.type_of_pointed @@
                  if Logic_const.is_set_type arg.term_type then
                    Logic_const.type_of_element arg.term_type
                  else
                    arg.term_type
                in
                let arg' =
-                 Logic_const.taddrof ~loc (TVar lv, toffset') lty_noset
+                 Logic_utils.mk_logic_AddrOf ~loc (TVar lv, toffset') lty_noset
                in
                arg', quantifiers'
              with Range_elimination_exception ->
diff --git a/src/plugins/instantiate/stdlib/calloc.ml b/src/plugins/instantiate/stdlib/calloc.ml
index dbecd7887f93d798f55858a988d443fbdb78f377..60001c8cb08e1a278abb7728942d23836dcc38b0 100644
--- a/src/plugins/instantiate/stdlib/calloc.ml
+++ b/src/plugins/instantiate/stdlib/calloc.ml
@@ -65,7 +65,8 @@ let pinitialized_len ?loc alloc_type num size =
   let result = tresult ?loc (ptr_of alloc_type) in
   let initialized ?loc t =
     let t = match t.term_node, Logic_utils.unroll_type t.term_type with
-      | TLval (lv), Ctype t -> taddrof ?loc lv (Ctype (ptr_of t))
+      | TLval (lv), (Ctype _ as t) ->
+        Logic_utils.mk_logic_AddrOf ?loc lv t
       | _ -> unexpected "non lvalue or non c-type during initialized generation"
     in
     pinitialized ?loc (here_label, t)