[eacsl] Add functions to strip and add casts

Contrary to the function `Cil.stripCasts`, the function
`Misc.strip_casts` returns the list of removed casts.

Contrary to the function `Cil.mkCast`, the function `Misc.add_casts` is
able to successively add a list of cast like the one returned by
`Misc.strip_casts`.

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, [])))
 

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 ../../../../.."