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 a707b074b303fa9d250ce5d385ca87191c3a81c6..95da5a87e63143693060237f4e031f0f46f9348d 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -254,7 +254,7 @@ let range_to_ptr_and_size ~loc kf env ptr r p =
 let term_to_ptr_and_size ~loc kf env t =
   let e, env = !term_to_exp_ref kf (Env.rte env true) t in
   let ty = Misc.cty t.term_type in
-  let sizeof = Misc.mk_ptr_sizeof ty loc in
+  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]
diff --git a/src/plugins/e-acsl/src/code_generator/smart_exp.ml b/src/plugins/e-acsl/src/code_generator/smart_exp.ml
index f3dac85ffd20bd197d046e874ae3a7a40f68e207..c9fd5ff96c0dcf13d24b8c3727b3a495efebad9d 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_exp.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_exp.ml
@@ -39,6 +39,11 @@ let subscript ~loc array idx =
       Cil_types_debug.pp_exp
       array
 
+let ptr_sizeof ~loc typ =
+  match Cil.unrollType typ with
+  | TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
+  | _ -> assert false
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/code_generator/smart_exp.mli b/src/plugins/e-acsl/src/code_generator/smart_exp.mli
index 566702f1e8012f361cfb3beaf9e3683bf50f94a4..45ec7b3809254c7ad3326c39a55c6d813ee40405 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_exp.mli
+++ b/src/plugins/e-acsl/src/code_generator/smart_exp.mli
@@ -36,6 +36,10 @@ val subscript: loc:location -> exp -> exp -> exp
 (** [mk_subscript ~loc array idx] Create an expression to access the [idx]'th
     element of the [array]. *)
 
+val ptr_sizeof: loc:location -> typ -> exp
+(** [ptr_sizeof ~loc ptr_typ] takes the pointer typ [ptr_typ] that points
+    to a [typ] typ and returns [sizeof(typ)]. *)
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 284d57621d5e2f242f8ada787f1acc8c0d8648af..c502d6a42afd535ab13b7ea5b74e2a5817dc3a1d 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -146,11 +146,6 @@ let term_has_lv_from_vi t =
   with Lv_from_vi_found ->
     true
 
-let mk_ptr_sizeof typ loc =
-  match Cil.unrollType typ with
-  | TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
-  | _ -> assert false
-
 let finite_min_and_max i = match Ival.min_and_max i with
   | Some min, Some max -> min, max
   | None, _ | _, None -> assert false
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index ca3f8fd00e6107a4ba74dba379519f1a6a9806e2..2c0a1ca4b418201028573f824ba827dc60f7acf2 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -68,10 +68,6 @@ val term_has_lv_from_vi: term -> bool
 (** @return true iff the given term contains a variables that originates from
     a C varinfo, that is a non-purely logic variable. *)
 
-val mk_ptr_sizeof: typ -> location -> exp
-(** [mk_ptr_sizeof ptr_typ loc] takes the pointer typ [ptr_typ] that points
-    to a [typ] typ and returns [sizeof(typ)]. *)
-
 val name_of_binop: binop -> string
 (** @return the name of the given binop as a string. *)