[Ada] Add query for extended precision floating-point types
Commit Message
This query is used in GNATprove to identify extended precision (80-bits)
floating-point types.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* sem_util.adb (Is_Extended_Precision_Floating_Point_Type): New
function.
* sem_util.ads (Is_Extended_Precision_Floating_Point_Type): New
function.
@@ -17541,6 +17541,20 @@ package body Sem_Util is
end if;
end Is_Expression_Function_Or_Completion;
+ -----------------------------------------------
+ -- Is_Extended_Precision_Floating_Point_Type --
+ -----------------------------------------------
+
+ function Is_Extended_Precision_Floating_Point_Type
+ (E : Entity_Id) return Boolean is
+ begin
+ return Is_Floating_Point_Type (E)
+ and then Machine_Radix_Value (E) = Uint_2
+ and then Machine_Mantissa_Value (E) = Uint_64
+ and then Machine_Emax_Value (E) = Uint_2 ** Uint_14
+ and then Machine_Emin_Value (E) = Uint_3 - (Uint_2 ** Uint_14);
+ end Is_Extended_Precision_Floating_Point_Type;
+
-----------------------
-- Is_EVF_Expression --
-----------------------
@@ -2045,6 +2045,15 @@ package Sem_Util is
-- Determine whether subprogram [body] Subp denotes an expression function
-- or is completed by an expression function body.
+ function Is_Extended_Precision_Floating_Point_Type
+ (E : Entity_Id) return Boolean;
+ -- Return whether E is an extended precision floating point type,
+ -- characterized by:
+ -- . machine_radix = 2
+ -- . machine_mantissa = 64
+ -- . machine_emax = 2**14
+ -- . machine_emin = 3 - machine_emax
+
function Is_EVF_Expression (N : Node_Id) return Boolean;
-- Determine whether node N denotes a reference to a formal parameter of
-- a specific tagged type whose related subprogram is subject to pragma