ada: Do minimal expansion of fixedpoint operations for GNATprove

A minimal expansion of fixedpoint operations is needed for GNATprove, because
the subsequent resolution of type conversion relies on this expansion being
done.

gcc/ada/ChangeLog:

	* exp_ch4.adb (Fixup_Universal_Fixed_Operation): Move to spec.
	* exp_ch4.ads (Fixup_Universal_Fixed_Operation): Move from body.
	* exp_spark.adb (Expand_SPARK): Call a fixup expansion routine.

diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index c9040bf5ba017ec7d965855f5f8c5755eb65ca06..b4270021fafdc75b96eba57a9dd750d71f9cb0ba 100644 (file)
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -177,12 +177,6 @@ package body Exp_Ch4 is
    --  integer type. This is a case where top level processing is required to
    --  handle overflow checks in subtrees.
 
-   procedure Fixup_Universal_Fixed_Operation (N : Node_Id);
-   --  N is a N_Op_Divide or N_Op_Multiply node whose result is universal
-   --  fixed. We do not have such a type at runtime, so the purpose of this
-   --  routine is to find the real type by looking up the tree. We also
-   --  determine if the operation must be rounded.
-
    procedure Get_First_Index_Bounds (T : Entity_Id; Lo, Hi : out Uint);
    --  T is an array whose index bounds are all known at compile time. Return
    --  the value of the low and high bounds of the first index of T.

diff --git a/gcc/ada/exp_ch4.ads b/gcc/ada/exp_ch4.ads
index d954852b16590c86ddc1df242466da7ca3959d9c..42077158ca6006c093b084c8d08055f0fb72bf17 100644 (file)
--- a/gcc/ada/exp_ch4.ads
+++ b/gcc/ada/exp_ch4.ads
@@ -124,4 +124,10 @@ package Exp_Ch4 is
    --  have special circuitry in Expand_N_Type_Conversion to promote both of
    --  the operands to type Integer.
 
+   procedure Fixup_Universal_Fixed_Operation (N : Node_Id);
+   --  N is a N_Op_Divide or N_Op_Multiply node whose result is universal
+   --  fixed. We do not have such a type at runtime, so the purpose of this
+   --  routine is to find the real type by looking up the tree. We also
+   --  determine if the operation must be rounded.
+
 end Exp_Ch4;

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index b75b31b674dbe260df2fb8450691c24d6e616812..6e1c86acc39eace40bf2dcf1c4cfdf7029da78e6 100644 (file)
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -172,6 +172,14 @@ package body Exp_SPARK is
          when N_Op_Ne =>
             Expand_SPARK_N_Op_Ne (N);
 
+         --  Resolution of type conversion relies on minimal expansion of
+         --  fixedpoint operations to insert the range check on their result.
+
+         when N_Op_Multiply | N_Op_Divide =>
+            if Etype (N) = Universal_Fixed then
+               Exp_Ch4.Fixup_Universal_Fixed_Operation (N);
+            end if;
+
          when N_Freeze_Entity =>
             --  Currently we only expand type freeze entities, so ignore other
             --  freeze entites, because it is expensive to create a suitable