diff options
| author | Yannick Moy <moy@adacore.com> | 2022-03-11 11:19:37 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-17 08:25:48 +0000 |
| commit | 3c802e974955085696b6ba3ca20bcde2e2c53921 (patch) | |
| tree | 981dce3e0621d37e60a6bc67d45b9cf4915312f4 /gcc/fortran/trans-openmp.cc | |
| parent | 867bf6f087e9566339cecce358319603ecd08248 (diff) | |
| download | gcc-3c802e974955085696b6ba3ca20bcde2e2c53921.zip gcc-3c802e974955085696b6ba3ca20bcde2e2c53921.tar.gz gcc-3c802e974955085696b6ba3ca20bcde2e2c53921.tar.bz2 | |
[Ada] Allow inlining for proof inside generics
For local subprograms without contracts inside generics, allow their
inlining for proof in GNATprove mode. This requires forbidding the
inlining of subprograms which contain references to object renamings,
which would be replaced in the SPARK expansion and violate assumptions
of the inlining code.
gcc/ada/
* exp_spark.adb (Expand_SPARK_Potential_Renaming): Deal with no
entity case.
* inline.ads (Check_Object_Renaming_In_GNATprove_Mode): New
procedure.
* inline.adb (Check_Object_Renaming_In_GNATprove_Mode): New
procedure.
(Can_Be_Inlined_In_GNATprove_Mode): Remove case forbidding
inlining for subprograms inside generics.
* sem_ch12.adb (Copy_Generic_Node): Preserve global entities
when inlining in GNATprove mode.
* sem_ch6.adb (Analyse_Subprogram_Body_Helper): Remove body to
inline if renaming is detected in GNATprove mode.
Diffstat (limited to 'gcc/fortran/trans-openmp.cc')
0 files changed, 0 insertions, 0 deletions