From a1feaa25cd6d087b28821fce54a68160b344f717 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 24 Mar 2021 16:37:12 +0100
Subject: [PATCH] [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 | 15 +++++++++++++++
src/plugins/e-acsl/src/libraries/misc.mli | 11 +++++++++++
2 files changed, 26 insertions(+)
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 11c177a2735..0bba97a9acf 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 f5a2c283597..f5388826807 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 ../../../../.."
--
GitLab