[multiple changes]

2014-01-21  Robert Dewar  <dewar@adacore.com>

	* exp_aggr.adb: Minor reformatting.

2014-01-21  Johannes Kanig  <kanig@adacore.com>

	* gnat1drv.adb (Gnat1drv) remove obsolete reference to -gnatd.H.

2014-01-21  Bob Duff  <duff@adacore.com>

	* gnat_ugn.texi: Document the "checks" attribute in gnat2xml.

2014-01-21  Steve Baird  <baird@adacore.com>

	* gnat_rm.texi: Improve description of SPARK_Mode pragma.

2014-01-21  Vincent Celier  <celier@adacore.com>

	* prj-part.adb (Parse_Single_Project): Accept to extend a project
	if it has only be imported by an project being extended. When a
	project that has only been imported by a project being extended
	is imported by another project that is not being extended,
	reset the previous indication, so that it will be an error if
	this project is extended later.
	* prj-tree.adb (Create_Project): Include component From_Extended
	in table Projects_HT
	* prj-tree.ads (Project_Name_And_Node): New Boolean component
	From_Extended

2014-01-21  Robert Dewar  <dewar@adacore.com>

	* atree.ads, atree.adb: Add Node33 and Set_Node33.
	* einfo.ads, einfo.adb (SPARK_Pragma): New field (SPARK_Aux_Pragma):
	New field (SPARK_Pragma_Inherited): New flag
	(SPARK_Aux_Pragma_Inherited): New flag (SPARK_Mode_Pragmas):
	Removed.
	* lib.ads, lib.adb: Remove SPARK_Mode_Pragma, no longer used.
	* opt.ads (SPARK_Mode_Pragma): New global variable.
	* sem.ads: Add Save_SPARK_Mode_Pragma field to Scope_Stack_Entry.
	* sem_ch3.adb: Use new SPARK_Mode data structures.
	* sem_ch6.adb: Set SPARK_Mode fields in subprogram specs and bodies.
	* sem_ch7.adb: Set SPARK_Mode fields in package spec and body entities.
	* sem_ch8.adb (Push_Scope): Save SPARK_Mode_Pragma.
	(Pop_Scope): Restore SPARK_Mode_Pragma.
	* sem_prag.adb (Analyze_Pragma, case SPARK_Mode): Rewrite for
	new data structures.

2014-01-21  Arnaud Charlet  <charlet@adacore.com>

	* back_end.adb: Undo previous change, not needed. Minor reformatting.

From-SVN: r206879

22 files changed, 480 insertions, 259 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 859e5e0..8e93a32 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,54 @@
+2014-01-21  Robert Dewar  <dewar@adacore.com>
+
+	* exp_aggr.adb: Minor reformatting.
+
+2014-01-21  Johannes Kanig  <kanig@adacore.com>
+
+	* gnat1drv.adb (Gnat1drv) remove obsolete reference to -gnatd.H.
+
+2014-01-21  Bob Duff  <duff@adacore.com>
+
+	* gnat_ugn.texi: Document the "checks" attribute in gnat2xml.
+
+2014-01-21  Steve Baird  <baird@adacore.com>
+
+	* gnat_rm.texi: Improve description of SPARK_Mode pragma.
+
+2014-01-21  Vincent Celier  <celier@adacore.com>
+
+	* prj-part.adb (Parse_Single_Project): Accept to extend a project
+	if it has only be imported by an project being extended. When a
+	project that has only been imported by a project being extended
+	is imported by another project that is not being extended,
+	reset the previous indication, so that it will be an error if
+	this project is extended later.
+	* prj-tree.adb (Create_Project): Include component From_Extended
+	in table Projects_HT
+	* prj-tree.ads (Project_Name_And_Node): New Boolean component
+	From_Extended
+
+2014-01-21  Robert Dewar  <dewar@adacore.com>
+
+	* atree.ads, atree.adb: Add Node33 and Set_Node33.
+	* einfo.ads, einfo.adb (SPARK_Pragma): New field (SPARK_Aux_Pragma):
+	New field (SPARK_Pragma_Inherited): New flag
+	(SPARK_Aux_Pragma_Inherited): New flag (SPARK_Mode_Pragmas):
+	Removed.
+	* lib.ads, lib.adb: Remove SPARK_Mode_Pragma, no longer used.
+	* opt.ads (SPARK_Mode_Pragma): New global variable.
+	* sem.ads: Add Save_SPARK_Mode_Pragma field to Scope_Stack_Entry.
+	* sem_ch3.adb: Use new SPARK_Mode data structures.
+	* sem_ch6.adb: Set SPARK_Mode fields in subprogram specs and bodies.
+	* sem_ch7.adb: Set SPARK_Mode fields in package spec and body entities.
+	* sem_ch8.adb (Push_Scope): Save SPARK_Mode_Pragma.
+	(Pop_Scope): Restore SPARK_Mode_Pragma.
+	* sem_prag.adb (Analyze_Pragma, case SPARK_Mode): Rewrite for
+	new data structures.
+
+2014-01-21  Arnaud Charlet  <charlet@adacore.com>
+
+	* back_end.adb: Undo previous change, not needed. Minor reformatting.
+
 2014-01-21  Thomas Quinot  <quinot@adacore.com>
 
 	* exp_ch5.adb: Fix comment.
diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb
index 95b3132..44cad86 100644
--- a/gcc/ada/atree.adb
+++ b/gcc/ada/atree.adb
@@ -2595,6 +2595,12 @@ package body Atree is
          return Node_Id (Nodes.Table (N + 5).Field8);
       end Node32;
 
+      function Node33 (N : Node_Id) return Node_Id is
+      begin
+         pragma Assert (Nkind (N) in N_Entity);
+         return Node_Id (Nodes.Table (N + 5).Field9);
+      end Node33;
+
       function List1 (N : Node_Id) return List_Id is
       begin
          pragma Assert (N <= Nodes.Last);
@@ -5336,6 +5342,12 @@ package body Atree is
          Nodes.Table (N + 5).Field8 := Union_Id (Val);
       end Set_Node32;
 
+      procedure Set_Node33 (N : Node_Id; Val : Node_Id) is
+      begin
+         pragma Assert (Nkind (N) in N_Entity);
+         Nodes.Table (N + 5).Field9 := Union_Id (Val);
+      end Set_Node33;
+
       procedure Set_List1 (N : Node_Id; Val : List_Id) is
       begin
          pragma Assert (N <= Nodes.Last);
diff --git a/gcc/ada/atree.ads b/gcc/ada/atree.ads
index 415f96f..94fd5b2 100644
--- a/gcc/ada/atree.ads
+++ b/gcc/ada/atree.ads
@@ -1209,6 +1209,9 @@ package Atree is
       function Node32 (N : Node_Id) return Node_Id;
       pragma Inline (Node32);
 
+      function Node33 (N : Node_Id) return Node_Id;
+      pragma Inline (Node33);
+
       function List1 (N : Node_Id) return List_Id;
       pragma Inline (List1);
 
@@ -2509,6 +2512,9 @@ package Atree is
       procedure Set_Node32 (N : Node_Id; Val : Node_Id);
       pragma Inline (Set_Node32);
 
+      procedure Set_Node33 (N : Node_Id; Val : Node_Id);
+      pragma Inline (Set_Node33);
+
       procedure Set_List1 (N : Node_Id; Val : List_Id);
       pragma Inline (Set_List1);
 
diff --git a/gcc/ada/back_end.adb b/gcc/ada/back_end.adb
index 89cf303..0b8920d 100644
--- a/gcc/ada/back_end.adb
+++ b/gcc/ada/back_end.adb
@@ -183,7 +183,6 @@ package body Back_End is
    -----------------------------
 
    procedure Scan_Compiler_Arguments is
-
       Next_Arg : Positive;
       --  Next argument to be scanned
 
@@ -247,7 +246,6 @@ package body Back_End is
             elsif Switch_Chars (First .. Last) = "fdump-scos" then
                Opt.Generate_SCO := True;
                Opt.Generate_SCO_Instance_Table := True;
-
             end if;
          end if;
       end Scan_Back_End_Switches;
@@ -255,7 +253,7 @@ package body Back_End is
       --  Local variables
 
       Arg_Count : constant Natural := Natural (save_argc - 1);
-      Args : Argument_List (1 .. Arg_Count);
+      Args      : Argument_List (1 .. Arg_Count);
 
    --  Start of processing for Scan_Compiler_Arguments
 
@@ -271,7 +269,7 @@ package body Back_End is
             Argv_Ptr : constant Big_String_Ptr := save_argv (Arg);
             Argv_Len : constant Nat            := Len_Arg (Arg);
             Argv     : constant String         :=
-              Argv_Ptr (1 .. Natural (Argv_Len));
+                         Argv_Ptr (1 .. Natural (Argv_Len));
          begin
             Args (Positive (Arg)) := new String'(Argv);
          end;
@@ -289,20 +287,9 @@ package body Back_End is
             --  flag (that is we have seen a -gnatO), then the next argument
             --  is the name of the output object file.
 
-            if Output_File_Name_Present
-              and then not Output_File_Name_Seen
-            then
+            if Output_File_Name_Present and then not Output_File_Name_Seen then
                if Is_Switch (Argv) then
                   Fail ("Object file name missing after -gnatO");
-
-               --  In GNATprove_Mode, such an object file is never written, and
-               --  the call to Set_Output_Object_File_Name may fail (e.g. when
-               --  the object file name does not have the expected suffix). So
-               --  we skip that call when GNATprove_Mode is set.
-
-               elsif GNATprove_Mode then
-                  Output_File_Name_Seen := True;
-
                else
                   Set_Output_Object_File_Name (Argv);
                   Output_File_Name_Seen := True;
@@ -320,7 +307,9 @@ package body Back_End is
                   Search_Directory_Present := False;
                end if;
 
-            elsif not Is_Switch (Argv) then -- must be a file name
+            --  If not a switch, must be a file name
+
+            elsif not Is_Switch (Argv) then
                Add_File (Argv);
 
             --  We must recognize -nostdinc to suppress visibility on the
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 399afa8..45088b2 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -248,9 +248,9 @@ package body Einfo is
 
    --    Thunk_Entity                    Node31
 
-   --    SPARK_Mode_Pragmas              Node32
+   --    SPARK_Pragma                    Node32
 
-   --    (unused)                        Node33
+   --    SPARK_Aux_Pragma                Node33
 
    --    (unused)                        Node34
 
@@ -554,9 +554,9 @@ package body Einfo is
    --    May_Inherit_Delayed_Rep_Aspects Flag262
    --    Has_Visible_Refinement          Flag263
    --    Has_Body_References             Flag264
+   --    SPARK_Pragma_Inherited          Flag265
+   --    SPARK_Aux_Pragma_Inherited      Flag266
 
-   --    (unused)                        Flag265
-   --    (unused)                        Flag266
    --    (unused)                        Flag267
    --    (unused)                        Flag268
    --    (unused)                        Flag269
@@ -2835,7 +2835,25 @@ package body Einfo is
       return Ureal21 (Id);
    end Small_Value;
 
-   function SPARK_Mode_Pragmas (Id : E) return N is
+   function SPARK_Aux_Pragma (Id : E) return N is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+      return Node33 (Id);
+   end SPARK_Aux_Pragma;
+
+   function SPARK_Aux_Pragma_Inherited (Id : E) return B is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+      return Flag266 (Id);
+   end SPARK_Aux_Pragma_Inherited;
+
+   function SPARK_Pragma (Id : E) return N is
    begin
       pragma Assert
         (Ekind_In (Id, E_Function,         --  subprogram variants
@@ -2848,7 +2866,22 @@ package body Einfo is
                        E_Package,
                        E_Package_Body));
       return Node32 (Id);
-   end SPARK_Mode_Pragmas;
+   end SPARK_Pragma;
+
+   function SPARK_Pragma_Inherited (Id : E) return B is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Function,         --  subprogram variants
+                       E_Generic_Function,
+                       E_Generic_Procedure,
+                       E_Procedure,
+                       E_Subprogram_Body)
+           or else
+         Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+      return Flag265 (Id);
+   end SPARK_Pragma_Inherited;
 
    function Spec_Entity (Id : E) return E is
    begin
@@ -5527,7 +5560,27 @@ package body Einfo is
       Set_Ureal21 (Id, V);
    end Set_Small_Value;
 
-   procedure Set_SPARK_Mode_Pragmas (Id : E; V : N) is
+   procedure Set_SPARK_Aux_Pragma (Id : E; V : N) is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+
+      Set_Node33 (Id, V);
+   end Set_SPARK_Aux_Pragma;
+
+   procedure Set_SPARK_Aux_Pragma_Inherited (Id : E; V : B := True) is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+
+      Set_Flag266 (Id, V);
+   end Set_SPARK_Aux_Pragma_Inherited;
+
+   procedure Set_SPARK_Pragma (Id : E; V : N) is
    begin
       pragma Assert
         (Ekind_In (Id, E_Function,         --  subprogram variants
@@ -5541,7 +5594,23 @@ package body Einfo is
                        E_Package_Body));
 
       Set_Node32 (Id, V);
-   end Set_SPARK_Mode_Pragmas;
+   end Set_SPARK_Pragma;
+
+   procedure Set_SPARK_Pragma_Inherited (Id : E; V : B := True) is
+   begin
+      pragma Assert
+        (Ekind_In (Id, E_Function,         --  subprogram variants
+                       E_Generic_Function,
+                       E_Generic_Procedure,
+                       E_Procedure,
+                       E_Subprogram_Body)
+           or else
+         Ekind_In (Id, E_Generic_Package,  --  package variants
+                       E_Package,
+                       E_Package_Body));
+
+      Set_Flag265 (Id, V);
+   end Set_SPARK_Pragma_Inherited;
 
    procedure Set_Spec_Entity (Id : E; V : E) is
    begin
@@ -8227,6 +8296,8 @@ package body Einfo is
       W ("Sec_Stack_Needed_For_Return",     Flag167 (Id));
       W ("Size_Depends_On_Discriminant",    Flag177 (Id));
       W ("Size_Known_At_Compile_Time",      Flag92  (Id));
+      W ("SPARK_Aux_Pragma_Inherited",      Flag266 (Id));
+      W ("SPARK_Pragma_Inherited",          Flag265 (Id));
       W ("Static_Elaboration_Desired",      Flag77  (Id));
       W ("Strict_Alignment",                Flag145 (Id));
       W ("Suppress_Elaboration_Warnings",   Flag148 (Id));
@@ -9366,7 +9437,7 @@ package body Einfo is
               E_Package_Body                               |
               E_Procedure                                  |
               E_Subprogram_Body                            =>
-            Write_Str ("SPARK_Mode_Pragmas");
+            Write_Str ("SPARK_Pragma");
 
          when others                                       =>
             Write_Str ("Field32??");
@@ -9380,6 +9451,11 @@ package body Einfo is
    procedure Write_Field33_Name (Id : Entity_Id) is
    begin
       case Ekind (Id) is
+         when E_Generic_Package                            |
+              E_Package                                    |
+              E_Package_Body                               =>
+            Write_Str ("SPARK_Aux_Pragma");
+
          when others                                       =>
             Write_Str ("Field33??");
       end case;
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 9f4726c..fc710da 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -3801,10 +3801,35 @@ package Einfo is
 --       Small of the type, either as given in a representation clause, or
 --       as computed (as a power of two) by the compiler.
 
---    SPARK_Mode_Pragmas (Node32)
+--    SPARK_Aux_Pragma (Node33)
+--       Present in package spec and body entities. For a package spec entity
+--       it relates to the SPARK mode setting for the private part. This field
+--       points to the N_Pragma node that applies to the private part. This is
+--       either set with a local SPARK_Mode pragma in the private part or it is
+--       inherited from the SPARK mode that applies to the rest of the spec.
+--       For a package body, it similarly applies to the SPARK mode setting for
+--       the elaboration sequence after the BEGIN. In the case where the pragma
+--       is inherited, the SPARK_Aux_Pragma_Inherited flag is set in the
+--       package spec or body entity.
+
+--    SPARK_Aux_Pragma_Inherited (Flag266)
+--       Present in the entities of subprogram specs and bodies as well as
+--       in package specs and bodies. Set if the SPARK_Aux_Pragma field
+--       points to a pragma that is inherited, rather than a local one.
+
+--    SPARK_Pragma (Node32)
 --       Present in the entities of subprogram specs and bodies as well as in
---       package specs and bodies. Points to a list of SPARK_Mode pragmas that
---       apply to the related construct. Add note of what this is used for ???
+--       package specs and bodies. Points to the N_Pragma node that applies to
+--       the spec or body. This is either set by a local SPARK_Mode pragma or
+--       is inherited from the context (from an outer scope for the spec case
+--       or from the spec for the body case). In the case where it is inherited
+--       the flag SPARK_Pragma_Inherited is set. Empty if no SPARK_Mode pragma
+--       is applicable.
+
+--    SPARK_Pragma_Inherited (Flag265)
+--       Present in the entities of subprogram specs and bodies as well as in
+--       package specs and bodies. Set if the SPARK_Pragma field points to a
+--       pragma that is inherited, rather than a local one.
 
 --    Spec_Entity (Node19)
 --       Defined in package body entities. Points to corresponding package
@@ -5455,7 +5480,7 @@ package Einfo is
    --    Subprograms_For_Type                (Node29)
    --    Corresponding_Equality              (Node30)   (implicit /= only)
    --    Thunk_Entity                        (Node31)   (thunk case only)
-   --    SPARK_Mode_Pragmas                  (Node32)
+   --    SPARK_Pragma                        (Node32)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Elaboration_Entity_Required         (Flag174)
    --    Default_Expressions_Processed       (Flag108)
@@ -5493,6 +5518,7 @@ package Einfo is
    --    Return_Present                      (Flag54)
    --    Returns_By_Ref                      (Flag90)
    --    Sec_Stack_Needed_For_Return         (Flag167)
+   --    SPARK_Pragma_Inherited              (Flag265)
    --    Uses_Sec_Stack                      (Flag95)
    --    Address_Clause                      (synth)
    --    First_Formal                        (synth)
@@ -5655,7 +5681,8 @@ package Einfo is
    --    Package_Instantiation               (Node26)
    --    Current_Use_Clause                  (Node27)
    --    Finalizer                           (Node28)   (non-generic case only)
-   --    SPARK_Mode_Pragmas                  (Node32)
+   --    SPARK_Aux_Pragma                    (Node33)
+   --    SPARK_Pragma                        (Node32)
    --    Delay_Subprogram_Descriptors        (Flag50)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Discard_Names                       (Flag88)
@@ -5674,6 +5701,8 @@ package Einfo is
    --    Is_Private_Descendant               (Flag53)
    --    Is_Visible_Lib_Unit                 (Flag116)
    --    Renamed_In_Spec                     (Flag231)  (non-generic case only)
+   --    SPARK_Aux_Pragma_Inherited          (Flag266)
+   --    SPARK_Pragma_Inherited              (Flag265)
    --    Static_Elaboration_Desired          (Flag77)   (non-generic case only)
    --    Has_Null_Abstract_State             (synth)
    --    Is_Wrapper_Package                  (synth)    (non-generic case only)
@@ -5688,9 +5717,12 @@ package Einfo is
    --    Scope_Depth_Value                   (Uint22)
    --    Contract                            (Node24)
    --    Finalizer                           (Node28)   (non-generic case only)
-   --    SPARK_Mode_Pragmas                  (Node32)
+   --    SPARK_Aux_Pragma                    (Node33)
+   --    SPARK_Pragma                        (Node32)
    --    Delay_Subprogram_Descriptors        (Flag50)
    --    Has_Anonymous_Master                (Flag253)
+   --    SPARK_Aux_Pragma_Inherited          (Flag266)
+   --    SPARK_Pragma_Inherited              (Flag265)
    --    Scope_Depth                         (synth)
 
    --  E_Private_Type
@@ -5735,7 +5767,7 @@ package Einfo is
    --    Extra_Formals                       (Node28)
    --    Static_Initialization               (Node30)   (init_proc only)
    --    Thunk_Entity                        (Node31)   (thunk case only)
-   --    SPARK_Mode_Pragmas                  (Node32)
+   --    SPARK_Pragma                        (Node32)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Delay_Cleanups                      (Flag114)
    --    Discard_Names                       (Flag88)
@@ -5774,6 +5806,7 @@ package Einfo is
    --    No_Return                           (Flag113)
    --    Requires_Overriding                 (Flag213)  (non-generic case only)
    --    Sec_Stack_Needed_For_Return         (Flag167)
+   --    SPARK_Pragma_Inherited              (Flag265)
    --    Address_Clause                      (synth)
    --    First_Formal                        (synth)
    --    First_Formal_With_Extras            (synth)
@@ -5907,7 +5940,8 @@ package Einfo is
    --    Scope_Depth_Value                   (Uint22)
    --    Contract                            (Node24)
    --    Extra_Formals                       (Node28)
-   --    SPARK_Mode_Pragmas                  (Node32)
+   --    SPARK_Pragma                        (Node32)
+   --    SPARK_Pragma_Inherited              (Flag265)
    --    Scope_Depth                         (synth)
 
    --  E_Subprogram_Type
@@ -6609,7 +6643,10 @@ package Einfo is
    function Size_Depends_On_Discriminant        (Id : E) return B;
    function Size_Known_At_Compile_Time          (Id : E) return B;
    function Small_Value                         (Id : E) return R;
-   function SPARK_Mode_Pragmas                  (Id : E) return N;
+   function SPARK_Aux_Pragma                    (Id : E) return N;
+   function SPARK_Aux_Pragma_Inherited          (Id : E) return B;
+   function SPARK_Pragma                        (Id : E) return N;
+   function SPARK_Pragma_Inherited              (Id : E) return B;
    function Spec_Entity                         (Id : E) return E;
    function Static_Elaboration_Desired          (Id : E) return B;
    function Static_Initialization               (Id : E) return N;
@@ -7232,7 +7269,10 @@ package Einfo is
    procedure Set_Size_Depends_On_Discriminant    (Id : E; V : B := True);
    procedure Set_Size_Known_At_Compile_Time      (Id : E; V : B := True);
    procedure Set_Small_Value                     (Id : E; V : R);
-   procedure Set_SPARK_Mode_Pragmas              (Id : E; V : N);
+   procedure Set_SPARK_Aux_Pragma                (Id : E; V : N);
+   procedure Set_SPARK_Aux_Pragma_Inherited      (Id : E; V : B := True);
+   procedure Set_SPARK_Pragma                    (Id : E; V : N);
+   procedure Set_SPARK_Pragma_Inherited          (Id : E; V : B := True);
    procedure Set_Spec_Entity                     (Id : E; V : E);
    procedure Set_Static_Elaboration_Desired      (Id : E; V : B);
    procedure Set_Static_Initialization           (Id : E; V : N);
@@ -7994,7 +8034,10 @@ package Einfo is
    pragma Inline (Size_Depends_On_Discriminant);
    pragma Inline (Size_Known_At_Compile_Time);
    pragma Inline (Small_Value);
-   pragma Inline (SPARK_Mode_Pragmas);
+   pragma Inline (SPARK_Aux_Pragma);
+   pragma Inline (SPARK_Aux_Pragma_Inherited);
+   pragma Inline (SPARK_Pragma);
+   pragma Inline (SPARK_Pragma_Inherited);
    pragma Inline (Spec_Entity);
    pragma Inline (Static_Elaboration_Desired);
    pragma Inline (Static_Initialization);
@@ -8414,7 +8457,10 @@ package Einfo is
    pragma Inline (Set_Size_Depends_On_Discriminant);
    pragma Inline (Set_Size_Known_At_Compile_Time);
    pragma Inline (Set_Small_Value);
-   pragma Inline (Set_SPARK_Mode_Pragmas);
+   pragma Inline (Set_SPARK_Aux_Pragma);
+   pragma Inline (Set_SPARK_Aux_Pragma_Inherited);
+   pragma Inline (Set_SPARK_Pragma);
+   pragma Inline (Set_SPARK_Pragma_Inherited);
    pragma Inline (Set_Spec_Entity);
    pragma Inline (Set_Static_Elaboration_Desired);
    pragma Inline (Set_Static_Initialization);
diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb
index 1492650..6147001 100644
--- a/gcc/ada/exp_aggr.adb
+++ b/gcc/ada/exp_aggr.adb
@@ -1164,8 +1164,8 @@ package body Exp_Aggr is
             elsif Is_Access_Type (Ctype) then
                Append_To (L,
                   Make_Assignment_Statement (Loc,
-                     Name => Indexed_Comp,
-                     Expression => Make_Null (Loc)));
+                    Name       => Indexed_Comp,
+                    Expression => Make_Null (Loc)));
             end if;
 
             if Needs_Finalization (Ctype) then
@@ -1205,14 +1205,15 @@ package body Exp_Aggr is
             --  assignment in a block.
 
             if Present (Comp_Type)
-                 and then Needs_Finalization (Comp_Type)
-                 and then Is_Array_Type (Comp_Type)
-                 and then Present (Expr)
+              and then Needs_Finalization (Comp_Type)
+              and then Is_Array_Type (Comp_Type)
+              and then Present (Expr)
             then
-               A := Make_Block_Statement (Loc,
-                      Handled_Statement_Sequence =>
-                        Make_Handled_Sequence_Of_Statements (Loc,
-                           Statements => New_List (A)));
+               A :=
+                 Make_Block_Statement (Loc,
+                   Handled_Statement_Sequence =>
+                     Make_Handled_Sequence_Of_Statements (Loc,
+                       Statements => New_List (A)));
             end if;
 
             Append_To (L, A);
@@ -1231,9 +1232,9 @@ package body Exp_Aggr is
                begin
                   A :=
                     Make_OK_Assignment_Statement (Loc,
-                      Name =>
+                      Name       =>
                         Make_Selected_Component (Loc,
-                          Prefix =>  New_Copy_Tree (Indexed_Comp),
+                          Prefix        =>  New_Copy_Tree (Indexed_Comp),
                           Selector_Name =>
                             New_Reference_To
                               (First_Tag_Component (Full_Typ), Loc)),
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 91f846e..e95cbb3 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -858,34 +858,9 @@ begin
       Original_Operating_Mode := Operating_Mode;
       Frontend;
 
-      --  Exit with errors if the main source could not be parsed. Also, when
-      --  -gnatd.H is present, the source file is not set.
+      --  Exit with errors if the main source could not be parsed.
 
       if Sinput.Main_Source_File = No_Source_File then
-
-         --  Handle -gnatd.H debug mode
-
-         if Debug_Flag_Dot_HH then
-
-            --  For -gnatd.H, lock all the tables to keep the convention that
-            --  the backend needs to unlock the tables it wants to touch.
-
-            Atree.Lock;
-            Elists.Lock;
-            Fname.UF.Lock;
-            Inline.Lock;
-            Lib.Lock;
-            Nlists.Lock;
-            Sem.Lock;
-            Sinput.Lock;
-            Namet.Lock;
-            Stringt.Lock;
-
-            --  And all we need to do is to call the back end
-
-            Back_End.Call_Back_End (Back_End.Generate_Object);
-         end if;
-
          Errout.Finalize (Last_Call => True);
          Errout.Output_Messages;
          Exit_Program (E_Errors);
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index d9bee98..146936c 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -6287,7 +6287,8 @@ an implicit argument of On is assumed.
 
 A SPARK_Mode pragma may be used as a configuration pragma and then has the
 semantics described below. A SPARK_Mode pragma which is not used as a
-configuration pragma shall not have an argument of Auto.
+configuration pragma (or an equivalent SPARK_Mode aspect_specification)
+shall not have an argument of Auto.
 
 A SPARK_Mode pragma can be used as a local pragma only
 in the following contexts:
diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi
index c17ca38..58b7e71 100644
--- a/gcc/ada/gnat_ugn.texi
+++ b/gcc/ada/gnat_ugn.texi
@@ -15393,6 +15393,17 @@ mode indicates that the parameter is of mode 'in', 'in out', or 'out'.
 @end itemize
 
 @noindent
+All elements other than Not_An_Element have this attribute:
+
+@itemize @bullet
+@item
+checks is a comma-separated list of run-time checks that are needed
+for that element. The possible checks are: do_accessibility_check,
+do_discriminant_check,do_division_check,do_length_check,
+do_overflow_check,do_range_check,do_storage_check,do_tag_check.
+@end itemize
+
+@noindent
 The "kind" part of the "def" and "ref" attributes is taken from the ASIS
 enumeration type Flat_Declaration_Kinds, declared in
 Asis.Extensions.Flat_Kinds, with the leading "An_" or "A_" removed, and
diff --git a/gcc/ada/lib.adb b/gcc/ada/lib.adb
index e220b20..b43ad98 100644
--- a/gcc/ada/lib.adb
+++ b/gcc/ada/lib.adb
@@ -166,11 +166,6 @@ package body Lib is
       return Units.Table (U).Source_Index;
    end Source_Index;
 
-   function SPARK_Mode_Pragma (U : Unit_Number_Type) return Node_Id is
-   begin
-      return Units.Table (U).SPARK_Mode_Pragma;
-   end SPARK_Mode_Pragma;
-
    function Unit_File_Name (U : Unit_Number_Type) return File_Name_Type is
    begin
       return Units.Table (U).Unit_File_Name;
@@ -259,11 +254,6 @@ package body Lib is
       Units.Table (U).OA_Setting := C;
    end Set_OA_Setting;
 
-   procedure Set_SPARK_Mode_Pragma (U : Unit_Number_Type; N : Node_Id) is
-   begin
-      Units.Table (U).SPARK_Mode_Pragma := N;
-   end Set_SPARK_Mode_Pragma;
-
    procedure Set_Unit_Name (U : Unit_Number_Type; N : Unit_Name_Type) is
    begin
       Units.Table (U).Unit_Name := N;
diff --git a/gcc/ada/lib.ads b/gcc/ada/lib.ads
index 5370e4a..00959cd 100644
--- a/gcc/ada/lib.ads
+++ b/gcc/ada/lib.ads
@@ -371,10 +371,6 @@ package Lib is
    --      Set when the entry is created by a call to Lib.Load and then cannot
    --      be changed.
 
-   --    SPARK_Mode_Pragma
-   --      Pointer to the configuration pragma SPARK_Mode that applies to the
-   --      whole unit. Add note of what this is used for ???
-
    --    Unit_File_Name
    --      The name of the source file containing the unit. Set when the entry
    --      is created by a call to Lib.Load, and then cannot be changed.
@@ -426,7 +422,6 @@ package Lib is
    function Munit_Index       (U : Unit_Number_Type) return Nat;
    function OA_Setting        (U : Unit_Number_Type) return Character;
    function Source_Index      (U : Unit_Number_Type) return Source_File_Index;
-   function SPARK_Mode_Pragma (U : Unit_Number_Type) return Node_Id;
    function Unit_File_Name    (U : Unit_Number_Type) return File_Name_Type;
    function Unit_Name         (U : Unit_Number_Type) return Unit_Name_Type;
    --  Get value of named field from given units table entry
@@ -445,7 +440,6 @@ package Lib is
    procedure Set_Main_CPU          (U : Unit_Number_Type; P : Int);
    procedure Set_Main_Priority     (U : Unit_Number_Type; P : Int);
    procedure Set_OA_Setting        (U : Unit_Number_Type; C : Character);
-   procedure Set_SPARK_Mode_Pragma (U : Unit_Number_Type; N : Node_Id);
    procedure Set_Unit_Name         (U : Unit_Number_Type; N : Unit_Name_Type);
    --  Set value of named field for given units table entry. Note that we
    --  do not have an entry for each possible field, since some of the fields
@@ -749,10 +743,8 @@ private
    pragma Inline (Set_Main_CPU);
    pragma Inline (Set_Main_Priority);
    pragma Inline (Set_OA_Setting);
-   pragma Inline (Set_SPARK_Mode_Pragma);
    pragma Inline (Set_Unit_Name);
    pragma Inline (Source_Index);
-   pragma Inline (SPARK_Mode_Pragma);
    pragma Inline (Unit_File_Name);
    pragma Inline (Unit_Name);
 
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 11de156..05cea8a 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -1,5 +1,5 @@
 ------------------------------------------------------------------------------
---                                SPARK                                          --
+--                                                                          --
 --                         GNAT COMPILER COMPONENTS                         --
 --                                                                          --
 --                                  O P T                                   --
@@ -1272,6 +1272,11 @@ package Opt is
    --  GNAT
    --  Current SPARK mode setting
 
+   SPARK_Mode_Pragma : Node_Id := Empty;
+   --  GNAT
+   --  If the current SPARK_Mode (above) was set by a pragma, this records
+   --  the pragma that set this mode.
+
    SPARK_Switches_File_Name : String_Ptr := null;
    --  GNAT
    --  Set to non-null file name by use of the -gnates switch to specify
@@ -1909,8 +1914,13 @@ package Opt is
    --  start of analyzing each unit.
 
    SPARK_Mode_Config : SPARK_Mode_Type := None;
+   --  GNAT
    --  The setting of SPARK_Mode from configuration pragmas
 
+   SPARK_Mode_Pragma_Config : Node_Id := Empty;
+   --  If a SPARK_Mode pragma appeared in the configuration pragmas (setting
+   --  SPARK_Mode_Config appropriately), then this points to the N_Pragma node.
+
    Use_VADS_Size_Config : Boolean;
    --  GNAT
    --  This is the value of the configuration switch that controls the use of
@@ -2056,6 +2066,7 @@ private
       Polling_Required               : Boolean;
       Short_Descriptors              : Boolean;
       SPARK_Mode                     : SPARK_Mode_Type;
+      SPARK_Mode_Pragma              : Node_Id;
       Use_VADS_Size                  : Boolean;
    end record;
 
diff --git a/gcc/ada/prj-part.adb b/gcc/ada/prj-part.adb
index 7f617a0..ffcd69a 100644
--- a/gcc/ada/prj-part.adb
+++ b/gcc/ada/prj-part.adb
@@ -1325,11 +1325,20 @@ package body Prj.Part is
                         "cannot extend the same project file several times",
                         Token_Ptr);
                   end if;
-               else
+               elsif not A_Project_Name_And_Node.From_Extended then
                   Error_Msg
                     (Env.Flags,
                      "cannot extend an already imported project file",
                      Token_Ptr);
+
+               else
+                  --  Register this project as being extended
+
+                  A_Project_Name_And_Node.Extended := True;
+                  Tree_Private_Part.Projects_Htable.Set
+                    (In_Tree.Projects_HT,
+                     A_Project_Name_And_Node.Name,
+                     A_Project_Name_And_Node);
                end if;
 
             elsif A_Project_Name_And_Node.Extended then
@@ -1372,6 +1381,16 @@ package body Prj.Part is
                      "cannot import an already extended project file",
                      Token_Ptr);
                end if;
+
+            elsif A_Project_Name_And_Node.From_Extended then
+               --  This project is now imported from a non extending project.
+               --  Indicate this in has table Projects.HT.
+
+               A_Project_Name_And_Node.From_Extended := False;
+               Tree_Private_Part.Projects_Htable.Set
+                 (In_Tree.Projects_HT,
+                  A_Project_Name_And_Node.Name,
+                  A_Project_Name_And_Node);
             end if;
 
             Project := A_Project_Name_And_Node.Node;
@@ -1933,6 +1952,7 @@ package body Prj.Part is
                   Node           => Project,
                   Canonical_Path => Canonical_Path_Name,
                   Extended       => Extended,
+                  From_Extended  => From_Extended /= None,
                   Proj_Qualifier => Project_Qualifier_Of (Project, In_Tree)));
       end if;
 
diff --git a/gcc/ada/prj-tree.adb b/gcc/ada/prj-tree.adb
index c121521..13abf83 100644
--- a/gcc/ada/prj-tree.adb
+++ b/gcc/ada/prj-tree.adb
@@ -1321,8 +1321,7 @@ package body Prj.Tree is
    begin
       pragma Assert
         (Present (Node)
-          and then
-            In_Tree.Project_Nodes.Table (Node).Kind = N_Term);
+          and then In_Tree.Project_Nodes.Table (Node).Kind = N_Term);
       return In_Tree.Project_Nodes.Table (Node).Field2;
    end Next_Term;
 
@@ -1332,18 +1331,17 @@ package body Prj.Tree is
 
    function Next_Variable
      (Node    : Project_Node_Id;
-      In_Tree : Project_Node_Tree_Ref)
-      return Project_Node_Id
+      In_Tree : Project_Node_Tree_Ref) return Project_Node_Id
    is
    begin
       pragma Assert
         (Present (Node)
           and then
-           (In_Tree.Project_Nodes.Table (Node).Kind =
-              N_Typed_Variable_Declaration
+            (In_Tree.Project_Nodes.Table (Node).Kind =
+                                                  N_Typed_Variable_Declaration
                or else
-            In_Tree.Project_Nodes.Table (Node).Kind =
-              N_Variable_Declaration));
+             In_Tree.Project_Nodes.Table (Node).Kind =
+                                                  N_Variable_Declaration));
 
       return In_Tree.Project_Nodes.Table (Node).Field3;
    end Next_Variable;
@@ -2925,6 +2923,7 @@ package body Prj.Tree is
                Canonical_Path => No_Path,
                Node           => Project,
                Extended       => False,
+               From_Extended  => False,
                Proj_Qualifier => Qualifier));
       end if;
 
diff --git a/gcc/ada/prj-tree.ads b/gcc/ada/prj-tree.ads
index 0d585a3..7859d4a 100644
--- a/gcc/ada/prj-tree.ads
+++ b/gcc/ada/prj-tree.ads
@@ -1476,6 +1476,10 @@ package Prj.Tree is
          Extended : Boolean;
          --  True when the project is being extended by another project
 
+         From_Extended : Boolean;
+         --  True when the project is only imported by projects that are
+         --  extended.
+
          Proj_Qualifier : Project_Qualifier;
          --  The project qualifier of the project, if any
       end record;
@@ -1486,6 +1490,7 @@ package Prj.Tree is
          Node           => Empty_Node,
          Canonical_Path => No_Path,
          Extended       => True,
+         From_Extended  => False,
          Proj_Qualifier => Unspecified);
 
       package Projects_Htable is new GNAT.Dynamic_HTables.Simple_HTable
diff --git a/gcc/ada/sem.ads b/gcc/ada/sem.ads
index c6b11db..3430818 100644
--- a/gcc/ada/sem.ads
+++ b/gcc/ada/sem.ads
@@ -478,6 +478,9 @@ package Sem is
       Save_SPARK_Mode : SPARK_Mode_Type;
       --  Setting of SPARK_Mode on entry to restore on exit
 
+      Save_SPARK_Mode_Pragma : Node_Id;
+      --  Setting of SPARK_Mode_Pragma on entry to restore on exit
+
       Is_Transient : Boolean;
       --  Marks transient scopes (see Exp_Ch7 body for details)
 
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index ffc233d..c1b9435 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -2162,15 +2162,15 @@ package body Sem_Ch3 is
          --  it is and the mode is Off, the package body is considered to be in
          --  regular Ada and does not require refinement.
 
-         elsif Mode_Is_Off (SPARK_Mode_Pragmas (Body_Id)) then
+         elsif Mode_Is_Off (SPARK_Pragma (Body_Id)) then
             return False;
 
          --  The body's SPARK_Mode may be inherited from a similar pragma that
          --  appears in the private declarations of the spec. The pragma we are
-         --  interested appears as the second entry in SPARK_Mode_Pragmas.
+         --  interested appears as the second entry in SPARK_Pragma.
 
-         elsif Present (SPARK_Mode_Pragmas (Spec_Id))
-           and then Mode_Is_Off (Next_Pragma (SPARK_Mode_Pragmas (Spec_Id)))
+         elsif Present (SPARK_Pragma (Spec_Id))
+           and then Mode_Is_Off (Next_Pragma (SPARK_Pragma (Spec_Id)))
          then
             return False;
 
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 1120c60..078b771 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -1186,6 +1186,9 @@ package body Sem_Ch6 is
             end loop;
          end;
 
+         Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+         Set_SPARK_Pragma_Inherited (Body_Id, True);
+
          Analyze_Declarations (Declarations (N));
          Check_Completion;
          Analyze (Handled_Statement_Sequence (N));
@@ -2923,6 +2926,8 @@ package body Sem_Ch6 is
             Reference_Body_Formals (Spec_Id, Body_Id);
          end if;
 
+         Set_Ekind (Body_Id, E_Subprogram_Body);
+
          if Nkind (N) = N_Subprogram_Body_Stub then
             Set_Corresponding_Spec_Of_Stub (N, Spec_Id);
 
@@ -2989,9 +2994,17 @@ package body Sem_Ch6 is
 
             --  Set SPARK_Mode from spec if spec had a SPARK_Mode pragma
 
-            if Present (SPARK_Mode_Pragmas (Spec_Id)) then
-               SPARK_Mode :=
-                 Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragmas (Spec_Id));
+            if Present (SPARK_Pragma (Spec_Id)) then
+               SPARK_Mode_Pragma := SPARK_Pragma (Spec_Id);
+               SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragma);
+               Set_SPARK_Pragma (Body_Id, SPARK_Pragma (Spec_Id));
+               Set_SPARK_Pragma_Inherited (Body_Id, True);
+
+            --  Otherwise set from context
+
+            else
+               Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+               Set_SPARK_Pragma_Inherited (Body_Id, True);
             end if;
 
             --  Make sure that the subprogram is immediately visible. For
@@ -3003,7 +3016,6 @@ package body Sem_Ch6 is
 
          Set_Corresponding_Body (Unit_Declaration_Node (Spec_Id), Body_Id);
          Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id)));
-         Set_Ekind (Body_Id, E_Subprogram_Body);
          Set_Scope (Body_Id, Scope (Spec_Id));
          Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Spec_Id));
 
@@ -3550,8 +3562,9 @@ package body Sem_Ch6 is
    ------------------------------------
 
    procedure Analyze_Subprogram_Declaration (N : Node_Id) is
-      Scop       : constant Entity_Id  := Current_Scope;
+      Scop       : constant Entity_Id := Current_Scope;
       Designator : Entity_Id;
+
       Is_Completion : Boolean;
       --  Indicates whether a null procedure declaration is a completion
 
@@ -3585,6 +3598,9 @@ package body Sem_Ch6 is
 
       Generate_Definition (Designator);
 
+      Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
+      Set_SPARK_Pragma_Inherited (Designator, True);
+
       if Debug_Flag_C then
          Write_Str ("==> subprogram spec ");
          Write_Name (Chars (Designator));
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index 30704ff..322785a 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.adb
@@ -346,13 +346,29 @@ package body Sem_Ch7 is
 
       Push_Scope (Spec_Id);
 
-      --  Set SPARK_Mode from spec if package spec had SPARK_Mode pragma
+      --  Set SPARK_Mode from private part of spec if it has a SPARK pragma.
+      --  Note that in the default case, SPARK_Aux_Pragma will be a copy of
+      --  SPARK_Pragma in the spec, so this properly handles the case where
+      --  there is no explicit SPARK_Pragma mode in the private part.
 
-      if Present (SPARK_Mode_Pragmas (Spec_Id)) then
-         SPARK_Mode :=
-           Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragmas (Spec_Id));
+      if Present (SPARK_Pragma (Spec_Id)) then
+         SPARK_Mode_Pragma := SPARK_Aux_Pragma (Spec_Id);
+         SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragma);
+         Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+         Set_SPARK_Pragma_Inherited (Body_Id, True);
+
+      --  Otherwise set from context
+
+      else
+         Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+         Set_SPARK_Pragma_Inherited (Body_Id, True);
       end if;
 
+      --  Set elaboration code SPARK mode the same for now
+
+      Set_SPARK_Aux_Pragma (Body_Id, SPARK_Pragma (Body_Id));
+      Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
+
       Set_Categorization_From_Pragmas (N);
 
       Install_Visible_Declarations (Spec_Id);
@@ -798,6 +814,13 @@ package body Sem_Ch7 is
       Set_Etype    (Id, Standard_Void_Type);
       Set_Contract (Id, Make_Contract (Sloc (Id)));
 
+      --  Inherit spark mode from context for now
+
+      Set_SPARK_Pragma               (Id, SPARK_Mode_Pragma);
+      Set_SPARK_Aux_Pragma           (Id, SPARK_Mode_Pragma);
+      Set_SPARK_Pragma_Inherited     (Id, True);
+      Set_SPARK_Aux_Pragma_Inherited (Id, True);
+
       --  Analyze aspect specifications immediately, since we need to recognize
       --  things like Pure early enough to diagnose violations during analysis.
 
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index 792b85f..070d38a 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -7400,6 +7400,7 @@ package body Sem_Ch8 is
       Check_Policy_List        := SST.Save_Check_Policy_List;
       Default_Pool             := SST.Save_Default_Storage_Pool;
       SPARK_Mode               := SST.Save_SPARK_Mode;
+      SPARK_Mode_Pragma        := SST.Save_SPARK_Mode_Pragma;
 
       if Debug_Flag_W then
          Write_Str ("<-- exiting scope: ");
@@ -7474,6 +7475,7 @@ package body Sem_Ch8 is
          SST.Save_Check_Policy_List        := Check_Policy_List;
          SST.Save_Default_Storage_Pool     := Default_Pool;
          SST.Save_SPARK_Mode               := SPARK_Mode;
+         SST.Save_SPARK_Mode_Pragma        := SPARK_Mode_Pragma;
 
          if Scope_Stack.Last > Scope_Stack.First then
             SST.Component_Alignment_Default := Scope_Stack.Table
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 399753a..937ca4b 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -18056,116 +18056,58 @@ package body Sem_Prag is
          --  pragma SPARK_Mode [(On | Off | Auto)];
 
          when Pragma_SPARK_Mode => SPARK_Mod : declare
-            procedure Chain_Pragma (Context : Entity_Id; Prag : Node_Id);
-            --  Associate a SPARK_Mode pragma with the context where it lives.
-            --  If the context is a package spec or a body, the routine checks
-            --  the consistency between modes of visible/private declarations
-            --  and body declarations/statements.
-
-            procedure Check_Spark_Mode_Conformance
-              (Governing_Id : Entity_Id;
-               New_Id       : Entity_Id);
-            --  Verify the "monotonicity" of SPARK modes between two entities.
-            --  The order of modes is Off < Auto < On. Governing_Id establishes
-            --  the mode of the context. New_Id is the desired new mode.
-
-            procedure Check_Pragma_Conformance
-              (Governing_Mode : Node_Id;
-               New_Mode       : Node_Id);
-            --  Verify the "monotonicity" of two SPARK_Mode pragmas. The order
-            --  of modes is Off < Auto < On. Governing_Mode is the established
-            --  mode dictated by the context. New_Mode attempts to redefine the
-            --  governing mode.
+            Body_Id : Entity_Id;
+            Context : Node_Id;
+            Mode    : Name_Id;
+            Mode_Id : SPARK_Mode_Type;
+            Spec_Id : Entity_Id;
+            Stmt    : Node_Id;
+
+            procedure Check_Pragma_Conformance (Old_Pragma : Node_Id);
+            --  Verify the monotonicity of SPARK modes between the new pragma
+            --  N, and the old pragma, Old_Pragma, that was inherited. If
+            --  Old_Pragma is Empty, the call has no effect, otherwise we
+            --  verify that the new mode is less restrictive than the old mode.
+            --  For example, if the old mode is ON, then the new mode can be
+            --  anything. But if the old mode is OFF, then the only allowed
+            --  new mode is also OFF. If there is no error, this routine also
+            --  sets SPARK_Mode_Pragma to N, and SPARK_Mode to Mode_Id.
 
             function Get_SPARK_Mode_Name (Id : SPARK_Mode_Type) return Name_Id;
             --  Convert a value of type SPARK_Mode_Type to corresponding name
 
-            ------------------
-            -- Chain_Pragma --
-            ------------------
-
-            procedure Chain_Pragma (Context : Entity_Id; Prag : Node_Id) is
-               Existing_Prag : constant Node_Id :=
-                                 SPARK_Mode_Pragmas (Context);
-
-            begin
-               --  Chain existing pragmas to this one, checking consistency
-
-               if Present (Existing_Prag) then
-                  Check_Pragma_Conformance
-                    (Governing_Mode => Existing_Prag,
-                     New_Mode       => Prag);
-
-                  Set_Next_Pragma (Prag, Existing_Prag);
-               end if;
-
-               Set_SPARK_Mode_Pragmas (Context, Prag);
-            end Chain_Pragma;
-
-            ----------------------------------
-            -- Check_Spark_Mode_Conformance --
-            ----------------------------------
-
-            procedure Check_Spark_Mode_Conformance
-              (Governing_Id : Entity_Id;
-               New_Id       : Entity_Id)
-            is
-               Gov_Prag : constant Node_Id :=
-                            SPARK_Mode_Pragmas (Governing_Id);
-               New_Prag : constant Node_Id := SPARK_Mode_Pragmas (New_Id);
-
-            begin
-               --  Nothing to do when one or both entities lack a mode
-
-               if No (Gov_Prag) or else No (New_Prag) then
-                  return;
-               end if;
-
-               --  Do not compare the modes of a package spec and body when the
-               --  spec mode appears in the private part. In this case the spec
-               --  mode does not affect the body.
-
-               if Ekind_In (Governing_Id, E_Generic_Package, E_Package)
-                 and then Ekind (New_Id) = E_Package_Body
-                 and then Is_Private_SPARK_Mode (Gov_Prag)
-               then
-                  null;
-
-               --  Test the pragmas
-
-               else
-                  Check_Pragma_Conformance
-                    (Governing_Mode => Gov_Prag,
-                     New_Mode       => New_Prag);
-               end if;
-            end Check_Spark_Mode_Conformance;
-
             ------------------------------
             -- Check_Pragma_Conformance --
             ------------------------------
 
-            procedure Check_Pragma_Conformance
-              (Governing_Mode : Node_Id;
-               New_Mode       : Node_Id)
-            is
-               Gov_M : constant SPARK_Mode_Type :=
-                         Get_SPARK_Mode_From_Pragma (Governing_Mode);
-               New_M : constant SPARK_Mode_Type :=
-                         Get_SPARK_Mode_From_Pragma (New_Mode);
-
+            procedure Check_Pragma_Conformance (Old_Pragma : Node_Id) is
             begin
-               --  The new mode is less restrictive than the established mode
+               if Present (Old_Pragma) then
+                  pragma Assert (Nkind (Old_Pragma) = N_Pragma);
 
-               if Gov_M < New_M then
-                  Error_Msg_Name_1 := Get_SPARK_Mode_Name (New_M);
-                  Error_Msg_N ("cannot define 'S'P'A'R'K mode %", New_Mode);
+                  declare
+                     Gov_M : constant SPARK_Mode_Type :=
+                                Get_SPARK_Mode_From_Pragma (Old_Pragma);
 
-                  Error_Msg_Name_1 := Get_SPARK_Mode_Name (Gov_M);
-                  Error_Msg_Sloc   := Sloc (Governing_Mode);
-                  Error_Msg_N
-                    ("\mode is less restrictive than mode % defined #",
-                     New_Mode);
+                  begin
+                     --  New mode less restrictive than the established mode
+
+                     if Gov_M < Mode_Id then
+                        Error_Msg_Name_1 := Mode;
+                        Error_Msg_N ("cannot define 'S'P'A'R'K mode %", Arg1);
+
+                        Error_Msg_Name_1 := Get_SPARK_Mode_Name (SPARK_Mode);
+                        Error_Msg_Sloc   := Sloc (SPARK_Mode_Pragma);
+                        Error_Msg_N
+                          ("\mode is less restrictive than mode "
+                           & "% defined #", Arg1);
+                        raise Pragma_Exit;
+                     end if;
+                  end;
                end if;
+
+               SPARK_Mode_Pragma := N;
+               SPARK_Mode := Mode_Id;
             end Check_Pragma_Conformance;
 
             -------------------------
@@ -18190,15 +18132,6 @@ package body Sem_Prag is
                end if;
             end Get_SPARK_Mode_Name;
 
-            --  Local variables
-
-            Body_Id : Entity_Id;
-            Context : Node_Id;
-            Mode    : Name_Id;
-            Mode_Id : SPARK_Mode_Type;
-            Spec_Id : Entity_Id;
-            Stmt    : Node_Id;
-
          --  Start of processing for SPARK_Mod
 
          begin
@@ -18217,19 +18150,29 @@ package body Sem_Prag is
 
             Mode_Id := Get_SPARK_Mode_Type (Mode);
             Context := Parent (N);
-            SPARK_Mode := Mode_Id;
 
-            --  The pragma appears in a configuration file
+            --  The pragma appears in a configuration pragmas file
 
             if No (Context) then
                Check_Valid_Configuration_Pragma;
 
+               if Present (SPARK_Mode_Pragma) then
+                  Error_Msg_Sloc := Sloc (SPARK_Mode_Pragma);
+                  Error_Msg_N ("pragma% duplicates pragma declared#", N);
+                  raise Pragma_Exit;
+               end if;
+
+               SPARK_Mode_Pragma := N;
+               SPARK_Mode := Mode_Id;
+
             --  When the pragma is placed before the declaration of a unit, it
             --  configures the whole unit.
 
             elsif Nkind (Context) = N_Compilation_Unit then
                Check_Valid_Configuration_Pragma;
-                  Set_SPARK_Mode_Pragma (Current_Sem_Unit, N);
+
+               SPARK_Mode_Pragma := N;
+               SPARK_Mode := Mode_Id;
 
             --  The pragma applies to a [library unit] subprogram or package
 
@@ -18238,8 +18181,8 @@ package body Sem_Prag is
 
                if Mode_Id = Auto then
                   Error_Pragma_Arg
-                    ("mode `Auto` can only apply to the configuration variant "
-                     & "of pragma %", Arg1);
+                    ("mode `Auto` is only allowed when pragma % appears as "
+                     & "a configuration pragma", Arg1);
                end if;
 
                --  Verify the placement of the pragma with respect to package
@@ -18255,6 +18198,7 @@ package body Sem_Prag is
                         Error_Msg_Name_1 := Pname;
                         Error_Msg_Sloc   := Sloc (Stmt);
                         Error_Msg_N ("pragma% duplicates pragma declared#", N);
+                        raise Pragma_Exit;
                      end if;
 
                   --  Skip internally generated code
@@ -18262,15 +18206,31 @@ package body Sem_Prag is
                   elsif not Comes_From_Source (Stmt) then
                      null;
 
-                  --  The pragma applies to a package or subprogram declaration
+                  --  The pragma applies to a package declaration
 
                   elsif Nkind_In (Stmt, N_Generic_Package_Declaration,
-                                        N_Generic_Subprogram_Declaration,
-                                        N_Package_Declaration,
+                                        N_Package_Declaration)
+                  then
+                     Spec_Id := Defining_Unit_Name (Specification (Stmt));
+                     Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+
+                     Set_SPARK_Pragma               (Spec_Id, N);
+                     Set_SPARK_Pragma_Inherited     (Spec_Id, False);
+                     Set_SPARK_Aux_Pragma           (Spec_Id, N);
+                     Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True);
+
+                     return;
+
+                  --  The pragma applies to a subprogram declaration
+
+                  elsif Nkind_In (Stmt, N_Generic_Subprogram_Declaration,
                                         N_Subprogram_Declaration)
                   then
                      Spec_Id := Defining_Unit_Name (Specification (Stmt));
-                     Chain_Pragma (Spec_Id, N);
+                     Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+
+                     Set_SPARK_Pragma               (Spec_Id, N);
+                     Set_SPARK_Pragma_Inherited     (Spec_Id, False);
                      return;
 
                   --  The pragma does not apply to a legal construct, issue an
@@ -18304,48 +18264,79 @@ package body Sem_Prag is
                   end if;
                end if;
 
-               --  The pragma is at the top level of a package spec or appears
-               --  as an aspect on a subprogram.
-
-               --    function F ... with SPARK_Mode => ...;
+               --  The pragma is at the top level of a package spec
 
                --    package P is
                --       pragma SPARK_Mode;
 
-               if Nkind_In (Context, N_Function_Specification,
-                                     N_Package_Specification,
-                                     N_Procedure_Specification)
+               --      or
+
+               --    package P is
+               --      ...
+               --    private
+               --      pragma SPARK_Mode;
+
+               if Nkind (Context) = N_Package_Specification then
+                  Spec_Id := Defining_Unit_Name (Context);
+
+                  --  Pragma applies to private part
+
+                  if List_Containing (N) = Private_Declarations (Context) then
+                     Check_Pragma_Conformance (SPARK_Aux_Pragma (Spec_Id));
+                     Set_SPARK_Aux_Pragma           (Spec_Id, N);
+                     Set_SPARK_Aux_Pragma_Inherited (Spec_Id, False);
+
+                  --  Pragma applies to public part
+
+                  else
+                     Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+                     Set_SPARK_Pragma               (Spec_Id, N);
+                     Set_SPARK_Pragma_Inherited     (Spec_Id, False);
+                     Set_SPARK_Aux_Pragma           (Spec_Id, N);
+                     Set_SPARK_Aux_Pragma_Inherited (Spec_Id, True);
+                  end if;
+
+               --  The pragma appears as an aspect on a subprogram.
+
+               --    function F ... with SPARK_Mode => ...;
+
+               elsif Nkind_In (Context, N_Function_Specification,
+                                        N_Procedure_Specification)
                then
                   Spec_Id := Defining_Unit_Name (Context);
-                  Chain_Pragma (Spec_Id, N);
+                  Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
 
-               --  Pragma is immediately within a package or subprogram body
+                  Set_SPARK_Pragma           (Spec_Id, N);
+                  Set_SPARK_Pragma_Inherited (Spec_Id, False);
 
-               --    function F ... is
-               --       pragma SPARK_Mode;
+               --  Pragma is immediately within a package body
 
                --    package body P is
                --       pragma SPARK_Mode;
 
-               elsif Nkind_In (Context, N_Package_Body,
-                                        N_Subprogram_Body)
-               then
+               elsif Nkind (Context) = N_Package_Body then
                   Spec_Id := Corresponding_Spec (Context);
+                  Body_Id := Defining_Entity (Context);
+                  Check_Pragma_Conformance (SPARK_Pragma (Body_Id));
 
-                  if Nkind (Context) = N_Subprogram_Body then
-                     Context := Specification (Context);
-                  end if;
+                  Set_SPARK_Pragma               (Body_Id, N);
+                  Set_SPARK_Pragma_Inherited     (Body_Id, False);
+                  Set_SPARK_Aux_Pragma           (Body_Id, N);
+                  Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
 
-                  Body_Id := Defining_Entity (Context);
+               --  Pragma is immediately within a subprogram body
 
-                  Chain_Pragma (Body_Id, N);
+               --    function F ... is
+               --       pragma SPARK_Mode;
 
-                  --  Verify that the SPARK modes are consistent between
-                  --  body and spec, if any.
+               elsif Nkind (Context) = N_Subprogram_Body then
+                  Spec_Id := Corresponding_Spec (Context);
+                  Context := Specification (Context);
+                  Body_Id := Defining_Entity (Context);
+                  Check_Pragma_Conformance (SPARK_Pragma (Body_Id));
 
-                  if Present (Spec_Id) then
-                     Check_Spark_Mode_Conformance (Spec_Id, Body_Id);
-                  end if;
+                  Set_SPARK_Pragma           (Body_Id, N);
+                  Set_SPARK_Pragma_Inherited (Body_Id, False);
 
                --  The pragma applies to the statements of a package body
 
@@ -18359,9 +18350,10 @@ package body Sem_Prag is
                   Context := Parent (Context);
                   Spec_Id := Corresponding_Spec (Context);
                   Body_Id := Defining_Unit_Name (Context);
+                  Check_Pragma_Conformance (SPARK_Aux_Pragma (Body_Id));
 
-                  Chain_Pragma (Body_Id, N);
-                  Check_Spark_Mode_Conformance (Spec_Id, Body_Id);
+                  Set_SPARK_Aux_Pragma           (Body_Id, N);
+                  Set_SPARK_Aux_Pragma_Inherited (Body_Id, False);
 
                --  The pragma does not apply to a legal construct, issue error