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/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index 2d351e35a444bbc673d3bd549ab28542c0b138df..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 =