Merge branch 'fix/integer/gmp-overflow' into 'master'

Handling GMP overflow in `power_int_positive_int`

Closes #414

See merge request frama-c/frama-c!4464

src/libraries/stdlib/integer.ml

@@ -38,7 +38,9 @@ let two_power n =
   else
     two_power_of_int k
 
-let power_int_positive_int = Big_int_Z.power_int_positive_int
+let power_int_positive_int_opt n e =
+  try Some (Big_int_Z.power_int_positive_int n e)
+  with Invalid_argument _ -> None
 
 let popcount = Z.popcount
 

src/libraries/stdlib/integer.mli

@@ -203,7 +203,7 @@ val two_power : t -> t
 val two_power_of_int : int -> t
 (** Computes [2^n] *)
 
-val power_int_positive_int: int -> int -> t
+val power_int_positive_int_opt : int -> int -> t option
 (** Exponentiation *)
 
 val extract_bits : start:t -> stop:t -> t -> t

src/plugins/eva/engine/subdivided_evaluation.ml

@@ -767,10 +767,8 @@ module Make
                subvalues that are all evaluated. Limits the number of splits to
                keep the number of evaluations linear on [nb]. *)
             let subdivnb =
-              if nb > 3
-              then
-                let pow = Integer.power_int_positive_int in
-                (subdivnb * nb) / (Integer.to_int_exn (pow 2 (nb - 1)))
+              if 3 < nb && nb < 63
+              then (subdivnb * nb) / (1 lsl (nb - 1))
               else subdivnb
             in
             Self.result ~current:true ~once:true ~dkey