[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

gcc/ada/ChangeLog

+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

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.