diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml index 6e9c4550927a121e88848ed51d0a292232d211b2..fbfc904dc2a8963412e321eaa01982d36048325e 100644 --- a/src/kernel_services/ast_printing/cil_printer.ml +++ b/src/kernel_services/ast_printing/cil_printer.ml @@ -2435,7 +2435,7 @@ class cil_printer () = object (self) begin match ty, t.term_node with | TFloat(fk,_) , TConst(LReal r as cst) when not Kernel.(is_debug_key_enabled dkey_print_logic_coercions) && - Cil.isExactFloat fk r -> + Floating_point.has_suffix fk r.r_literal -> self#logic_constant fmt cst | _ -> fprintf fmt "(%a)%a" (self#typ None) ty term e diff --git a/src/libraries/utils/floating_point.ml b/src/libraries/utils/floating_point.ml index 8311b3e64490f7267df51dc6dde29789a97277ab..13227afdd5da5ff1abadabed250a4c13aff26dd2 100644 --- a/src/libraries/utils/floating_point.ml +++ b/src/libraries/utils/floating_point.ml @@ -274,6 +274,14 @@ let parse string = Kernel.fatal ~current:true "Unexpected error parsing floating-point constant: %s." string +let has_suffix fk lit = + let s = match fk with + | Cil_types.FFloat -> 'F' + | Cil_types.FDouble -> 'D' + | Cil_types.FLongDouble -> 'L' in + let ln = String.length lit in + ln > 0 && Char.uppercase_ascii lit.[ln-1] = s + let pretty_normal ~use_hex fmt f = let double_norm = Int64.shift_left 1L 52 in let double_mask = Int64.pred double_norm in diff --git a/src/libraries/utils/floating_point.mli b/src/libraries/utils/floating_point.mli index 6588bd2367c85eae711a7ae3f5eb0d178e7bab7a..599d4770d1c3ae301e85f128695b981a423a8cfd 100644 --- a/src/libraries/utils/floating_point.mli +++ b/src/libraries/utils/floating_point.mli @@ -69,6 +69,10 @@ type parsed_float = { with no suffix are parsed as double. *) val parse: string -> Cil_types.fkind * parsed_float +(** Checks if the (uppercased) string ends with an explicit `F|D|L` + suffix for the given float kind. *) +val has_suffix: Cil_types.fkind -> string -> bool + val pretty_normal : use_hex : bool -> Format.formatter -> float -> unit val pretty : Format.formatter -> float -> unit