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

	* checks.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* exp_ch4.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* opt.adb (SPARK_Mode_Config): Handled like other config flags
	* opt.ads (SPARK_Mode_Type): Moved here from types (renamed from
	SPARK_Mode_Id) (SPARK_Mode_Type): Add pragma Ordered, remove
	SPARK_ from names (SPARK_Mode): New flag (SPARK_Mode_Config):
	New flag (Config_Switches_Type): Add SPARK_Mode field
	* sem.adb: Minor code reorganization (remove unnecessary with)
	* sem.ads (Scope_Stack_Entry): Add Save_SPARK_Mode field
	* sem_aggr.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* sem_attr.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* sem_ch3.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* sem_ch4.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Reset SPARK_Mode
	from spec if needed
	* sem_ch7.adb (Analyze_Package_Body_Helper): Reset SPARK_Mode
	from spec if needed
	* sem_ch8.adb (Push_Scope): Save SPARK_Mode (Pop_Scope):
	Restore SPARK_Mode
	* sem_elab.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* sem_prag.adb (Get_SPARK_Mode_From_Pragma): New function
	(Get_SPARK_Mode_Id): Removed (Get_SPARK_Mode_Type): New name
	of Get_SPARK_Mode_Id
	* sem_prag.ads (Get_SPARK_Mode_From_Pragma): New function
	* sem_res.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* sem_util.adb: Check SPARK_Mode instead of GNATProve_Mode for
	converting warnings on inevitable exceptions to errors.
	* types.ads (SPARK_Mode_Id): Moved to opt.ads and renamed
	SPARK_Mode_Type

2014-01-20  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch13.adb: Add semantic information to rewritten type
	reference.

2014-01-20  Ed Schonberg  <schonberg@adacore.com>

	* exp_ch5.adb (Expand_N_Assignment_Statement): If both sides
	are of a type with unknown discriminants, convert both to the
	underlying view of the type, so that the proper constraint check
	can be applied to the right-hand side.

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

	* atree.adb (Copy_Node): Fix failure to copy last component
	(Exchange_Entities): Fix failure to exchange last entity

2014-01-20  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch12.adb: Code clean up.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@206844 138bc75d-0d04-0410-961f-82ee72b054a4

24 files changed, 215 insertions, 111 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 6fc4554f77e..0ae1c7adeaa 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,66 @@
 2014-01-20  Robert Dewar  <dewar@adacore.com>
 
+	* checks.adb: Check SPARK_Mode instead of GNATProve_Mode for
+	converting warnings on inevitable exceptions to errors.
+	* exp_ch4.adb: Check SPARK_Mode instead of GNATProve_Mode for
+	converting warnings on inevitable exceptions to errors.
+	* opt.adb (SPARK_Mode_Config): Handled like other config flags
+	* opt.ads (SPARK_Mode_Type): Moved here from types (renamed from
+	SPARK_Mode_Id) (SPARK_Mode_Type): Add pragma Ordered, remove
+	SPARK_ from names (SPARK_Mode): New flag (SPARK_Mode_Config):
+	New flag (Config_Switches_Type): Add SPARK_Mode field
+	* sem.adb: Minor code reorganization (remove unnecessary with)
+	* sem.ads (Scope_Stack_Entry): Add Save_SPARK_Mode field
+	* sem_aggr.adb: Check SPARK_Mode instead of GNATProve_Mode for
+	converting warnings on inevitable exceptions to errors.
+	* sem_attr.adb: Check SPARK_Mode instead of GNATProve_Mode for
+	converting warnings on inevitable exceptions to errors.
+	* sem_ch3.adb: Check SPARK_Mode instead of GNATProve_Mode for
+	converting warnings on inevitable exceptions to errors.
+	* sem_ch4.adb: Check SPARK_Mode instead of GNATProve_Mode for
+	converting warnings on inevitable exceptions to errors.
+	* sem_ch6.adb (Analyze_Subprogram_Body_Helper): Reset SPARK_Mode
+	from spec if needed
+	* sem_ch7.adb (Analyze_Package_Body_Helper): Reset SPARK_Mode
+	from spec if needed
+	* sem_ch8.adb (Push_Scope): Save SPARK_Mode (Pop_Scope):
+	Restore SPARK_Mode
+	* sem_elab.adb: Check SPARK_Mode instead of GNATProve_Mode for
+	converting warnings on inevitable exceptions to errors.
+	* sem_prag.adb (Get_SPARK_Mode_From_Pragma): New function
+	(Get_SPARK_Mode_Id): Removed (Get_SPARK_Mode_Type): New name
+	of Get_SPARK_Mode_Id
+	* sem_prag.ads (Get_SPARK_Mode_From_Pragma): New function
+	* sem_res.adb: Check SPARK_Mode instead of GNATProve_Mode for
+	converting warnings on inevitable exceptions to errors.
+	* sem_util.adb: Check SPARK_Mode instead of GNATProve_Mode for
+	converting warnings on inevitable exceptions to errors.
+	* types.ads (SPARK_Mode_Id): Moved to opt.ads and renamed
+	SPARK_Mode_Type
+
+2014-01-20  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch13.adb: Add semantic information to rewritten type
+	reference.
+
+2014-01-20  Ed Schonberg  <schonberg@adacore.com>
+
+	* exp_ch5.adb (Expand_N_Assignment_Statement): If both sides
+	are of a type with unknown discriminants, convert both to the
+	underlying view of the type, so that the proper constraint check
+	can be applied to the right-hand side.
+
+2014-01-20  Robert Dewar  <dewar@adacore.com>
+
+	* atree.adb (Copy_Node): Fix failure to copy last component
+	(Exchange_Entities): Fix failure to exchange last entity
+
+2014-01-20  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch12.adb: Code clean up.
+
+2014-01-20  Robert Dewar  <dewar@adacore.com>
+
 	* gnat_rm.texi, sem_ch4.adb: Minor reformatting.
 
 2014-01-20  Ed Schonberg  <schonberg@adacore.com>
diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb
index a44a247b896..e7d4b20741f 100644
--- a/gcc/ada/atree.adb
+++ b/gcc/ada/atree.adb
@@ -733,6 +733,7 @@ package body Atree is
          Nodes.Table (Destination + 2) := Nodes.Table (Source + 2);
          Nodes.Table (Destination + 3) := Nodes.Table (Source + 3);
          Nodes.Table (Destination + 4) := Nodes.Table (Source + 4);
+         Nodes.Table (Destination + 5) := Nodes.Table (Source + 5);
 
       else
          pragma Assert (not Has_Extension (Source));
@@ -1105,19 +1106,27 @@ package body Atree is
       Temp_Ent := Nodes.Table (E1);
       Nodes.Table (E1) := Nodes.Table (E2);
       Nodes.Table (E2) := Temp_Ent;
+
       Temp_Ent := Nodes.Table (E1 + 1);
       Nodes.Table (E1 + 1) := Nodes.Table (E2 + 1);
       Nodes.Table (E2 + 1) := Temp_Ent;
+
       Temp_Ent := Nodes.Table (E1 + 2);
       Nodes.Table (E1 + 2) := Nodes.Table (E2 + 2);
       Nodes.Table (E2 + 2) := Temp_Ent;
+
       Temp_Ent := Nodes.Table (E1 + 3);
       Nodes.Table (E1 + 3) := Nodes.Table (E2 + 3);
       Nodes.Table (E2 + 3) := Temp_Ent;
+
       Temp_Ent := Nodes.Table (E1 + 4);
       Nodes.Table (E1 + 4) := Nodes.Table (E2 + 4);
       Nodes.Table (E2 + 4) := Temp_Ent;
 
+      Temp_Ent := Nodes.Table (E1 + 5);
+      Nodes.Table (E1 + 5) := Nodes.Table (E2 + 5);
+      Nodes.Table (E2 + 5) := Temp_Ent;
+
       --  That exchange exchanged the parent pointers as well, which is what
       --  we want, but we need to patch up the defining identifier pointers
       --  in the parent nodes (the child pointers) to match this switch
diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index eb6c5b74343..496c3a23329 100644
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -3697,7 +3697,7 @@ package body Checks is
       --  Here we have the optimizable case, warn if not short-circuited
 
       if K = N_Op_And or else K = N_Op_Or then
-         Error_Msg_Warn := not GNATprove_Mode;
+         Error_Msg_Warn := SPARK_Mode /= On;
 
          case Check is
             when Access_Check =>
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index b154a6f6e3f..7d1ec81446e 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -9654,7 +9654,7 @@ package body Exp_Ch4 is
 
       procedure Raise_Accessibility_Error is
       begin
-         Error_Msg_Warn := not GNATprove_Mode;
+         Error_Msg_Warn := SPARK_Mode /= On;
          Rewrite (N,
            Make_Raise_Program_Error (Sloc (N),
              Reason => PE_Accessibility_Check_Failed));
diff --git a/gcc/ada/exp_ch5.adb b/gcc/ada/exp_ch5.adb
index f166ff464ae..1fb6dc7ee1c 100644
--- a/gcc/ada/exp_ch5.adb
+++ b/gcc/ada/exp_ch5.adb
@@ -1850,12 +1850,14 @@ package body Exp_Ch5 is
          --  If the Lhs has a private type with unknown discriminants, it
          --  may have a full view with discriminants, but those are nameable
          --  only in the underlying type, so convert the Rhs to it before
-         --  potential checking.
+         --  potential checking. Convert Lhs as well, otherwise the actual
+         --  subtype might not be constructible.
 
       elsif Has_Unknown_Discriminants (Base_Type (Etype (Lhs)))
         and then Has_Discriminants (Typ)
       then
          Rewrite (Rhs, OK_Convert_To (Base_Type (Typ), Rhs));
+         Rewrite (Lhs, OK_Convert_To (Base_Type (Typ), Lhs));
          Apply_Discriminant_Check (Rhs, Typ, Lhs);
 
       --  In the access type case, we need the same discriminant check, and
diff --git a/gcc/ada/opt.adb b/gcc/ada/opt.adb
index 0f65614811b..ce23faacaab 100644
--- a/gcc/ada/opt.adb
+++ b/gcc/ada/opt.adb
@@ -63,6 +63,7 @@ package body Opt is
       Persistent_BSS_Mode_Config            := Persistent_BSS_Mode;
       Polling_Required_Config               := Polling_Required;
       Short_Descriptors_Config              := Short_Descriptors;
+      SPARK_Mode_Config                     := SPARK_Mode;
       Use_VADS_Size_Config                  := Use_VADS_Size;
 
       --  Reset the indication that Optimize_Alignment was set locally, since
@@ -98,6 +99,7 @@ package body Opt is
       Persistent_BSS_Mode            := Save.Persistent_BSS_Mode;
       Polling_Required               := Save.Polling_Required;
       Short_Descriptors              := Save.Short_Descriptors;
+      SPARK_Mode                     := Save.SPARK_Mode;
       Use_VADS_Size                  := Save.Use_VADS_Size;
 
       --  Update consistently the value of Init_Or_Norm_Scalars. The value of
@@ -134,6 +136,7 @@ package body Opt is
       Save.Persistent_BSS_Mode            := Persistent_BSS_Mode;
       Save.Polling_Required               := Polling_Required;
       Save.Short_Descriptors              := Short_Descriptors;
+      Save.SPARK_Mode                     := SPARK_Mode;
       Save.Use_VADS_Size                  := Use_VADS_Size;
    end Save_Opt_Config_Switches;
 
@@ -164,6 +167,7 @@ package body Opt is
          Persistent_BSS_Mode         := False;
          Use_VADS_Size               := False;
          Optimize_Alignment_Local    := True;
+         SPARK_Mode                  := Auto;
 
          --  For an internal unit, assertions/debug pragmas are off unless this
          --  is the main unit and they were explicitly enabled. We also make
@@ -198,6 +202,7 @@ package body Opt is
          Optimize_Alignment          := Optimize_Alignment_Config;
          Optimize_Alignment_Local    := False;
          Persistent_BSS_Mode         := Persistent_BSS_Mode_Config;
+         SPARK_Mode                  := SPARK_Mode_Config;
          Use_VADS_Size               := Use_VADS_Size_Config;
 
          --  Update consistently the value of Init_Or_Norm_Scalars. The value
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 28381bf15df..6b291ac2f7c 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -1,5 +1,5 @@
 ------------------------------------------------------------------------------
---                                                                          --
+--                                SPARK                                          --
 --                         GNAT COMPILER COMPONENTS                         --
 --                                                                          --
 --                                  O P T                                   --
@@ -1264,6 +1264,14 @@ package Opt is
    --  GNAT
    --  Set True if a pragma Short_Descriptors applies to the current unit.
 
+   type SPARK_Mode_Type is (None, Off, Auto, On);
+   pragma Ordered (SPARK_Mode_Type);
+   --  Possible legal modes that can be set by aspect/pragma SPARK_Mode
+
+   SPARK_Mode : SPARK_Mode_Type := None;
+   --  GNAT
+   --  Current SPARK mode setting
+
    Special_Exception_Package_Used : Boolean := False;
    --  GNAT
    --  Set to True if either of the unit GNAT.Most_Recent_Exception or
@@ -1895,6 +1903,9 @@ package Opt is
    --  This flag is used to set the initial value for Short_Descriptors at the
    --  start of analyzing each unit.
 
+   SPARK_Mode_Config : SPARK_Mode_Type := None;
+   --  The setting of SPARK_Mode from configuration pragmas
+
    Use_VADS_Size_Config : Boolean;
    --  GNAT
    --  This is the value of the configuration switch that controls the use of
@@ -2001,10 +2012,6 @@ package Opt is
    -- Modes for Formal Verification --
    -----------------------------------
 
-   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.
-
    GNATprove_Mode : Boolean := False;
    --  Specific compiling mode targeting formal verification for those parts
    --  of the input code that belong to the SPARK 2014 subset of Ada. Set True
@@ -2043,6 +2050,7 @@ private
       Persistent_BSS_Mode            : Boolean;
       Polling_Required               : Boolean;
       Short_Descriptors              : Boolean;
+      SPARK_Mode                     : SPARK_Mode_Type;
       Use_VADS_Size                  : Boolean;
    end record;
 
diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb
index ced4d41a165..3e66a0e0563 100644
--- a/gcc/ada/sem.adb
+++ b/gcc/ada/sem.adb
@@ -32,7 +32,6 @@ with Fname;    use Fname;
 with Lib;      use Lib;
 with Lib.Load; use Lib.Load;
 with Nlists;   use Nlists;
-with Opt;      use Opt;
 with Output;   use Output;
 with Restrict; use Restrict;
 with Sem_Attr; use Sem_Attr;
diff --git a/gcc/ada/sem.ads b/gcc/ada/sem.ads
index 9bc7ff757bc..c6b11dbca69 100644
--- a/gcc/ada/sem.ads
+++ b/gcc/ada/sem.ads
@@ -203,6 +203,7 @@
 
 with Alloc;
 with Einfo;  use Einfo;
+with Opt;    use Opt;
 with Table;
 with Types;  use Types;
 
@@ -474,6 +475,9 @@ package Sem is
       Save_Default_Storage_Pool : Node_Id;
       --  Save contents of Default_Storage_Pool on entry to restore on exit
 
+      Save_SPARK_Mode : SPARK_Mode_Type;
+      --  Setting of SPARK_Mode on entry to restore on exit
+
       Is_Transient : Boolean;
       --  Marks transient scopes (see Exp_Ch7 body for details)
 
diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb
index 7096aae5bed..03930f5e3cf 100644
--- a/gcc/ada/sem_aggr.adb
+++ b/gcc/ada/sem_aggr.adb
@@ -597,7 +597,7 @@ package body Sem_Aggr is
 
                elsif Expr_Value (This_Low) /= Expr_Value (Aggr_Low (Dim)) then
                   Set_Raises_Constraint_Error (N);
-                  Error_Msg_Warn := not GNATprove_Mode;
+                  Error_Msg_Warn := SPARK_Mode /= On;
                   Error_Msg_N ("sub-aggregate low bound mismatch<<", N);
                   Error_Msg_N ("\Constraint_Error [<<", N);
                end if;
@@ -611,7 +611,7 @@ package body Sem_Aggr is
                  Expr_Value (This_High) /= Expr_Value (Aggr_High (Dim))
                then
                   Set_Raises_Constraint_Error (N);
-                  Error_Msg_Warn := not GNATprove_Mode;
+                  Error_Msg_Warn := SPARK_Mode /= On;
                   Error_Msg_N ("sub-aggregate high bound mismatch<<", N);
                   Error_Msg_N ("\Constraint_Error [<<", N);
                end if;
@@ -1456,7 +1456,7 @@ package body Sem_Aggr is
 
          if OK_BH and then OK_AH and then Val_BH < Val_AH then
             Set_Raises_Constraint_Error (N);
-            Error_Msg_Warn := not GNATprove_Mode;
+            Error_Msg_Warn := SPARK_Mode /= On;
             Error_Msg_N ("upper bound out of range<<", AH);
             Error_Msg_N ("\Constraint_Error [<<", AH);
 
@@ -1500,14 +1500,14 @@ package body Sem_Aggr is
 
          if OK_L and then Val_L > Val_AL then
             Set_Raises_Constraint_Error (N);
-            Error_Msg_Warn := not GNATprove_Mode;
+            Error_Msg_Warn := SPARK_Mode /= On;
             Error_Msg_N ("lower bound of aggregate out of range<<", N);
             Error_Msg_N ("\Constraint_Error [<<", N);
          end if;
 
          if OK_H and then Val_H < Val_AH then
             Set_Raises_Constraint_Error (N);
-            Error_Msg_Warn := not GNATprove_Mode;
+            Error_Msg_Warn := SPARK_Mode /= On;
             Error_Msg_N ("upper bound of aggregate out of range<<", N);
             Error_Msg_N ("\Constraint_Error [<<", N);
          end if;
@@ -1548,7 +1548,7 @@ package body Sem_Aggr is
 
          if Range_Len < Len then
             Set_Raises_Constraint_Error (N);
-            Error_Msg_Warn := not GNATprove_Mode;
+            Error_Msg_Warn := SPARK_Mode /= On;
             Error_Msg_N ("too many elements<<", N);
             Error_Msg_N ("\Constraint_Error [<<", N);
          end if;
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 5ff96d7843e..1b585cb61fa 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -5396,7 +5396,7 @@ package body Sem_Attr is
                                            Name_Simple_Storage_Pool_Type))
                then
                   Error_Msg_Name_1 := Aname;
-                     Error_Msg_Warn := not GNATprove_Mode;
+                     Error_Msg_Warn := SPARK_Mode /= On;
                   Error_Msg_N ("cannot use % attribute for type with simple "
                                & "storage pool<<", N);
                   Error_Msg_N ("\Program_Error [<<", N);
@@ -9311,7 +9311,7 @@ package body Sem_Attr is
          --  know will fail, so generate an appropriate warning.
 
          if In_Instance_Body then
-            Error_Msg_Warn := not GNATprove_Mode;
+            Error_Msg_Warn := SPARK_Mode /= On;
             Error_Msg_F
               ("non-local pointer cannot point to local object<<", P);
             Error_Msg_F ("\Program_Error [<<", P);
@@ -9792,7 +9792,7 @@ package body Sem_Attr is
                   --  know will fail, so generate an appropriate warning.
 
                   if In_Instance_Body then
-                     Error_Msg_Warn := not GNATprove_Mode;
+                     Error_Msg_Warn := SPARK_Mode /= On;
                      Error_Msg_F
                        ("non-local pointer cannot point to local object<<", P);
                      Error_Msg_F ("\Program_Error [<<", P);
diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb
index 5388f63ca97..12f53d3eddf 100644
--- a/gcc/ada/sem_ch12.adb
+++ b/gcc/ada/sem_ch12.adb
@@ -13061,13 +13061,13 @@ package body Sem_Ch12 is
                --  ASIS tree traversal, so we recover the original entity to
                --  expose the renaming. Take into account that the context may
                --  be a nested generic and that the original node may itself
-               --  have an associated node.
+               --  have an associated node that had better be an entity.
 
                if Ekind (E) = E_Package
                  and then Nkind (Parent (N)) = N_Expanded_Name
                  and then Present (Original_Node (N2))
+                 and then Is_Entity_Name (Original_Node (N2))
                  and then Present (Entity (Original_Node (N2)))
-                 and then Is_Entity_Name (Entity (Original_Node (N2)))
                then
                   if Is_Global (Entity (Original_Node (N2))) then
                      N2 := Original_Node (N2);
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 9d452b13ea5..630892a4a9f 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -5939,6 +5939,20 @@ package body Sem_Ch13 is
 
          procedure Replace_Type_Reference (N : Node_Id) is
          begin
+
+            --  Add semantic information to node to be rewritten, for ASIS
+            --  navigation needs.
+
+            if Nkind (N) = N_Identifier then
+               Set_Entity (N, T);
+               Set_Etype  (N, T);
+
+            elsif Nkind (N) = N_Selected_Component then
+               Analyze (Prefix (N));
+               Set_Entity (Selector_Name (N), T);
+               Set_Etype  (Selector_Name (N), T);
+            end if;
+
             --  Invariant'Class, replace with T'Class (obj)
 
             if Class_Present (Ritem) then
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 68cffb6ba37..ffc233d28be 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -3797,7 +3797,7 @@ package body Sem_Ch3 is
                     and then Present (Get_Attribute_Definition_Clause
                                         (E, Attribute_Address))
                   then
-                     Error_Msg_Warn := not GNATprove_Mode;
+                     Error_Msg_Warn := SPARK_Mode /= On;
                      Error_Msg_N
                        ("more than one task with same entry address<<", N);
                      Error_Msg_N ("\Program_Error [<<", N);
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 3e02d38d043..867406ed625 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -4651,7 +4651,7 @@ package body Sem_Ch4 is
                      --  In SPARK mode, this is made into an error to simplify
                      --  the processing of the formal verification backend.
 
-                     Error_Msg_Warn := not GNATprove_Mode;
+                     Error_Msg_Warn := SPARK_Mode /= On;
                      Apply_Compile_Time_Constraint_Error
                        (N, "component not present in }<<",
                         CE_Discriminant_Check_Failed,
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 22b661a21ba..1120c6033fe 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -983,7 +983,7 @@ package body Sem_Ch6 is
                    Reason => PE_Accessibility_Check_Failed));
                Analyze (N);
 
-               Error_Msg_Warn := not GNATprove_Mode;
+               Error_Msg_Warn := SPARK_Mode /= On;
                Error_Msg_N ("cannot return a local value by reference<<", N);
                Error_Msg_NE ("\& [<<", N, Standard_Program_Error);
             end if;
@@ -2987,6 +2987,13 @@ package body Sem_Ch6 is
 
             Push_Scope (Spec_Id);
 
+            --  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));
+            end if;
+
             --  Make sure that the subprogram is immediately visible. For
             --  child units that have no separate spec this is indispensable.
             --  Otherwise it is safe albeit redundant.
@@ -7223,7 +7230,7 @@ package body Sem_Ch6 is
 
                --  In GNATprove mode, it is an error to have a missing return
 
-               Error_Msg_Warn := not GNATprove_Mode;
+               Error_Msg_Warn := SPARK_Mode /= On;
                Error_Msg_N
                  ("RETURN statement missing following this statement<<!",
                   Last_Stm);
@@ -7252,7 +7259,7 @@ package body Sem_Ch6 is
                      & "will raise Program_Error??", Last_Stm);
                end if;
 
-               Error_Msg_Warn := not GNATprove_Mode;
+               Error_Msg_Warn := SPARK_Mode /= On;
                Error_Msg_NE
                  ("\procedure & is marked as No_Return<<!", Last_Stm, Proc);
             end if;
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index 76875b27afc..30704ff877c 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.adb
@@ -56,6 +56,7 @@ with Sem_Ch12; use Sem_Ch12;
 with Sem_Ch13; use Sem_Ch13;
 with Sem_Disp; use Sem_Disp;
 with Sem_Eval; use Sem_Eval;
+with Sem_Prag; use Sem_Prag;
 with Sem_Util; use Sem_Util;
 with Sem_Warn; use Sem_Warn;
 with Snames;   use Snames;
@@ -345,6 +346,13 @@ package body Sem_Ch7 is
 
       Push_Scope (Spec_Id);
 
+      --  Set SPARK_Mode from spec if package spec had SPARK_Mode pragma
+
+      if Present (SPARK_Mode_Pragmas (Spec_Id)) then
+         SPARK_Mode :=
+           Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragmas (Spec_Id));
+      end if;
+
       Set_Categorization_From_Pragmas (N);
 
       Install_Visible_Declarations (Spec_Id);
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index fecfcc89e9e..33c3dbf7aac 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -7395,6 +7395,7 @@ package body Sem_Ch8 is
       Local_Suppress_Stack_Top := SST.Save_Local_Suppress_Stack_Top;
       Check_Policy_List        := SST.Save_Check_Policy_List;
       Default_Pool             := SST.Save_Default_Storage_Pool;
+      SPARK_Mode               := SST.Save_SPARK_Mode;
 
       if Debug_Flag_W then
          Write_Str ("<-- exiting scope: ");
@@ -7468,6 +7469,7 @@ package body Sem_Ch8 is
          SST.Save_Local_Suppress_Stack_Top := Local_Suppress_Stack_Top;
          SST.Save_Check_Policy_List        := Check_Policy_List;
          SST.Save_Default_Storage_Pool     := Default_Pool;
+         SST.Save_SPARK_Mode               := SPARK_Mode;
 
          if Scope_Stack.Last > Scope_Stack.First then
             SST.Component_Alignment_Default := Scope_Stack.Table
diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index 0c789c20211..4e6436194c8 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -1138,7 +1138,7 @@ package body Sem_Elab is
 
       --  Here we definitely have a bad instantiation
 
-      Error_Msg_Warn := not GNATprove_Mode;
+      Error_Msg_Warn := SPARK_Mode /= On;
       Error_Msg_NE ("cannot instantiate& before body seen<<", N, Ent);
 
       if Present (Instance_Spec (N)) then
@@ -2179,7 +2179,7 @@ package body Sem_Elab is
       --  level, and the ABE is bound to occur.
 
       if Elab_Call.Last = 0 then
-         Error_Msg_Warn := not GNATprove_Mode;
+         Error_Msg_Warn := SPARK_Mode /= On;
 
          if Inst_Case then
             Error_Msg_NE
@@ -2263,7 +2263,7 @@ package body Sem_Elab is
            and then (Nkind (Original_Node (N)) /= N_Function_Call
                       or else not In_Assertion_Expression (Original_Node (N)))
          then
-            Error_Msg_Warn := not GNATprove_Mode;
+            Error_Msg_Warn := SPARK_Mode /= On;
 
             if Inst_Case then
                Error_Msg_NE
@@ -2370,7 +2370,7 @@ package body Sem_Elab is
                       or else
                     Scope (Proc) = Scope (Defining_Identifier (Decl)))
                then
-                  Error_Msg_Warn := not GNATprove_Mode;
+                  Error_Msg_Warn := SPARK_Mode /= On;
                   Error_Msg_N
                     ("task will be activated before elaboration of its body<<",
                       Decl);
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 9055ba83bfd..880a829853e 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -47,7 +47,6 @@ with Lib.Xref; use Lib.Xref;
 with Namet.Sp; use Namet.Sp;
 with Nlists;   use Nlists;
 with Nmake;    use Nmake;
-with Opt;      use Opt;
 with Output;   use Output;
 with Par_SCO;  use Par_SCO;
 with Restrict; use Restrict;
@@ -253,10 +252,10 @@ 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;
+   function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type;
    --  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.
+   --  Get_SPARK_Mode_Type. Convert a name into a corresponding value of type
+   --  SPARK_Mode_Type.
 
    function Is_Part_Of
      (State    : Entity_Id;
@@ -18065,8 +18064,7 @@ package body Sem_Prag is
                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.
+            --  the mode of the context. New_Id is the desired new mode.
 
             procedure Check_Pragma_Conformance
               (Governing_Mode : Node_Id;
@@ -18076,8 +18074,8 @@ package body Sem_Prag is
             --  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
+            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 --
@@ -18086,22 +18084,19 @@ package body Sem_Prag is
             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);
+            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;
 
             ----------------------------------
@@ -18150,9 +18145,10 @@ package body Sem_Prag is
               (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);
+               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);
 
             begin
                --  The new mode is less restrictive than the established mode
@@ -18173,13 +18169,15 @@ package body Sem_Prag is
             -- Get_SPARK_Mode_Name --
             -------------------------
 
-            function Get_SPARK_Mode_Name (Id : SPARK_Mode_Id) return Name_Id is
+            function Get_SPARK_Mode_Name
+              (Id : SPARK_Mode_Type) return Name_Id
+            is
             begin
-               if Id = SPARK_On then
+               if Id = On then
                   return Name_On;
-               elsif Id = SPARK_Off then
+               elsif Id = Off then
                   return Name_Off;
-               elsif Id = SPARK_Auto then
+               elsif Id = Auto then
                   return Name_Auto;
 
                --  Mode "None" should never be used in error message generation
@@ -18194,51 +18192,48 @@ package body Sem_Prag is
             Body_Id : Entity_Id;
             Context : Node_Id;
             Mode    : Name_Id;
-            Mode_Id : SPARK_Mode_Id;
+            Mode_Id : SPARK_Mode_Type;
             Spec_Id : Entity_Id;
             Stmt    : Node_Id;
 
-         --  Start of processing for SPARK_Mode
+         --  Start of processing for SPARK_Mod
 
          begin
             GNAT_Pragma;
             Check_No_Identifiers;
             Check_At_Most_N_Arguments (1);
 
-            --  Check the legality of the mode
+            --  Check the legality of the mode (no argument = ON)
 
             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);
+            Mode_Id := Get_SPARK_Mode_Type (Mode);
             Context := Parent (N);
+            SPARK_Mode := Mode_Id;
 
             --  The pragma appears in a configuration file
 
             if No (Context) then
                Check_Valid_Configuration_Pragma;
-               Global_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);
+                  Set_SPARK_Mode_Pragma (Current_Sem_Unit, N);
 
             --  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
+               if Mode_Id = Auto then
                   Error_Pragma_Arg
                     ("mode `Auto` can only apply to the configuration variant "
                      & "of pragma %", Arg1);
@@ -18256,8 +18251,7 @@ package body Sem_Prag is
                      if Pragma_Name (Stmt) = Pname then
                         Error_Msg_Name_1 := Pname;
                         Error_Msg_Sloc   := Sloc (Stmt);
-                        Error_Msg_N
-                          ("pragma % duplicates pragma declared #", N);
+                        Error_Msg_N ("pragma% duplicates pragma declared#", N);
                      end if;
 
                   --  Skip internally generated code
@@ -18322,8 +18316,7 @@ package body Sem_Prag is
                   Spec_Id := Defining_Unit_Name (Context);
                   Chain_Pragma (Spec_Id, N);
 
-               --  The pragma is immediately within a package or subprogram
-               --  body.
+               --  Pragma is immediately within a package or subprogram body
 
                --    function F ... is
                --       pragma SPARK_Mode;
@@ -22845,30 +22838,30 @@ package body Sem_Prag is
    end Get_Base_Subprogram;
 
    -----------------------
-   -- Get_SPARK_Mode_Id --
+   -- Get_SPARK_Mode_Type --
    -----------------------
 
-   function Get_SPARK_Mode_Id (N : Name_Id) return SPARK_Mode_Id is
+   function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type is
    begin
       if N = Name_On then
-         return SPARK_On;
+         return On;
       elsif N = Name_Off then
-         return SPARK_Off;
+         return Off;
       elsif N = Name_Auto then
-         return SPARK_Auto;
+         return Auto;
 
       --  Any other argument is erroneous
 
       else
          raise Program_Error;
       end if;
-   end Get_SPARK_Mode_Id;
+   end Get_SPARK_Mode_Type;
 
-   -----------------------
-   -- Get_SPARK_Mode_Id --
-   -----------------------
+   --------------------------------
+   -- Get_SPARK_Mode_From_Pragma --
+   --------------------------------
 
-   function Get_SPARK_Mode_Id (N : Node_Id) return SPARK_Mode_Id is
+   function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type is
       Args : List_Id;
       Mode : Node_Id;
 
@@ -22880,14 +22873,14 @@ package body Sem_Prag is
 
       if Present (Args) then
          Mode := First (Pragma_Argument_Associations (N));
-         return Get_SPARK_Mode_Id (Chars (Get_Pragma_Arg (Mode)));
+         return Get_SPARK_Mode_Type (Chars (Get_Pragma_Arg (Mode)));
 
-      --  When SPARK_Mode appears without an argument, the default is ON
+      --  If SPARK_Mode pragma has no argument, default is ON
 
       else
-         return SPARK_On;
+         return On;
       end if;
-   end Get_SPARK_Mode_Id;
+   end Get_SPARK_Mode_From_Pragma;
 
    ----------------
    -- Initialize --
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index c03799dd56f..8dcee63b635 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -27,6 +27,7 @@
 --  (logically this processing belongs in chapter 4)
 
 with Namet;  use Namet;
+with Opt;    use Opt;
 with Snames; use Snames;
 with Types;  use Types;
 
@@ -130,8 +131,8 @@ 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
+   function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type;
+   --  Given a pragma SPARK_Mode node, return corresponding mode id
 
    procedure Initialize;
    --  Initializes data structures used for pragma processing. Must be called
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 1b003772578..3919dc5cce5 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -769,7 +769,7 @@ package body Sem_Res is
               and then Nkind (Parent (P)) = N_Subprogram_Body
               and then Is_Empty_List (Declarations (Parent (P)))
             then
-               Error_Msg_Warn := not GNATprove_Mode;
+               Error_Msg_Warn := SPARK_Mode /= On;
                Error_Msg_N ("!infinite recursion<<", N);
                Error_Msg_N ("\!Storage_Error [<<", N);
                Insert_Action (N,
@@ -868,7 +868,7 @@ package body Sem_Res is
          end if;
       end loop;
 
-      Error_Msg_Warn := not GNATprove_Mode;
+      Error_Msg_Warn := SPARK_Mode /= On;
       Error_Msg_N ("!possible infinite recursion<<", N);
       Error_Msg_N ("\!??Storage_Error ]<<", N);
 
@@ -4555,7 +4555,7 @@ package body Sem_Res is
                  Deepest_Type_Access_Level (Typ)
             then
                if In_Instance_Body then
-                  Error_Msg_Warn := not GNATprove_Mode;
+                  Error_Msg_Warn := SPARK_Mode /= On;
                   Error_Msg_N
                     ("type in allocator has deeper level than "
                      & "designated class-wide type<<", E);
@@ -4666,7 +4666,7 @@ package body Sem_Res is
         and then Ekind (Current_Scope) = E_Package
         and then not In_Package_Body (Current_Scope)
       then
-         Error_Msg_Warn := not GNATprove_Mode;
+         Error_Msg_Warn := SPARK_Mode /= On;
          Error_Msg_N ("cannot activate task before body seen<<", N);
          Error_Msg_N ("\Program_Error [<<", N);
       end if;
@@ -4680,7 +4680,7 @@ package body Sem_Res is
         and then Present (Subpool_Handle_Name (N))
         and then Has_Task (Desig_T)
       then
-         Error_Msg_Warn := not GNATprove_Mode;
+         Error_Msg_Warn := SPARK_Mode /= On;
          Error_Msg_N ("cannot allocate task on subpool<<", N);
          Error_Msg_N ("\Program_Error [<<", N);
 
@@ -5396,7 +5396,7 @@ package body Sem_Res is
                            and then Is_Entry_Barrier_Function (P))
                then
                   Rtype := Etype (N);
-                  Error_Msg_Warn := not GNATprove_Mode;
+                  Error_Msg_Warn := SPARK_Mode /= On;
                   Error_Msg_NE
                     ("& should not be used in entry body (RM C.7(17))<<",
                      N, Nam);
@@ -5697,7 +5697,7 @@ package body Sem_Res is
                      --  Here warning is to be issued
 
                      Set_Has_Recursive_Call (Nam);
-                     Error_Msg_Warn := not GNATprove_Mode;
+                     Error_Msg_Warn := SPARK_Mode /= On;
                      Error_Msg_N ("possible infinite recursion<<!", N);
                      Error_Msg_N ("\Storage_Error ]<<!", N);
                   end if;
@@ -6011,7 +6011,7 @@ package body Sem_Res is
             end loop;
 
             if not Call_OK then
-               Error_Msg_Warn := not GNATprove_Mode;
+               Error_Msg_Warn := SPARK_Mode /= On;
                Error_Msg_N ("!cannot determine tag of result<<", N);
                Error_Msg_N ("\Program_Error [<<!", N);
                Insert_Action (N,
@@ -10877,7 +10877,7 @@ package body Sem_Res is
                     Deepest_Type_Access_Level (Opnd_Type)
                then
                   if In_Instance_Body then
-                     Error_Msg_Warn := not GNATprove_Mode;
+                     Error_Msg_Warn := SPARK_Mode /= On;
                      Conversion_Error_N
                        ("source array type has deeper accessibility "
                         & "level than target<<", Operand);
@@ -11186,7 +11186,7 @@ package body Sem_Res is
                --  will be generated by Expand_N_Type_Conversion.
 
                if In_Instance_Body then
-                  Error_Msg_Warn := not GNATprove_Mode;
+                  Error_Msg_Warn := SPARK_Mode /= On;
                   Conversion_Error_N
                     ("cannot convert local pointer to non-local access type<<",
                      Operand);
@@ -11219,7 +11219,7 @@ package body Sem_Res is
                   --  will be generated by Expand_N_Type_Conversion.
 
                   if In_Instance_Body then
-                     Error_Msg_Warn := not GNATprove_Mode;
+                     Error_Msg_Warn := SPARK_Mode /= On;
                      Conversion_Error_N
                        ("cannot convert access discriminant to non-local "
                         & "access type<<", Operand);
@@ -11366,7 +11366,7 @@ package body Sem_Res is
                --  will be generated by Expand_N_Type_Conversion.
 
                if In_Instance_Body then
-                  Error_Msg_Warn := not GNATprove_Mode;
+                  Error_Msg_Warn := SPARK_Mode /= On;
                   Conversion_Error_N
                     ("cannot convert local pointer to non-local access type<<",
                      Operand);
@@ -11406,7 +11406,7 @@ package body Sem_Res is
                   --  will be generated by Expand_N_Type_Conversion.
 
                   if In_Instance_Body then
-                     Error_Msg_Warn := not GNATprove_Mode;
+                     Error_Msg_Warn := SPARK_Mode /= On;
                      Conversion_Error_N
                        ("cannot convert access discriminant to non-local "
                         & "access type<<", Operand);
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index cce45be570a..15c6a251e5f 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -578,7 +578,7 @@ package body Sem_Util is
    begin
       if Has_Predicates (Typ) then
          if Is_Generic_Actual_Type (Typ) then
-            Error_Msg_Warn := not GNATprove_Mode;
+            Error_Msg_Warn := SPARK_Mode /= On;
             Error_Msg_FE (Msg & "<<", N, Typ);
             Error_Msg_F ("\Program_Error [<<", N);
             Insert_Action (N,
@@ -3268,11 +3268,10 @@ package body Sem_Util is
       Eloc : Source_Ptr;
 
    begin
-      --  If this is a warning, convert it into an error if we are operating
-      --  in GNATprove mode, because in SPARK, we are allowed to consider
-      --  such warnings as illegalities, and we choose to do so!
+      --  If this is a warning, convert it into an error if we are in code
+      --  subject to SPARK_Mode being set ON.
 
-      Error_Msg_Warn := not GNATprove_Mode;
+      Error_Msg_Warn := SPARK_Mode /= On;
 
       --  A static constraint error in an instance body is not a fatal error.
       --  we choose to inhibit the message altogether, because there is no
@@ -3414,7 +3413,7 @@ package body Sem_Util is
          end loop;
 
          if Msgs then
-            Error_Msg_Warn := not GNATprove_Mode;
+            Error_Msg_Warn := SPARK_Mode /= On;
 
             if Present (Ent) then
                Error_Msg_NEL (Msgc (1 .. Msgl), N, Ent, Eloc);
diff --git a/gcc/ada/types.ads b/gcc/ada/types.ads
index 4888d69e190..6ab03820fd5 100644
--- a/gcc/ada/types.ads
+++ b/gcc/ada/types.ads
@@ -882,12 +882,4 @@ 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;