diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml index 83bd2e974ce67d51d82abe711bfecbf41b6ef443..4ddcf1835217ca9caa6cdfdd8bd8c3f28c1979ce 100644 --- a/src/plugins/value/partitioning/partitioning_parameters.ml +++ b/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"; diff --git a/tests/syntax/oracle/very_large_integers.11.res.oracle b/tests/syntax/oracle/very_large_integers.11.res.oracle index f34db553ef8c687e47299e28108dd501d96c45ca..fca174f9e7043bb9e87dee4ab0b78776cc93d95f 100644 --- a/tests/syntax/oracle/very_large_integers.11.res.oracle +++ b/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.