From 538a9bd43c28cf2d2663f53106095aac5e40f1a5 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 19 Sep 2013 09:34:39 +0000
Subject: [PATCH] [E-ACSL] still few gmp's
---
src/plugins/e-acsl/typing.ml | 20 ++++++++++----------
1 file changed, 10 insertions(+), 10 deletions(-)
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 30e38e31738..bed8d187216 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -59,6 +59,8 @@ let pretty_eacsl_typ fmt = function
exception Not_representable
+(* TODO: replace it by Cil.intKindForValue as soon as Frama-C Fluorine is not
+ required anymore. *)
let typ_of_integer i unsigned =
(* int whenever possible *)
if Cil.fitsInInt IInt i then IInt
@@ -77,15 +79,10 @@ let typ_of_eacsl_typ = function
| Interv(l, u) ->
let is_pos = Z.ge l Z.zero in
(try
- let mk n k =
- if is_representable n k then TInt(k, [])
- else raise Not_representable
- in
- let ty_l = mk l (Cil.intKindForValue l is_pos) in
- let ty_u = mk u (Cil.intKindForValue u is_pos) in
+ let ty_l = TInt(typ_of_integer l is_pos, []) in
+ let ty_u = TInt(typ_of_integer u is_pos, []) in
Cil.arithmeticConversion ty_l ty_u
- with
- | Not_found | Not_representable ->
+ with Not_representable ->
Mpz.t ())
| Z -> Mpz.t ()
| No_integral (Ctype ty) -> ty
@@ -99,7 +96,8 @@ let typ_of_eacsl_typ = function
TFloat(FLongDouble, [])
| No_integral (Larrow _) -> Error.not_yet "functional type"
-let eacsl_typ_of_typ ty = match Cil.unrollType ty with
+let eacsl_typ_of_typ ty =
+ match Cil.unrollType ty with
| TInt(k, _) as ty ->
let n = Cil.bitsSizeOf ty in
let l, u =
@@ -231,7 +229,9 @@ let clear () =
(******************************************************************************)
let type_constant ty = function
- | Integer(n, _) -> Interv(n, n)
+ | Integer(n, _) ->
+ if Cil.fitsInInt ILongLong n || Cil.fitsInInt IULongLong n then Interv(n, n)
+ else Z
| LChr c ->
(match Cil.charConstToInt c with
| CInt64(n, _, _) -> Interv(n, n)
--
GitLab