diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 984fef51c452bc6ffd8b2cab48b3e9c352650d11..00315ab1904b8f67d1cc066f48233f9f5bc195d6 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5365,7 +5365,7 @@ and isIntegerConstant ghost (aexp) : int option =
match doExp (ghost_local_env ghost) true aexp (AExp None) with
| (_, c, e, _) when isEmpty c -> begin
match Cil.constFoldToInt e with
- | Some i64 -> Some (Integer.to_int i64)
+ | Some n -> (try Some (Integer.to_int n) with Z.Overflow -> None)
| _ -> None
end
| _ -> None
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index ce2e6ad7ca77b84a1848fc74c0a9dcb318db2f4a..980c2865415f3b632d64086395f4ec2dab469bdb 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -1988,7 +1988,7 @@ let shift_aux scale op (x: t) (y: t) =
let modu = match min_factor with None -> Int.one | Some m -> m in
let factor = inject_top min_factor max_factor Int.zero modu in
op x factor
- with Integer.Too_big ->
+ with Z.Overflow ->
Lattice_messages.emit_imprecision emitter "Ival.shift_aux";
(* We only preserve the sign of the result *)
if is_included x positive_integers then positive_integers
@@ -2199,7 +2199,7 @@ let rec extract_bits ~start ~stop ~size v =
try
let dived = scale_div ~pos:true (Int.two_power start) d in
scale_rem ~pos:true (Int.two_power (Int.length start stop)) dived
- with Integer.Too_big ->
+ with Z.Overflow ->
Lattice_messages.emit_imprecision emitter "Ival.extract_bits";
top
;;
@@ -2428,7 +2428,7 @@ let cast_int_to_float_inverse_not_nan ~single_precision (min, max) =
values on each extremity. *)
let min = ceil min in
let max = floor max in
- let conv f = try Some (Integer.of_float f) with Integer.Too_big -> None in
+ let conv f = try Some (Integer.of_float f) with Z.Overflow -> None in
let r = inject_range (conv min) (conv max) in
(* Kernel.result "Cast I->F inv: %a -> %a@." pretty f pretty r; *)
r
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 86eb84205298d80638abceaf63fc096dda62aa85..2d351e35a444bbc673d3bd549ab28542c0b138df 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5309,7 +5309,7 @@ and offsetOfFieldAcc_GCC last (fi: fieldinfo) (sofar: offsetAcc) : offsetAcc =
let sz' =
try
Integer.to_int sz
- with Failure _ ->
+ with Z.Overflow ->
raise
(SizeOfError
("Array is so long that its size can't be "
diff --git a/src/libraries/stdlib/integer.ml b/src/libraries/stdlib/integer.ml
index b8edece5d016039761a7aa1f758b1fb7639b801b..00fe1fc795db028fb338b6c9092da825236eccc3 100644
--- a/src/libraries/stdlib/integer.ml
+++ b/src/libraries/stdlib/integer.ml
@@ -22,25 +22,17 @@
type t = Z.t
-exception Too_big
-
let equal = Z.equal
let compare = Z.compare
-
let two_power_of_int k =
- Z.shift_left Z.one k
-
-let two_power y =
- try
- let k = Z.to_int y in
- if k > 1024 then
- (* avoid memory explosion *)
- raise Too_big
- else
- two_power_of_int k
- with Z.Overflow -> raise Too_big
+ if k > 1024 then
+ raise Z.Overflow
+ else
+ Z.shift_left Z.one k
+
+let two_power n = two_power_of_int (Z.to_int n)
let popcount = Z.popcount
@@ -78,7 +70,7 @@ let shift_left x y = Z.shift_left x (Z.to_int y)
let shift_right x y = Z.shift_right x (Z.to_int y)
let shift_right_logical x y = (* no meaning for negative value of x *)
if (Z.lt x Z.zero)
- then failwith "log_shift_right_big_int"
+ then raise (Invalid_argument "Integer.shift_right_logical")
else Z.shift_right x (Z.to_int y)
let logand = Z.logand
@@ -91,32 +83,22 @@ let ge a b = Z.compare a b >= 0
let lt a b = Z.compare a b < 0
let gt a b = Z.compare a b > 0
-
let of_int = Z.of_int
-
let of_int64 = Z.of_int64
let of_int32 = Z.of_int32
-(* Return the same exceptions as [Big_int] *)
let to_int = Big_int_Z.int_of_big_int
let to_int64 = Big_int_Z.int64_of_big_int
let to_int32 = Big_int_Z.int32_of_big_int
-let of_string s =
- try Z.of_string s
- with Invalid_argument _ ->
- (* We intentionally do NOT specify a string in the .mli, as Big_int
- raises multiple [Failure _] exceptions *)
- failwith "Integer.of_string"
+let of_string = Z.of_string
+let to_string = Z.to_string
+let of_float = Z.of_float
+let to_float = Z.to_float
let max_int64 = of_int64 Int64.max_int
let min_int64 = of_int64 Int64.min_int
-let to_string = Z.to_string
-let to_float = Z.to_float
-let of_float z =
- try Z.of_float z
- with Z.Overflow -> raise Too_big
let bdigits = [|
"0000" ; (* 0 *)
@@ -187,7 +169,6 @@ let pp_hex ?(nbits=1) ?(sep="") fmt v =
( Format.pp_print_string fmt "1x" ;
pp_digits { nbits ; sep ; bsize=16 ;
bmask = bmask_hex ; pp = pp_hex_neg } fmt 0 (Z.lognot v) )
-
let pretty ?(hexa=false) fmt v =
let rec aux v =
if gt v two_power_60 then
@@ -205,13 +186,14 @@ let pretty ?(hexa=false) fmt v =
Format.pp_print_string fmt (to_string v)
let is_one v = equal one v
-let pos_div = div
+let pos_div = div
let pos_rem = rem
let native_div = div
let divexact = Z.divexact
let div_rem = Z.div_rem
+(*
let _c_div u v =
let bad_div = div u v in
if (lt u zero) && not (is_zero (rem u v))
@@ -231,9 +213,11 @@ let _c_div u v =
Z.sprint res
Z.sprint res2)
else res2
+*)
let c_div = Z.div
+(*
let _c_rem u v =
sub u (mul v (c_div u v))
@@ -247,6 +231,7 @@ let _c_rem u v =
Z.sprint res
Z.sprint res2)
else res2
+*)
let c_rem = Z.rem
diff --git a/src/libraries/stdlib/integer.mli b/src/libraries/stdlib/integer.mli
index e57173cb7e648e071a59028e5e1d98af5d8d0a1c..3b9e69a8fd2b8859c975bb1002f90555d643304c 100644
--- a/src/libraries/stdlib/integer.mli
+++ b/src/libraries/stdlib/integer.mli
@@ -25,9 +25,6 @@
type t = Z.t
-exception Too_big (** Produced by values whose physical representation is too
- costly (e.g. in terms of memory usage). *)
-
val equal : t -> t -> bool
val compare : t -> t -> int
@@ -41,8 +38,14 @@ val sub : t -> t -> t
val mul : t -> t -> t
val shift_left : t -> t -> t
+(** @raise Invalid_argument if second argument (count) is negative *)
+
val shift_right : t -> t -> t
+(** @raise Invalid_argument if second argument (count) is negative *)
+
val shift_right_logical : t -> t -> t
+(** @raise Invalid_argument if any argument is negative *)
+
val logand : t -> t -> t
val logor : t -> t -> t
val logxor : t -> t -> t
@@ -52,24 +55,31 @@ val min : t -> t -> t
val max : t -> t -> t
val native_div : t -> t -> t
+
val div : t -> t -> t
(** Euclidean division (that returns a positive rem) *)
+
val pos_div : t -> t -> t
(** Euclidean division. Equivalent to C division if both operands are positive.
Equivalent to a floored division if b > 0 (rounds downwards),
otherwise rounds upwards.
Note: it is possible that pos_div (-a) b <> pos_div a (-b). *)
+
val divexact: t -> t -> t
(** Faster, but produces correct results only when b evenly divides a. *)
+
val c_div : t -> t -> t
(** Truncated division towards 0 (like in C99) *)
val rem : t -> t -> t
(** Remainder of the Euclidean division (always positive) *)
+
val c_rem : t -> t -> t
(** Remainder of the truncated division towards 0 (like in C99) *)
+
val div_rem: t -> t -> (t * t)
(** [div_rem a b] returns [(pos_div a b, pos_rem a b)] *)
+
val pos_rem : t -> t -> t
(** Remainder of the Euclidean division (always positive) *)
@@ -79,9 +89,6 @@ val pgcd : t -> t -> t
val ppcm : t -> t -> t
(** [ppcm v 0 == ppcm 0 v == 0]. Result is always positive *)
-val power_int_positive_int: int -> int -> t
-(** Exponentiation *)
-
val cast: size:t -> signed:bool -> value:t -> t
val abs : t -> t
@@ -113,16 +120,13 @@ val length : t -> t -> t (** b - a + 1 *)
val of_int : int -> t
val of_int64 : Int64.t -> t
val of_int32 : Int32.t -> t
-val to_int64 : t -> int64
-val to_int32 : t -> int32
-val to_int : t -> int
-(** @raise Failure if the argument does not fit in an OCaml int *)
+val to_int : t -> int (** @raise Z.Overflow if too big *)
+val to_int64 : t -> int64 (** @raise Z.Overflow if too big *)
+val to_int32 : t -> int32 (** @raise Z.Overflow if too big *)
val to_float : t -> float
val of_float : float -> t
-(** Converts from a floating-point value. The value is truncated.
- Raises [Overflow] on infinity and NaN arguments. *)
val round_up_to_r : min:t -> r:t -> modu:t -> t
(** [round_up_to_r m r modu] is the smallest number [n] such that
@@ -133,20 +137,22 @@ val round_down_to_r : max:t -> r:t -> modu:t -> t
[n]<=[m] and [n] = [r] modulo [modu] *)
val two_power : t -> t
-(** [two_power x] computes 2^x. Can raise [Too_big]. *)
+(** [two_power x] computes 2^x.
+ @raise Z.Overflow for exponents greater than 1024 *)
+
val two_power_of_int : int -> t
(** Similar to [two_power x], but x is an OCaml int. *)
-val extract_bits : start:t -> stop:t -> t -> t
+val power_int_positive_int: int -> int -> t
+(** Exponentiation *)
+val extract_bits : start:t -> stop:t -> t -> t
+val popcount: t -> int
val hash : t -> int
-val of_string : string -> t
-(** @raise Failure _ when the string cannot be parsed. *)
-
val to_string : t -> string
-
-val popcount: t -> int
+val of_string : string -> t
+(** @raise Invalid_argument when the string cannot be parsed. *)
val pretty : ?hexa:bool -> t Pretty_utils.formatter
diff --git a/src/plugins/loop_analysis/loop_analysis.ml b/src/plugins/loop_analysis/loop_analysis.ml
index de7974e693b2dbf55feef29cd5271fc1bdbc12a7..9236b5240a4b5f0a8a1029e54a193344ec8c860a 100644
--- a/src/plugins/loop_analysis/loop_analysis.ml
+++ b/src/plugins/loop_analysis/loop_analysis.ml
@@ -462,7 +462,7 @@ module Store(* (B:sig *)
success := true;
add_loop_bound stmt adjusted_value
end
- with Failure _ -> (* overflow in Integer.to_int *)
+ with Z.Overflow -> (* overflow in Integer.to_int *)
()
(* TODO: check if this is useful and does not cause false alarms
else
diff --git a/src/plugins/loop_analysis/slevel_analysis.ml b/src/plugins/loop_analysis/slevel_analysis.ml
index 26625cfa02de3c3ccd0c17a96f764ab233db90f1..898570e199963d3bf2c370398828f262c43aeb63 100644
--- a/src/plugins/loop_analysis/slevel_analysis.ml
+++ b/src/plugins/loop_analysis/slevel_analysis.ml
@@ -123,9 +123,9 @@ module Specific(KF:sig val kf: Kernel_function.t end) = struct
then Some result
else raise Exit
with
- | Invalid_argument _ (* Possible exponent too big *)
- | Failure _ (* Integer too big *)
- | Exit -> (* Above MaxIterations. *)
+ | Invalid_argument _ (* Possible negative exponent *)
+ | Z.Overflow (* Integer too big *)
+ | Exit -> (* Above MaxIterations. *)
update_max_slevel_encountered
(Some (Integer.mul entry (Integer.mul in_loop
(Integer.of_int max_iteration))));
@@ -197,8 +197,7 @@ module SpecificNoBranches(KF:sig val kf: Kernel_function.t end) = struct
Some Integer.(pred (mul (succ (of_int in_loop_i))
(of_int max_iteration)))
with
- | Invalid_argument _ (* Possible exponent too big *)
- | Failure _ (* Integer too big *)
+ | Z.Overflow (* Integer too big *)
-> update_max_slevel_encountered
(Some (Integer.mul entry (Integer.mul in_loop
(Integer.of_int max_iteration))));
diff --git a/src/plugins/value/domains/apron/apron_domain.ok.ml b/src/plugins/value/domains/apron/apron_domain.ok.ml
index 6c7817dff14e3c75d297c337029daa911d0d6d9a..27aa29d81c1fb68e1a7fccaddc91b732dd74962b 100644
--- a/src/plugins/value/domains/apron/apron_domain.ok.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ok.ml
@@ -252,7 +252,7 @@ let translate_lval = function
let translate_constant = function
| CInt64 (i, _, _) -> begin
try Coeff.s_of_int (Integer.to_int i) (* TODO: skip OCaml int type *)
- with Failure _ -> raise (Out_of_Scope "translate_constant big int")
+ with Z.Overflow | Failure _ -> raise (Out_of_Scope "translate_constant big int")
end
| _ -> raise (Out_of_Scope "translate_constant not integer")
@@ -501,7 +501,7 @@ module Make
(* May happen when evaluating an expression in the GUI, while the states
of Apron have not been saved. In this case, we evaluate in the top
apron state, whose environment raises the Failure exception. *)
- | Failure _ -> top
+ | Z.Overflow | Failure _ -> top
let extract_expr _oracle state expr =
compute state expr (Cil.typeOf expr)
diff --git a/src/plugins/value/domains/cvalue/builtins_print_c.ml b/src/plugins/value/domains/cvalue/builtins_print_c.ml
index f32792786051a017156a912f62ad8b92542688bb..dc13b3c198bf1d6b72b6453abdbce44a0801fb10 100644
--- a/src/plugins/value/domains/cvalue/builtins_print_c.ml
+++ b/src/plugins/value/domains/cvalue/builtins_print_c.ml
@@ -280,7 +280,7 @@ let state_pretty cas fmt m =
begin
try offsetmap_pretty cas name print_ampamp fmt offs
with
- | Failure _
+ | Z.Overflow
| Too_large_to_enumerate ->
Value_parameters.warning "base %s too large, \
will not print it" name
diff --git a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
index fbebe367bbff602be7ae2806f782669b01358ff8..c8a2c01c80691c941addde50bee86e9388863795 100644
--- a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
+++ b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
@@ -89,7 +89,7 @@ let make_watch_cardinal target_value =
let target_value = Cvalue.V.project_ival target_value in
Cardinal (Integer.to_int (Ival.project_int target_value))
with V.Not_based_on_null | Ival.Not_Singleton_Int
- | Failure _ (* from Integer.to_int *) ->
+ | Z.Overflow (* from Integer.to_int *) ->
raise Db.Value.Outside_builtin_possibilities
let () =
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ok.ml b/src/plugins/value/domains/numerors/numerors_domain.ok.ml
index daf171d6528b56b29e439ba2b843f0927a835d62..c385ee3a1f37c30e99efc18590ee2ddb462048fe 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ok.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ok.ml
@@ -110,7 +110,7 @@ let add_numerors_value (module Value: Abstract_value.Internal) =
Numerors_value.of_ints ~prec min max
| _, _ -> num
(* Integer.to_int may fail for too big integers. *)
- with Cvalue.V.Not_based_on_null | Failure _ -> num
+ with Cvalue.V.Not_based_on_null | Z.Overflow -> num
end
| _, _ -> num
in
diff --git a/src/plugins/value/slevel/split_strategy.ml b/src/plugins/value/slevel/split_strategy.ml
index cc8b20271d996dcc80bd9b6c414945a7abd545c3..9ab22e48e569688454dd2bb2a64bd81b07646e44 100644
--- a/src/plugins/value/slevel/split_strategy.ml
+++ b/src/plugins/value/slevel/split_strategy.ml
@@ -80,7 +80,7 @@ let of_string s =
let r = Str.regexp ":" in
let conv s =
try Integer.of_string s
- with Failure _ -> raise (ParseFailure s)
+ with Invalid_argument _ -> raise (ParseFailure s)
in SplitEqList (List.map conv (Str.split r s))
let to_string = function
diff --git a/src/plugins/value_types/cvalue.ml b/src/plugins/value_types/cvalue.ml
index 86e61503023a0e0a5a52bc0dff2daa06f7a2a4e4..0801bc27aeaae7fe35af12942c61d04ab113c446 100644
--- a/src/plugins/value_types/cvalue.ml
+++ b/src/plugins/value_types/cvalue.ml
@@ -635,7 +635,7 @@ module V = struct
if Integer.is_zero factor
then v
else topify_with_origin_kind topify v
- | Integer.Too_big -> top_int
+ | Z.Overflow -> top_int
let restrict_topint_to_size value size =
if is_topint value
diff --git a/src/plugins/wp/Auto.ml b/src/plugins/wp/Auto.ml
index c06565117dbefde36dc23a426b09aedadfb82cc5..86d62474d957176721e555f38477e58f3346b108 100644
--- a/src/plugins/wp/Auto.ml
+++ b/src/plugins/wp/Auto.ml
@@ -162,12 +162,12 @@ struct
Tmap.interf
(fun _ a b ->
try Some(Integer.to_int a,Integer.to_int b)
- with Integer.Too_big -> None
+ with Z.Overflow -> None
) rg.vmin rg.vmax
let small = function
| None -> None
- | Some z -> try Some(Integer.to_int z) with Integer.Too_big -> None
+ | Some z -> try Some(Integer.to_int z) with Z.Overflow -> None
let bounds rg =
Tmap.merge
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 763bd314ff3aafc55d210aeb6c95fdea123eadc3..462cf49b991556092fdc92911adfe197762e1061 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -621,7 +621,7 @@ let smp_eq_with_lnot a b = (* b1==~e <==> ~b1==e *)
let two_power_k_minus1 k =
try Integer.pred (Integer.two_power k)
- with Integer.Too_big -> raise Not_found
+ with Z.Overflow -> raise Not_found
let smp_eq_with_lsl_cst a0 b0 =
let b1 = match_integer b0 in
diff --git a/src/plugins/wp/Filtering.ml b/src/plugins/wp/Filtering.ml
index a74546d4d09099ff3e3c7f25d99d70cd631f4468..adf5bbd31779b2ab6a62b9f9f1ffcfd97ce8d63f 100644
--- a/src/plugins/wp/Filtering.ml
+++ b/src/plugins/wp/Filtering.ml
@@ -211,7 +211,7 @@ struct
begin match F.repr k with
| Kint z ->
let d =
- try Dindex(Integer.to_int z) with Integer.Too_big -> Darray in
+ try Dindex(Integer.to_int z) with Z.Overflow -> Darray in
X( x , ds @ [ d ] )
| _ ->
let ds = ds @ [ Darray ] in
diff --git a/src/plugins/wp/GuiComposer.ml b/src/plugins/wp/GuiComposer.ml
index a50bd4ab9ef0e62427554e46c1ee8b5f5fa82542..779d9f467f79b19a280785b206c5bd3f2bf9da1f 100644
--- a/src/plugins/wp/GuiComposer.ml
+++ b/src/plugins/wp/GuiComposer.ml
@@ -91,7 +91,7 @@ class composer (focused : GuiSequent.focused) =
method private get_int = function
| Tactical.Compose(Tactical.Cint z) ->
- (try Some (Integer.to_int z) with _ -> None)
+ (try Some (Integer.to_int z) with Z.Overflow -> None)
| _ -> None
method private op1 title job args fmt = match args with
diff --git a/src/plugins/wp/TacShift.ml b/src/plugins/wp/TacShift.ml
index 7f5cfe3bc98f8b18489027db420f373ebb2d11c3..f0ac610edabdee568aaba4a00ca715d89e63ea1f 100644
--- a/src/plugins/wp/TacShift.ml
+++ b/src/plugins/wp/TacShift.ml
@@ -47,7 +47,7 @@ let select_op f =
let select_int n =
match F.repr n with
| Qed.Logic.Kint n ->
- (try Integer.to_int n with Integer.Too_big -> raise Not_found)
+ (try Integer.to_int n with Z.Overflow -> raise Not_found)
| _ -> raise Not_found
class shift =
diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index 0f41386b7f696ae9ad8e59a6b8b908a7511ab2b0..40bdc019497d18bcfeca31652a95564ac9b475be 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/src/plugins/wp/Vlist.ml
@@ -160,7 +160,7 @@ and get_nth_list k = function
let rewrite_nth s k =
match F.repr k with
| L.Kint z ->
- let k = try Integer.to_int z with _ -> raise Not_found in
+ let k = try Integer.to_int z with Z.Overflow -> raise Not_found in
if 0 <= k then get_nth k s else raise Not_found
| _ -> raise Not_found