[eacsl:codegen] Move `Memory_translate.exp_to_base_and_baseaddr` to `Misc.ptr_base`

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

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

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]. *)