diff --git a/.Makefile.lint b/.Makefile.lint
index f213229e55714480b8766486a7538600f510672a..695336bd5d4b737229ee559472ea7aa6535cef08 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -194,8 +194,6 @@ ML_LINT_KO+=src/libraries/stdlib/FCSet.ml
ML_LINT_KO+=src/libraries/stdlib/FCSet.mli
ML_LINT_KO+=src/libraries/stdlib/extlib.ml
ML_LINT_KO+=src/libraries/stdlib/extlib.mli
-ML_LINT_KO+=src/libraries/stdlib/integer.ml
-ML_LINT_KO+=src/libraries/stdlib/integer.mli
ML_LINT_KO+=src/libraries/utils/bag.ml
ML_LINT_KO+=src/libraries/utils/binary_cache.ml
ML_LINT_KO+=src/libraries/utils/bitvector.ml
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/base.ml b/src/kernel_services/abstract_interp/base.ml
index 87254965dd6ab4feac9e7fcfffa6109a7ab4d2eb..b6b7af3832f22e69cd11f0c07c54bb41da7729cf 100644
--- a/src/kernel_services/abstract_interp/base.ml
+++ b/src/kernel_services/abstract_interp/base.ml
@@ -205,7 +205,8 @@ let () =
(mul_CHAR_BIT (Int.of_string min));
MaxValidAbsoluteAddress.set
((Int.pred (mul_CHAR_BIT (Int.succ (Int.of_string max))))))
- with End_of_file | Scanf.Scan_failure _ | Failure _ as e ->
+ with End_of_file | Scanf.Scan_failure _ | Failure _
+ | Invalid_argument _ as e ->
Kernel.abort "Invalid -absolute-valid-range integer-integer: each integer may be in decimal, hexadecimal (0x, 0X), octal (0o) or binary (0b) notation and has to hold in 64 bits. A correct example is -absolute-valid-range 1-0xFFFFFF0.@\nError was %S@."
(Printexc.to_string e))
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..3a629307b8ffa492fd77b66c90f64fc1020c51de 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5034,7 +5034,7 @@ and intOfAttrparam (a:attrparam) : int option =
let n = doit a in
ignoreAlignmentAttrs := false;
Some n
- with Failure _ | SizeOfError _ -> (* Can't compile *)
+ with Z.Overflow | SizeOfError _ -> (* Can't compile *)
ignoreAlignmentAttrs := false;
None
and process_aligned_attribute (pp:Format.formatter->unit) ~may_reduce attrs default_align =
@@ -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 1a7e593f79aede19b4ecddaf53d51964fa7020ce..e6ac8c03d7742176424a2b04d138482c6ffbc3e6 100644
--- a/src/libraries/stdlib/integer.ml
+++ b/src/libraries/stdlib/integer.ml
@@ -22,277 +22,264 @@
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
-
-let popcount = Z.popcount
+let two_power n =
+ let k = Z.to_int n in
+ if k > 1024 then
+ raise Z.Overflow
+ else
+ two_power_of_int k
- let zero = Z.zero
- let one = Z.one
- let minus_one = Z.minus_one
- let two = Z.of_int 2
- let four = Z.of_int 4
- let eight = Z.of_int 8
- let sixteen = Z.of_int 16
- let thirtytwo = Z.of_int 32
- let onethousand = Z.of_int 1000
- let billion_one = Z.of_int 1_000_000_001
- let two_power_32 = two_power_of_int 32
- let two_power_60 = two_power_of_int 60
- let two_power_64 = two_power_of_int 64
-
- let is_zero v = Z.equal v Z.zero
-
- let add = Z.add
- let sub = Z.sub
- let succ = Z.succ
- let pred = Z.pred
- let neg = Z.neg
-
- let rem = Z.erem
- let div = Z.ediv
- let mul = Z.mul
-
- let abs = Z.abs
-
- let hash = Z.hash
-
- 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"
- else Z.shift_right x (Z.to_int y)
-
- let logand = Z.logand
- let lognot = Z.lognot
- let logor = Z.logor
- let logxor = Z.logxor
-
- let le a b = Z.compare a b <= 0
- 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 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 *)
- "0001" ; (* 1 *)
- "0010" ; (* 2 *)
- "0011" ; (* 3 *)
- "0100" ; (* 4 *)
- "0101" ; (* 5 *)
- "0110" ; (* 6 *)
- "0111" ; (* 7 *)
- "1000" ; (* 8 *)
- "1001" ; (* 9 *)
- "1010" ; (* 10 *)
- "1011" ; (* 11 *)
- "1100" ; (* 12 *)
- "1101" ; (* 13 *)
- "1110" ; (* 14 *)
- "1111" ; (* 15 *)
- |]
-
- let pp_bin_pos fmt r = Format.pp_print_string fmt bdigits.(r)
- let pp_bin_neg fmt r = Format.pp_print_string fmt bdigits.(15-r)
-
- let pp_hex_pos fmt r = Format.fprintf fmt "%04X" r
- let pp_hex_neg fmt r = Format.fprintf fmt "%04X" (0xFFFF-r)
-
- let bmask_bin = Z.of_int 0xF (* 4 bits mask *)
- let bmask_hex = Z.of_int 0xFFFF (* 64 bits mask *)
-
- type digits = {
- nbits : int ; (* max number of bits *)
- bsize : int ; (* bits in each bloc *)
- bmask : Z.t ; (* block mask, must be (1 << bsize) - 1 *)
- sep : string ;
- pp : Format.formatter -> int -> unit ; (* print one block *)
- }
-
- let rec pp_digits d fmt n v =
- if gt v zero || n < d.nbits then
- begin
- let r = Z.to_int (Z.logand v d.bmask) in
- let k = d.bsize in
- pp_digits d fmt (n + k) (Z.shift_right_trunc v k) ;
- if gt v d.bmask || (n + k) < d.nbits
- then Format.pp_print_string fmt d.sep ;
- d.pp fmt r ;
- end
-
- let pp_bin ?(nbits=1) ?(sep="") fmt v =
- let nbits = if nbits <= 0 then 1 else nbits in
- if le zero v then
- ( Format.pp_print_string fmt "0b" ;
- pp_digits { nbits ; sep ; bsize=4 ;
- bmask = bmask_bin ; pp = pp_bin_pos } fmt 0 v )
- else
- ( Format.pp_print_string fmt "1b" ;
- pp_digits { nbits ; sep ; bsize=4 ;
- bmask = bmask_bin ; pp = pp_bin_neg } fmt 0 (Z.lognot v) )
+let power_int_positive_int = Big_int_Z.power_int_positive_int
- let pp_hex ?(nbits=1) ?(sep="") fmt v =
- let nbits = if nbits <= 0 then 1 else nbits in
- if le zero v then
- ( Format.pp_print_string fmt "0x" ;
- pp_digits { nbits ; sep ; bsize=16 ;
- bmask = bmask_hex ; pp = pp_hex_pos } fmt 0 v )
+let popcount = Z.popcount
+let zero = Z.zero
+let one = Z.one
+let minus_one = Z.minus_one
+let two = Z.of_int 2
+let four = Z.of_int 4
+let eight = Z.of_int 8
+let sixteen = Z.of_int 16
+let thirtytwo = Z.of_int 32
+let onethousand = Z.of_int 1000
+let billion_one = Z.of_int 1_000_000_001
+let two_power_32 = two_power_of_int 32
+let two_power_60 = two_power_of_int 60
+let two_power_64 = two_power_of_int 64
+
+let is_zero v = Z.equal v Z.zero
+
+let add = Z.add
+let sub = Z.sub
+let succ = Z.succ
+let pred = Z.pred
+let neg = Z.neg
+
+let rem = Z.erem
+let div = Z.ediv
+let mul = Z.mul
+
+let abs = Z.abs
+
+let hash = Z.hash
+
+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 raise (Invalid_argument "Integer.shift_right_logical")
+ else Z.shift_right x (Z.to_int y)
+
+let logand = Z.logand
+let lognot = Z.lognot
+let logor = Z.logor
+let logxor = Z.logxor
+
+let le a b = Z.compare a b <= 0
+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
+
+let to_int = Z.to_int
+let to_int64 = Z.to_int64
+let to_int32 = Z.to_int32
+
+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 bdigits = [|
+ "0000" ; (* 0 *)
+ "0001" ; (* 1 *)
+ "0010" ; (* 2 *)
+ "0011" ; (* 3 *)
+ "0100" ; (* 4 *)
+ "0101" ; (* 5 *)
+ "0110" ; (* 6 *)
+ "0111" ; (* 7 *)
+ "1000" ; (* 8 *)
+ "1001" ; (* 9 *)
+ "1010" ; (* 10 *)
+ "1011" ; (* 11 *)
+ "1100" ; (* 12 *)
+ "1101" ; (* 13 *)
+ "1110" ; (* 14 *)
+ "1111" ; (* 15 *)
+|]
+
+let pp_bin_pos fmt r = Format.pp_print_string fmt bdigits.(r)
+let pp_bin_neg fmt r = Format.pp_print_string fmt bdigits.(15-r)
+
+let pp_hex_pos fmt r = Format.fprintf fmt "%04X" r
+let pp_hex_neg fmt r = Format.fprintf fmt "%04X" (0xFFFF-r)
+
+let bmask_bin = Z.of_int 0xF (* 4 bits mask *)
+let bmask_hex = Z.of_int 0xFFFF (* 64 bits mask *)
+
+type digits = {
+ nbits : int ; (* max number of bits *)
+ bsize : int ; (* bits in each bloc *)
+ bmask : Z.t ; (* block mask, must be (1 << bsize) - 1 *)
+ sep : string ;
+ pp : Format.formatter -> int -> unit ; (* print one block *)
+}
+
+let rec pp_digits d fmt n v =
+ if gt v zero || n < d.nbits then
+ begin
+ let r = Z.to_int (Z.logand v d.bmask) in
+ let k = d.bsize in
+ pp_digits d fmt (n + k) (Z.shift_right_trunc v k) ;
+ if gt v d.bmask || (n + k) < d.nbits
+ then Format.pp_print_string fmt d.sep ;
+ d.pp fmt r ;
+ end
+
+let pp_bin ?(nbits=1) ?(sep="") fmt v =
+ let nbits = if nbits <= 0 then 1 else nbits in
+ if le zero v then
+ ( Format.pp_print_string fmt "0b" ;
+ pp_digits { nbits ; sep ; bsize=4 ;
+ bmask = bmask_bin ; pp = pp_bin_pos } fmt 0 v )
+ else
+ ( Format.pp_print_string fmt "1b" ;
+ pp_digits { nbits ; sep ; bsize=4 ;
+ bmask = bmask_bin ; pp = pp_bin_neg } fmt 0 (Z.lognot v) )
+
+let pp_hex ?(nbits=1) ?(sep="") fmt v =
+ let nbits = if nbits <= 0 then 1 else nbits in
+ if le zero v then
+ ( Format.pp_print_string fmt "0x" ;
+ pp_digits { nbits ; sep ; bsize=16 ;
+ bmask = bmask_hex ; pp = pp_hex_pos } fmt 0 v )
+
+ else
+ ( 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
+ let quo, rem = Z.ediv_rem v two_power_60 in
+ aux quo;
+ Format.fprintf fmt "%015LX" (to_int64 rem)
else
- ( 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
- let quo, rem = Z.ediv_rem v two_power_60 in
- aux quo;
- Format.fprintf fmt "%015LX" (to_int64 rem)
- else
- Format.fprintf fmt "%LX" (to_int64 v)
- in
- if hexa then
- if equal v zero then Format.pp_print_string fmt "0"
- else if gt v zero then (Format.pp_print_string fmt "0x"; aux v)
- else (Format.pp_print_string fmt "-0x"; aux (Z.neg v))
- else
- Format.pp_print_string fmt (to_string v)
-
- let is_one v = equal one v
- 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))
- then
- if lt v zero
- then pred bad_div
- else succ bad_div
- else bad_div
-
- let _c_div u v =
- let res = _c_div u v in
- let res2 = Z.div u v in
- if not (equal res res2) then
- failwith (Printf.sprintf "division of %a %a c_div %a div %a"
- Z.sprint u
- Z.sprint 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))
-
- let _c_rem u v =
- let res = _c_rem u v in
- let res2 = Z.rem u v in
- if not (equal res res2) then
- failwith (Printf.sprintf "division of %a %a c_rem %a rem %a"
- Z.sprint u
- Z.sprint v
- Z.sprint res
- Z.sprint res2)
- else res2
-
- let c_rem = Z.rem
-
- let cast ~size ~signed ~value =
- if (not signed)
- then
- let factor = two_power size in logand value (pred factor)
+ Format.fprintf fmt "%LX" (to_int64 v)
+ in
+ if hexa then
+ if equal v zero then Format.pp_print_string fmt "0"
+ else if gt v zero then (Format.pp_print_string fmt "0x"; aux v)
+ else (Format.pp_print_string fmt "-0x"; aux (Z.neg v))
+ else
+ Format.pp_print_string fmt (to_string v)
+
+let is_one v = equal one v
+
+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))
+ then
+ if lt v zero
+ then pred bad_div
+ else succ bad_div
+ else bad_div
+
+let _c_div u v =
+ let res = _c_div u v in
+ let res2 = Z.div u v in
+ if not (equal res res2) then
+ failwith (Printf.sprintf "division of %a %a c_div %a div %a"
+ Z.sprint u
+ Z.sprint 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))
+
+let _c_rem u v =
+ let res = _c_rem u v in
+ let res2 = Z.rem u v in
+ if not (equal res res2) then
+ failwith (Printf.sprintf "division of %a %a c_rem %a rem %a"
+ Z.sprint u
+ Z.sprint v
+ Z.sprint res
+ Z.sprint res2)
+ else res2
+*)
+
+let c_rem = Z.rem
+
+let cast ~size ~signed ~value =
+ if (not signed)
+ then
+ let factor = two_power size in logand value (pred factor)
+ else
+ let mask = two_power (sub size one) in
+ let p_mask = pred mask in
+ if equal (logand mask value) zero
+ then logand value p_mask
else
- let mask = two_power (sub size one) in
- let p_mask = pred mask in
- if equal (logand mask value) zero
- then logand value p_mask
- else
- logor (lognot p_mask) value
-
- let length u v = succ (sub v u)
+ logor (lognot p_mask) value
- let extract_bits ~start ~stop v =
- assert (ge start zero && ge stop start);
- (*Format.printf "%a[%a..%a]@\n" pretty v pretty start pretty stop;*)
- let r = Z.extract v (to_int start) (to_int (length start stop)) in
- (*Format.printf "%a[%a..%a]=%a@\n" pretty v pretty start pretty stop pretty r;*)
- r
+let length u v = succ (sub v u)
- let is_even v = is_zero (logand one v)
+let extract_bits ~start ~stop v =
+ assert (ge start zero && ge stop start);
+ (*Format.printf "%a[%a..%a]@\n" pretty v pretty start pretty stop;*)
+ let r = Z.extract v (to_int start) (to_int (length start stop)) in
+ (*Format.printf "%a[%a..%a]=%a@\n" pretty v pretty start pretty stop pretty r;*)
+ r
- let pgcd u v =
- if is_zero v then abs u (* Zarith raises an exception on zero arguments *)
- else if is_zero u then abs v
- else Z.gcd u v
+let is_even v = is_zero (logand one v)
- let ppcm u v =
- if u = zero || v = zero
- then zero
- else Z.lcm u v
+let pgcd u v =
+ if is_zero v then abs u (* Zarith raises an exception on zero arguments *)
+ else if is_zero u then abs v
+ else Z.gcd u v
- let min = Z.min
- let max = Z.max
+let ppcm u v =
+ if u = zero || v = zero
+ then zero
+ else Z.lcm u v
- let round_down_to_zero v modu =
- mul (pos_div v modu) modu
+let min = Z.min
+let max = Z.max
- let round_up_to_r ~min:m ~r ~modu =
- add (add (round_down_to_zero (pred (sub m r)) modu) r) modu
+let round_down_to_zero v modu =
+ mul (pos_div v modu) modu
- let round_down_to_r ~max:m ~r ~modu =
- add (round_down_to_zero (sub m r) modu) r
+let round_up_to_r ~min:m ~r ~modu =
+ add (add (round_down_to_zero (pred (sub m r)) modu) r) modu
- let power_int_positive_int = Big_int_Z.power_int_positive_int
+let round_down_to_r ~max:m ~r ~modu =
+ add (round_down_to_zero (sub m r) modu) r
diff --git a/src/libraries/stdlib/integer.mli b/src/libraries/stdlib/integer.mli
index 3ed0f1297471b8c393056437955eec4085c79363..1e8202750a985b5318dcfb11f1cb0c12286c17c9 100644
--- a/src/libraries/stdlib/integer.mli
+++ b/src/libraries/stdlib/integer.mli
@@ -20,14 +20,11 @@
(* *)
(**************************************************************************)
-(** Extension of [Big_int] compatible with [Zarith].
+(** Extension of [Big_int] compatible with [Zarith].
@since Nitrogen-20111001 *)
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]. *)
+(** Computes [2^n]
+ @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. *)
+(** Computes [2^n] *)
-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
@@ -154,16 +160,16 @@ val pp_bin : ?nbits:int -> ?sep:string -> t Pretty_utils.formatter
(** Print binary format. Digits are output by blocs of 4 bits
separated by [~sep] with at least [~nbits] total bits. If [nbits] is
non positive, it will be ignored.
-
- Positive values are prefixed with ["0b"] and negative values
+
+ Positive values are prefixed with ["0b"] and negative values
are printed as their 2-complement ([lnot]) with prefix ["1b"]. *)
val pp_hex : ?nbits:int -> ?sep:string -> t Pretty_utils.formatter
-(** Print hexadecimal format. Digits are output by blocs of 16 bits
- (4 hex digits) separated by [~sep] with at least [~nbits] total bits.
+(** Print hexadecimal format. Digits are output by blocs of 16 bits
+ (4 hex digits) separated by [~sep] with at least [~nbits] total bits.
If [nbits] is non positive, it will be ignored.
-
- Positive values are preffixed with ["0x"] and negative values
+
+ Positive values are preffixed with ["0x"] and negative values
are printed as their 2-complement ([lnot]) with prefix ["1x"]. *)
(*
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 a4c3d080764c24e54f4eb4e71a9e4981d951774a..02c88290a4e5bf52db262ee8661d51cce8d337a2 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -609,7 +609,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/Plang.ml b/src/plugins/wp/Plang.ml
index 31634612ec9a6dca92caa640ee584610be91b209..bc6277756c078987be36f7cf5b8b7946d6d57aed 100644
--- a/src/plugins/wp/Plang.ml
+++ b/src/plugins/wp/Plang.ml
@@ -109,8 +109,8 @@ class engine =
if -256 <= n && n <= 256 then
Format.pp_print_int fmt n
else
- raise Integer.Too_big
- with Integer.Too_big ->
+ raise Z.Overflow
+ with Z.Overflow ->
match iformat with
| `Dec -> Integer.pretty ~hexa:false fmt z
| `Hex -> Integer.pp_hex ~sep:"," fmt z
diff --git a/src/plugins/wp/TacShift.ml b/src/plugins/wp/TacShift.ml
index 3da39d9bc4894348efa696e89c69ffc11a0fe336..fff37a69094cfad98a268ab90100b7834634d576 100644
--- a/src/plugins/wp/TacShift.ml
+++ b/src/plugins/wp/TacShift.ml
@@ -45,7 +45,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/Tactical.ml b/src/plugins/wp/Tactical.ml
index 489b729091213327c6d50406a9c62ef78d40340e..8bfb88d4f40c115f861e642236f18c71dec6a6c4 100644
--- a/src/plugins/wp/Tactical.ml
+++ b/src/plugins/wp/Tactical.ml
@@ -107,7 +107,7 @@ let selected = function
| Compose code -> composed code
let get_int_z z =
- try Some (Integer.to_int z) with _ -> None
+ try Some (Integer.to_int z) with Z.Overflow -> None
let get_int = function
| Empty -> None
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