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

	* a-cfhama.adb, a-cfhase.adb, a-cforma.adb, a-cforse.adb Add
	SPARK_Mode in the body.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Restore the original
	way to verify the consistency of SPARK_Mode between a spec and
	a body.
	* sem_ch12.adb (Analyze_Package_Instantiation): Remove the call
	to Set_Ignore_Pragma_SPARK_Mode. Set flag Ignore_Pragma_SPARK_Mode
	manually.
	(Analyze_Subprogram_Instantiation): Remove the call to
	Set_Ignore_Pragma_SPARK_Mode. Set flag Ignore_Pragma_SPARK_Mode
	manually.
	* sem_prag.adb (Analyze_Pragma): Remove local variable
	Inst_Id. SPARK_Mode can no longer be applied to a package or
	subprogram instantiation.
	* sem_util.adb, sem_util.ads (Set_Ignore_Pragma_SPARK_Mode):
	Removed.

From-SVN: r213578

10 files changed, 78 insertions, 223 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 6a25643..e2a5837 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,22 @@
+2014-08-04  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* a-cfhama.adb, a-cfhase.adb, a-cforma.adb, a-cforse.adb Add
+	SPARK_Mode in the body.
+	* sem_ch7.adb (Analyze_Package_Body_Helper): Restore the original
+	way to verify the consistency of SPARK_Mode between a spec and
+	a body.
+	* sem_ch12.adb (Analyze_Package_Instantiation): Remove the call
+	to Set_Ignore_Pragma_SPARK_Mode. Set flag Ignore_Pragma_SPARK_Mode
+	manually.
+	(Analyze_Subprogram_Instantiation): Remove the call to
+	Set_Ignore_Pragma_SPARK_Mode. Set flag Ignore_Pragma_SPARK_Mode
+	manually.
+	* sem_prag.adb (Analyze_Pragma): Remove local variable
+	Inst_Id. SPARK_Mode can no longer be applied to a package or
+	subprogram instantiation.
+	* sem_util.adb, sem_util.ads (Set_Ignore_Pragma_SPARK_Mode):
+	Removed.
+
 2014-08-04  Robert Dewar  <dewar@adacore.com>
 
 	* sem_prag.adb, osint.adb, osint.ads: Minor reformatting.
diff --git a/gcc/ada/a-cfhama.adb b/gcc/ada/a-cfhama.adb
index 858216f..1780bbb 100644
--- a/gcc/ada/a-cfhama.adb
+++ b/gcc/ada/a-cfhama.adb
@@ -33,9 +33,10 @@ pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Keys);
 
 with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers;
 
-with System;  use type System.Address;
+with System; use type System.Address;
 
 package body Ada.Containers.Formal_Hashed_Maps is
+   pragma SPARK_Mode (Off);
 
    -----------------------
    -- Local Subprograms --
diff --git a/gcc/ada/a-cfhase.adb b/gcc/ada/a-cfhase.adb
index de09ce8..7c1f954 100644
--- a/gcc/ada/a-cfhase.adb
+++ b/gcc/ada/a-cfhase.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2010-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 2010-2014, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -36,6 +36,7 @@ with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers;
 with System; use type System.Address;
 
 package body Ada.Containers.Formal_Hashed_Sets is
+   pragma SPARK_Mode (Off);
 
    -----------------------
    -- Local Subprograms --
diff --git a/gcc/ada/a-cforma.adb b/gcc/ada/a-cforma.adb
index 69f2cc7..8a85cae 100644
--- a/gcc/ada/a-cforma.adb
+++ b/gcc/ada/a-cforma.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2010-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 2010-2014, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -35,6 +35,7 @@ pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Bounded_Keys);
 with System; use type System.Address;
 
 package body Ada.Containers.Formal_Ordered_Maps is
+   pragma SPARK_Mode (Off);
 
    -----------------------------
    -- Node Access Subprograms --
diff --git a/gcc/ada/a-cforse.adb b/gcc/ada/a-cforse.adb
index d1e6b8c..966853a1 100644
--- a/gcc/ada/a-cforse.adb
+++ b/gcc/ada/a-cforse.adb
@@ -36,9 +36,10 @@ with Ada.Containers.Red_Black_Trees.Generic_Bounded_Set_Operations;
 pragma Elaborate_All
   (Ada.Containers.Red_Black_Trees.Generic_Bounded_Set_Operations);
 
-with System;  use type System.Address;
+with System; use type System.Address;
 
 package body Ada.Containers.Formal_Ordered_Sets is
+   pragma SPARK_Mode (Off);
 
    ------------------------------
    -- Access to Fields of Node --
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index a54b9aa..dd8badb 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -3739,11 +3739,13 @@ package body Sem_Ch12 is
          goto Leave;
 
       else
-         --  If the instance or its context is subject to SPARK_Mode "off",
+         --  If the context of the instance is subject to SPARK_Mode "off",
          --  set the global flag which signals Analyze_Pragma to ignore all
          --  SPARK_Mode pragmas within the instance.
 
-         Set_Ignore_Pragma_SPARK_Mode (N);
+         if SPARK_Mode = Off then
+            Ignore_Pragma_SPARK_Mode := True;
+         end if;
 
          Gen_Decl := Unit_Declaration_Node (Gen_Unit);
 
@@ -4914,11 +4916,13 @@ package body Sem_Ch12 is
          Error_Msg_NE ("instantiation of & within itself", N, Gen_Unit);
 
       else
-         --  If the instance or its context is subject to SPARK_Mode "off",
+         --  If the context of the instance is subject to SPARK_Mode "off",
          --  set the global flag which signals Analyze_Pragma to ignore all
          --  SPARK_Mode pragmas within the instance.
 
-         Set_Ignore_Pragma_SPARK_Mode (N);
+         if SPARK_Mode = Off then
+            Ignore_Pragma_SPARK_Mode := True;
+         end if;
 
          Set_Entity (Gen_Id, Gen_Unit);
          Set_Is_Instantiated (Gen_Unit);
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index 4cda00c..4821db5 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/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_Pragma (Spec_Id)) then
-            if Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) = Off
+         if Present (SPARK_Aux_Pragma (Spec_Id)) then
+            if Get_SPARK_Mode_From_Pragma (SPARK_Aux_Pragma (Spec_Id)) = Off
                  and then
                Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On
             then
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 40ce62f..8ef209d 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -19226,7 +19226,6 @@ package body Sem_Prag is
 
             Body_Id : Entity_Id;
             Context : Node_Id;
-            Inst_Id : Entity_Id;
             Mode    : Name_Id;
             Mode_Id : SPARK_Mode_Type;
             Spec_Id : Entity_Id;
@@ -19261,12 +19260,6 @@ package body Sem_Prag is
             Mode_Id := Get_SPARK_Mode_Type (Mode);
             Context := Parent (N);
 
-            --  Handle a compilation unit with configuration pragmas
-
-            if Nkind (Context) = N_Compilation_Unit_Aux then
-               Context := Parent (Context);
-            end if;
-
             --  The pragma appears in a configuration pragmas file
 
             if No (Context) then
@@ -19281,59 +19274,17 @@ package body Sem_Prag is
                SPARK_Mode_Pragma := N;
                SPARK_Mode := Mode_Id;
 
-            --  The pragma applies to a compilation unit
-
-            elsif Nkind (Context) = N_Compilation_Unit then
-
-               --  The pragma acts as a configuration pragma
-
-               --    pragma SPARK_Mode ...;
-               --    package Pack is ...;
-
-               if List_Containing (N) = Context_Items (Context) then
-                  Check_Valid_Configuration_Pragma;
-                  SPARK_Mode_Pragma := N;
-                  SPARK_Mode := Mode_Id;
-
-               --  The pragma applies to a package instantiation that acts as a
-               --  compilation unit.
-
-               --    package Inst is new Gen ...;
-               --    pragma SPARK_Mode ...;
-
-               elsif Nkind (Unit (Context)) = N_Package_Instantiation then
-                  Inst_Id := Defining_Entity (Instance_Spec (Unit (Context)));
-                  Check_Library_Level_Entity (Inst_Id);
-                  Check_Pragma_Conformance
-                    (Context_Pragma => SPARK_Mode_Pragma,
-                     Entity_Pragma  => Empty,
-                     Entity         => Empty);
-
-                  Set_SPARK_Pragma           (Inst_Id, N);
-                  Set_SPARK_Pragma_Inherited (Inst_Id, False);
-
-               --  Otherwise the pragma applies to a subprogram instantiation
-               --  that acts as a compilation unit.
-
-               else
-                  Spec_Id := Defining_Entity (Unit (Context));
-                  Check_Library_Level_Entity (Spec_Id);
-                  Check_Pragma_Conformance
-                    (Context_Pragma => SPARK_Mode_Pragma,
-                     Entity_Pragma  => Empty,
-                     Entity         => Empty);
+            --  The pragma acts as a configuration pragma in a compilation unit
 
-                  Set_SPARK_Pragma           (Spec_Id, N);
-                  Set_SPARK_Pragma_Inherited (Spec_Id, False);
+            --    pragma SPARK_Mode ...;
+            --    package Pack is ...;
 
-                  if Ekind (Spec_Id) = E_Package
-                    and then Present (Related_Instance (Spec_Id))
-                  then
-                     Inst_Id := Related_Instance (Spec_Id);
-                     Set_SPARK_Pragma           (Inst_Id, N);
-                     Set_SPARK_Pragma_Inherited (Inst_Id, False);
-                  end if;
-               end if;
+            elsif Nkind (Context) = N_Compilation_Unit
+              and then List_Containing (N) = Context_Items (Context)
+            then
+               Check_Valid_Configuration_Pragma;
+               SPARK_Mode_Pragma := N;
+               SPARK_Mode := Mode_Id;
 
             --  Otherwise the placement of the pragma within the tree dictates
             --  its associated construct. Inspect the declarative list where
@@ -19353,37 +19304,11 @@ package body Sem_Prag is
                         raise Pragma_Exit;
                      end if;
 
-                  --  Skip internally generated code, but consider subprogram
-                  --  instantiations housed within their wrapper packages.
+                  --  Skip internally generated code
 
-                  elsif not Comes_From_Source (Stmt)
-                    and then
-                      (Nkind (Stmt) /= N_Subprogram_Declaration
-                        or else No (Generic_Parent (Specification (Stmt))))
-                  then
+                  elsif not Comes_From_Source (Stmt) then
                      null;
 
-                  --  The pragma is associated with a package or subprogram
-                  --  instantiation that does not act as a compilation unit.
-
-                  --    package Inst is new Gen ...;
-                  --    pragma SPARK_Mode ...;
-
-                  elsif Nkind_In (Stmt, N_Function_Instantiation,
-                                        N_Package_Instantiation,
-                                        N_Procedure_Instantiation)
-                  then
-                     Inst_Id := Defining_Entity (Instance_Spec (Stmt));
-                     Check_Library_Level_Entity (Inst_Id);
-                     Check_Pragma_Conformance
-                       (Context_Pragma => SPARK_Mode_Pragma,
-                        Entity_Pragma  => Empty,
-                        Entity         => Empty);
-
-                     Set_SPARK_Pragma           (Inst_Id, N);
-                     Set_SPARK_Pragma_Inherited (Inst_Id, False);
-                     return;
-
                   --  The pragma applies to a [generic] subprogram declaration
 
                   --    [generic]
@@ -19416,6 +19341,16 @@ package body Sem_Prag is
                   Prev (Stmt);
                end loop;
 
+               --  The pragma applies to a package or a subprogram that acts as
+               --  a compilation unit.
+
+               --    procedure Proc ...;
+               --    pragma SPARK_Mode ...;
+
+               if Nkind (Context) = N_Compilation_Unit_Aux then
+                  Context := Unit (Parent (Context));
+               end if;
+
                --  The pragma appears within package declarations
 
                if Nkind (Context) = N_Package_Specification then
@@ -19502,6 +19437,26 @@ package body Sem_Prag is
                   Set_SPARK_Aux_Pragma           (Body_Id, N);
                   Set_SPARK_Aux_Pragma_Inherited (Body_Id, False);
 
+               --  The pragma appeared as an aspect of a [generic] subprogram
+               --  declaration that acts as a compilation unit.
+
+               --    [generic]
+               --    procedure Proc ...;
+               --    pragma SPARK_Mode ...;
+
+               elsif Nkind_In (Context, N_Generic_Subprogram_Declaration,
+                                        N_Subprogram_Declaration)
+               then
+                  Spec_Id := Defining_Entity (Context);
+                  Check_Library_Level_Entity (Spec_Id);
+                  Check_Pragma_Conformance
+                    (Context_Pragma => SPARK_Pragma (Spec_Id),
+                     Entity_Pragma  => Empty,
+                     Entity         => Empty);
+
+                  Set_SPARK_Pragma           (Spec_Id, N);
+                  Set_SPARK_Pragma_Inherited (Spec_Id, False);
+
                --  The pragma appears at the top of subprogram body
                --  declarations.
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 107ce11..71a6429 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -16456,128 +16456,6 @@ package body Sem_Util is
       Set_Entity (N, Val);
    end Set_Entity_With_Checks;
 
-   ----------------------------------
-   -- Set_Ignore_Pragma_SPARK_Mode --
-   ----------------------------------
-
-   procedure Set_Ignore_Pragma_SPARK_Mode (N : Node_Id) is
-      procedure Set_SPARK_Mode (Expr : Node_Id);
-      --  Set flag Ignore_Pragma_SPARK_Mode based on the argument of aspect or
-      --  pragma SPARK_Mode denoted by Expr.
-
-      --------------------
-      -- Set_SPARK_Mode --
-      --------------------
-
-      procedure Set_SPARK_Mode (Expr : Node_Id) is
-      begin
-         --  When pragma SPARK_Mode with argument "off" applies to an instance,
-         --  all SPARK_Mode pragmas within the instance are ignored.
-
-         if Present (Expr)
-           and then Nkind (Expr) = N_Identifier
-           and then Chars (Expr) = Name_Off
-         then
-            Ignore_Pragma_SPARK_Mode := True;
-         end if;
-      end Set_SPARK_Mode;
-
-      --  Local variables
-
-      Aspects : constant List_Id := Aspect_Specifications (N);
-      Context : constant Node_Id := Parent (N);
-      Args    : List_Id;
-      Aspect  : Node_Id;
-      Decl    : Node_Id;
-
-   --  Start of processing for Set_Ignore_Pragma_SPARK_Mode
-
-   begin
-      --  When the enclosing context of the instance has SPARK_Mode "off", all
-      --  SPARK_Mode pragmas within the instance are ignored. Note that there
-      --  is no point in checking whether the instantiation itself carries
-      --  aspect/pragma SPARK_Mode because it is either illegal ("on") or has
-      --  no effect ("off").
-
-      if SPARK_Mode = Off then
-         Ignore_Pragma_SPARK_Mode := True;
-         return;
-      end if;
-
-      --  Inspect the aspects of the instantiation and locate SPARK_Mode. Note
-      --  that the aspect form of SPARK_Mode precedes a potentially duplicate
-      --  pragma.
-
-      if Present (Aspects) then
-         Aspect := First (Aspects);
-         while Present (Aspect) loop
-            if Get_Aspect_Id (Aspect) = Aspect_SPARK_Mode then
-               Set_SPARK_Mode (Expression (Aspect));
-               return;
-            end if;
-
-            Next (Aspect);
-         end loop;
-      end if;
-
-      --  Peek ahead of the instance and locate pragma SPARK_Mode. Even though
-      --  the pragma is analyzed after the instance, its mode must be known now
-      --  as it governs the legality of SPARK_Mode pragmas within the instance.
-
-      Decl := Empty;
-
-      --  The instance is a compilation unit, the pragma appears on the
-      --  Pragmas_After list.
-
-      if Present (Context)
-        and then Nkind (Context) = N_Compilation_Unit
-        and then Present (Aux_Decls_Node (Context))
-        and then Present (Pragmas_After (Aux_Decls_Node (Context)))
-      then
-         Decl := First (Pragmas_After (Aux_Decls_Node (Context)));
-
-      --  The instance is part of a declarative list, the pragma appears after
-      --  the instance.
-
-      elsif Is_List_Member (N) then
-         Decl := Next (N);
-      end if;
-
-      --  Inspect all declarations following the instance
-
-      while Present (Decl) loop
-         if Nkind (Decl) = N_Pragma then
-            if Get_Pragma_Id (Decl) = Pragma_SPARK_Mode then
-               Args := Pragma_Argument_Associations (Decl);
-
-               --  The pragma argument dictates the mode
-
-               if Present (Args) then
-                  Set_SPARK_Mode (Get_Pragma_Arg (First (Args)));
-               end if;
-
-               --  Only the first SPARK_Mode following the instance is
-               --  considered, any extra (illegal) pragmas are ignored.
-
-               exit;
-            end if;
-
-         --  Skip internally generated code
-
-         elsif not Comes_From_Source (Decl) then
-            null;
-
-         --  Otherwise a source construct exhaust the range where the pragma
-         --  may appear.
-
-         else
-            exit;
-         end if;
-
-         Next (Decl);
-      end loop;
-   end Set_Ignore_Pragma_SPARK_Mode;
-
    ------------------------
    -- Set_Name_Entity_Id --
    ------------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 9ac981e..b567e43 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1837,11 +1837,6 @@ package Sem_Util is
    --    If restriction No_Implementation_Identifiers is set, then it checks
    --    that the entity is not implementation defined.
 
-   procedure Set_Ignore_Pragma_SPARK_Mode (N : Node_Id);
-   --  Determine whether [the enclosing context of] package or subprogram N is
-   --  subject to pragma SPARK_Mode with mode "off". If this is the case, set
-   --  global flag Ignore_Pragma_SPARK_Mode to True.
-
    procedure Set_Name_Entity_Id (Id : Name_Id; Val : Entity_Id);
    pragma Inline (Set_Name_Entity_Id);
    --  Sets the Entity_Id value associated with the given name, which is the