sem_ch7.adb (Analyze_Package_Body_Helper): When verifying the compatibility of…

sem_ch7.adb (Analyze_Package_Body_Helper): When verifying the compatibility of SPARK_Mode between a spec and a body...

2014-08-04  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch7.adb (Analyze_Package_Body_Helper): When verifying the
	compatibility of SPARK_Mode between a spec and a body, use the
	SPARK_Mode of the public part.
	* sem_ch12.adb (Analyze_Generic_Subprogram_Declaration): Use
	the already available routine to exchange the aspects between
	the template and its copy. Analyze the aspects of copy to
	ensure that the corresponding pragmas perform their semantic
	effects.  The partial analysis of aspects is no longer needed.
	(Analyze_Package_Instantiation): Save and restore the SPARK_Mode
	of the context.
	(Analyze_Subprogram_Instantiation): Save and restore the SPARK_Mode of
	the context.
	* sem_prag.adb (Analyze_Pragma): Do not bypass a subprogram
	instantiation which does not come from source.

From-SVN: r213576

gcc/ada/ChangeLog

 2014-08-04  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* sem_ch7.adb (Analyze_Package_Body_Helper): When verifying the
+	compatibility of SPARK_Mode between a spec and a body, use the
+	SPARK_Mode of the public part.
+	* sem_ch12.adb (Analyze_Generic_Subprogram_Declaration): Use
+	the already available routine to exchange the aspects between
+	the template and its copy. Analyze the aspects of copy to
+	ensure that the corresponding pragmas perform their semantic
+	effects.  The partial analysis of aspects is no longer needed.
+	(Analyze_Package_Instantiation): Save and restore the SPARK_Mode
+	of the context.
+	(Analyze_Subprogram_Instantiation): Save and restore the SPARK_Mode of
+	the context.
+	* sem_prag.adb (Analyze_Pragma): Do not bypass a subprogram
+	instantiation which does not come from source.
+
+2014-08-04  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* a-cfhama.ads, a-cfhase.ads, a-cforma.ads, a-cforse.ads Add
 	SPARK_Mode pragmas to the public and private part of the unit.
 	* sem_ch3.adb (Derive_Type_Declaration): Ensure that a derived

gcc/ada/sem_ch12.adb

@@ -3342,19 +3342,10 @@ package body Sem_Ch12 is
       Set_Parent_Spec (New_N, Save_Parent);
       Rewrite (N, New_N);
 
-      --  The aspect specifications are not attached to the tree, and must
-      --  be copied and attached to the generic copy explicitly.
+      --  Once the contents of the generic copy and the template are swapped,
+      --  do the same for their respective aspect specifications.
 
-      if Present (Aspect_Specifications (New_N)) then
-         declare
-            Aspects : constant List_Id := Aspect_Specifications (N);
-         begin
-            Set_Has_Aspects (N, False);
-            Move_Aspects (New_N, To => N);
-            Set_Has_Aspects (Original_Node (N), False);
-            Set_Aspect_Specifications (Original_Node (N), Aspects);
-         end;
-      end if;
+      Exchange_Aspects (N, New_N);
 
       Spec := Specification (N);
       Id := Defining_Entity (Spec);
@@ -3369,8 +3360,15 @@ package body Sem_Ch12 is
       Start_Generic;
 
       Enter_Name (Id);
-
       Set_Scope_Depth_Value (Id, Scope_Depth (Current_Scope) + 1);
+
+      --  Analyze the aspects of the generic copy to ensure that all generated
+      --  pragmas (if any) perform their semantic effects.
+
+      if Has_Aspects (N) then
+         Analyze_Aspect_Specifications (N, Id);
+      end if;
+
       Push_Scope (Id);
       Enter_Generic_Scope (Id);
       Set_Inner_Instances (Id, New_Elmt_List);
@@ -3460,41 +3458,6 @@ package body Sem_Ch12 is
          Make_Aspect_For_PPC_In_Gen_Sub_Decl (N);
       end if;
 
-      --  To capture global references, analyze the expressions of aspects,
-      --  and propagate information to original tree. Note that in this case
-      --  analysis of attributes is not delayed until the freeze point.
-
-      --  It seems very hard to recreate the proper visibility of the generic
-      --  subprogram at a later point because the analysis of an aspect may
-      --  create pragmas after the generic copies have been made ???
-
-      if Has_Aspects (N) then
-         declare
-            Aspect : Node_Id;
-
-         begin
-            Aspect := First (Aspect_Specifications (N));
-            while Present (Aspect) loop
-               if Get_Aspect_Id (Aspect) /= Aspect_Warnings
-                 and then Present (Expression (Aspect))
-               then
-                  Analyze (Expression (Aspect));
-               end if;
-
-               Next (Aspect);
-            end loop;
-
-            Aspect := First (Aspect_Specifications (Original_Node (N)));
-            while Present (Aspect) loop
-               if Present (Expression (Aspect)) then
-                  Save_Global_References (Expression (Aspect));
-               end if;
-
-               Next (Aspect);
-            end loop;
-         end;
-      end if;
-
       End_Generic;
       End_Scope;
       Exit_Generic_Scope (Id);
@@ -3533,6 +3496,10 @@ package body Sem_Ch12 is
       Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
       --  Save flag Ignore_Pragma_SPARK_Mode for restore on exit
 
+      Save_SM  : constant SPARK_Mode_Type := SPARK_Mode;
+      Save_SMP : constant Node_Id         := SPARK_Mode_Pragma;
+      --  Save the SPARK_Mode-related data for restore on exit
+
       Save_Style_Check : constant Boolean := Style_Check;
       --  Save style check mode for restore on exit
 
@@ -4283,7 +4250,9 @@ package body Sem_Ch12 is
       end if;
 
       Ignore_Pragma_SPARK_Mode := Save_IPSM;
-      Style_Check := Save_Style_Check;
+      SPARK_Mode               := Save_SM;
+      SPARK_Mode_Pragma        := Save_SMP;
+      Style_Check              := Save_Style_Check;
 
       --  Check that if N is an instantiation of System.Dim_Float_IO or
       --  System.Dim_Integer_IO, the formal type has a dimension system.
@@ -4318,7 +4287,9 @@ package body Sem_Ch12 is
          end if;
 
          Ignore_Pragma_SPARK_Mode := Save_IPSM;
-         Style_Check := Save_Style_Check;
+         SPARK_Mode               := Save_SM;
+         SPARK_Mode_Pragma        := Save_SMP;
+         Style_Check              := Save_Style_Check;
    end Analyze_Package_Instantiation;
 
    --------------------------
@@ -4875,6 +4846,10 @@ package body Sem_Ch12 is
       Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode;
       --  Save flag Ignore_Pragma_SPARK_Mode for restore on exit
 
+      Save_SM  : constant SPARK_Mode_Type := SPARK_Mode;
+      Save_SMP : constant Node_Id         := SPARK_Mode_Pragma;
+      --  Save the SPARK_Mode-related data for restore on exit
+
       Vis_Prims_List : Elist_Id := No_Elist;
       --  List of primitives made temporarily visible in the instantiation
       --  to match the visibility of the formal type
@@ -5157,6 +5132,8 @@ package body Sem_Ch12 is
          Generic_Renamings_HTable.Reset;
 
          Ignore_Pragma_SPARK_Mode := Save_IPSM;
+         SPARK_Mode               := Save_SM;
+         SPARK_Mode_Pragma        := Save_SMP;
       end if;
 
    <<Leave>>
@@ -5175,6 +5152,8 @@ package body Sem_Ch12 is
          end if;
 
          Ignore_Pragma_SPARK_Mode := Save_IPSM;
+         SPARK_Mode               := Save_SM;
+         SPARK_Mode_Pragma        := Save_SMP;
    end Analyze_Subprogram_Instantiation;
 
    -------------------------

gcc/ada/sem_ch7.adb

@@ -440,8 +440,8 @@ package body Sem_Ch7 is
       --  Verify that the SPARK_Mode of the body agrees with that of its spec
 
       if Present (SPARK_Pragma (Body_Id)) then
-         if Present (SPARK_Aux_Pragma (Spec_Id)) then
-            if Get_SPARK_Mode_From_Pragma (SPARK_Aux_Pragma (Spec_Id)) = Off
+         if Present (SPARK_Pragma (Spec_Id)) then
+            if Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) = Off
                  and then
                Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On
             then

gcc/ada/sem_prag.adb

@@ -19353,6 +19353,16 @@ package body Sem_Prag is
                         raise Pragma_Exit;
                      end if;
 
+                  --  Skip internally generated code, but consider subprogram
+                  --  instantiations housed within their wrapper packages.
+
+                  elsif not Comes_From_Source (Stmt)
+                    and then
+                      (Nkind (Stmt) /= N_Subprogram_Declaration
+                         or else No (Generic_Parent (Specification (Stmt))))
+                  then
+                     null;
+
                   --  The pragma is associated with a package or subprogram
                   --  instantiation that does not act as a compilation unit.
 
@@ -19374,12 +19384,15 @@ package body Sem_Prag is
                      Set_SPARK_Pragma_Inherited (Inst_Id, False);
                      return;
 
-                  --  The pragma applies to a subprogram declaration
+                  --  The pragma applies to a [generic] subprogram declaration
 
+                  --    [generic]
                   --    procedure Proc ...;
                   --    pragma SPARK_Mode ..;
 
-                  elsif Nkind (Stmt) = N_Subprogram_Declaration then
+                  elsif Nkind_In (Stmt, N_Generic_Subprogram_Declaration,
+                                        N_Subprogram_Declaration)
+                  then
                      Spec_Id := Defining_Entity (Stmt);
                      Check_Library_Level_Entity (Spec_Id);
                      Check_Pragma_Conformance
@@ -19387,15 +19400,10 @@ package body Sem_Prag is
                         Entity_Pragma  => Empty,
                         Entity         => Empty);
 
-                     Set_SPARK_Pragma               (Spec_Id, N);
-                     Set_SPARK_Pragma_Inherited     (Spec_Id, False);
+                     Set_SPARK_Pragma           (Spec_Id, N);
+                     Set_SPARK_Pragma_Inherited (Spec_Id, False);
                      return;
 
-                  --  Skip internally generated code
-
-                  elsif not Comes_From_Source (Stmt) then
-                     null;
-
                   --  Otherwise the pragma does not apply to a legal construct
                   --  or it does not appear at the top of a declarative or a
                   --  statement list. Issue an error and stop the analysis.
@@ -19405,7 +19413,7 @@ package body Sem_Prag is
                      exit;
                   end if;
 
-                  Stmt := Prev (Stmt);
+                  Prev (Stmt);
                end loop;
 
                --  The pragma appears within package declarations