From c811dd91e184db204073d04c28ed107888b39518 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 19 Aug 2019 08:35:35 +0000 Subject: [PATCH] [Ada] Do not skip non-aliasing checking when inlining in GNATprove When code is inlinined for proof in the special mode for GNATprove, Ada rules about non-aliasing should still be checked. Now fixed. There is no impact on compilation. 2019-08-19 Yannick Moy gcc/ada/ * sem_res.adb (Resolve_Call): Check non-aliasing rules before GNATprove inlining. From-SVN: r274640 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/sem_res.adb | 8 ++++---- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 9fc8c9e1139..9222a98150d 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-08-19 Yannick Moy + + * sem_res.adb (Resolve_Call): Check non-aliasing rules before + GNATprove inlining. + 2019-08-19 Eric Botcazou * inline.adb (Add_Inlined_Body): Do not add pending diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index b27171f0be5..8f2e35894d4 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -6968,6 +6968,10 @@ package body Sem_Res is Build_Call_Marker (N); + Mark_Use_Clauses (Subp); + + Warn_On_Overlapping_Actuals (Nam, N); + -- In GNATprove mode, expansion is disabled, but we want to inline some -- subprograms to facilitate formal verification. Indirect calls through -- a subprogram type or within a generic cannot be inlined. Inlining is @@ -7116,10 +7120,6 @@ package body Sem_Res is end if; end if; end if; - - Mark_Use_Clauses (Subp); - - Warn_On_Overlapping_Actuals (Nam, N); end Resolve_Call; -----------------------------