diff mbox series

[Ada] More precise propagation of Size attribute in generic instances

Message ID 20190821083143.GA71911@adacore.com
State New
Headers show
Series [Ada] More precise propagation of Size attribute in generic instances | expand

Commit Message

Pierre-Marie de Rodat Aug. 21, 2019, 8:31 a.m. UTC 
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.
diff mbox series

Patch

--- 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