This is the mail archive of the
gcc-patches@gcc.gnu.org
mailing list for the GCC project.
[Ada] More precise propagation of Size attribute in generic instances
- From: Pierre-Marie de Rodat <derodat at adacore dot com>
- To: gcc-patches at gcc dot gnu dot org
- Cc: Yannick Moy <moy at adacore dot com>
- Date: Wed, 21 Aug 2019 04:31:43 -0400
- Subject: [Ada] More precise propagation of Size attribute in generic instances
GNATprove analyzer for SPARK code depends on the frontend to accurately
propagate the known value of Size attribute. This was not done for
formal type parameters in generic instantiations. Now fixed.
There is no impact on compilation.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-08-21 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_ch3.adb (Analyze_Subtype_Declaration): Inherit RM_Size
field for formal type parameters in generic instantiations.
--- gcc/ada/sem_ch3.adb
+++ gcc/ada/sem_ch3.adb
@@ -5555,6 +5555,14 @@ package body Sem_Ch3 is
=>
Set_Ekind (Id, E_Record_Subtype);
+ -- Subtype declarations introduced for formal type parameters
+ -- in generic instantiations should inherit the Size value of
+ -- the type they rename.
+
+ if Present (Generic_Parent_Type (N)) then
+ Set_RM_Size (Id, RM_Size (T));
+ end if;
+
if Ekind (T) = E_Record_Subtype
and then Present (Cloned_Subtype (T))
then