[kernel] remove deprecated taddrof

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))

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
 

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

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 ->

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)