From 2a3171cf6e8e45189331ac9cd17fb3ec09f5a3ce Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 23 Aug 2019 17:45:45 +0200
Subject: [PATCH] [translate] improve add_cast
---
src/plugins/e-acsl/translate.ml | 59 +++++++++++++++------------------
1 file changed, 26 insertions(+), 33 deletions(-)
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 4bb94006097..a969738ea00 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -93,46 +93,37 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
e, env
| Some ctx ->
let ty = Cil.typeOf e in
- (* TODO RATIONAL:
- spaghetti code below. Would be nice to be improved (or at least
- more commented) ==> boolean pattern matching? *)
- if Gmp.Z.is_t ctx then
- if Gmp.Z.is_t ty then
- e, env
- else if Real.is_t ty then
+ match Gmp.Z.is_t ty, Gmp.Z.is_t ctx with
+ | true, true ->
+ (* Z --> Z *)
+ e, env
+ | false, true ->
+ if Real.is_t ty then
+ (* R --> Z *)
Real.cast_to_z ~loc ?name e env
else
- (* Convert the C integer into a mpz.
- Remember:
- - very long constants have been temporary converted into strings;
- - possible to get a non integral type (or Gmp.z_t) with a non-one in
- the case of \null *)
+ (* C integer --> Z *)
let e =
- if Cil.isIntegralType ty || strnum = Str_Z then
- e
- else if not (Cil.isIntegralType ty) && strnum = C_number then
+ if not (Cil.isIntegralType ty) && strnum = C_number then
+ (* special case for \null that must be casted to long: it is the
+ only non integral value that can be seen as an integer, while the
+ type system infers that it is C-representable (see
+ tests/runtime/null.i) *)
Cil.mkCast e Cil.longType (* \null *)
- else begin
- (* TODO RATIONAL: this case seems to be possible:
- getting a very long rational constants (so a string) to be casted
- to an integer *)
- assert (not (Cil.isIntegralType ty) && strnum = Str_R);
- assert false
- end
+ else
+ e
in
mk_mpz e
- else if Real.is_t ctx then
- if Real.is_t (Cil.typeOf e) then e, env
- else Real.mk_real ~loc ?name e env t_opt
- else (* the context is neither MPZ nor MPQ *)
- (* handle a C-integer context *)
- if Gmp.Z.is_t ty || strnum = Str_Z then
- (* we get an mpz, but it fits into a C integer: convert it *)
+ | _, false ->
+ if Real.is_t ctx then
+ if Real.is_t (Cil.typeOf e) then (* R --> R *) e, env
+ else (* C integer or Z --> R *) Real.mk_real ~loc ?name e env t_opt
+ else if Gmp.Z.is_t ty || strnum = Str_Z then
+ (* Z --> C type or the integer is represented by a string:
+ anyway, it fits into a C integer: convert it *)
let fname, new_ty =
- if Cil.isSignedInteger ctx then
- "__gmpz_get_si", Cil.longType
- else
- "__gmpz_get_ui", Cil.ulongType
+ if Cil.isSignedInteger ctx then "__gmpz_get_si", Cil.longType
+ else "__gmpz_get_ui", Cil.ulongType
in
let _, e, env =
Env.new_var
@@ -145,8 +136,10 @@ let add_cast ~loc ?name env ctx strnum t_opt e =
in
e, env
else if Real.is_t ty || strnum = Str_R then
+ (* R --> C type or the real is represented by a string *)
Real.add_cast ~loc ?name e env ctx
else
+ (* C type --> another C type *)
Cil.mkCastT ~force:false ~e ~oldt:ty ~newt:ctx, env
let constant_to_exp ~loc t c =
--
GitLab