From: Piotr Trojanek <troja...@adacore.com>
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.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/exp_ch4.adb | 6 ------
gcc/ada/exp_ch4.ads | 6 ++++++
gcc/ada/exp_spark.adb | 8 ++++++++
3 files changed, 14 insertions(+), 6 deletions(-)
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index c9040bf5ba0..b4270021faf 100644
--- 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 d954852b165..42077158ca6 100644
--- 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 b75b31b674d..6e1c86acc39 100644
--- 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
--
2.43.0
