From fbfec08b7379a7d2b05603fce45d0eb70c04f8a8 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 15 Apr 2022 08:56:16 +0200
Subject: [PATCH] [kernel] remove deprecated taddrof
---
src/kernel_services/ast_queries/logic_const.ml | 5 -----
src/kernel_services/ast_queries/logic_const.mli | 4 ----
src/plugins/aorai/data_for_aorai.ml | 14 +++++++-------
.../e-acsl/src/code_generator/memory_translate.ml | 3 ++-
src/plugins/instantiate/stdlib/calloc.ml | 3 ++-
5 files changed, 11 insertions(+), 18 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index 78fcbdb2cb8..8b003070708 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 adf4ec86d56..608071816f2 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 96f4b22d28f..2fb16615125 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 28c79c7a0fd..5e7c6b27d43 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 dbecd7887f9..60001c8cb08 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)
--
GitLab