This is the mail archive of the
gcc-patches@gcc.gnu.org
mailing list for the GCC project.
[Ada] Mark parameters as coming from source for GNATprove
- From: Pierre-Marie de Rodat <derodat at adacore dot com>
- To: gcc-patches at gcc dot gnu dot org
- Cc: Yannick Moy <moy at adacore dot com>
- Date: Mon, 11 Jun 2018 05:23:40 -0400
- Subject: [Ada] Mark parameters as coming from source for GNATprove
When building a separate subprogram declaration for possible inlining of
local subprograms in GNATprove mode, correctly mark subprogram parameters
as coming from source.
This has no impact on compilation.
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-06-11 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_ch6.adb (Build_Subprogram_Declaration): Mark parameters as coming
from source.
--- gcc/ada/sem_ch6.adb
+++ gcc/ada/sem_ch6.adb
@@ -2712,6 +2712,22 @@ package body Sem_Ch6 is
Specification => Copy_Subprogram_Spec (Body_Spec));
Set_Comes_From_Source (Subp_Decl, True);
+ -- Also mark parameters as coming from source
+
+ if Present (Parameter_Specifications (Specification (Subp_Decl))) then
+ declare
+ Form : Entity_Id;
+ begin
+ Form :=
+ First (Parameter_Specifications (Specification (Subp_Decl)));
+
+ while Present (Form) loop
+ Set_Comes_From_Source (Defining_Identifier (Form), True);
+ Next (Form);
+ end loop;
+ end;
+ end if;
+
-- Relocate the aspects and relevant pragmas from the subprogram body
-- to the generated spec because it acts as the initial declaration.