aspects.adb: Add an entry for SPARK_Mode in table Canonical_Aspect.

2013-07-05  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb: Add an entry for SPARK_Mode in table Canonical_Aspect.
	* aspects.ads: Add an entry for SPARK_Mode in tables Aspect_Id,
	Aspect_Argument, Aspect_Names.
	* atree.adb (Node32): New routine.
	(Set_Node32): New routine.
	* atree.ads (Node32): New routine.
	(Set_Node32): New routine.
	* einfo.adb: Node32 is now used as SPARK_Mode_Pragmas.
	(Set_SPARK_Mode_Pragmas): New routine.
	(SPARK_Mode_Pragmas): New routine.
	(Write_Field32_Name): Add and entry for SPARK_Modes.
	* einfo.ads: Add attribute SPARK_Mode_Pragmas along with usage
	in various entities.
	(Set_SPARK_Mode_Pragmas): New routine and
	pragma Inline.
	(SPARK_Mode_Pragmas): New routine and pragma Inline.
	* gnat_rm.texi: Add sections explaining the syntax and semantics
	of aspect/pragma SPARK_Mode.
	* gnat_ugn.texi: Add pragma SPARK_Mode to the list of
	configuration pragmas.
	* lib.adb (Set_SPARK_Mode_Pragma): New routine.
	(SPARK_Mode_Pragma): New routine.
	* lib.ads: Alphabetize the comments on fields of record
	Unit_Record. Add new field SPARK_Mode_Pragma along with
	comment on its usage. Update the layout of record Unit_Record.
	(Set_SPARK_Mode_Pragma): New routine and pragma Inline.
	(SPARK_Mode_Pragma): New routine and pragma Inline.
	* lib-load.adb (Create_Dummy_Package_Unit): Initialize
	field SPARK_Mode_Pragma.
	(Load_Main_Source): Initialize field SPARK_Mode_Pragma.
	(Load_Unit): Initialize field SPARK_Mode_Pragma.
	* lib-writ.adb (Add_Preprocessing_Dependency): Initialize field
	SPARK_Mode_Pragma.
	(Ensure_System_Dependency): Initialize field SPARK_Mode_Pragma.
	* opt.ads: Alphabetize verification flags. Store the
	compilation-wide SPARK mode in variable Global_SPARK_Mode.
	* par-prag.adb: Pragma SPARK_Mode does not need special processing
	by the parser.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Convert aspect
	SPARK_Mode into a pragma.
	(Check_Aspect_At_Freeze_Point): Aspect SPARK_Mode does not need
	delayed processing.
	* sem_prag.adb: Add an entry for SPARK_Mode in table Sig_Flags.
	(Analyze_Pragma): Add processing for pragma SPARK_Mode.
	(Get_SPARK_Mode_Id): New routine.
	(Is_Elaboration_SPARK_Mode): New routine.
	(Is_Private_SPARK_Mode): New routine.
	* sem_prag.ads (Get_SPARK_Mode_Id): New routine.
	(Is_Elaboration_SPARK_Mode): New routine.
	(Is_Private_SPARK_Mode): New routine.
	* sinfo.ads: Update the comment on the usage of field Next_Pragma.
	* snames.ads-tmpl: Add new predefined name for SPARK_Mode and
	Auto. Add new pragma Id for SPARK_Mode.
	* types.ads: Add new type SPARK_Mode_Id.

From-SVN: r200711

21 files changed, 958 insertions, 243 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 6bec4e8..5d222e7 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,60 @@
+2013-07-05  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* aspects.adb: Add an entry for SPARK_Mode in table Canonical_Aspect.
+	* aspects.ads: Add an entry for SPARK_Mode in tables Aspect_Id,
+	Aspect_Argument, Aspect_Names.
+	* atree.adb (Node32): New routine.
+	(Set_Node32): New routine.
+	* atree.ads (Node32): New routine.
+	(Set_Node32): New routine.
+	* einfo.adb: Node32 is now used as SPARK_Mode_Pragmas.
+	(Set_SPARK_Mode_Pragmas): New routine.
+	(SPARK_Mode_Pragmas): New routine.
+	(Write_Field32_Name): Add and entry for SPARK_Modes.
+	* einfo.ads: Add attribute SPARK_Mode_Pragmas along with usage
+	in various entities.
+	(Set_SPARK_Mode_Pragmas): New routine and
+	pragma Inline.
+	(SPARK_Mode_Pragmas): New routine and pragma Inline.
+	* gnat_rm.texi: Add sections explaining the syntax and semantics
+	of aspect/pragma SPARK_Mode.
+	* gnat_ugn.texi: Add pragma SPARK_Mode to the list of
+	configuration pragmas.
+	* lib.adb (Set_SPARK_Mode_Pragma): New routine.
+	(SPARK_Mode_Pragma): New routine.
+	* lib.ads: Alphabetize the comments on fields of record
+	Unit_Record. Add new field SPARK_Mode_Pragma along with
+	comment on its usage. Update the layout of record Unit_Record.
+	(Set_SPARK_Mode_Pragma): New routine and pragma Inline.
+	(SPARK_Mode_Pragma): New routine and pragma Inline.
+	* lib-load.adb (Create_Dummy_Package_Unit): Initialize
+	field SPARK_Mode_Pragma.
+	(Load_Main_Source): Initialize field SPARK_Mode_Pragma.
+	(Load_Unit): Initialize field SPARK_Mode_Pragma.
+	* lib-writ.adb (Add_Preprocessing_Dependency): Initialize field
+	SPARK_Mode_Pragma.
+	(Ensure_System_Dependency): Initialize field SPARK_Mode_Pragma.
+	* opt.ads: Alphabetize verification flags. Store the
+	compilation-wide SPARK mode in variable Global_SPARK_Mode.
+	* par-prag.adb: Pragma SPARK_Mode does not need special processing
+	by the parser.
+	* sem_ch13.adb (Analyze_Aspect_Specifications): Convert aspect
+	SPARK_Mode into a pragma.
+	(Check_Aspect_At_Freeze_Point): Aspect SPARK_Mode does not need
+	delayed processing.
+	* sem_prag.adb: Add an entry for SPARK_Mode in table Sig_Flags.
+	(Analyze_Pragma): Add processing for pragma SPARK_Mode.
+	(Get_SPARK_Mode_Id): New routine.
+	(Is_Elaboration_SPARK_Mode): New routine.
+	(Is_Private_SPARK_Mode): New routine.
+	* sem_prag.ads (Get_SPARK_Mode_Id): New routine.
+	(Is_Elaboration_SPARK_Mode): New routine.
+	(Is_Private_SPARK_Mode): New routine.
+	* sinfo.ads: Update the comment on the usage of field Next_Pragma.
+	* snames.ads-tmpl: Add new predefined name for SPARK_Mode and
+	Auto. Add new pragma Id for SPARK_Mode.
+	* types.ads: Add new type SPARK_Mode_Id.
+
 2013-07-05  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_ch13.adb (Analyze_Aspect_Specifications): For
diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb
index 71f7493..d02edb2 100644
--- a/gcc/ada/aspects.adb
+++ b/gcc/ada/aspects.adb
@@ -403,6 +403,7 @@ package body Aspects is
     Aspect_Simple_Storage_Pool_Type     => Aspect_Simple_Storage_Pool_Type,
     Aspect_Size                         => Aspect_Size,
     Aspect_Small                        => Aspect_Small,
+    Aspect_SPARK_Mode                   => Aspect_SPARK_Mode,
     Aspect_Static_Predicate             => Aspect_Predicate,
     Aspect_Storage_Pool                 => Aspect_Storage_Pool,
     Aspect_Storage_Size                 => Aspect_Storage_Size,
diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads
index 6941cc1..5a093af 100644
--- a/gcc/ada/aspects.ads
+++ b/gcc/ada/aspects.ads
@@ -116,6 +116,7 @@ package Aspects is
       Aspect_Simple_Storage_Pool,           -- GNAT
       Aspect_Size,
       Aspect_Small,
+      Aspect_SPARK_Mode,                    -- GNAT
       Aspect_Static_Predicate,
       Aspect_Storage_Pool,
       Aspect_Storage_Size,
@@ -322,6 +323,7 @@ package Aspects is
       Aspect_Simple_Storage_Pool     => Name,
       Aspect_Size                    => Expression,
       Aspect_Small                   => Expression,
+      Aspect_SPARK_Mode              => Name,
       Aspect_Static_Predicate        => Expression,
       Aspect_Storage_Pool            => Name,
       Aspect_Storage_Size            => Expression,
@@ -423,6 +425,7 @@ package Aspects is
       Aspect_Simple_Storage_Pool_Type     => Name_Simple_Storage_Pool_Type,
       Aspect_Size                         => Name_Size,
       Aspect_Small                        => Name_Small,
+      Aspect_SPARK_Mode                   => Name_SPARK_Mode,
       Aspect_Static_Predicate             => Name_Static_Predicate,
       Aspect_Storage_Pool                 => Name_Storage_Pool,
       Aspect_Storage_Size                 => Name_Storage_Size,
diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb
index 40a27a1..a6105e2 100644
--- a/gcc/ada/atree.adb
+++ b/gcc/ada/atree.adb
@@ -2532,6 +2532,12 @@ package body Atree is
          return Node_Id (Nodes.Table (N + 5).Field7);
       end Node31;
 
+      function Node32 (N : Node_Id) return Node_Id is
+      begin
+         pragma Assert (Nkind (N) in N_Entity);
+         return Node_Id (Nodes.Table (N + 5).Field8);
+      end Node32;
+
       function List1 (N : Node_Id) return List_Id is
       begin
          pragma Assert (N <= Nodes.Last);
@@ -5243,6 +5249,12 @@ package body Atree is
          Nodes.Table (N + 5).Field7 := Union_Id (Val);
       end Set_Node31;
 
+      procedure Set_Node32 (N : Node_Id; Val : Node_Id) is
+      begin
+         pragma Assert (Nkind (N) in N_Entity);
+         Nodes.Table (N + 5).Field8 := Union_Id (Val);
+      end Set_Node32;
+
       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 07e8e51..d1056b0 100644
--- a/gcc/ada/atree.ads
+++ b/gcc/ada/atree.ads
@@ -1174,6 +1174,9 @@ package Atree is
       function Node31 (N : Node_Id) return Node_Id;
       pragma Inline (Node31);
 
+      function Node32 (N : Node_Id) return Node_Id;
+      pragma Inline (Node32);
+
       function List1 (N : Node_Id) return List_Id;
       pragma Inline (List1);
 
@@ -2459,6 +2462,9 @@ package Atree is
       procedure Set_Node31 (N : Node_Id; Val : Node_Id);
       pragma Inline (Set_Node31);
 
+      procedure Set_Node32 (N : Node_Id; Val : Node_Id);
+      pragma Inline (Set_Node32);
+
       procedure Set_List1 (N : Node_Id; Val : List_Id);
       pragma Inline (Set_List1);
 
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index bfe5b37..bca2044 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -246,7 +246,7 @@ package body Einfo is
 
    --    Thunk_Entity                    Node31
 
-   --    (unused)                        Node32
+   --    SPARK_Mode_Pragmas              Node32
 
    --    (unused)                        Node33
 
@@ -2825,6 +2825,21 @@ package body Einfo is
       return Ureal21 (Id);
    end Small_Value;
 
+   function SPARK_Mode_Pragmas (Id : E) return N 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 Node32 (Id);
+   end SPARK_Mode_Pragmas;
+
    function Spec_Entity (Id : E) return E is
    begin
       pragma Assert (Ekind (Id) = E_Package_Body or else Is_Formal (Id));
@@ -5469,6 +5484,22 @@ package body Einfo is
       Set_Ureal21 (Id, V);
    end Set_Small_Value;
 
+   procedure Set_SPARK_Mode_Pragmas (Id : E; V : N) 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_Node32 (Id, V);
+   end Set_SPARK_Mode_Pragmas;
+
    procedure Set_Spec_Entity (Id : E; V : E) is
    begin
       pragma Assert (Ekind (Id) = E_Package_Body or else Is_Formal (Id));
@@ -9149,6 +9180,16 @@ package body Einfo is
    procedure Write_Field32_Name (Id : Entity_Id) is
    begin
       case Ekind (Id) is
+         when E_Function                                   |
+              E_Generic_Function                           |
+              E_Generic_Package                            |
+              E_Generic_Procedure                          |
+              E_Package                                    |
+              E_Package_Body                               |
+              E_Procedure                                  |
+              E_Subprogram_Body                            =>
+            Write_Str ("SPARK_Mode_Pragmas");
+
          when others                                       =>
             Write_Str ("Field32??");
       end case;
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index a3d05d8..0df2880 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -3757,6 +3757,11 @@ 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)
+--       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.
+
 --    Spec_Entity (Node19)
 --       Defined in package body entities. Points to corresponding package
 --       spec entity. Also defined in subprogram body parameters in the
@@ -5394,6 +5399,7 @@ package Einfo is
    --    Subprograms_For_Type                (Node29)
    --    Corresponding_Equality              (Node30)   (implicit /= only)
    --    Thunk_Entity                        (Node31)   (thunk case only)
+   --    SPARK_Mode_Pragmas                  (Node32)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Elaboration_Entity_Required         (Flag174)
    --    Default_Expressions_Processed       (Flag108)
@@ -5591,6 +5597,7 @@ package Einfo is
    --    Abstract_States                     (Elist25)
    --    Package_Instantiation               (Node26)
    --    Current_Use_Clause                  (Node27)
+   --    SPARK_Mode_Pragmas                  (Node32)
    --    Delay_Subprogram_Descriptors        (Flag50)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Discard_Names                       (Flag88)
@@ -5621,6 +5628,7 @@ package Einfo is
    --    Last_Entity                         (Node20)
    --    Scope_Depth_Value                   (Uint22)
    --    Finalizer                           (Node24)   (non-generic case only)
+   --    SPARK_Mode_Pragmas                  (Node32)
    --    Delay_Subprogram_Descriptors        (Flag50)
    --    Has_Anonymous_Master                (Flag253)
    --    Scope_Depth                         (synth)
@@ -5667,6 +5675,7 @@ package Einfo is
    --    Extra_Formals                       (Node28)
    --    Static_Initialization               (Node30)   (init_proc only)
    --    Thunk_Entity                        (Node31)   (thunk case only)
+   --    SPARK_Mode_Pragmas                  (Node32)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Delay_Cleanups                      (Flag114)
    --    Discard_Names                       (Flag88)
@@ -5837,6 +5846,7 @@ package Einfo is
    --    Last_Entity                         (Node20)
    --    Scope_Depth_Value                   (Uint22)
    --    Extra_Formals                       (Node28)
+   --    SPARK_Mode_Pragmas                  (Node32)
    --    Scope_Depth                         (synth)
 
    --  E_Subprogram_Type
@@ -6531,6 +6541,7 @@ 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 Spec_Entity                         (Id : E) return E;
    function Static_Elaboration_Desired          (Id : E) return B;
    function Static_Initialization               (Id : E) return N;
@@ -7145,6 +7156,7 @@ 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_Spec_Entity                     (Id : E; V : E);
    procedure Set_Static_Elaboration_Desired      (Id : E; V : B);
    procedure Set_Static_Initialization           (Id : E; V : N);
@@ -7891,6 +7903,7 @@ 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 (Spec_Entity);
    pragma Inline (Static_Elaboration_Desired);
    pragma Inline (Static_Initialization);
@@ -8305,6 +8318,7 @@ 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_Spec_Entity);
    pragma Inline (Set_Static_Elaboration_Desired);
    pragma Inline (Set_Static_Initialization);
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index 1943009..4b0c37c 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -232,6 +232,7 @@ Implementation Defined Pragmas
 * Pragma Source_File_Name::
 * Pragma Source_File_Name_Project::
 * Pragma Source_Reference::
+* Pragma SPARK_Mode::
 * Pragma Static_Elaboration_Desired::
 * Pragma Stream_Convert::
 * Pragma Style_Checks::
@@ -290,6 +291,7 @@ Implementation Defined Aspects
 * Aspect Shared::
 * Aspect Simple_Storage_Pool::
 * Aspect Simple_Storage_Pool_Type::
+* Aspect SPARK_Mode::
 * Aspect Suppress_Debug_Info::
 * Aspect Test_Case::
 * Aspect Universal_Aliasing::
@@ -1044,6 +1046,7 @@ consideration, the use of these pragmas should be minimized.
 * Pragma Source_File_Name::
 * Pragma Source_File_Name_Project::
 * Pragma Source_Reference::
+* Pragma SPARK_Mode::
 * Pragma Static_Elaboration_Desired::
 * Pragma Stream_Convert::
 * Pragma Style_Checks::
@@ -5996,6 +5999,80 @@ The second argument must be a string literal, it cannot be a static
 string expression other than a string literal.  This is because its value
 is needed for error messages issued by all phases of the compiler.
 
+@node Pragma SPARK_Mode
+@unnumberedsec Pragma SPARK_Mode
+@findex SPARK_Mode
+@noindent
+Syntax:
+
+@smallexample @c ada
+pragma SPARK_Mode [ (On | Off | Auto) ] ;
+@end smallexample
+
+@noindent
+This pragma is used to designate whether a contract and its implementation must
+follow the SPARK 2014 programming language syntactic and semantic rules. The
+pragma is intended for use with formal verification tools and has no effect on
+the generated code.
+
+When used as a configuration pragma over a whole compilation or in a particular
+compilation unit, it sets the mode of the units involved, in particular:
+
+@itemize @bullet
+
+@item
+@code{On}: All entities in the units must follow the SPARK 2014 language, and
+an error will be generated if not, unless locally overridden by a local
+SPARK_Mode pragma or aspect. @code{On} is the default mode when pragma
+SPARK_Mode is used without an argument.
+
+@item
+@code{Off}: The units are considered to be in Ada by default and therefore not
+part of SPARK 2014 unless overridden locally. These units may be called by SPARK
+2014 units.
+
+@item
+@code{Auto}: The formal verification tools will automatically detect whether
+each entity is in SPARK 2014 or in Ada.
+
+@end itemize
+
+Pragma SPARK_Mode can be used as a local pragma with the following semantics:
+
+@itemize @bullet
+
+@item
+Auto cannot be used as a mode argument.
+
+@item
+When the pragma appears immediately within the visible declarations of a
+package, it marks the whole package (spec and body) in or out of SPARK 2014.
+
+@item
+When the pragma appears immediately within the private declarations of a
+package, it marks the private part in or out of SPARK 2014.
+
+@item
+When the pragma appears immediately within the declarations of a package body,
+it marks the whole body in or out of SPARK 2014.
+
+@item
+When the pragma appears immediately within the elaboration statements of a
+package body, it marks the statements in or out of SPARK 2014.
+
+@item
+When the pragma appears after a subprogram declaration, it marks the whole
+subprogram (spec and body) in or out of SPARK 2014.
+
+@item
+When the pragma appears immediately within the declarations of a subprogram
+body, it marks the whole body in or out of SPARK 2014.
+
+@item
+Any other use of the pragma is illegal.
+
+@end itemize
+
 @node Pragma Static_Elaboration_Desired
 @unnumberedsec Pragma Static_Elaboration_Desired
 @findex Static_Elaboration_Desired
@@ -6048,8 +6125,7 @@ of this type.  It must name a function whose argument type may be any
 subtype, and whose returned type must be the type given as the first
 argument to the pragma.
 
-The meaning of the @var{Read}
-parameter is that if a stream attribute directly
+The meaning of the @var{Read} parameter is that if a stream attribute directly
 or indirectly specifies reading of the type given as the first parameter,
 then a value of the type given as the argument to the Read function is
 read from the stream, and then the Read function is used to convert this
@@ -7180,6 +7256,7 @@ clause.
 * Aspect Shared::
 * Aspect Simple_Storage_Pool::
 * Aspect Simple_Storage_Pool_Type::
+* Aspect SPARK_Mode::
 * Aspect Suppress_Debug_Info::
 * Aspect Test_Case::
 * Aspect Universal_Aliasing::
@@ -7433,6 +7510,12 @@ attribute definition clause.
 @noindent
 This aspect is equivalent to pragma @code{Simple_Storage_Pool_Type}.
 
+@node Aspect SPARK_Mode
+@unnumberedsec Aspect SPARK_Mode
+@findex SPARK_Mode
+@noindent
+This aspect is equivalent to pragma @code{SPARK_Mode}.
+
 @node Aspect Suppress_Debug_Info
 @unnumberedsec Aspect Suppress_Debug_Info
 @findex Suppress_Debug_Info
diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi
index 5a6b6af..86eb6b3 100644
--- a/gcc/ada/gnat_ugn.texi
+++ b/gcc/ada/gnat_ugn.texi
@@ -11611,6 +11611,7 @@ recognized by GNAT:
    Short_Circuit_And_Or
    Source_File_Name
    Source_File_Name_Project
+   SPARK_Mode
    Style_Checks
    Suppress
    Suppress_Exception_Locations
diff --git a/gcc/ada/lib-load.adb b/gcc/ada/lib-load.adb
index be4c537..6d65c81 100644
--- a/gcc/ada/lib-load.adb
+++ b/gcc/ada/lib-load.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, 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- --
@@ -206,28 +206,29 @@ package body Lib.Load is
       Unum := Units.Last;
 
       Units.Table (Unum) := (
-        Cunit            => Cunit,
-        Cunit_Entity     => Cunit_Entity,
-        Dependency_Num   => 0,
-        Dynamic_Elab     => False,
-        Error_Location   => Sloc (With_Node),
-        Expected_Unit    => Spec_Name,
-        Fatal_Error      => True,
-        Generate_Code    => False,
-        Has_Allocator    => False,
-        Has_RACW         => False,
-        Is_Compiler_Unit => False,
-        Ident_String     => Empty,
-        Loading          => False,
-        Main_Priority    => Default_Main_Priority,
-        Main_CPU         => Default_Main_CPU,
-        Munit_Index      => 0,
-        Serial_Number    => 0,
-        Source_Index     => No_Source_File,
-        Unit_File_Name   => Get_File_Name (Spec_Name, Subunit => False),
-        Unit_Name        => Spec_Name,
-        Version          => 0,
-        OA_Setting       => 'O');
+        Cunit             => Cunit,
+        Cunit_Entity      => Cunit_Entity,
+        Dependency_Num    => 0,
+        Dynamic_Elab      => False,
+        Error_Location    => Sloc (With_Node),
+        Expected_Unit     => Spec_Name,
+        Fatal_Error       => True,
+        Generate_Code     => False,
+        Has_Allocator     => False,
+        Has_RACW          => False,
+        Is_Compiler_Unit  => False,
+        Ident_String      => Empty,
+        Loading           => False,
+        Main_Priority     => Default_Main_Priority,
+        Main_CPU          => Default_Main_CPU,
+        Munit_Index       => 0,
+        Serial_Number     => 0,
+        Source_Index      => No_Source_File,
+        Unit_File_Name    => Get_File_Name (Spec_Name, Subunit => False),
+        Unit_Name         => Spec_Name,
+        Version           => 0,
+        OA_Setting        => 'O',
+        SPARK_Mode_Pragma => Empty);
 
       Set_Comes_From_Source_Default (Save_CS);
       Set_Error_Posted (Cunit_Entity);
@@ -312,28 +313,29 @@ package body Lib.Load is
          end if;
 
          Units.Table (Main_Unit) := (
-           Cunit            => Empty,
-           Cunit_Entity     => Empty,
-           Dependency_Num   => 0,
-           Dynamic_Elab     => False,
-           Error_Location   => No_Location,
-           Expected_Unit    => No_Unit_Name,
-           Fatal_Error      => False,
-           Generate_Code    => False,
-           Has_Allocator    => False,
-           Has_RACW         => False,
-           Is_Compiler_Unit => False,
-           Ident_String     => Empty,
-           Loading          => True,
-           Main_Priority    => Default_Main_Priority,
-           Main_CPU         => Default_Main_CPU,
-           Munit_Index      => 0,
-           Serial_Number    => 0,
-           Source_Index     => Main_Source_File,
-           Unit_File_Name   => Fname,
-           Unit_Name        => No_Unit_Name,
-           Version          => Version,
-           OA_Setting       => 'O');
+           Cunit             => Empty,
+           Cunit_Entity      => Empty,
+           Dependency_Num    => 0,
+           Dynamic_Elab      => False,
+           Error_Location    => No_Location,
+           Expected_Unit     => No_Unit_Name,
+           Fatal_Error       => False,
+           Generate_Code     => False,
+           Has_Allocator     => False,
+           Has_RACW          => False,
+           Is_Compiler_Unit  => False,
+           Ident_String      => Empty,
+           Loading           => True,
+           Main_Priority     => Default_Main_Priority,
+           Main_CPU          => Default_Main_CPU,
+           Munit_Index       => 0,
+           Serial_Number     => 0,
+           Source_Index      => Main_Source_File,
+           Unit_File_Name    => Fname,
+           Unit_Name         => No_Unit_Name,
+           Version           => Version,
+           OA_Setting        => 'O',
+           SPARK_Mode_Pragma => Empty);
       end if;
    end Load_Main_Source;
 
@@ -675,28 +677,29 @@ package body Lib.Load is
 
          if Src_Ind /= No_Source_File then
             Units.Table (Unum) := (
-              Cunit            => Empty,
-              Cunit_Entity     => Empty,
-              Dependency_Num   => 0,
-              Dynamic_Elab     => False,
-              Error_Location   => Sloc (Error_Node),
-              Expected_Unit    => Uname_Actual,
-              Fatal_Error      => False,
-              Generate_Code    => False,
-              Has_Allocator    => False,
-              Has_RACW         => False,
-              Is_Compiler_Unit => False,
-              Ident_String     => Empty,
-              Loading          => True,
-              Main_Priority    => Default_Main_Priority,
-              Main_CPU         => Default_Main_CPU,
-              Munit_Index      => 0,
-              Serial_Number    => 0,
-              Source_Index     => Src_Ind,
-              Unit_File_Name   => Fname,
-              Unit_Name        => Uname_Actual,
-              Version          => Source_Checksum (Src_Ind),
-              OA_Setting       => 'O');
+              Cunit             => Empty,
+              Cunit_Entity      => Empty,
+              Dependency_Num    => 0,
+              Dynamic_Elab      => False,
+              Error_Location    => Sloc (Error_Node),
+              Expected_Unit     => Uname_Actual,
+              Fatal_Error       => False,
+              Generate_Code     => False,
+              Has_Allocator     => False,
+              Has_RACW          => False,
+              Is_Compiler_Unit  => False,
+              Ident_String      => Empty,
+              Loading           => True,
+              Main_Priority     => Default_Main_Priority,
+              Main_CPU          => Default_Main_CPU,
+              Munit_Index       => 0,
+              Serial_Number     => 0,
+              Source_Index      => Src_Ind,
+              Unit_File_Name    => Fname,
+              Unit_Name         => Uname_Actual,
+              Version           => Source_Checksum (Src_Ind),
+              OA_Setting        => 'O',
+              SPARK_Mode_Pragma => Empty);
 
             --  Parse the new unit
 
diff --git a/gcc/ada/lib-writ.adb b/gcc/ada/lib-writ.adb
index e786f47..e5c0912 100644
--- a/gcc/ada/lib-writ.adb
+++ b/gcc/ada/lib-writ.adb
@@ -71,28 +71,29 @@ package body Lib.Writ is
    begin
       Units.Increment_Last;
       Units.Table (Units.Last) :=
-        (Unit_File_Name   => File_Name (S),
-         Unit_Name        => No_Unit_Name,
-         Expected_Unit    => No_Unit_Name,
-         Source_Index     => S,
-         Cunit            => Empty,
-         Cunit_Entity     => Empty,
-         Dependency_Num   => 0,
-         Dynamic_Elab     => False,
-         Fatal_Error      => False,
-         Generate_Code    => False,
-         Has_Allocator    => False,
-         Has_RACW         => False,
-         Is_Compiler_Unit => False,
-         Ident_String     => Empty,
-         Loading          => False,
-         Main_Priority    => -1,
-         Main_CPU         => -1,
-         Munit_Index      => 0,
-         Serial_Number    => 0,
-         Version          => 0,
-         Error_Location   => No_Location,
-         OA_Setting       => 'O');
+        (Unit_File_Name    => File_Name (S),
+         Unit_Name         => No_Unit_Name,
+         Expected_Unit     => No_Unit_Name,
+         Source_Index      => S,
+         Cunit             => Empty,
+         Cunit_Entity      => Empty,
+         Dependency_Num    => 0,
+         Dynamic_Elab      => False,
+         Fatal_Error       => False,
+         Generate_Code     => False,
+         Has_Allocator     => False,
+         Has_RACW          => False,
+         Is_Compiler_Unit  => False,
+         Ident_String      => Empty,
+         Loading           => False,
+         Main_Priority     => -1,
+         Main_CPU          => -1,
+         Munit_Index       => 0,
+         Serial_Number     => 0,
+         Version           => 0,
+         Error_Location    => No_Location,
+         OA_Setting        => 'O',
+         SPARK_Mode_Pragma => Empty);
    end Add_Preprocessing_Dependency;
 
    ------------------------------
@@ -128,28 +129,29 @@ package body Lib.Writ is
 
       Units.Increment_Last;
       Units.Table (Units.Last) := (
-        Unit_File_Name   => System_Fname,
-        Unit_Name        => System_Uname,
-        Expected_Unit    => System_Uname,
-        Source_Index     => System_Source_File_Index,
-        Cunit            => Empty,
-        Cunit_Entity     => Empty,
-        Dependency_Num   => 0,
-        Dynamic_Elab     => False,
-        Fatal_Error      => False,
-        Generate_Code    => False,
-        Has_Allocator    => False,
-        Has_RACW         => False,
-        Is_Compiler_Unit => False,
-        Ident_String     => Empty,
-        Loading          => False,
-        Main_Priority    => -1,
-        Main_CPU         => -1,
-        Munit_Index      => 0,
-        Serial_Number    => 0,
-        Version          => 0,
-        Error_Location   => No_Location,
-        OA_Setting       => 'O');
+        Unit_File_Name    => System_Fname,
+        Unit_Name         => System_Uname,
+        Expected_Unit     => System_Uname,
+        Source_Index      => System_Source_File_Index,
+        Cunit             => Empty,
+        Cunit_Entity      => Empty,
+        Dependency_Num    => 0,
+        Dynamic_Elab      => False,
+        Fatal_Error       => False,
+        Generate_Code     => False,
+        Has_Allocator     => False,
+        Has_RACW          => False,
+        Is_Compiler_Unit  => False,
+        Ident_String      => Empty,
+        Loading           => False,
+        Main_Priority     => -1,
+        Main_CPU          => -1,
+        Munit_Index       => 0,
+        Serial_Number     => 0,
+        Version           => 0,
+        Error_Location    => No_Location,
+        OA_Setting        => 'O',
+        SPARK_Mode_Pragma => Empty);
 
       --  Parse system.ads so that the checksum is set right
       --  Style checks are not applied.
diff --git a/gcc/ada/lib.adb b/gcc/ada/lib.adb
index fc62239..e220b20 100644
--- a/gcc/ada/lib.adb
+++ b/gcc/ada/lib.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, 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- --
@@ -166,6 +166,11 @@ 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;
@@ -254,6 +259,11 @@ 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 f2cc330..eb10a8b 100644
--- a/gcc/ada/lib.ads
+++ b/gcc/ada/lib.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, 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- --
@@ -265,38 +265,6 @@ package Lib is
    --  The first entry in the table, subscript Main_Unit, is for the main file.
    --  Each entry in this units table contains the following data.
 
-   --    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.
-
-   --    Source_Index
-   --      The index in the source file table of the corresponding source file.
-   --      Set when the entry is created by a call to Lib.Load and then cannot
-   --      be changed.
-
-   --    Munit_Index
-   --      The index of the unit within the file for multiple unit per file
-   --      mode. Set to zero in normal single unit per file mode.
-
-   --    Error_Location
-   --      This is copied from the Sloc field of the Enode argument passed
-   --      to Load_Unit. It refers to the enclosing construct which caused
-   --      this unit to be loaded, e.g. most typically the with clause that
-   --      referenced the unit, and is used for error handling in Par.Load.
-
-   --    Expected_Unit
-   --      This is the expected unit name for a file other than the main unit,
-   --      since these are cases where we load the unit using Lib.Load and we
-   --      know the unit that is expected. It must be the same as Unit_Name
-   --      if it is set (see test in Par.Load). Expected_Unit is set to
-   --      No_Name for the main unit.
-
-   --    Unit_Name
-   --      The name of the unit. Initialized to No_Name by Lib.Load, and then
-   --      set by the parser when the unit is parsed to the unit name actually
-   --      found in the file (which should, in the absence of errors) be the
-   --      same name as Expected_Unit.
-
    --    Cunit
    --      Pointer to the N_Compilation_Unit node. Initially set to Empty by
    --      Lib.Load, and then reset to the required node by the parser when
@@ -320,6 +288,19 @@ package Lib is
    --      checks specified (as the result of using the -gnatE compilation
    --      option or a pragma Elaboration_Checks (Dynamic).
 
+   --    Error_Location
+   --      This is copied from the Sloc field of the Enode argument passed
+   --      to Load_Unit. It refers to the enclosing construct which caused
+   --      this unit to be loaded, e.g. most typically the with clause that
+   --      referenced the unit, and is used for error handling in Par.Load.
+
+   --    Expected_Unit
+   --      This is the expected unit name for a file other than the main unit,
+   --      since these are cases where we load the unit using Lib.Load and we
+   --      know the unit that is expected. It must be the same as Unit_Name
+   --      if it is set (see test in Par.Load). Expected_Unit is set to
+   --      No_Name for the main unit.
+
    --    Fatal_Error
    --      A flag that is initialized to False, and gets set to True if a fatal
    --      error occurs during the processing of a unit. A fatal error is one
@@ -335,6 +316,10 @@ package Lib is
    --      code is to be generated. This includes the unit explicitly compiled,
    --      together with its specification, and any subunits.
 
+   --    Has_Allocator
+   --      This flag is set if a subprogram unit has an allocator after the
+   --      BEGIN (it is used to set the AB flag in the M ALI line).
+
    --    Has_RACW
    --      A Boolean flag, initially set to False when a unit entry is created,
    --      and set to True if the unit defines a remote access to class wide
@@ -366,9 +351,9 @@ package Lib is
    --      that the default affinity is to be used (and is also used for
    --      entries that do not correspond to possible main programs).
 
-   --    Has_Allocator
-   --      This flag is set if a subprogram unit has an allocator after the
-   --      BEGIN (it is used to set the AB flag in the M ALI line).
+   --    Munit_Index
+   --      The index of the unit within the file for multiple unit per file
+   --      mode. Set to zero in normal single unit per file mode.
 
    --    OA_Setting
    --      This is a character field containing L if Optimize_Alignment mode
@@ -381,6 +366,25 @@ package Lib is
    --      routine which increments the current value and returns it. This
    --      serial number is separate for each unit.
 
+   --    Source_Index
+   --      The index in the source file table of the corresponding source file.
+   --      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.
+
+   --    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.
+
+   --    Unit_Name
+   --      The name of the unit. Initialized to No_Name by Lib.Load, and then
+   --      set by the parser when the unit is parsed to the unit name actually
+   --      found in the file (which should, in the absence of errors) be the
+   --      same name as Expected_Unit.
+
    --    Version
    --      This field holds the version of the unit, which is computed as
    --      the exclusive or of the checksums of this unit, and all its
@@ -404,43 +408,45 @@ package Lib is
    Default_Main_CPU : constant Int := -1;
    --  Value used in Main_CPU field to indicate default main affinity
 
-   function Cunit            (U : Unit_Number_Type) return Node_Id;
-   function Cunit_Entity     (U : Unit_Number_Type) return Entity_Id;
-   function Dependency_Num   (U : Unit_Number_Type) return Nat;
-   function Dynamic_Elab     (U : Unit_Number_Type) return Boolean;
-   function Error_Location   (U : Unit_Number_Type) return Source_Ptr;
-   function Expected_Unit    (U : Unit_Number_Type) return Unit_Name_Type;
-   function Fatal_Error      (U : Unit_Number_Type) return Boolean;
-   function Generate_Code    (U : Unit_Number_Type) return Boolean;
-   function Ident_String     (U : Unit_Number_Type) return Node_Id;
-   function Has_Allocator    (U : Unit_Number_Type) return Boolean;
-   function Has_RACW         (U : Unit_Number_Type) return Boolean;
-   function Is_Compiler_Unit (U : Unit_Number_Type) return Boolean;
-   function Loading          (U : Unit_Number_Type) return Boolean;
-   function Main_CPU         (U : Unit_Number_Type) return Int;
-   function Main_Priority    (U : Unit_Number_Type) return Int;
-   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 Unit_File_Name   (U : Unit_Number_Type) return File_Name_Type;
-   function Unit_Name        (U : Unit_Number_Type) return Unit_Name_Type;
+   function Cunit             (U : Unit_Number_Type) return Node_Id;
+   function Cunit_Entity      (U : Unit_Number_Type) return Entity_Id;
+   function Dependency_Num    (U : Unit_Number_Type) return Nat;
+   function Dynamic_Elab      (U : Unit_Number_Type) return Boolean;
+   function Error_Location    (U : Unit_Number_Type) return Source_Ptr;
+   function Expected_Unit     (U : Unit_Number_Type) return Unit_Name_Type;
+   function Fatal_Error       (U : Unit_Number_Type) return Boolean;
+   function Generate_Code     (U : Unit_Number_Type) return Boolean;
+   function Ident_String      (U : Unit_Number_Type) return Node_Id;
+   function Has_Allocator     (U : Unit_Number_Type) return Boolean;
+   function Has_RACW          (U : Unit_Number_Type) return Boolean;
+   function Is_Compiler_Unit  (U : Unit_Number_Type) return Boolean;
+   function Loading           (U : Unit_Number_Type) return Boolean;
+   function Main_CPU          (U : Unit_Number_Type) return Int;
+   function Main_Priority     (U : Unit_Number_Type) return Int;
+   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
 
-   procedure Set_Cunit            (U : Unit_Number_Type; N : Node_Id);
-   procedure Set_Cunit_Entity     (U : Unit_Number_Type; E : Entity_Id);
-   procedure Set_Dynamic_Elab     (U : Unit_Number_Type; B : Boolean := True);
-   procedure Set_Error_Location   (U : Unit_Number_Type; W : Source_Ptr);
-   procedure Set_Fatal_Error      (U : Unit_Number_Type; B : Boolean := True);
-   procedure Set_Generate_Code    (U : Unit_Number_Type; B : Boolean := True);
-   procedure Set_Has_RACW         (U : Unit_Number_Type; B : Boolean := True);
-   procedure Set_Has_Allocator    (U : Unit_Number_Type; B : Boolean := True);
-   procedure Set_Is_Compiler_Unit (U : Unit_Number_Type; B : Boolean := True);
-   procedure Set_Ident_String     (U : Unit_Number_Type; N : Node_Id);
-   procedure Set_Loading          (U : Unit_Number_Type; B : Boolean := True);
-   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_Unit_Name        (U : Unit_Number_Type; N : Unit_Name_Type);
+   procedure Set_Cunit             (U : Unit_Number_Type; N : Node_Id);
+   procedure Set_Cunit_Entity      (U : Unit_Number_Type; E : Entity_Id);
+   procedure Set_Dynamic_Elab      (U : Unit_Number_Type; B : Boolean := True);
+   procedure Set_Error_Location    (U : Unit_Number_Type; W : Source_Ptr);
+   procedure Set_Fatal_Error       (U : Unit_Number_Type; B : Boolean := True);
+   procedure Set_Generate_Code     (U : Unit_Number_Type; B : Boolean := True);
+   procedure Set_Has_RACW          (U : Unit_Number_Type; B : Boolean := True);
+   procedure Set_Has_Allocator     (U : Unit_Number_Type; B : Boolean := True);
+   procedure Set_Is_Compiler_Unit  (U : Unit_Number_Type; B : Boolean := True);
+   procedure Set_Ident_String      (U : Unit_Number_Type; N : Node_Id);
+   procedure Set_Loading           (U : Unit_Number_Type; B : Boolean := True);
+   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
    --  can only be set by specialized interfaces (defined below).
@@ -707,34 +713,37 @@ 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);
 
    type Unit_Record is record
-      Unit_File_Name   : File_Name_Type;
-      Unit_Name        : Unit_Name_Type;
-      Munit_Index      : Nat;
-      Expected_Unit    : Unit_Name_Type;
-      Source_Index     : Source_File_Index;
-      Cunit            : Node_Id;
-      Cunit_Entity     : Entity_Id;
-      Dependency_Num   : Int;
-      Ident_String     : Node_Id;
-      Main_Priority    : Int;
-      Main_CPU         : Int;
-      Serial_Number    : Nat;
-      Version          : Word;
-      Error_Location   : Source_Ptr;
-      Fatal_Error      : Boolean;
-      Generate_Code    : Boolean;
-      Has_RACW         : Boolean;
-      Is_Compiler_Unit : Boolean;
-      Dynamic_Elab     : Boolean;
-      Loading          : Boolean;
-      Has_Allocator    : Boolean;
-      OA_Setting       : Character;
+      Unit_File_Name    : File_Name_Type;
+      Unit_Name         : Unit_Name_Type;
+      Munit_Index       : Nat;
+      Expected_Unit     : Unit_Name_Type;
+      Source_Index      : Source_File_Index;
+      Cunit             : Node_Id;
+      Cunit_Entity      : Entity_Id;
+      Dependency_Num    : Int;
+      Ident_String      : Node_Id;
+      Main_Priority     : Int;
+      Main_CPU          : Int;
+      Serial_Number     : Nat;
+      Version           : Word;
+      Error_Location    : Source_Ptr;
+      Fatal_Error       : Boolean;
+      Generate_Code     : Boolean;
+      Has_RACW          : Boolean;
+      Is_Compiler_Unit  : Boolean;
+      Dynamic_Elab      : Boolean;
+      Loading           : Boolean;
+      Has_Allocator     : Boolean;
+      OA_Setting        : Character;
+      SPARK_Mode_Pragma : Node_Id;
    end record;
 
    --  The following representation clause ensures that the above record
@@ -742,31 +751,32 @@ private
    --  written by Tree_Gen, we do not write uninitialized values to the file.
 
    for Unit_Record use record
-      Unit_File_Name   at  0 range 0 .. 31;
-      Unit_Name        at  4 range 0 .. 31;
-      Munit_Index      at  8 range 0 .. 31;
-      Expected_Unit    at 12 range 0 .. 31;
-      Source_Index     at 16 range 0 .. 31;
-      Cunit            at 20 range 0 .. 31;
-      Cunit_Entity     at 24 range 0 .. 31;
-      Dependency_Num   at 28 range 0 .. 31;
-      Ident_String     at 32 range 0 .. 31;
-      Main_Priority    at 36 range 0 .. 31;
-      Main_CPU         at 40 range 0 .. 31;
-      Serial_Number    at 44 range 0 .. 31;
-      Version          at 48 range 0 .. 31;
-      Error_Location   at 52 range 0 .. 31;
-      Fatal_Error      at 56 range 0 ..  7;
-      Generate_Code    at 57 range 0 ..  7;
-      Has_RACW         at 58 range 0 ..  7;
-      Dynamic_Elab     at 59 range 0 ..  7;
-      Is_Compiler_Unit at 60 range 0 ..  7;
-      OA_Setting       at 61 range 0 ..  7;
-      Loading          at 62 range 0 ..  7;
-      Has_Allocator    at 63 range 0 ..  7;
+      Unit_File_Name    at  0 range 0 .. 31;
+      Unit_Name         at  4 range 0 .. 31;
+      Munit_Index       at  8 range 0 .. 31;
+      Expected_Unit     at 12 range 0 .. 31;
+      Source_Index      at 16 range 0 .. 31;
+      Cunit             at 20 range 0 .. 31;
+      Cunit_Entity      at 24 range 0 .. 31;
+      Dependency_Num    at 28 range 0 .. 31;
+      Ident_String      at 32 range 0 .. 31;
+      Main_Priority     at 36 range 0 .. 31;
+      Main_CPU          at 40 range 0 .. 31;
+      Serial_Number     at 44 range 0 .. 31;
+      Version           at 48 range 0 .. 31;
+      Error_Location    at 52 range 0 .. 31;
+      Fatal_Error       at 56 range 0 ..  7;
+      Generate_Code     at 57 range 0 ..  7;
+      Has_RACW          at 58 range 0 ..  7;
+      Dynamic_Elab      at 59 range 0 ..  7;
+      Is_Compiler_Unit  at 60 range 0 ..  7;
+      OA_Setting        at 61 range 0 ..  7;
+      Loading           at 62 range 0 ..  7;
+      Has_Allocator     at 63 range 0 ..  7;
+      SPARK_Mode_Pragma at 64 range 0 .. 31;
    end record;
 
-   for Unit_Record'Size use 64 * 8;
+   for Unit_Record'Size use 68 * 8;
    --  This ensures that we did not leave out any fields
 
    package Units is new Table.Table (
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 54d39f8..a4cbafd 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -1970,6 +1970,21 @@ package Opt is
    -- Modes for Formal Verification --
    -----------------------------------
 
+   Frame_Condition_Mode : Boolean := False;
+   --  Specific mode to be used in combination with SPARK_Mode. If set to
+   --  true, ALI files containing the frame conditions (global effects) are
+   --  generated, and Why files are *not* generated. If not true, Why files
+   --  are generated. Set by debug flag -gnatd.G.
+
+   Formal_Extensions : Boolean := False;
+   --  When this flag is set, new aspects/pragmas/attributes are accepted,
+   --  whose main purpose is to facilitate formal verification. Set by debug
+   --  flag -gnatd.V.
+
+   Global_SPARK_Mode : SPARK_Mode_Id := None;
+   --  The mode applicable to the whole compilation. The global mode can be set
+   --  in a configuration file such as gnat.adc.
+
    SPARK_Mode : Boolean := False;
    --  Specific compiling mode targeting formal verification through the
    --  generation of Why code for those parts of the input code that belong to
@@ -1978,22 +1993,11 @@ package Opt is
    --  from the SPARK restriction defined in GNAT to detect violations of a
    --  subset of SPARK 2005 rules.
 
-   Frame_Condition_Mode : Boolean := False;
-   --  Specific mode to be used in combination with SPARK_Mode. If set to
-   --  true, ALI files containing the frame conditions (global effects) are
-   --  generated, and Why files are *not* generated. If not true, Why files
-   --  are generated. Set by debug flag -gnatd.G.
-
    SPARK_Strict_Mode : Boolean := False;
    --  Interpret compiler permissions as strictly as possible. E.g. base ranges
    --  for integers are limited to the strict minimum with this option. Set by
    --  debug flag -gnatd.D.
 
-   Formal_Extensions : Boolean := False;
-   --  When this flag is set, new aspects/pragmas/attributes are accepted,
-   --  whose main purpose is to facilitate formal verification. Set by debug
-   --  flag -gnatd.V.
-
    function Full_Expander_Active return Boolean;
    pragma Inline (Full_Expander_Active);
    --  Returns the value of (Expander_Active and not SPARK_Mode). This "flag"
diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb
index 3587dff..07242fb 100644
--- a/gcc/ada/par-prag.adb
+++ b/gcc/ada/par-prag.adb
@@ -1262,6 +1262,7 @@ begin
            Pragma_Short_Circuit_And_Or           |
            Pragma_Short_Descriptors              |
            Pragma_Simple_Storage_Pool_Type       |
+           Pragma_SPARK_Mode                     |
            Pragma_Storage_Size                   |
            Pragma_Storage_Unit                   |
            Pragma_Static_Elaboration_Desired     |
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 0eb18f1..5378fa3 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -1659,6 +1659,16 @@ package body Sem_Ch13 is
                   Insert_Delayed_Pragma (Aitem);
                   goto Continue;
 
+               --  SPARK_Mode
+
+               when Aspect_SPARK_Mode =>
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_SPARK_Mode);
+                  Delay_Required := False;
+
                --  Relative_Deadline
 
                when Aspect_Relative_Deadline =>
@@ -7390,6 +7400,7 @@ package body Sem_Ch13 is
               Aspect_Postcondition        |
               Aspect_Pre                  |
               Aspect_Precondition         |
+              Aspect_SPARK_Mode           |
               Aspect_Test_Case     =>
             raise Program_Error;
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 08d6f9a..36c3d7f 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -213,6 +213,11 @@ package body Sem_Prag is
    --  original one, following the renaming chain) is returned. Otherwise the
    --  entity is returned unchanged. Should be in Einfo???
 
+   function Get_SPARK_Mode_Id (N : Name_Id) return SPARK_Mode_Id;
+   --  Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram
+   --  Get_SPARK_Mode_Id. Convert a name into a corresponding value of type
+   --  SPARK_Mode_Id.
+
    function Original_Name (N : Node_Id) return Name_Id;
    --  N is a pragma node or aspect specification node. This function returns
    --  the name of the pragma or aspect in original source form, taking into
@@ -16315,6 +16320,351 @@ package body Sem_Prag is
          when Pragma_Source_Reference =>
             GNAT_Pragma;
 
+         ----------------
+         -- SPARK_Mode --
+         ----------------
+
+         --  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_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 attempts to redefine the known
+            --  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.
+
+            function Get_SPARK_Mode_Name (Id : SPARK_Mode_Id) return Name_Id;
+            --  Convert a value of type SPARK_Mode_Id into a corresponding name
+
+            procedure Redefinition_Error (Mode : SPARK_Mode_Id);
+            --  Emit an error on an attempt to redefine existing mode Mode. The
+            --  message is associated with the first argument of the current
+            --  pragma.
+
+            procedure Redefinition_Error (Prag : Node_Id);
+            --  Emit an error on an attempt to redefine the mode of Prag. The
+            --  message is associated with the first argument of the current
+            --  pragma.
+
+            ------------------
+            -- Chain_Pragma --
+            ------------------
+
+            procedure Chain_Pragma (Context : Entity_Id; Prag : Node_Id) is
+               Existing_Prag : constant Node_Id :=
+                                 SPARK_Mode_Pragmas (Context);
+            begin
+               --  The context does not have a prior mode defined
+
+               if No (Existing_Prag) then
+                  Set_SPARK_Mode_Pragmas (Context, Prag);
+
+               --  Chain the new mode on the list of SPARK_Mode pragmas. Verify
+               --  the consistency between the existing mode and the new one.
+
+               else
+                  Set_Next_Pragma (Existing_Prag, Prag);
+
+                  Check_Pragma_Conformance
+                    (Governing_Mode => Existing_Prag,
+                     New_Mode       => Prag);
+               end if;
+            end Chain_Pragma;
+
+            -----------------------
+            -- Check_Conformance --
+            -----------------------
+
+            procedure Check_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_Conformance;
+
+            ------------------------------
+            -- Check_Pragma_Conformance --
+            ------------------------------
+
+            procedure Check_Pragma_Conformance
+              (Governing_Mode : Node_Id;
+               New_Mode       : Node_Id)
+            is
+               Gov_M : constant SPARK_Mode_Id :=
+                         Get_SPARK_Mode_Id (Governing_Mode);
+               New_M : constant SPARK_Mode_Id := Get_SPARK_Mode_Id (New_Mode);
+
+            begin
+               --  The new mode is less restrictive than the established mode
+
+               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);
+
+                  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);
+               end if;
+            end Check_Pragma_Conformance;
+
+            -------------------------
+            -- Get_SPARK_Mode_Name --
+            -------------------------
+
+            function Get_SPARK_Mode_Name (Id : SPARK_Mode_Id) return Name_Id is
+            begin
+               if Id = SPARK_On then
+                  return Name_On;
+               elsif Id = SPARK_Off then
+                  return Name_Off;
+               elsif Id = SPARK_Auto then
+                  return Name_Auto;
+
+               --  Mode "None" should never be used in error message generation
+
+               else
+                  raise Program_Error;
+               end if;
+            end Get_SPARK_Mode_Name;
+
+            ------------------------
+            -- Redefinition_Error --
+            ------------------------
+
+            procedure Redefinition_Error (Mode : SPARK_Mode_Id) is
+            begin
+               Error_Msg_Name_1 := Get_SPARK_Mode_Name (Mode);
+               Error_Msg_N
+                 ("cannot redefine 'S'P'A'R'K mode, already set to %", Arg1);
+            end Redefinition_Error;
+
+            ------------------------
+            -- Redefinition_Error --
+            ------------------------
+
+            procedure Redefinition_Error (Prag : Node_Id) is
+               Mode : constant Name_Id :=
+                        Chars (Get_Pragma_Arg (First
+                         (Pragma_Argument_Associations (Prag))));
+            begin
+               Error_Msg_Name_1 := Mode;
+               Error_Msg_Sloc   := Sloc (Prag);
+               Error_Msg_N
+                 ("cannot redefine 'S'P'A'R'K mode, already set to % #", Arg1);
+            end Redefinition_Error;
+
+            --  Local variables
+
+            Body_Id   : Entity_Id;
+            Context   : Node_Id;
+            Mode      : Name_Id;
+            Mode_Id   : SPARK_Mode_Id;
+            Spec_Id   : Entity_Id;
+            Stmt      : Node_Id;
+            Unit_Prag : Node_Id;
+
+         --  Start of processing for SPARK_Mode
+
+         begin
+            GNAT_Pragma;
+            Check_No_Identifiers;
+            Check_At_Most_N_Arguments (1);
+
+            --  Check the legality of the mode
+
+            if Arg_Count = 1 then
+               Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off, Name_Auto);
+               Mode := Chars (Get_Pragma_Arg (Arg1));
+
+            --  A SPARK_Mode without an argument defaults to "On"
+
+            else
+               Mode := Name_On;
+            end if;
+
+            Mode_Id := Get_SPARK_Mode_Id (Mode);
+            Context := Parent (N);
+
+            --  The pragma appears in a configuration file
+
+            if No (Context) then
+               Check_Valid_Configuration_Pragma;
+
+               --  Set the global mode
+
+               if Global_SPARK_Mode = None then
+                  Global_SPARK_Mode := Mode_Id;
+
+               --  Catch an attempt to redefine an existing global mode by
+               --  using multiple configuration files.
+
+               elsif Global_SPARK_Mode /= Mode_Id then
+                  Redefinition_Error (Global_SPARK_Mode);
+               end if;
+
+            --  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;
+
+               Unit_Prag := SPARK_Mode_Pragma (Current_Sem_Unit);
+
+               --  Set the unit mode
+
+               if No (Unit_Prag) then
+                  Set_SPARK_Mode_Pragma (Current_Sem_Unit, N);
+
+               --  Catch an attempt to redefine the unit mode by using multiple
+               --  pragmas declared in the same region.
+
+               else
+                  Redefinition_Error (Unit_Prag);
+               end if;
+
+            --  The pragma applies to a [library unit] subprogram or package
+
+            else
+               --  Mode "Auto" cannot be used in nested subprograms or packages
+
+               if Mode_Id = SPARK_Auto then
+                  Error_Pragma_Arg
+                    ("mode `Auto` can only apply to the configuration variant "
+                     & "of pragma %", Arg1);
+               end if;
+
+               --  Verify the placement of the pragma with respect to package
+               --  or subprogram declarations and detect duplicates.
+
+               Stmt := Prev (N);
+               while Present (Stmt) loop
+
+                  --  Skip prior pragmas, but check for duplicates
+
+                  if Nkind (Stmt) = N_Pragma then
+                     if Pragma_Name (Stmt) = Pname then
+                        Error_Msg_Name_1 := Pname;
+                        Error_Msg_Sloc   := Sloc (Stmt);
+                        Error_Msg_N
+                          ("pragma % duplicates pragma declared #", N);
+                     end if;
+
+                  --  Skip internally generated code
+
+                  elsif not Comes_From_Source (Stmt) then
+                     null;
+
+                  --  The pragma applies to a package or subprogram declaration
+
+                  elsif Nkind_In (Stmt, N_Generic_Package_Declaration,
+                                        N_Generic_Subprogram_Declaration,
+                                        N_Package_Declaration,
+                                        N_Subprogram_Declaration)
+                  then
+                     Spec_Id := Defining_Unit_Name (Specification (Stmt));
+                     Chain_Pragma (Spec_Id, N);
+                     return;
+
+                  --  The pragma does not apply to a legal construct, issue an
+                  --  error and stop the analysis.
+
+                  else
+                     Pragma_Misplaced;
+                     exit;
+                  end if;
+
+                  Stmt := Prev (Stmt);
+               end loop;
+
+               --  If we get here, then we ran out of preceding statements. The
+               --  pragma is immediately within a body.
+
+               if Nkind_In (Context, N_Package_Body,
+                                     N_Subprogram_Body)
+               then
+                  Spec_Id := Corresponding_Spec (Context);
+
+                  if Nkind (Context) = N_Subprogram_Body then
+                     Context := Specification (Context);
+                  end if;
+
+                  Body_Id := Defining_Unit_Name (Context);
+
+                  Chain_Pragma (Body_Id, N);
+                  Check_Conformance (Spec_Id, Body_Id);
+
+               --  The pragma is at the top level of a package spec
+
+               elsif Nkind (Context) = N_Package_Specification then
+                  Spec_Id := Defining_Unit_Name (Context);
+                  Chain_Pragma (Spec_Id, N);
+
+               --  The pragma applies to the statements of a package body
+
+               elsif Nkind (Context) = N_Handled_Sequence_Of_Statements
+                 and then Nkind (Parent (Context)) = N_Package_Body
+               then
+                  Context := Parent (Context);
+                  Spec_Id := Corresponding_Spec (Context);
+                  Body_Id := Defining_Unit_Name (Context);
+
+                  Chain_Pragma (Body_Id, N);
+                  Check_Conformance (Spec_Id, Body_Id);
+
+               --  The pragma does not apply to a legal construct, issue an
+               --  error.
+
+               else
+                  Pragma_Misplaced;
+               end if;
+            end if;
+         end SPARK_Mod;
+
          --------------------------------
          -- Static_Elaboration_Desired --
          --------------------------------
@@ -18268,6 +18618,43 @@ package body Sem_Prag is
       return Result;
    end Get_Base_Subprogram;
 
+   -----------------------
+   -- Get_SPARK_Mode_Id --
+   -----------------------
+
+   function Get_SPARK_Mode_Id (N : Name_Id) return SPARK_Mode_Id is
+   begin
+      if N = Name_On then
+         return SPARK_On;
+      elsif N = Name_Off then
+         return SPARK_Off;
+      elsif N = Name_Auto then
+         return SPARK_Auto;
+
+      --  Any other argument is erroneous
+
+      else
+         raise Program_Error;
+      end if;
+   end Get_SPARK_Mode_Id;
+
+   -----------------------
+   -- Get_SPARK_Mode_Id --
+   -----------------------
+
+   function Get_SPARK_Mode_Id (N : Node_Id) return SPARK_Mode_Id is
+      Mode : Node_Id;
+
+   begin
+      pragma Assert
+        (Nkind (N) = N_Pragma
+          and then Present (Pragma_Argument_Associations (N)));
+
+      Mode := First (Pragma_Argument_Associations (N));
+
+      return Get_SPARK_Mode_Id (Chars (Get_Pragma_Arg (Mode)));
+   end Get_SPARK_Mode_Id;
+
    ----------------
    -- Initialize --
    ----------------
@@ -18332,11 +18719,33 @@ package body Sem_Prag is
    --  Start of processing for Is_Config_Static_String
 
    begin
-
       Name_Len := 0;
+
       return Add_Config_Static_String (Arg);
    end Is_Config_Static_String;
 
+   -------------------------------
+   -- Is_Elaboration_SPARK_Mode --
+   -------------------------------
+
+   function Is_Elaboration_SPARK_Mode (N : Node_Id) return Boolean is
+   begin
+      pragma Assert
+        (Nkind (N) = N_Pragma
+          and then Pragma_Name (N) = Name_SPARK_Mode
+          and then Is_List_Member (N));
+
+      --  Pragma SPARK_Mode affects the elaboration of a package body when it
+      --  appears in the statement part of the body.
+
+      return
+         Present (Parent (N))
+           and then Nkind (Parent (N)) = N_Handled_Sequence_Of_Statements
+           and then List_Containing (N) = Statements (Parent (N))
+           and then Present (Parent (Parent (N)))
+           and then Nkind (Parent (Parent (N))) = N_Package_Body;
+   end Is_Elaboration_SPARK_Mode;
+
    -----------------------------------------
    -- Is_Non_Significant_Pragma_Reference --
    -----------------------------------------
@@ -18524,6 +18933,7 @@ package body Sem_Prag is
       Pragma_Source_File_Name               => -1,
       Pragma_Source_File_Name_Project       => -1,
       Pragma_Source_Reference               => -1,
+      Pragma_SPARK_Mode                     =>  0,
       Pragma_Storage_Size                   => -1,
       Pragma_Storage_Unit                   => -1,
       Pragma_Static_Elaboration_Desired     => -1,
@@ -18682,6 +19092,26 @@ package body Sem_Prag is
       end if;
    end Is_Pragma_String_Literal;
 
+   ---------------------------
+   -- Is_Private_SPARK_Mode --
+   ---------------------------
+
+   function Is_Private_SPARK_Mode (N : Node_Id) return Boolean is
+   begin
+      pragma Assert
+        (Nkind (N) = N_Pragma
+          and then Pragma_Name (N) = Name_SPARK_Mode
+          and then Is_List_Member (N));
+
+      --  For pragma SPARK_Mode to be private, it has to appear in the private
+      --  declarations of a package.
+
+      return
+        Present (Parent (N))
+          and then Nkind (Parent (N)) = N_Package_Specification
+          and then List_Containing (N) = Private_Declarations (Parent (N));
+   end Is_Private_SPARK_Mode;
+
    -----------------------------
    -- Is_Valid_Assertion_Kind --
    -----------------------------
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index 3b8a3bc..fcbe988 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -113,6 +113,9 @@ package Sem_Prag is
    --  True have their analysis delayed until after the main program is parsed
    --  and analyzed.
 
+   function Get_SPARK_Mode_Id (N : Node_Id) return SPARK_Mode_Id;
+   --  Given a pragma SPARK_Mode node, return the corresponding mode id
+
    procedure Initialize;
    --  Initializes data structures used for pragma processing. Must be called
    --  before analyzing each new main source program.
@@ -127,6 +130,10 @@ package Sem_Prag is
    --  length, and then returns True. If it is not of the correct form, then an
    --  appropriate error message is posted, and False is returned.
 
+   function Is_Elaboration_SPARK_Mode (N : Node_Id) return Boolean;
+   --  Determine whether pragma SPARK_Mode appears in the statement part of a
+   --  package body.
+
    function Is_Non_Significant_Pragma_Reference (N : Node_Id) return Boolean;
    --  The node N is a node for an entity and the issue is whether the
    --  occurrence is a reference for the purposes of giving warnings about
@@ -143,6 +150,10 @@ package Sem_Prag is
    --  False is returned, then the argument is treated as an entity reference
    --  to the operator.
 
+   function Is_Private_SPARK_Mode (N : Node_Id) return Boolean;
+   --  Determine whether pragma SPARK_Mode appears in the private part of a
+   --  package.
+
    function Is_Valid_Assertion_Kind (Nam : Name_Id) return Boolean;
    --  Returns True if Nam is one of the names recognized as a valid assertion
    --  kind by the Assertion_Policy pragma. Note that the 'Class cases are
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index 2879579..f66aeee 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -1539,6 +1539,10 @@ package Sinfo is
    --      Used by processing for Pre/Postcondition pragmas to store a list of
    --      pragmas associated with the spec of a subprogram (see Sem_Prag for
    --      details).
+   --
+   --      Used by processing for pragma SPARK_Mode to store multiple pragmas
+   --      the apply to the same construct. These are visible/private mode for
+   --      a package spec and declarative/statement mode for package body.
 
    --  Next_Rep_Item (Node5-Sem)
    --    Present in pragma nodes, attribute definition nodes, enumeration rep
diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl
index ef983a7..bfe21bd 100644
--- a/gcc/ada/snames.ads-tmpl
+++ b/gcc/ada/snames.ads-tmpl
@@ -436,6 +436,7 @@ package Snames is
    Name_Short_Descriptors              : constant Name_Id := N + $; -- GNAT
    Name_Source_File_Name               : constant Name_Id := N + $; -- GNAT
    Name_Source_File_Name_Project       : constant Name_Id := N + $; -- GNAT
+   Name_SPARK_Mode                     : constant Name_Id := N + $; -- GNAT
    Name_Style_Checks                   : constant Name_Id := N + $; -- GNAT
    Name_Suppress                       : constant Name_Id := N + $;
    Name_Suppress_Exception_Locations   : constant Name_Id := N + $; -- GNAT
@@ -673,6 +674,7 @@ package Snames is
    Name_Assertion                      : constant Name_Id := N + $;
    Name_Assertions                     : constant Name_Id := N + $;
    Name_Attribute_Name                 : constant Name_Id := N + $;
+   Name_Auto                           : constant Name_Id := N + $;
    Name_Body_File_Name                 : constant Name_Id := N + $;
    Name_Boolean_Entry_Barriers         : constant Name_Id := N + $;
    Name_By_Any                         : constant Name_Id := N + $;
@@ -1748,6 +1750,7 @@ package Snames is
       Pragma_Short_Descriptors,
       Pragma_Source_File_Name,
       Pragma_Source_File_Name_Project,
+      Pragma_SPARK_Mode,
       Pragma_Style_Checks,
       Pragma_Suppress,
       Pragma_Suppress_Exception_Locations,
diff --git a/gcc/ada/types.ads b/gcc/ada/types.ads
index ec723dd..4bbaa6b 100644
--- a/gcc/ada/types.ads
+++ b/gcc/ada/types.ads
@@ -876,4 +876,12 @@ package Types is
      SE_Empty_Storage_Pool ..
      SE_Object_Too_Large;
 
+   ----------------------------------------
+   -- Types Used for SPARK Mode Handling --
+   ----------------------------------------
+
+   type SPARK_Mode_Id is (None, SPARK_Off, SPARK_Auto, SPARK_On);
+   --  Type used to represent all legal modes that can be set by aspect/pragma
+   --  SPARK_Mode.
+
 end Types;