OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[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  <moy@adacore.com>

gcc/ada/

	* sem_res.adb (Resolve_Call): Check non-aliasing rules before
	GNATprove inlining.

From-SVN: r274640
This commit is contained in:
Yannick Moy 2019-08-19 08:35:35 +00:00 committed by Pierre-Marie de Rodat
parent a4bbe10deb
commit c811dd91e1
2 changed files with 9 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
gcc/ada/ChangeLog
View File

@ -1,3 +1,8 @@
2019-08-19 Yannick Moy <moy@adacore.com>
* sem_res.adb (Resolve_Call): Check non-aliasing rules before
GNATprove inlining.
2019-08-19 Eric Botcazou <ebotcazou@adacore.com>
* inline.adb (Add_Inlined_Body): Do not add pending

8
gcc/ada/sem_res.adb
View File

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