From cdb6381cbffe244c0fd50150d1cd2b1d92074eaf Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 25 Aug 2023 17:22:04 +0200
Subject: [PATCH] [e-acsl] Create an exception to replace Cil.Not_representable
---
src/plugins/e-acsl/src/analyses/interval.ml | 26 ++++++++++++--------
src/plugins/e-acsl/src/analyses/interval.mli | 7 +++++-
src/plugins/e-acsl/src/analyses/typing.ml | 2 +-
3 files changed, 23 insertions(+), 12 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index ee8622a2749..837572f1e6a 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -319,24 +319,30 @@ let interv_of_logic_typ = function
| Lvar _ -> Error.not_yet "type variable"
| Larrow _ -> Nan
+exception Not_representable_ival
let ikind_of_ival iv =
if Ival.is_bottom iv then IInt
else match Ival.min_and_max iv with
| Some l, Some u ->
- let is_pos = Integer.ge l Integer.zero in
- let lkind = Cil.intKindForValue l is_pos in
- let ukind = Cil.intKindForValue u is_pos in
- (* kind corresponding to the interval *)
- let kind = if Cil.intTypeIncluded lkind ukind then ukind else lkind in
- (* convert the kind to [IInt] whenever smaller. *)
- if Cil.intTypeIncluded kind IInt then IInt else kind
- | None, None -> raise Cil.Not_representable (* GMP *)
+ begin
+ try
+ let is_pos = Integer.ge l Integer.zero in
+ let lkind = Cil.intKindForValue l is_pos in
+ let ukind = Cil.intKindForValue u is_pos in
+ (* kind corresponding to the interval *)
+ let kind = if Cil.intTypeIncluded lkind ukind then ukind else lkind in
+ (* convert the kind to [IInt] whenever smaller. *)
+ if Cil.intTypeIncluded kind IInt then IInt else kind
+ with Cil.Not_representable ->
+ raise Not_representable_ival
+ end
+ | None, None -> raise Not_representable_ival (* GMP *)
(* TODO: do not raise an exception, but returns a value instead *)
| None, Some _ | Some _, None ->
(* Semi-open interval that can happen when computing the interval of shift
operations if the computation overflows *)
(* TODO: do not raise an exception, but returns a value instead *)
- raise Cil.Not_representable (* GMP *)
+ raise Not_representable_ival (* GMP *)
let interv_of_typ_containing_interv = function
@@ -346,7 +352,7 @@ let interv_of_typ_containing_interv = function
try
let kind = ikind_of_ival i in
interv_of_typ (TInt(kind, []))
- with Cil.Not_representable ->
+ with Not_representable_ival ->
top_ival
let widen_profile =
diff --git a/src/plugins/e-acsl/src/analyses/interval.mli b/src/plugins/e-acsl/src/analyses/interval.mli
index 5a53508c93c..30383357459 100644
--- a/src/plugins/e-acsl/src/analyses/interval.mli
+++ b/src/plugins/e-acsl/src/analyses/interval.mli
@@ -67,9 +67,14 @@ val is_singleton_int: t -> bool
(** assume [Ival _] as argument *)
val extract_ival: t -> Ival.t
+exception Not_representable_ival
+(** raised by {!ikind_of_ival].
+ @since Frama-C+dev
+*)
+
val ikind_of_ival: Ival.t -> Cil_types.ikind
(** @return the smallest ikind that contains the given interval.
- @raise Cil.Not_representable if the given interval does not fit into any C
+ @raise Not_representable_ival if the given interval does not fit into any C
integral type. *)
val interv_of_typ: Cil_types.typ -> t
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index b7158f15100..0df15a3e715 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -260,7 +260,7 @@ let ty_of_interv ?ctx ?(use_gmp_opt = false) = function
if Cil.intTypeIncluded kind ik then ctx else C_integer kind
| Some (C_float _ | Rational | Real as ty) ->
ty)
- with Cil.Not_representable ->
+ with Interval.Not_representable_ival ->
match ctx with
| None | Some(C_integer _ | Gmpz | Nan) -> Gmpz
| Some (C_float _ | Rational) -> Rational
--
GitLab