diff options
| author | Yannick Moy <moy@adacore.com> | 2019-07-09 07:54:00 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-07-09 07:54:00 +0000 |
| commit | 554a9844f74932d2c6e9a690d04bfd96b361055b (patch) | |
| tree | 6312457ae3ef968364d1de177da993b606b6114c | |
| parent | 5dd6327237996b7f4103e11c76aac01bf2420e19 (diff) | |
| download | gcc-554a9844f74932d2c6e9a690d04bfd96b361055b.zip gcc-554a9844f74932d2c6e9a690d04bfd96b361055b.tar.gz gcc-554a9844f74932d2c6e9a690d04bfd96b361055b.tar.bz2 | |
[Ada] Prevent inconsistent state for inlining in GNATprove
In GNATprove mode, subprograms with a body to inline should have been
filtered in Analyze_Subprogram_Body_Helper to match the conditions for
inlining subprograms in GNATprove. Prevent a call to Set_Body_To_Inline
in GNATprove mode that did not go through this filtering.
There is no impact on compilation.
2019-07-09 Yannick Moy <moy@adacore.com>
gcc/ada/
* freeze.adb (Build_Renamed_Body): Do not set body to inline in
GNATprove mode.
From-SVN: r273274
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/freeze.adb | 5 |
2 files changed, 9 insertions, 1 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8c07082..b74910d 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,10 @@ 2019-07-09 Yannick Moy <moy@adacore.com> + * freeze.adb (Build_Renamed_Body): Do not set body to inline in + GNATprove mode. + +2019-07-09 Yannick Moy <moy@adacore.com> + * exp_util.adb (Expand_Subtype_From_Expr): Still expand the type of static expressions in GNATprove_Mode. * sem_ch3.adb (Analyze_Object_Declaration): Remove obsolete diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index 5b843f2..b29ff67 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -407,11 +407,14 @@ package body Freeze is -- calls to the renamed entity. The body must be generated in any case -- for calls that may appear elsewhere. This is not done in the case -- where the subprogram is an instantiation because the actual proper - -- body has not been built yet. + -- body has not been built yet. This is also not done in GNATprove mode + -- as we need to check other conditions for creating a body to inline + -- in that case, which are controlled in Analyze_Subprogram_Body_Helper. if Ekind_In (Old_S, E_Function, E_Procedure) and then Nkind (Decl) = N_Subprogram_Declaration and then not Is_Generic_Instance (Old_S) + and then not GNATprove_Mode then Set_Body_To_Inline (Decl, Old_S); end if; |