From 61e33106eda3d937fae9ba624da05938bda3af5e Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Wed, 21 Aug 2019 08:31:07 +0000 Subject: [PATCH] [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. 2019-08-21 Yannick Moy gcc/ada/ * sem_ch3.adb (Analyze_Subtype_Declaration): Inherit RM_Size field for formal type parameters in generic instantiations. From-SVN: r274788 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/sem_ch3.adb | 8 ++++++++ 2 files changed, 13 insertions(+) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 9133c6c1192..abe3524816d 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-08-21 Yannick Moy + + * sem_ch3.adb (Analyze_Subtype_Declaration): Inherit RM_Size + field for formal type parameters in generic instantiations. + 2019-08-21 Yannick Moy * sem_spark.adb: Update references to the SPARK RM. diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index f3acae1dd27..edde68921cf 100644 --- a/gcc/ada/sem_ch3.adb +++ b/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 -- 2.30.2