From 1cf3c003f8f48bc26fdf87545319e4e75d3498b4 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 1 Mar 2019 14:09:13 +0100
Subject: [PATCH] Interv.ikind_of_interv
---
src/plugins/e-acsl/interval.ml | 30 +++++++++++++++++++++++-------
src/plugins/e-acsl/interval.mli | 5 +++++
src/plugins/e-acsl/misc.ml | 13 -------------
src/plugins/e-acsl/misc.mli | 3 ---
src/plugins/e-acsl/typing.ml | 6 ++----
5 files changed, 30 insertions(+), 27 deletions(-)
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 7bd5aab9ec4..f2cea60613c 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -47,14 +47,29 @@ let rec interv_of_typ ty = match Cil.unrollType ty with
| _ ->
raise Not_an_integer
+let ikind_of_interv i =
+ if Ival.is_bottom i then IInt
+ else match Ival.min_and_max i 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 *)
+ | None, Some _ | Some _, None ->
+ Kernel.fatal ~current:true "ival: %a" Ival.pretty i
+
+(* TODO: why is it useful? Crash if not here, but why? *)
(* Return the interval over which ranges the smallest typ containing [i]. *)
let interv_of_typ_containing_interv i =
try
- let itv_kind = Misc.itv_kind i in
- (* convert the kind to [IInt] whenever smaller. *)
- let kind = if Cil.intTypeIncluded itv_kind IInt then IInt else itv_kind in
+ let kind = ikind_of_interv i in
interv_of_typ (TInt(kind, []))
with Cil.Not_representable ->
+ (* infinity *)
Ival.inject_range None None
let interv_of_unknown_block =
@@ -235,7 +250,8 @@ let rec infer t =
try
let i = interv_of_typ_containing_interv (infer arg) in
Env.add lv i
- with Not_an_integer -> ())
+ with Not_an_integer ->
+ ())
li.l_profile
_args;
let i =
@@ -341,10 +357,10 @@ and build_ieqs t ieqs ivars =
try
let i = interv_of_typ_containing_interv (infer arg) in
Env.add lv i;
- Ctype (TInt(Misc.itv_kind i, []))
+ Ctype (TInt(ikind_of_interv i, []))
with
- | Cil.Not_representable -> Linteger
- | Not_an_integer -> lv.lv_type)
+ | Cil.Not_representable -> Linteger
+ | Not_an_integer -> lv.lv_type)
li.l_profile
args
in
diff --git a/src/plugins/e-acsl/interval.mli b/src/plugins/e-acsl/interval.mli
index a900728f952..68313272fe2 100644
--- a/src/plugins/e-acsl/interval.mli
+++ b/src/plugins/e-acsl/interval.mli
@@ -52,6 +52,11 @@
exception Not_an_integer
+val ikind_of_interv: 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
+ integral type. *)
+
val interv_of_typ: Cil_types.typ -> Ival.t
(** @return the smallest interval which contains the given C type.
@raise Not_an_integer if the given type is not an integral type. *)
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 1d3e09cc8cc..efd0c173f59 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -356,19 +356,6 @@ let is_recursive li =
in
has_recursive_call t
-let itv_kind i =
- if Ival.is_bottom i then IInt
- else match Ival.min_and_max i 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 *)
- if Cil.intTypeIncluded lkind ukind then ukind else lkind
- | None, None -> raise Cil.Not_representable (* GMP *)
- | None, Some _ | Some _, None ->
- Kernel.fatal ~current:true "ival: %a" Ival.pretty i
-
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/misc.mli b/src/plugins/e-acsl/misc.mli
index e4806f0e157..b8270952d61 100644
--- a/src/plugins/e-acsl/misc.mli
+++ b/src/plugins/e-acsl/misc.mli
@@ -132,9 +132,6 @@ val fundec_of_kf: kernel_function -> fundec
val is_recursive: logic_info -> bool
(** [is_recursive li] returns true iff [li] is defined recursively. *)
-val itv_kind: Ival.t -> ikind
-(** Return the smallest iking that contains the given interval. *)
-
(*
Local Variables:
compile-command: "make"
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index f03b128958d..22799c4839d 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -198,15 +198,13 @@ let integer_ty_of_typ ty = ty_of_logic_ty (Ctype ty)
interval. It is the \theta operator of the JFLA's paper. *)
let ty_of_interv ?ctx i =
try
- let itv_kind = Misc.itv_kind i in
- (* convert the kind to [IInt] whenever smaller. *)
- let kind = if Cil.intTypeIncluded itv_kind IInt then IInt else itv_kind in
+ let kind = Interval.ikind_of_interv i in
(* ctx type whenever possible to prevent superfluous casts in the generated
code *)
(match ctx with
| None | Some (Gmp | Other) -> C_type kind
| Some (C_type ik as ctx) ->
- if Cil.intTypeIncluded itv_kind ik then ctx else C_type kind)
+ if Cil.intTypeIncluded kind ik then ctx else C_type kind)
with Cil.Not_representable ->
Gmp
--
GitLab