[Ada] Mark parameters as coming from source for GNATprove

Message ID 20180611092340.GA135072@adacore.com
State New
Headers show
Series
  • [Ada] Mark parameters as coming from source for GNATprove
Related show

Commit Message

Pierre-Marie de Rodat June 11, 2018, 9:23 a.m.
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.

Patch

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