From c3a9599d47f49686c29c0785ec6439465cdd4fd4 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 6 Oct 2020 16:17:32 +0200
Subject: [PATCH] [eacsl:codegen] Move
`Memory_translate.exp_to_base_and_baseaddr` to `Misc.ptr_base`
---
.../src/code_generator/memory_translate.ml | 17 ++---------------
src/plugins/e-acsl/src/libraries/misc.ml | 9 +++++++++
src/plugins/e-acsl/src/libraries/misc.mli | 6 ++++++
3 files changed, 17 insertions(+), 15 deletions(-)
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 95da5a87e63..be6fbc2bc7a 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -257,19 +257,6 @@ let term_to_ptr_and_size ~loc kf env t =
let sizeof = Smart_exp.ptr_sizeof ~loc ty in
e, sizeof, env
-(* Take an expression [e] and return a tuple [(base, base_addr)] where [base]
- is the address [p] if [e] is of the form [p + i] and [e] otherwise, and
- [base_addr] is the address [&p] if [e] is of the form [p + i] and 0
- otherwise. *)
-let exp_to_base_and_baseaddr ~loc e =
- let base, _ = Misc.ptr_index ~loc e in
- let base_addr = match base.enode with
- | AddrOf _ | Const _ -> Cil.zero ~loc
- | Lval lv | StartOf lv -> Cil.mkAddrOrStartOf ~loc lv
- | _ -> assert false
- in
- base, base_addr
-
(* [fname_to_pred name args] returns the memory predicate corresponding to
[name] with the given [args]. *)
let fname_to_pred ?loc name args =
@@ -510,12 +497,12 @@ let call_valid ~loc kf name ctx env t p =
assert (name = "valid" || name = "valid_read");
let arg_from_term ~loc kf env rev_args t _p =
let ptr, size, env = term_to_ptr_and_size ~loc kf env t in
- let base, base_addr = exp_to_base_and_baseaddr ~loc ptr in
+ let base, base_addr = Misc.ptr_base ~loc ptr in
base_addr :: base :: size :: ptr :: rev_args, env
in
let arg_from_range ~loc kf env rev_args ptr r p =
let ptr, size, env = range_to_ptr_and_size ~loc kf env ptr r p in
- let base, base_addr = exp_to_base_and_baseaddr ~loc ptr in
+ let base, base_addr = Misc.ptr_base ~loc ptr in
base_addr :: base :: size :: ptr :: rev_args, env
in
let prepend_n_args = false in
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index c502d6a42af..2c123e74461 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -87,6 +87,15 @@ let rec ptr_index ?(loc=Location.unknown) ?(index=(Cil.zero loc)) exp =
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
-> assert false
+let ptr_base ~loc e =
+ let base, _ = ptr_index ~loc e in
+ let base_addr = match base.enode with
+ | AddrOf _ | Const _ -> Cil.zero ~loc
+ | Lval lv | StartOf lv -> Cil.mkAddrOrStartOf ~loc lv
+ | _ -> assert false
+ in
+ base, base_addr
+
(* TODO: should not be in this file *)
let term_of_li li = match li.l_body with
| LBterm t -> t
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index 2c0a1ca4b41..090b2377531 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -50,6 +50,12 @@ val ptr_index: ?loc:location -> ?index:exp -> exp
(** Split pointer-arithmetic expression of the type [p + i] into its
pointer and integer parts. *)
+val ptr_base: loc:location -> exp -> exp * exp
+(* Takes an expression [e] and return a tuple [(base, base_addr)] where [base]
+ is the address [p] if [e] is of the form [p + i] and [e] otherwise, and
+ [base_addr] is the address [&p] if [e] is of the form [p + i] and 0
+ otherwise. *)
+
val term_of_li: logic_info -> term
(** [term_of_li li] assumes that [li.l_body] matches [LBterm t]
and returns [t]. *)
--
GitLab