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 <m...@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;
-----------------------------
