From 8e6921d0d49ec468c36e4b04d463452aa3f3ee38 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 11 Jun 2021 16:27:45 +0200
Subject: [PATCH] [eacsl] Remove `Misc.term_addr_of`
The function `Logic_utils.mk_logic_AddrOf` serves the same purpose so
the `Misc` function is removed in favor of that one.
---
src/plugins/e-acsl/src/code_generator/translate.ml | 6 ++++--
src/plugins/e-acsl/src/libraries/misc.ml | 3 ---
src/plugins/e-acsl/src/libraries/misc.mli | 2 --
3 files changed, 4 insertions(+), 7 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 2c4ace3aea3..562aa9e561d 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 95e8177eaab..69a788246b6 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 60c4934e495..daddb3fee08 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. *)
--
GitLab