diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index c6d918435e6e8611bc05d7d2cce51fe8d3d3b8ce..29eb29a9c9fcb99a545976c585da94eb1f912ddd 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5764,7 +5764,7 @@ and doExp local_env
| Cabs.CONST_FLOAT str -> begin
Floating_point.(set_rounding_mode Nearest_even) ;
- let Parsed (format, parsed) = Typed_float.parse str in
+ let Parsed (format, parsed) = Typed_float.parse_exn str in
let nearest_float = Typed_float.to_float parsed.nearest in
if Typed_float.(parsed.lower <> parsed.upper) then
Kernel.warning ~wkey:Kernel.wkey_decimal_float ~current:true
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 9da2b79b105a49f146894f5b6218f7c46d847cd8..f652344a316ef66245991c1b7f5299b0d7c23d2e 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -314,7 +314,7 @@ let parse_float ?loc literal =
let len = String.length literal in
let last = Char.uppercase_ascii literal.[len-1] in
let is_nearest_exact = last = 'F' || last = 'D' in
- let Parsed (format, p) = Typed_float.parse literal in
+ let Parsed (format, p) = Typed_float.parse_exn literal in
let nearest = Typed_float.(to_float p.nearest) in
let fkind = Typed_float.parsed_fkind format in
let creal =
diff --git a/src/libraries/floating_point/typed_float.ml b/src/libraries/floating_point/typed_float.ml
index 61bd9c7e580e2b79bb53c67c22c80a52da839771..9648d2ea1fb86a51aa58758c54c1347fb86454bd 100644
--- a/src/libraries/floating_point/typed_float.ml
+++ b/src/libraries/floating_point/typed_float.ml
@@ -403,15 +403,15 @@ let pretty_format fmt (Format (supported, format)) =
| Long_unsupported, Double -> Format.fprintf fmt "long double precision"
let cannot_be_parsed string format =
- Kernel.abort ~current:true
- "The string %s cannot be parsed as a %a floating-point constant"
- string pretty_format format
+ let msg =
+ Format.asprintf
+ "The string %s cannot be parsed as a %a floating-point constant"
+ string pretty_format format
+ in
+ Error msg
let empty_string () =
- Kernel.abort ~current:true
- "Parsing an empty string as a floating-point constant."
-
-
+ Error "Parsing an empty string as a floating-point constant."
module Regexp = struct
let sign = "\\([+-]?\\)"
@@ -435,7 +435,7 @@ let parse str =
let str = if suffix then String.sub str 0 length else str in
match parse_hexadecimal ~format str with
| None -> cannot_be_parsed str resulting_format
- | Some result -> Parsed (supported, result)
+ | Some result -> Ok (Parsed (supported, result))
else if Str.string_match num_dot_frac_exp str 0 then
let sign = Str.matched_group 1 str in
let integral = Str.matched_group 2 str in
@@ -444,7 +444,7 @@ let parse str =
let format = Str.matched_group 5 str in
let Format (supported, format) = format_of_string format in
let normalizing = normalize integral fractional exponent format in
- Parsed (supported, apply_sign sign normalizing)
+ Ok (Parsed (supported, apply_sign sign normalizing))
else if Str.string_match num_dot_frac str 0 then
let sign = Str.matched_group 1 str in
let integral = Str.matched_group 2 str in
@@ -453,7 +453,7 @@ let parse str =
let format = Str.matched_group 4 str in
let Format (supported, format) = format_of_string format in
let normalizing = normalize integral fractional exponent format in
- Parsed (supported, apply_sign sign normalizing)
+ Ok (Parsed (supported, apply_sign sign normalizing))
else if Str.string_match num_exp str 0 then
let sign = Str.matched_group 1 str in
let integral = Str.matched_group 2 str in
@@ -462,7 +462,12 @@ let parse str =
let format = Str.matched_group 4 str in
let Format (supported, format) = format_of_string format in
let normalizing = normalize integral fractional exponent format in
- Parsed (supported, apply_sign sign normalizing)
+ Ok (Parsed (supported, apply_sign sign normalizing))
else
let format = format_of_string (String.make 1 str.[length]) in
cannot_be_parsed str format
+
+let parse_exn str =
+ match parse str with
+ | Ok parsed -> parsed
+ | Error msg -> Kernel.abort ~current:true "%s" msg
diff --git a/src/libraries/floating_point/typed_float.mli b/src/libraries/floating_point/typed_float.mli
index 20398c281c7d185cee674ef1ba4d5a84a6ffe80f..e1c24ff1132f0ee43b2c7cfd4dda83b9db288555 100644
--- a/src/libraries/floating_point/typed_float.mli
+++ b/src/libraries/floating_point/typed_float.mli
@@ -141,10 +141,15 @@ type ('format, 'encoded_as) parsed_format =
type parsed_result =
| Parsed : ('f, 'k) parsed_format * 'k parsed_float -> parsed_result
-(** Parses the given string and returns the parsed float and its kind (single,
- double or long) according to its suffix, if any. Strings with no suffix
- are parsed as double. *)
-val parse : string -> parsed_result
+(** Parses the given string and returns [Ok Parsed (kind, float)] with the
+ parsed [float] and its [kind] (single, double or long) according to its
+ suffix, if any. Strings with no suffix are parsed as double. Returns
+ [Error msg] if the parsing fails, where [msg] is the error message. *)
+val parse : string -> (parsed_result, string) result
+
+(** Calls {!parse} and evaluates the result type.
+ @raise Log.AbortError if the parsing fails. *)
+val parse_exn : string -> parsed_result
(** Returns the floating-point kind parsed by [parse]. *)
val parsed_fkind : ('k, 'f) parsed_format -> Cil_types.fkind
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index cd7ac25ec760c0b1bfef5d2d9fda215367695220..43539f50277e85373dd719391338784f6ccbb8f4 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -399,7 +399,7 @@ let rec term_to_exp t res =
| TConst (LWStr l) -> new_exp ~loc (Const (CWStr l))
| TConst (LChr c) -> new_exp ~loc (Const (CChr c))
| TConst (LReal l_real) ->
- let Parsed (format, _) = Typed_float.parse l_real.r_literal in
+ let Parsed (format, _) = Typed_float.parse_exn l_real.r_literal in
let fk = Typed_float.parsed_fkind format in
let cst =
if Cil.isExactFloat fk l_real then
diff --git a/src/plugins/eva/values/cvalue_forward.ml b/src/plugins/eva/values/cvalue_forward.ml
index d824bb303b5104db82441f44edb0bce27640ba73..7ce0f301d00af32107396a9815da98f8e53bc36d 100644
--- a/src/plugins/eva/values/cvalue_forward.ml
+++ b/src/plugins/eva/values/cvalue_forward.ml
@@ -532,7 +532,7 @@ let eval_float_constant f fkind fstring =
let fl, fu = match fstring with
| Some "INFINITY" -> f, f (* Special case for the INFINITY macro. *)
| Some string when fkind = Cil_types.FLongDouble || all_rounding () ->
- let Parsed (_, p) = Typed_float.parse string in
+ let Parsed (_, p) = Typed_float.parse_exn string in
(* Computations are done in double. For long double constants, if we
reach infinity, we must use the interval [max_double..infty] to be
sound. Here we even use [-infty..infty]. *)