[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  <moy@adacore.com>

gcc/ada/

	* sem_ch3.adb (Analyze_Subtype_Declaration): Inherit RM_Size
	field for formal type parameters in generic instantiations.

git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@274788 138bc75d-0d04-0410-961f-82ee72b054a4

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 9133c6c1192abf300d26937e0a255bcc2b02f912..abe3524816d00dae0804a09cb52ecaeab4a7d470 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-08-21  Yannick Moy  <moy@adacore.com>
+
+       * sem_ch3.adb (Analyze_Subtype_Declaration): Inherit RM_Size
+       field for formal type parameters in generic instantiations.
+
 2019-08-21  Yannick Moy  <moy@adacore.com>
 
        * sem_spark.adb: Update references to the SPARK RM.

diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index f3acae1dd27483d4673ef9f701bf46e715e6b489..edde68921cf2446a80401f8b41a45ff30b75f9cf 100644 (file)
--- 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