[Eva] Minor simplification to catch exceptions when reading loop unroll limits.

src/plugins/value/partitioning/partitioning_parameters.ml

@@ -93,22 +93,13 @@ struct
         let t =
           Cil.visitCilTerm (new Logic_utils.simplify_const_lval global_init) t
         in
-        match Logic_utils.constFoldTermToInt t with
-        | Some n ->
-          begin
-            match Integer.to_int_opt n with
-            | Some n' -> Partition.IntLimit n'
-            | None ->
-              warn "invalid loop unrolling parameter (%a); ignoring"
-                (Integer.pretty ~hexa:false) n;
-              default
-          end
-        | None   ->
-          try Partition.ExpLimit (term_to_exp t)
-          with Db.Properties.Interp.No_conversion ->
-            warn "loop unrolling parameters must be valid expressions; \
-                  ignoring";
-            default
+        try
+          match Logic_utils.constFoldTermToInt t with
+          | Some n -> Partition.IntLimit (Integer.to_int_exn n)
+          | None   -> Partition.ExpLimit (term_to_exp t)
+        with Z.Overflow | Db.Properties.Interp.No_conversion ->
+          warn "invalid loop unrolling parameter; ignoring";
+          default
       end
     | _ ->
       warn "invalid unroll annotation; ignoring";

tests/syntax/oracle/very_large_integers.11.res.oracle

@@ -10,6 +10,6 @@
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
 [kernel:annot-error] tests/syntax/very_large_integers.c:92: Warning: 
-  invalid loop unrolling parameter (-9999999999999999999); ignoring
+  invalid loop unrolling parameter; ignoring
 [kernel] User Error: warning annot-error treated as fatal error.
 [kernel] Frama-C aborted: invalid user input.