From: Yannick Moy <moy@adacore.com>
Date: Mon, 11 Jun 2018 09:19:07 +0000 (+0000)
Subject: [Ada] Mark parameters as coming from source for GNATprove
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=90265b93430c82d817deae512208a76f5241ea1c;p=gcc.git

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

2018-06-11  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_ch6.adb (Build_Subprogram_Declaration): Mark parameters as coming
	from source.

From-SVN: r261423
---

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 2393bfaa0c6..84dd18b7767 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2018-06-11  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch6.adb (Build_Subprogram_Declaration): Mark parameters as coming
+	from source.
+
 2018-06-11  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_ch13.adb (Build_Predicate_Functions): For a derived type, ensure
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 3413e2185b5..304e35c18c5 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/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.