diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 0bba97a9acffb9cef45ccaf1b22e959c551fc11c..92d0e9bfef74a16e235e04f84301a1f25b2ce6cc 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -21,7 +21,6 @@
 (**************************************************************************)
 
 open Cil_types
-open Cil_datatype
 
 (* ************************************************************************** *)
 (** {2 Handling the E-ACSL's C-libraries, part I} *)
@@ -82,36 +81,52 @@ let cty = function
   | Ctype ty -> ty
   | lty -> Options.fatal "Expecting a C type. Got %a" Printer.pp_logic_type lty
 
-let rec ptr_index ?(loc=Location.unknown) ?(index=(Cil.zero loc)) exp =
-  let arith_op = function
-    | MinusPI -> MinusA
-    | PlusPI -> PlusA
-    | IndexPI -> PlusA
-    | _ -> assert false in
+(* Replace all trailing array subscripts of an lval with zero indices. *)
+let rec shift_offsets lv loc =
+  let lv, off = Cil.removeOffsetLval lv in
+  match off with
+  | Index _ ->
+    let lv = shift_offsets lv loc in
+    (* since the offset has been removed at the start of the function, add a new
+       0 offset to preserve the type of the lvalue. *)
+    Cil.addOffsetLval (Index (Cil.zero ~loc, NoOffset)) lv
+  | NoOffset | Field _ -> Cil.addOffsetLval off lv
+
+let rec ptr_base ~loc exp =
   match exp.enode with
-  | BinOp(op, lhs, rhs, _) ->
+  | BinOp(op, lhs, _, _) ->
     (match op with
      (* Pointer arithmetic: split pointer and integer parts *)
-     | MinusPI | PlusPI | IndexPI ->
-       let index = Cil.mkBinOp exp.eloc (arith_op op) index rhs in
-       ptr_index ~index lhs
+     | MinusPI | PlusPI | IndexPI -> ptr_base ~loc lhs
      (* Other arithmetic: treat the whole expression as pointer address *)
      | MinusPP | PlusA | MinusA | Mult | Div | Mod
      | BAnd | BXor | BOr | Shiftlt | Shiftrt
-     | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr -> (exp, index))
-  | CastE _ -> ptr_index ~loc ~index (Cil.stripCasts exp)
-  | Info (exp, _) -> ptr_index ~loc ~index exp
-  | Const _ | StartOf _ | AddrOf _ | Lval _ | UnOp _ -> (exp, index)
+     | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr -> exp)
+  (* AddressOf: if it is an addressof array then replace all trailing offsets
+     with zero offsets to get the base. *)
+  | AddrOf lv -> Cil.mkAddrOf ~loc (shift_offsets lv loc)
+  (* StartOf already points to the start of an array, return exp directly *)
+  | StartOf _ -> exp
+  (* Cast: strip cast and continue, then recast to original type. *)
+  | CastE _ ->
+    let exp, casts = strip_casts exp in
+    let base = ptr_base ~loc exp in
+    add_casts casts base
+  | Info (exp, _) -> ptr_base ~loc exp
+  | Const _ | Lval _ | UnOp _ -> 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
+let ptr_base_and_base_addr ~loc e =
+  let rec ptr_base_addr ~loc base =
+    match base.enode with
+    | AddrOf _ | StartOf _ | Const _ -> Cil.zero ~loc
+    | Lval lv -> Cil.mkAddrOrStartOf ~loc lv
+    | CastE _ -> ptr_base_addr ~loc (Cil.stripCasts base)
     | _ -> assert false
   in
+  let base = ptr_base ~loc e in
+  let base_addr  = ptr_base_addr ~loc base in
   base, base_addr
 
 (* TODO: should not be in this file *)
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index f5388826807268f5d8c3fc6c57d9a715a5326065..60c4934e4951628512da4010fb60a44787d60560 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -49,12 +49,11 @@ 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. *)
 
-val ptr_index: ?loc:location -> ?index:exp -> exp
-  -> Cil_types.exp * Cil_types.exp
-(** Split pointer-arithmetic expression of the type [p + i] into its
-    pointer and integer parts. *)
+val ptr_base: loc:location -> exp -> exp
+(** Takes an expression [e] and return [base] where [base] is the address [p]
+    if [e] is of the form [p + i] and [e] otherwise. *)
 
-val ptr_base: loc:location -> exp -> exp * exp
+val ptr_base_and_base_addr: 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