diff options
| author | Yannick Moy <moy@adacore.com> | 2019-08-21 08:31:07 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-08-21 08:31:07 +0000 |
| commit | 61e33106eda3d937fae9ba624da05938bda3af5e (patch) | |
| tree | 53e8ec52d8bb6004662a1607e9cc6ef38059269e | |
| parent | e9934e8c79c4eafbb231ed53b3a6e1c6632a1a15 (diff) | |
| download | gcc-61e33106eda3d937fae9ba624da05938bda3af5e.zip gcc-61e33106eda3d937fae9ba624da05938bda3af5e.tar.gz gcc-61e33106eda3d937fae9ba624da05938bda3af5e.tar.bz2 | |
[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.
From-SVN: r274788
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/sem_ch3.adb | 8 |
2 files changed, 13 insertions, 0 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 9133c6c..abe3524 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,10 @@ 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. 2019-08-21 Eric Botcazou <ebotcazou@adacore.com> diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index f3acae1..edde689 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 |