This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

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

Tested on x86_64-pc-linux-gnu, committed on trunk

2019-08-19  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_res.adb (Resolve_Call): Check non-aliasing rules before
	GNATprove inlining.
--- gcc/ada/sem_res.adb
+++ 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;
 
    -----------------------------


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]