diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 11c177a27354c2c1881b88aece05394544979fff..0bba97a9acffb9cef45ccaf1b22e959c551fc11c 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -60,6 +60,21 @@ let result_vi kf = match result_lhost kf with
 (** {2 Other stuff} *)
 (* ************************************************************************** *)
 
+let strip_casts e =
+  let rec aux casts e =
+    match e.enode with
+    | CastE(ty, e') -> aux (ty :: casts) e'
+    | _ -> e, casts
+  in
+  aux [] e
+
+let rec add_casts tys e =
+  match tys with
+  | [] -> e
+  | newt :: tl ->
+    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, [])))
 
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index f5a2c28359790d6d6cd4a9285b30c3333944bebe..f5388826807268f5d8c3fc6c57d9a715a5326065 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -94,6 +94,17 @@ val extract_uncoerced_lval: exp -> exp option
     If at some point the expression is neither a [CastE] nor an [Lval], then
     return [None]. *)
 
+val strip_casts: exp -> exp * typ list
+(** [strip casts e] strips the casts from the expression [e] and returns the
+    uncasted expression and the list of casts that were removed in order of
+    application. For example calling [strip_casts ((A)((B)((C)e)))] will return
+    the expression [e] and the list [[C; B; A]]. *)
+
+val add_casts: typ list -> exp -> exp
+(** [add_casts typs e] successively adds the casts in [typs] to the expression
+    [e]. For example calling [add_casts [C; B; A] e] will return the expression
+    [(A)((B)((C)e))]. *)
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."