Commit 1cf3c003 authored by Julien Signoles's avatar Julien Signoles
Browse files

Interv.ikind_of_interv

parent aadd2bd8
......@@ -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
......
......@@ -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. *)
......
......@@ -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"
......
......@@ -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"
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment