sem_aggr.adb, [...]: cleanup of SPARK mode

2011-08-02  Yannick Moy  <moy@adacore.com>

	* sem_aggr.adb, err_vars.ads, sem_ch3.adb, sem_ch5.adb, sem_ch9.adb,
	debug.adb, sem_util.adb, sem_res.adb, sem_attr.adb, gnat1drv.adb,
	errout.adb, errout.ads, exp_ch6.adb, sem_ch4.adb, restrict.adb,
	restrict.ads, sem_ch6.adb, sem_ch8.adb, sem_ch11.adb,
	opt.ads: cleanup of SPARK mode

From-SVN: r177175

21 files changed, 218 insertions, 282 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index d9c354f..7330a20 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,13 @@
 2011-08-02  Yannick Moy  <moy@adacore.com>
 
+	* sem_aggr.adb, err_vars.ads, sem_ch3.adb, sem_ch5.adb, sem_ch9.adb,
+	debug.adb, sem_util.adb, sem_res.adb, sem_attr.adb, gnat1drv.adb,
+	errout.adb, errout.ads, exp_ch6.adb, sem_ch4.adb, restrict.adb,
+	restrict.ads, sem_ch6.adb, sem_ch8.adb, sem_ch11.adb,
+	opt.ads: cleanup of SPARK mode
+
+2011-08-02  Yannick Moy  <moy@adacore.com>
+
 	* cstand.adb (Create_Standard): sets Is_In_ALFA component of standard
 	types.
 	* einfo.adb, einfo.ads (Is_In_ALFA): add flag for all entities
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index 27ce9b0..8f38609 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -121,7 +121,7 @@ package body Debug is
    --  d.A  Read/write Aspect_Specifications hash table to tree
    --  d.B
    --  d.C  Generate concatenation call, do not generate inline code
-   --  d.D  Accept only the SPARK subset of Ada
+   --  d.D
    --  d.E  SPARK generation mode
    --  d.F  Why generation mode
    --  d.G
@@ -574,13 +574,6 @@ package body Debug is
    --  d.C  Generate call to System.Concat_n.Str_Concat_n routines in cases
    --       where we would normally generate inline concatenation code.
 
-   --  d.D  Issue compiler errors on Ada input outside the SPARK subset of
-   --       Ada. This only deals currently with the Ada code, not SPARK
-   --       annotations, so it may well be the case that code which passes
-   --       the compiler with this flag is rejected by the SPARK Examiner,
-   --       e.g. due to the different visibility rules of the Examiner based
-   --       on 'inherit' SPARK annotations.
-
    --  d.E  SPARK generation mode. Generate intermediate code for the sake of
    --       formal verification through SPARK and the SPARK toolset.
 
diff --git a/gcc/ada/err_vars.ads b/gcc/ada/err_vars.ads
index 2f1b048..10a0262 100644
--- a/gcc/ada/err_vars.ads
+++ b/gcc/ada/err_vars.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -150,9 +150,4 @@ package Err_Vars is
    --  Used if current message contains a ~ insertion character to indicate
    --  insertion of the string Error_Msg_String (1 .. Error_Msg_Strlen).
 
-   Error_Msg_Lang : String (1 .. 16);
-   Error_Msg_Langlen : Natural;
-   --  Used if current message contains a ~~ insertion character to indicate
-   --  insertion of the string Error_Msg_Lang (1 .. Error_Msg_Langlen).
-
 end Err_Vars;
diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index 169540e..e794057 100644
--- a/gcc/ada/errout.adb
+++ b/gcc/ada/errout.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -2185,19 +2185,6 @@ package body Errout is
       Set_Casing (Desired_Case);
    end Set_Identifier_Casing;
 
-   ------------------------
-   -- Set_Error_Msg_Lang --
-   ------------------------
-
-   procedure Set_Error_Msg_Lang (To : String) is
-   begin
-      Error_Msg_Lang (1) := '(';
-      Error_Msg_Lang (2 .. To'Length + 1) := To;
-      Error_Msg_Lang (To'Length + 2) := ')';
-      Error_Msg_Lang (To'Length + 3) := ' ';
-      Error_Msg_Langlen := To'Length + 3;
-   end Set_Error_Msg_Lang;
-
    -----------------------
    -- Set_Ignore_Errors --
    -----------------------
@@ -2716,12 +2703,7 @@ package body Errout is
                P := P + 1;
 
             when '~' =>
-               if P <= Text'Last and then Text (P) = '~' then
-                  P := P + 1;
-                  Set_Msg_Str (Error_Msg_Lang (1 .. Error_Msg_Langlen));
-               else
-                  Set_Msg_Str (Error_Msg_String (1 .. Error_Msg_Strlen));
-               end if;
+               Set_Msg_Str (Error_Msg_String (1 .. Error_Msg_Strlen));
 
             --  Upper case letter
 
diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads
index fc2cf49..2e850f8 100644
--- a/gcc/ada/errout.ads
+++ b/gcc/ada/errout.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -346,16 +346,6 @@ package Errout is
    --      inserted to replace the ~ character. The string is inserted in the
    --      literal form it appears, without any action on special characters.
 
-   --    Insertion character ~~ (Two tildes: insert language string)
-   --      Indicates that Error_Msg_Lang (1 .. Error_Msg_Langlen) is to be
-   --      inserted to replace the ~~ character. Typically the language string
-   --      will be inserted in parentheses as a prefix of the error message, as
-   --      in "(spark) error msg". The string is inserted in the literal form
-   --      it appears, without any action on special characters. Error_Msg_Lang
-   --      and Error_Msg_Langlen are expected to be set only once before
-   --      parsing starts, so that the caller to an error procedure does not
-   --      need to set them repeatedly.
-
    ----------------------------------------
    -- Specialization of Messages for VMS --
    ----------------------------------------
@@ -469,11 +459,6 @@ package Errout is
    --  Used if current message contains a ~ insertion character to indicate
    --  insertion of the string Error_Msg_String (1 .. Error_Msg_Strlen).
 
-   Error_Msg_Lang : String  renames Err_Vars.Error_Msg_Lang;
-   Error_Msg_Langlen : Natural renames Err_Vars.Error_Msg_Langlen;
-   --  Used if current message contains a ~~ insertion character to indicate
-   --  insertion of the string Error_Msg_Lang (1 .. Error_Msg_Langlen).
-
    -----------------------------------------------------
    -- Format of Messages and Manual Quotation Control --
    -----------------------------------------------------
@@ -765,11 +750,6 @@ package Errout is
    --  Remove warnings on all elements of a list (Calls Remove_Warning_Messages
    --  on each element of the list, see above).
 
-   procedure Set_Error_Msg_Lang (To : String);
-   --  Set Error_Msg_Lang/Error_Msg_Langlen used for insertion character ~~.
-   --  The argument is just the language name, e.g. "spark". The stored string
-   --  is of the form "(langname) ".
-
    procedure Set_Ignore_Errors (To : Boolean);
    --  Following a call to this procedure with To=True, all error calls are
    --  ignored. A call with To=False restores the default treatment in which
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index 8a842fb..bf7b44e 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -5449,26 +5449,26 @@ package body Exp_Ch6 is
       Prot_Id   : Entity_Id;
 
    begin
-      --  In SPARK or ALFA, subprogram declarations are only allowed in
-      --  package specifications.
+      --  In SPARK, subprogram declarations are only allowed in package
+      --  specifications.
 
       if Nkind (Parent (N)) /= N_Package_Specification then
          if Nkind (Parent (N)) = N_Compilation_Unit then
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("subprogram declaration is not a library item", N);
 
          elsif Present (Next (N))
            and then Nkind (Next (N)) = N_Pragma
            and then Get_Pragma_Id (Pragma_Name (Next (N))) = Pragma_Import
          then
-            --  In SPARK or ALFA, subprogram declarations are also permitted in
+            --  In SPARK, subprogram declarations are also permitted in
             --  declarative parts when immediately followed by a corresponding
             --  pragma Import. We only check here that there is some pragma
             --  Import.
 
             null;
          else
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("subprogram declaration is not allowed here", N);
          end if;
       end if;
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 06ab52c..4336277 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -392,10 +392,6 @@ procedure Gnat1drv is
 
       --  Set switches for formal verification modes
 
-      if Debug_Flag_Dot_DD then
-         SPARK_Mode := True;
-      end if;
-
       if Debug_Flag_Dot_EE then
          ALFA_Through_SPARK_Mode := True;
       end if;
@@ -405,14 +401,6 @@ procedure Gnat1drv is
       end if;
 
       ALFA_Mode := ALFA_Through_SPARK_Mode or ALFA_Through_Why_Mode;
-
-      if ALFA_Mode then
-         Set_Error_Msg_Lang ("alfa");
-         Formal_Verification_Mode := True;
-      elsif SPARK_Mode then
-         Set_Error_Msg_Lang ("spark");
-         Formal_Verification_Mode := True;
-      end if;
    end Adjust_Global_Switches;
 
    --------------------
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 732fc4d..e611c04 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -1870,9 +1870,6 @@ package Opt is
 
    --  These modes are currently defined through debug flags
 
-   Formal_Verification_Mode : Boolean := False;
-   --  Set True if ALFA_Mode or SPARK_Mode
-
    ALFA_Mode : Boolean := False;
    --  Set True if ALFA_Through_SPARK_Mode or else ALFA_Through_Why_Mode
 
diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb
index 883128a..c68475b 100644
--- a/gcc/ada/restrict.adb
+++ b/gcc/ada/restrict.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -109,7 +109,7 @@ package body Restrict is
    -- Check_Formal_Restriction --
    ------------------------------
 
-   procedure Check_Formal_Restriction
+   procedure Check_SPARK_Restriction
      (Msg   : String;
       N     : Node_Id;
       Force : Boolean := False)
@@ -129,11 +129,9 @@ package body Restrict is
 
          if Msg_Issued then
             Error_Msg_F ("\\| " & Msg, N);
-         elsif SPARK_Mode then
-            Error_Msg_F ("|~~" & Msg, N);
          end if;
       end if;
-   end Check_Formal_Restriction;
+   end Check_SPARK_Restriction;
 
    procedure Check_Formal_Restriction (Msg1, Msg2 : String; N : Node_Id) is
       Msg_Issued          : Boolean;
@@ -154,9 +152,6 @@ package body Restrict is
          if Msg_Issued then
             Error_Msg_F ("\\| " & Msg1, N);
             Error_Msg_F (Msg2, N);
-         elsif SPARK_Mode then
-            Error_Msg_F ("|~~" & Msg1, N);
-            Error_Msg_F (Msg2, N);
          end if;
       end if;
    end Check_Formal_Restriction;
@@ -380,7 +375,7 @@ package body Restrict is
       --  No_Dispatch restriction is not set.
 
       if R = No_Dispatch then
-         Check_Formal_Restriction ("class-wide is not allowed", N);
+         Check_SPARK_Restriction ("class-wide is not allowed", N);
       end if;
 
       if UI_Is_In_Int_Range (V) then
diff --git a/gcc/ada/restrict.ads b/gcc/ada/restrict.ads
index f0dcb31..46626c9 100644
--- a/gcc/ada/restrict.ads
+++ b/gcc/ada/restrict.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -228,7 +228,7 @@ package Restrict is
    --  an elaboration routine. If elaboration code is not allowed, an error
    --  message is posted on the node given as argument.
 
-   procedure Check_Formal_Restriction
+   procedure Check_SPARK_Restriction
      (Msg   : String;
       N     : Node_Id;
       Force : Boolean := False);
diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb
index 89db3d0..e704586 100644
--- a/gcc/ada/sem_aggr.adb
+++ b/gcc/ada/sem_aggr.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -809,7 +809,7 @@ package body Sem_Aggr is
    begin
       if Level = 0 then
          if Nkind (Parent (Expr)) /= N_Qualified_Expression then
-            Check_Formal_Restriction ("aggregate should be qualified", Expr);
+            Check_SPARK_Restriction ("aggregate should be qualified", Expr);
          end if;
 
       else
@@ -978,7 +978,7 @@ package body Sem_Aggr is
          return;
       end if;
 
-      --  An unqualified aggregate is restricted in SPARK or ALFA to:
+      --  An unqualified aggregate is restricted in SPARK to:
 
       --    An aggregate item inside an aggregate for a multi-dimensional array
 
@@ -997,12 +997,12 @@ package body Sem_Aggr is
            and then not Is_Constrained (Etype (Name (Parent (N))))
          then
             if not Is_Others_Aggregate (N) then
-               Check_Formal_Restriction
+               Check_SPARK_Restriction
                  ("array aggregate should have only OTHERS", N);
             end if;
 
          elsif Is_Top_Level_Aggregate (N) then
-            Check_Formal_Restriction ("aggregate should be qualified", N);
+            Check_SPARK_Restriction ("aggregate should be qualified", N);
 
          --  The legality of this unqualified aggregate is checked by calling
          --  Check_Qualified_Aggregate from one of its enclosing aggregate,
@@ -1873,13 +1873,13 @@ package body Sem_Aggr is
 
                      Set_Do_Range_Check (Choice, False);
 
-                     --  In SPARK or ALFA, the choice must be static
+                     --  In SPARK, the choice must be static
 
                      if not (Is_Static_Expression (Choice)
                               or else (Nkind (Choice) = N_Range
                                         and then Is_Static_Range (Choice)))
                      then
-                        Check_Formal_Restriction
+                        Check_SPARK_Restriction
                           ("choice should be static", Choice);
                      end if;
                   end if;
@@ -2523,12 +2523,12 @@ package body Sem_Aggr is
       Analyze (A);
       Check_Parameterless_Call (A);
 
-      --  In SPARK or ALFA, the ancestor part cannot be a type mark
+      --  In SPARK, the ancestor part cannot be a type mark
 
       if Is_Entity_Name (A)
         and then Is_Type (Entity (A))
       then
-         Check_Formal_Restriction ("ancestor part cannot be a type mark", A);
+         Check_SPARK_Restriction ("ancestor part cannot be a type mark", A);
       end if;
 
       if not Is_Tagged_Type (Typ) then
@@ -3212,7 +3212,7 @@ package body Sem_Aggr is
    --  Start of processing for Resolve_Record_Aggregate
 
    begin
-      --  A record aggregate is restricted in SPARK or ALFA:
+      --  A record aggregate is restricted in SPARK:
       --    Each named association can have only a single choice.
       --    OTHERS cannot be used.
       --    Positional and named associations cannot be mixed.
@@ -3222,7 +3222,7 @@ package body Sem_Aggr is
       then
 
          if Present (Expressions (N)) then
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("named association cannot follow positional one",
                First (Choices (First (Component_Associations (N)))));
          end if;
@@ -3234,13 +3234,13 @@ package body Sem_Aggr is
             Assoc := First (Component_Associations (N));
             while Present (Assoc) loop
                if List_Length (Choices (Assoc)) > 1 then
-                  Check_Formal_Restriction
+                  Check_SPARK_Restriction
                     ("component association in record aggregate must "
                      & "contain a single choice", Assoc);
                end if;
 
                if Nkind (First (Choices (Assoc))) = N_Others_Choice then
-                  Check_Formal_Restriction
+                  Check_SPARK_Restriction
                     ("record aggregate cannot contain OTHERS", Assoc);
                end if;
 
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 4ff4ff4..01a9bef 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -1296,7 +1296,7 @@ package body Sem_Attr is
       procedure Check_Formal_Restriction_On_Attribute is
       begin
          Error_Msg_Name_1 := Aname;
-         Check_Formal_Restriction ("attribute % is not allowed", P);
+         Check_SPARK_Restriction ("attribute % is not allowed", P);
       end Check_Formal_Restriction_On_Attribute;
 
       ------------------------
@@ -2068,8 +2068,8 @@ package body Sem_Attr is
          end if;
       end if;
 
-      --  In SPARK or ALFA, attributes of private types are only allowed if
-      --  the full type declaration is visible.
+      --  In SPARK, attributes of private types are only allowed if the full
+      --  type declaration is visible.
 
       if Is_Entity_Name (P)
         and then Present (Entity (P))  --  needed in some cases
@@ -2079,7 +2079,7 @@ package body Sem_Attr is
         and then not In_Spec_Expression
       then
          Error_Msg_Node_1 := First_Subtype (P_Type);
-         Check_Formal_Restriction ("invisible attribute of}", N);
+         Check_SPARK_Restriction ("invisible attribute of}", N);
       end if;
 
       --  Remaining processing depends on attribute
@@ -2460,7 +2460,7 @@ package body Sem_Attr is
 
          if Nkind (Parent (N)) /= N_Attribute_Reference then
             Error_Msg_Name_1 := Aname;
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("attribute% is only allowed as prefix of another attribute", P);
          end if;
 
@@ -3877,7 +3877,7 @@ package body Sem_Attr is
          if Is_Boolean_Type (P_Type) then
             Error_Msg_Name_1 := Aname;
             Error_Msg_Name_2 := Chars (P_Type);
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("attribute% is not allowed for type%", P);
          end if;
 
@@ -3903,7 +3903,7 @@ package body Sem_Attr is
          if Is_Real_Type (P_Type) or else Is_Boolean_Type (P_Type) then
             Error_Msg_Name_1 := Aname;
             Error_Msg_Name_2 := Chars (P_Type);
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("attribute% is not allowed for type%", P);
          end if;
 
@@ -4461,7 +4461,7 @@ package body Sem_Attr is
          if Is_Real_Type (P_Type) or else Is_Boolean_Type (P_Type) then
             Error_Msg_Name_1 := Aname;
             Error_Msg_Name_2 := Chars (P_Type);
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("attribute% is not allowed for type%", P);
          end if;
 
@@ -4786,7 +4786,7 @@ package body Sem_Attr is
          if Is_Boolean_Type (P_Type) then
             Error_Msg_Name_1 := Aname;
             Error_Msg_Name_2 := Chars (P_Type);
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("attribute% is not allowed for type%", P);
          end if;
 
diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb
index 26ac6d0..357b3f1 100644
--- a/gcc/ada/sem_ch11.adb
+++ b/gcc/ada/sem_ch11.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -443,7 +443,7 @@ package body Sem_Ch11 is
       P              : Node_Id;
 
    begin
-      Check_Formal_Restriction ("raise statement is not allowed", N);
+      Check_SPARK_Restriction ("raise statement is not allowed", N);
       Check_Unreachable_Code (N);
 
       --  Check exception restrictions on the original source
@@ -610,7 +610,7 @@ package body Sem_Ch11 is
    --  Start of processing for Analyze_Raise_xxx_Error
 
    begin
-      Check_Formal_Restriction ("raise statement is not allowed", N);
+      Check_SPARK_Restriction ("raise statement is not allowed", N);
 
       if No (Etype (N)) then
          Set_Etype (N, Standard_Void_Type);
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index afa0f85..55d4c3b 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -714,7 +714,7 @@ package body Sem_Ch3 is
       Enclosing_Prot_Type : Entity_Id := Empty;
 
    begin
-      Check_Formal_Restriction ("access type is not allowed", N);
+      Check_SPARK_Restriction ("access type is not allowed", N);
 
       if Is_Entry (Current_Scope)
         and then Is_Task_Type (Etype (Scope (Current_Scope)))
@@ -1028,7 +1028,7 @@ package body Sem_Ch3 is
    --  Start of processing for Access_Subprogram_Declaration
 
    begin
-      Check_Formal_Restriction ("access type is not allowed", T_Def);
+      Check_SPARK_Restriction ("access type is not allowed", T_Def);
 
       --  Associate the Itype node with the inner full-type declaration or
       --  subprogram spec or entry body. This is required to handle nested
@@ -1282,7 +1282,7 @@ package body Sem_Ch3 is
       S : constant Node_Id := Subtype_Indication (Def);
       P : constant Node_Id := Parent (Def);
    begin
-      Check_Formal_Restriction ("access type is not allowed", Def);
+      Check_SPARK_Restriction ("access type is not allowed", Def);
 
       --  Check for permissible use of incomplete type
 
@@ -1786,7 +1786,7 @@ package body Sem_Ch3 is
                 (Subtype_Indication (Component_Definition (N)), N);
 
          if not Nkind_In (Typ, N_Identifier, N_Expanded_Name) then
-            Check_Formal_Restriction ("subtype mark required", Typ);
+            Check_SPARK_Restriction ("subtype mark required", Typ);
          end if;
 
       --  Ada 2005 (AI-230): Access Definition case
@@ -1839,7 +1839,7 @@ package body Sem_Ch3 is
       --  package Sem).
 
       if Present (E) then
-         Check_Formal_Restriction ("default expression is not allowed", E);
+         Check_SPARK_Restriction ("default expression is not allowed", E);
          Preanalyze_Spec_Expression (E, T);
          Check_Initialization (T, E);
 
@@ -2046,12 +2046,12 @@ package body Sem_Ch3 is
       while Present (D) loop
 
          --  Package specification cannot contain a package declaration in
-         --  SPARK or ALFA.
+         --  SPARK.
 
          if Nkind (D) = N_Package_Declaration
            and then Nkind (Parent (L)) = N_Package_Specification
          then
-            Check_Formal_Restriction ("package specification cannot contain "
+            Check_SPARK_Restriction ("package specification cannot contain "
                                       & "a package declaration", D);
          end if;
 
@@ -2273,11 +2273,11 @@ package body Sem_Ch3 is
             null;
 
          --  For record types, discriminants are allowed, unless we are in
-         --  SPARK or ALFA.
+         --  SPARK.
 
          when N_Record_Definition =>
             if Present (Discriminant_Specifications (N)) then
-               Check_Formal_Restriction
+               Check_SPARK_Restriction
                  ("discriminant type is not allowed",
                   Defining_Identifier
                     (First (Discriminant_Specifications (N))));
@@ -2383,10 +2383,10 @@ package body Sem_Ch3 is
          return;
       end if;
 
-      --  Controlled type is not allowed in SPARK and ALFA
+      --  Controlled type is not allowed in SPARK
 
       if Is_Visibly_Controlled (T) then
-         Check_Formal_Restriction ("controlled type is not allowed", N);
+         Check_SPARK_Restriction ("controlled type is not allowed", N);
       end if;
 
       --  Some common processing for all types
@@ -2495,7 +2495,7 @@ package body Sem_Ch3 is
       T : Entity_Id;
 
    begin
-      Check_Formal_Restriction ("incomplete type is not allowed", N);
+      Check_SPARK_Restriction ("incomplete type is not allowed", N);
 
       Generate_Definition (Defining_Identifier (N));
 
@@ -3040,29 +3040,29 @@ package body Sem_Ch3 is
       --  is considered, so that the Object_Definition node is still the same
       --  as in source code.
 
-      --  In SPARK or ALFA, the nominal subtype shall be given by a subtype
-      --  mark and shall not be unconstrained. (The only exception to this
-      --  is the admission of declarations of constants of type String.)
+      --  In SPARK, the nominal subtype shall be given by a subtype mark and
+      --  shall not be unconstrained. (The only exception to this is the
+      --  admission of declarations of constants of type String.)
 
       if not
         Nkind_In (Object_Definition (N), N_Identifier, N_Expanded_Name)
       then
-         Check_Formal_Restriction
+         Check_SPARK_Restriction
            ("subtype mark required", Object_Definition (N));
 
       elsif Is_Array_Type (T)
         and then not Is_Constrained (T)
         and then T /= Standard_String
       then
-         Check_Formal_Restriction
+         Check_SPARK_Restriction
            ("subtype mark of constrained type expected",
             Object_Definition (N));
       end if;
 
-      --  There are no aliased objects in SPARK or ALFA
+      --  There are no aliased objects in SPARK
 
       if Aliased_Present (N) then
-         Check_Formal_Restriction ("aliased object is not allowed", N);
+         Check_SPARK_Restriction ("aliased object is not allowed", N);
       end if;
 
       --  Process initialization expression if present and not in error
@@ -3186,11 +3186,10 @@ package body Sem_Ch3 is
 
            --  Only call test if needed
 
-           and then (Formal_Verification_Mode
-                      or else Restriction_Check_Required (SPARK))
+           and then Restriction_Check_Required (SPARK)
            and then not Is_SPARK_Initialization_Expr (E)
          then
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("initialization expression is not appropriate", E);
          end if;
       end if;
@@ -4029,12 +4028,12 @@ package body Sem_Ch3 is
          Set_Has_Delayed_Freeze (Id);
       end if;
 
-      --  Subtype of Boolean cannot have a constraint in SPARK or ALFA
+      --  Subtype of Boolean cannot have a constraint in SPARK
 
       if Is_Boolean_Type (T)
         and then Nkind (Subtype_Indication (N)) = N_Subtype_Indication
       then
-         Check_Formal_Restriction
+         Check_SPARK_Restriction
            ("subtype of Boolean cannot have constraint", N);
       end if;
 
@@ -4050,13 +4049,13 @@ package body Sem_Ch3 is
                One_Cstr := First (Constraints (Cstr));
                while Present (One_Cstr) loop
 
-                  --  Index or discriminant constraint in SPARK or ALFA must be
-                  --  a subtype mark.
+                  --  Index or discriminant constraint in SPARK must be a
+                  --  subtype mark.
 
                   if not
                     Nkind_In (One_Cstr, N_Identifier, N_Expanded_Name)
                   then
-                     Check_Formal_Restriction
+                     Check_SPARK_Restriction
                        ("subtype mark required", One_Cstr);
 
                   --  String subtype must have a lower bound of 1 in SPARK.
@@ -4070,7 +4069,7 @@ package body Sem_Ch3 is
                      if Is_OK_Static_Expression (Low)
                        and then Expr_Value (Low) /= 1
                      then
-                        Check_Formal_Restriction
+                        Check_SPARK_Restriction
                           ("String subtype must have lower bound of 1", N);
                      end if;
                   end if;
@@ -4089,12 +4088,12 @@ package body Sem_Ch3 is
          Set_Etype (Id, Base_Type (T));
 
          --  Subtype of unconstrained array without constraint is not allowed
-         --  in SPARK or ALFA.
+         --  in SPARK.
 
          if Is_Array_Type (T)
            and then not Is_Constrained (T)
          then
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("subtype of unconstrained array must have constraint", N);
          end if;
 
@@ -4617,7 +4616,7 @@ package body Sem_Ch3 is
          Analyze (Index);
 
          if not Nkind_In (Index, N_Identifier, N_Expanded_Name) then
-            Check_Formal_Restriction ("subtype mark required", Index);
+            Check_SPARK_Restriction ("subtype mark required", Index);
          end if;
 
          --  Add a subtype declaration for each index of private array type
@@ -4692,7 +4691,7 @@ package body Sem_Ch3 is
          Element_Type := Process_Subtype (Component_Typ, P, Related_Id, 'C');
 
          if not Nkind_In (Component_Typ, N_Identifier, N_Expanded_Name) then
-            Check_Formal_Restriction ("subtype mark required", Component_Typ);
+            Check_SPARK_Restriction ("subtype mark required", Component_Typ);
          end if;
 
       --  Ada 2005 (AI-230): Access Definition case
@@ -4801,7 +4800,7 @@ package body Sem_Ch3 is
       Set_Packed_Array_Type (T, Empty);
 
       if Aliased_Present (Component_Definition (Def)) then
-         Check_Formal_Restriction
+         Check_SPARK_Restriction
            ("aliased is not allowed", Component_Definition (Def));
          Set_Has_Aliased_Components (Etype (T));
       end if;
@@ -11312,7 +11311,7 @@ package body Sem_Ch3 is
       else
          pragma Assert (Nkind (C) = N_Digits_Constraint);
 
-         Check_Formal_Restriction ("digits constraint is not allowed", S);
+         Check_SPARK_Restriction ("digits constraint is not allowed", S);
 
          Digits_Expr := Digits_Expression (C);
          Analyze_And_Resolve (Digits_Expr, Any_Integer);
@@ -11551,7 +11550,7 @@ package body Sem_Ch3 is
 
       if Nkind (C) = N_Digits_Constraint then
 
-         Check_Formal_Restriction ("digits constraint is not allowed", S);
+         Check_SPARK_Restriction ("digits constraint is not allowed", S);
          Check_Restriction (No_Obsolescent_Features, C);
 
          if Warn_On_Obsolescent_Feature then
@@ -11783,7 +11782,7 @@ package body Sem_Ch3 is
 
       if Nkind (C) = N_Delta_Constraint then
 
-         Check_Formal_Restriction ("delta constraint is not allowed", S);
+         Check_SPARK_Restriction ("delta constraint is not allowed", S);
          Check_Restriction (No_Obsolescent_Features, C);
 
          if Warn_On_Obsolescent_Feature then
@@ -12440,7 +12439,7 @@ package body Sem_Ch3 is
       Bound_Val     : Ureal;
 
    begin
-      Check_Formal_Restriction
+      Check_SPARK_Restriction
         ("decimal fixed point type is not allowed", Def);
       Check_Restriction (No_Fixed_Point, Def);
 
@@ -13946,7 +13945,7 @@ package body Sem_Ch3 is
       --  parent is also an interface.
 
       if Interface_Present (Def) then
-         Check_Formal_Restriction ("interface is not allowed", Def);
+         Check_SPARK_Restriction ("interface is not allowed", Def);
 
          if not Is_Interface (Parent_Type) then
             Diagnose_Interface (Indic, Parent_Type);
@@ -14188,8 +14187,7 @@ package body Sem_Ch3 is
       end if;
 
       --  Only composite types other than array types are allowed to have
-      --  discriminants. In SPARK and in ALFA, no types are allowed to have
-      --  discriminants.
+      --  discriminants. In SPARK, no types are allowed to have discriminants.
 
       if Present (Discriminant_Specifications (N)) then
          if (Is_Elementary_Type (Parent_Type)
@@ -14201,7 +14199,7 @@ package body Sem_Ch3 is
                Defining_Identifier (First (Discriminant_Specifications (N))));
             Set_Has_Discriminants (T, False);
          else
-            Check_Formal_Restriction ("discriminant type is not allowed", N);
+            Check_SPARK_Restriction ("discriminant type is not allowed", N);
          end if;
       end if;
 
@@ -14388,11 +14386,11 @@ package body Sem_Ch3 is
          end if;
       end if;
 
-      --  In SPARK or ALFA, there are no derived type definitions other than
-      --  type extensions of tagged record types.
+      --  In SPARK, there are no derived type definitions other than type
+      --  extensions of tagged record types.
 
       if No (Extension) then
-         Check_Formal_Restriction ("derived type is not allowed", N);
+         Check_SPARK_Restriction ("derived type is not allowed", N);
       end if;
    end Derived_Type_Declaration;
 
@@ -16543,7 +16541,7 @@ package body Sem_Ch3 is
          --  Non-binary case
 
          elsif M_Val < 2 ** Bits then
-            Check_Formal_Restriction ("modulus should be a power of 2", T);
+            Check_SPARK_Restriction ("modulus should be a power of 2", T);
             Set_Non_Binary_Modulus (T);
 
             if Bits > System_Max_Nonbinary_Modulus_Power then
@@ -17402,7 +17400,7 @@ package body Sem_Ch3 is
 
             if Priv_Parent /= Full_Parent then
                Error_Msg_Name_1 := Chars (Priv_Parent);
-               Check_Formal_Restriction ("% expected", Full_Indic);
+               Check_SPARK_Restriction ("% expected", Full_Indic);
             end if;
 
             --  Check the rules of 7.3(10): if the private extension inherits
@@ -17967,7 +17965,7 @@ package body Sem_Ch3 is
          if not In_Iter_Schm
            and then not Is_Static_Range (R)
          then
-            Check_Formal_Restriction ("range should be static", R);
+            Check_SPARK_Restriction ("range should be static", R);
          end if;
 
          Lo := Low_Bound (R);
@@ -18986,11 +18984,11 @@ package body Sem_Ch3 is
         or else not Interface_Present (Def)
       then
          if Limited_Present (Def) then
-            Check_Formal_Restriction ("limited is not allowed", N);
+            Check_SPARK_Restriction ("limited is not allowed", N);
          end if;
 
          if Abstract_Present (Def) then
-            Check_Formal_Restriction ("abstract is not allowed", N);
+            Check_SPARK_Restriction ("abstract is not allowed", N);
          end if;
 
          --  The flag Is_Tagged_Type might have already been set by
@@ -19012,7 +19010,7 @@ package body Sem_Ch3 is
                                       or else Abstract_Present (Def));
 
       else
-         Check_Formal_Restriction ("interface is not allowed", N);
+         Check_SPARK_Restriction ("interface is not allowed", N);
 
          Is_Tagged := True;
          Analyze_Interface_Declaration (T, Def);
@@ -19152,8 +19150,8 @@ package body Sem_Ch3 is
          T := Prev_T;
       end if;
 
-      --  In SPARK or ALFA, tagged types and type extensions may only be
-      --  declared in the specification of library unit packages.
+      --  In SPARK, tagged types and type extensions may only be declared in
+      --  the specification of library unit packages.
 
       if Present (Def) and then Is_Tagged_Type (T) then
          declare
@@ -19174,13 +19172,13 @@ package body Sem_Ch3 is
             if Nkind (Ctxt) = N_Package_Body
               and then Nkind (Parent (Ctxt)) = N_Compilation_Unit
             then
-               Check_Formal_Restriction
+               Check_SPARK_Restriction
                  ("type should be defined in package specification", Typ);
 
             elsif Nkind (Ctxt) /= N_Package_Specification
               or else Nkind (Parent (Parent (Ctxt))) /= N_Compilation_Unit
             then
-               Check_Formal_Restriction
+               Check_SPARK_Restriction
                  ("type should be defined in library unit package", Typ);
             end if;
          end;
@@ -19209,14 +19207,14 @@ package body Sem_Ch3 is
         or else Null_Present (Component_List (Def))
       then
          if not Is_Tagged_Type (T) then
-            Check_Formal_Restriction ("non-tagged record cannot be null", Def);
+            Check_SPARK_Restriction ("non-tagged record cannot be null", Def);
          end if;
 
       else
          Analyze_Declarations (Component_Items (Component_List (Def)));
 
          if Present (Variant_Part (Component_List (Def))) then
-            Check_Formal_Restriction ("variant part is not allowed", Def);
+            Check_SPARK_Restriction ("variant part is not allowed", Def);
             Analyze (Variant_Part (Component_List (Def)));
          end if;
       end if;
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index 5a5169b..ae169c2 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -369,7 +369,7 @@ package body Sem_Ch4 is
       C        : Node_Id;
 
    begin
-      Check_Formal_Restriction ("allocator is not allowed", N);
+      Check_SPARK_Restriction ("allocator is not allowed", N);
 
       --  Deal with allocator restrictions
 
@@ -818,7 +818,7 @@ package body Sem_Ch4 is
             case Nkind (Actual) is
                when N_Parameter_Association =>
                   if Named_Seen then
-                     Check_Formal_Restriction
+                     Check_SPARK_Restriction
                        ("named association cannot follow positional one",
                         Actual);
                      exit;
@@ -1506,7 +1506,7 @@ package body Sem_Ch4 is
          return;
       end if;
 
-      Check_Formal_Restriction ("conditional expression is not allowed", N);
+      Check_SPARK_Restriction ("conditional expression is not allowed", N);
 
       Else_Expr := Next (Then_Expr);
 
@@ -1706,7 +1706,7 @@ package body Sem_Ch4 is
    --  Start of processing for Analyze_Explicit_Dereference
 
    begin
-      Check_Formal_Restriction ("explicit dereference is not allowed", N);
+      Check_SPARK_Restriction ("explicit dereference is not allowed", N);
 
       Analyze (P);
       Set_Etype (N, Any_Type);
@@ -2588,7 +2588,7 @@ package body Sem_Ch4 is
 
    procedure Analyze_Null (N : Node_Id) is
    begin
-      Check_Formal_Restriction ("null is not allowed", N);
+      Check_SPARK_Restriction ("null is not allowed", N);
 
       Set_Etype (N, Any_Access);
    end Analyze_Null;
@@ -3274,7 +3274,7 @@ package body Sem_Ch4 is
       Iterator : Node_Id;
 
    begin
-      Check_Formal_Restriction ("quantified expression is not allowed", N);
+      Check_SPARK_Restriction ("quantified expression is not allowed", N);
 
       Set_Etype  (Ent,  Standard_Void_Type);
       Set_Parent (Ent, N);
@@ -4302,7 +4302,7 @@ package body Sem_Ch4 is
    --  Start of processing for Analyze_Slice
 
    begin
-      Check_Formal_Restriction ("slice is not allowed", N);
+      Check_SPARK_Restriction ("slice is not allowed", N);
 
       Analyze (P);
       Analyze (D);
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 177987c..bfd41d0 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -819,7 +819,7 @@ package body Sem_Ch5 is
       --  block statements generated by the expander is fine.
 
       if Nkind (Original_Node (N)) = N_Block_Statement then
-         Check_Formal_Restriction ("block statement is not allowed", N);
+         Check_SPARK_Restriction ("block statement is not allowed", N);
       end if;
 
       --  If no handled statement sequence is present, things are really messed
@@ -1108,12 +1108,12 @@ package body Sem_Ch5 is
       Analyze_Choices (N, Exp_Type, Dont_Care, Others_Present);
 
       --  A case statement with a single OTHERS alternative is not allowed
-      --  in SPARK or ALFA.
+      --  in SPARK.
 
       if Others_Present
         and then List_Length (Alternatives (N)) = 1
       then
-         Check_Formal_Restriction
+         Check_SPARK_Restriction
            ("OTHERS as unique case alternative is not allowed", N);
       end if;
 
@@ -1194,7 +1194,7 @@ package body Sem_Ch5 is
 
          else
             if Has_Loop_In_Inner_Open_Scopes (U_Name) then
-               Check_Formal_Restriction
+               Check_SPARK_Restriction
                  ("exit label must name the closest enclosing loop", N);
             end if;
 
@@ -1240,34 +1240,34 @@ package body Sem_Ch5 is
 
       if Present (Cond) then
          if Nkind (Parent (N)) /= N_Loop_Statement then
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("exit with when clause must be directly in loop", N);
          end if;
 
       else
          if Nkind (Parent (N)) /= N_If_Statement then
             if Nkind (Parent (N)) = N_Elsif_Part then
-               Check_Formal_Restriction
+               Check_SPARK_Restriction
                  ("exit must be in IF without ELSIF", N);
             else
-               Check_Formal_Restriction ("exit must be directly in IF", N);
+               Check_SPARK_Restriction ("exit must be directly in IF", N);
             end if;
 
          elsif Nkind (Parent (Parent (N))) /= N_Loop_Statement then
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("exit must be in IF directly in loop", N);
 
             --  First test the presence of ELSE, so that an exit in an ELSE
             --  leads to an error mentioning the ELSE.
 
          elsif Present (Else_Statements (Parent (N))) then
-            Check_Formal_Restriction ("exit must be in IF without ELSE", N);
+            Check_SPARK_Restriction ("exit must be in IF without ELSE", N);
 
             --  An exit in an ELSIF does not reach here, as it would have been
             --  detected in the case (Nkind (Parent (N)) /= N_If_Statement).
 
          elsif Present (Elsif_Parts (Parent (N))) then
-            Check_Formal_Restriction ("exit must be in IF without ELSIF", N);
+            Check_SPARK_Restriction ("exit must be in IF without ELSIF", N);
          end if;
       end if;
 
@@ -1295,7 +1295,7 @@ package body Sem_Ch5 is
       Label_Ent   : Entity_Id;
 
    begin
-      Check_Formal_Restriction ("goto statement is not allowed", N);
+      Check_SPARK_Restriction ("goto statement is not allowed", N);
 
       --  Actual semantic checks
 
@@ -1963,10 +1963,10 @@ package body Sem_Ch5 is
                end;
 
                --  Loop parameter specification must include subtype mark in
-               --  SPARK or ALFA.
+               --  SPARK.
 
                if Nkind (DS) = N_Range then
-                  Check_Formal_Restriction
+                  Check_SPARK_Restriction
                     ("loop parameter specification must include subtype mark",
                      N);
                end if;
@@ -2546,8 +2546,7 @@ package body Sem_Ch5 is
             --  we are in formal mode where goto statements are not allowed.
 
             if Nkind (Nxt) = N_Label
-              and then not (Formal_Verification_Mode
-                             or else Restriction_Check_Required (SPARK))
+              and then not Restriction_Check_Required (SPARK)
             then
                return;
 
@@ -2605,7 +2604,7 @@ package body Sem_Ch5 is
                   --  Now issue the warning (or error in formal mode)
 
                   if SPARK_Mode or else Restriction_Check_Required (SPARK) then
-                     Check_Formal_Restriction
+                     Check_SPARK_Restriction
                        ("unreachable code is not allowed", Error_Node);
                   else
                      Error_Msg ("?unreachable code!", Sloc (Error_Node));
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 170533d..3c8f02e 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -227,7 +227,7 @@ package body Sem_Ch6 is
       Scop       : constant Entity_Id := Current_Scope;
 
    begin
-      Check_Formal_Restriction ("abstract subprogram is not allowed", N);
+      Check_SPARK_Restriction ("abstract subprogram is not allowed", N);
 
       Generate_Definition (Designator);
       Set_Is_Abstract_Subprogram (Designator);
@@ -631,20 +631,20 @@ package body Sem_Ch6 is
          Analyze_And_Resolve (Expr, R_Type);
          Check_Limited_Return (Expr);
 
-         --  The only RETURN allowed in SPARK or ALFA is as the last statement
-         --  of the function.
+         --  The only RETURN allowed in SPARK is as the last statement of the
+         --  function.
 
          if Nkind (Parent (N)) /= N_Handled_Sequence_Of_Statements
            and then
              (Nkind (Parent (Parent (N))) /= N_Subprogram_Body
                or else Present (Next (N)))
          then
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("RETURN should be the last statement in function", N);
          end if;
 
       else
-         Check_Formal_Restriction ("extended RETURN is not allowed", N);
+         Check_SPARK_Restriction ("extended RETURN is not allowed", N);
 
          --  Analyze parts specific to extended_return_statement:
 
@@ -1425,7 +1425,7 @@ package body Sem_Ch6 is
 
       if Result_Definition (N) /= Error then
          if Nkind (Result_Definition (N)) = N_Access_Definition then
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("access result is not allowed", Result_Definition (N));
 
             --  Ada 2005 (AI-254): Handle anonymous access to subprograms
@@ -1463,12 +1463,12 @@ package body Sem_Ch6 is
                Set_Is_In_ALFA (Designator, False);
             end if;
 
-            --  Unconstrained array as result is not allowed in SPARK or ALFA
+            --  Unconstrained array as result is not allowed in SPARK
 
             if Is_Array_Type (Typ)
               and then not Is_Constrained (Typ)
             then
-               Check_Formal_Restriction
+               Check_SPARK_Restriction
                  ("returning an unconstrained array is not allowed",
                   Result_Definition (N));
             end if;
@@ -1910,7 +1910,7 @@ package body Sem_Ch6 is
                  and then not Nkind_In (Stat, N_Simple_Return_Statement,
                                               N_Extended_Return_Statement)
                then
-                  Check_Formal_Restriction
+                  Check_SPARK_Restriction
                     ("last statement in function should be RETURN", Stat);
                end if;
             end;
@@ -1928,7 +1928,7 @@ package body Sem_Ch6 is
             --  borrow the Check_Returns procedure here ???
 
             if Return_Present (Id) then
-               Check_Formal_Restriction
+               Check_SPARK_Restriction
                  ("procedure should not have RETURN", N);
             end if;
          end if;
@@ -2866,12 +2866,12 @@ package body Sem_Ch6 is
    --  Start of processing for Analyze_Subprogram_Declaration
 
    begin
-      --  Null procedures are not allowed in SPARK or ALFA
+      --  Null procedures are not allowed in SPARK
 
       if Nkind (Specification (N)) = N_Procedure_Specification
         and then Null_Present (Specification (N))
       then
-         Check_Formal_Restriction ("null procedure is not allowed", N);
+         Check_SPARK_Restriction ("null procedure is not allowed", N);
       end if;
 
       --  For a null procedure, capture the profile before analysis, for
@@ -3118,13 +3118,12 @@ package body Sem_Ch6 is
 
       Set_Is_In_ALFA (Designator);
 
-      --  User-defined operator is not allowed in SPARK or ALFA, except as
-      --  a renaming.
+      --  User-defined operator is not allowed in SPARK, except as a renaming
 
       if Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol
         and then Nkind (Parent (N)) /= N_Subprogram_Renaming_Declaration
       then
-         Check_Formal_Restriction ("user-defined operator is not allowed", N);
+         Check_SPARK_Restriction ("user-defined operator is not allowed", N);
       end if;
 
       --  Proceed with analysis
@@ -8572,10 +8571,10 @@ package body Sem_Ch6 is
          Check_Overriding_Indicator
            (S, Overridden_Subp, Is_Primitive => Is_Primitive_Subp);
 
-         --  Overloading is not allowed in SPARK or ALFA
+         --  Overloading is not allowed in SPARK
 
          Error_Msg_Sloc := Sloc (Homonym (S));
-         Check_Formal_Restriction ("overloading not allowed with entity#", S);
+         Check_SPARK_Restriction ("overloading not allowed with entity#", S);
 
          --  If S is a derived operation for an untagged type then by
          --  definition it's not a dispatching operation (even if the parent
@@ -8853,7 +8852,7 @@ package body Sem_Ch6 is
          Default := Expression (Param_Spec);
 
          if Present (Default) then
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("default expression is not allowed", Default);
 
             if Out_Present (Param_Spec) then
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index 4a1eedd..20b64a7 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -529,7 +529,7 @@ package body Sem_Ch8 is
       Nam : constant Node_Id := Name (N);
 
    begin
-      Check_Formal_Restriction ("exception renaming is not allowed", N);
+      Check_SPARK_Restriction ("exception renaming is not allowed", N);
 
       Enter_Name (Id);
       Analyze (Nam);
@@ -626,7 +626,7 @@ package body Sem_Ch8 is
          return;
       end if;
 
-      Check_Formal_Restriction ("generic renaming is not allowed", N);
+      Check_SPARK_Restriction ("generic renaming is not allowed", N);
 
       Generate_Definition (New_P);
 
@@ -718,7 +718,7 @@ package body Sem_Ch8 is
          return;
       end if;
 
-      Check_Formal_Restriction ("object renaming is not allowed", N);
+      Check_SPARK_Restriction ("object renaming is not allowed", N);
 
       Set_Is_Pure (Id, Is_Pure (Current_Scope));
       Enter_Name (Id);
@@ -1582,6 +1582,11 @@ package body Sem_Ch8 is
    procedure Analyze_Subprogram_Renaming (N : Node_Id) is
       Formal_Spec : constant Node_Id          := Corresponding_Formal_Spec (N);
       Is_Actual   : constant Boolean          := Present (Formal_Spec);
+
+      CW_Actual   : Boolean                   := False;
+      --  True if the renaming is for a defaulted formal subprogram when the
+      --  actual for a related formal type is class-wide. For AI05-0071.
+
       Inst_Node   : Node_Id                   := Empty;
       Nam         : constant Node_Id          := Name (N);
       New_S       : Entity_Id;
@@ -1734,6 +1739,7 @@ package body Sem_Ch8 is
          end loop;
 
          if Present (Formal_Type) then
+            CW_Actual := True;
 
             --  Create declaration and body for class-wide operation
 
@@ -2430,14 +2436,11 @@ package body Sem_Ch8 is
 
          elsif Ekind (Old_S) /= E_Operator then
 
-            --  If this is a default subprogram, it may be for a class-wide
-            --  actual, in which case there is no check for mode conformance,
-            --  given that the signatures do not match (the source mentions T,
-            --  but the actual mentions T'Class).
+            --  If this a defaulted subprogram for a class-wide actual there is
+            --  no check for mode conformance,  given that the signatures don't
+            --  match (the source mentions T but the actual mentions T'class).
 
-            if  Is_Actual
-              and then From_Default (N)
-            then
+            if  CW_Actual then
                null;
 
             else
@@ -2745,7 +2748,7 @@ package body Sem_Ch8 is
    --  Start of processing for Analyze_Use_Package
 
    begin
-      Check_Formal_Restriction ("use clause is not allowed", N);
+      Check_SPARK_Restriction ("use clause is not allowed", N);
 
       Set_Hidden_By_Use_Clause (N, No_Elist);
 
@@ -5551,12 +5554,12 @@ package body Sem_Ch8 is
 
       if SPARK_Mode or else Restriction_Check_Required (SPARK) then
          if Nkind (Selector_Name (N)) = N_Character_Literal then
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("character literal cannot be prefixed", N);
          elsif Nkind (Selector_Name (N)) = N_Operator_Symbol
            and then Nkind (Parent (N)) /= N_Subprogram_Renaming_Declaration
          then
-            Check_Formal_Restriction ("operator symbol cannot be prefixed", N);
+            Check_SPARK_Restriction ("operator symbol cannot be prefixed", N);
          end if;
       end if;
 
@@ -5888,10 +5891,10 @@ package body Sem_Ch8 is
            and then (SPARK_Mode or else Restriction_Check_Required (SPARK))
          then
             if Is_Subprogram (P_Name) then
-               Check_Formal_Restriction
+               Check_SPARK_Restriction
                  ("prefix of expanded name cannot be a subprogram", P);
             elsif Ekind (P_Name) = E_Loop then
-               Check_Formal_Restriction
+               Check_SPARK_Restriction
                  ("prefix of expanded name cannot be a loop statement", P);
             end if;
          end if;
@@ -6044,7 +6047,7 @@ package body Sem_Ch8 is
 
          elsif Attribute_Name (N) = Name_Base then
             Error_Msg_Name_1 := Name_Base;
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("attribute% is only allowed as prefix of another attribute", N);
 
             if Ada_Version = Ada_83 and then Comes_From_Source (N) then
diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb
index 09214b8..399d36e 100644
--- a/gcc/ada/sem_ch9.adb
+++ b/gcc/ada/sem_ch9.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -101,7 +101,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_Formal_Restriction ("abort statement is not allowed", N);
+      Check_SPARK_Restriction ("abort statement is not allowed", N);
 
       T_Name := First (Names (N));
       while Present (T_Name) loop
@@ -172,7 +172,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_Formal_Restriction ("accept statement is not allowed", N);
+      Check_SPARK_Restriction ("accept statement is not allowed", N);
 
       --  Entry name is initialized to Any_Id. It should get reset to the
       --  matching entry entity. An error is signalled if it is not reset.
@@ -403,7 +403,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_Formal_Restriction ("select statement is not allowed", N);
+      Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (Max_Asynchronous_Select_Nesting, N);
       Check_Restriction (No_Select_Statements, N);
 
@@ -449,7 +449,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_Formal_Restriction ("select statement is not allowed", N);
+      Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (No_Select_Statements, N);
 
       --  Ada 2005 (AI-345): The trigger may be a dispatching call
@@ -546,7 +546,7 @@ package body Sem_Ch9 is
       E : constant Node_Id := Expression (N);
    begin
       Tasking_Used := True;
-      Check_Formal_Restriction ("delay statement is not allowed", N);
+      Check_SPARK_Restriction ("delay statement is not allowed", N);
       Check_Restriction (No_Relative_Delay, N);
       Check_Restriction (No_Delay, N);
       Check_Potentially_Blocking_Operation (N);
@@ -564,7 +564,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_Formal_Restriction ("delay statement is not allowed", N);
+      Check_SPARK_Restriction ("delay statement is not allowed", N);
       Check_Restriction (No_Delay, N);
       Check_Potentially_Blocking_Operation (N);
       Analyze (E);
@@ -851,7 +851,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_Formal_Restriction ("entry call is not allowed", N);
+      Check_SPARK_Restriction ("entry call is not allowed", N);
 
       if Present (Pragmas_Before (N)) then
          Analyze_List (Pragmas_Before (N));
@@ -1114,7 +1114,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_Formal_Restriction ("protected definition is not allowed", N);
+      Check_SPARK_Restriction ("protected definition is not allowed", N);
       Analyze_Declarations (Visible_Declarations (N));
 
       if Present (Private_Declarations (N))
@@ -1308,7 +1308,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_Formal_Restriction ("requeue statement is not allowed", N);
+      Check_SPARK_Restriction ("requeue statement is not allowed", N);
       Check_Restriction (No_Requeue_Statements, N);
       Check_Unreachable_Code (N);
 
@@ -1582,7 +1582,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_Formal_Restriction ("select statement is not allowed", N);
+      Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (No_Select_Statements, N);
 
       --  Loop to analyze alternatives
@@ -1960,7 +1960,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_Formal_Restriction ("task definition is not allowed", N);
+      Check_SPARK_Restriction ("task definition is not allowed", N);
 
       if Present (Visible_Declarations (N)) then
          Analyze_Declarations (Visible_Declarations (N));
@@ -2120,7 +2120,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
-      Check_Formal_Restriction ("select statement is not allowed", N);
+      Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (No_Select_Statements, N);
 
       --  Ada 2005 (AI-345): The trigger may be a dispatching call
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index ef406e1..1f0cc13 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -3605,7 +3605,7 @@ package body Sem_Res is
 
                      begin
                         if not Is_SPARK_Object_Reference (Operand) then
-                           Check_Formal_Restriction
+                           Check_SPARK_Restriction
                              ("object required", Operand);
 
                         --  In formal mode, the only view conversions are those
@@ -3621,11 +3621,11 @@ package body Sem_Res is
                            if Ekind_In
                              (F, E_Out_Parameter, E_In_Out_Parameter)
                            then
-                              Check_Formal_Restriction
+                              Check_SPARK_Restriction
                                 ("ancestor conversion is the only permitted "
                                  & "view conversion", A);
                            else
-                              Check_Formal_Restriction
+                              Check_SPARK_Restriction
                                 ("ancestor conversion required", A);
                            end if;
 
@@ -3635,7 +3635,7 @@ package body Sem_Res is
                      end;
 
                   else
-                     Check_Formal_Restriction ("object required", A);
+                     Check_SPARK_Restriction ("object required", A);
                   end if;
 
                --  In formal mode, the only view conversions are those
@@ -3644,7 +3644,7 @@ package body Sem_Res is
                elsif Nkind (A) = N_Type_Conversion
                  and then Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter)
                then
-                  Check_Formal_Restriction
+                  Check_SPARK_Restriction
                     ("ancestor conversion is the only permitted view "
                      & "conversion", A);
                end if;
@@ -4887,9 +4887,9 @@ package body Sem_Res is
       Generate_Operator_Reference (N, Typ);
       Eval_Arithmetic_Op (N);
 
-      --  In SPARK and ALFA, a multiplication or division with operands of
-      --  fixed point types shall be qualified or explicitly converted to
-      --  identify the result type.
+      --  In SPARK, a multiplication or division with operands of fixed point
+      --  types shall be qualified or explicitly converted to identify the
+      --  result type.
 
       if (Is_Fixed_Point_Type (Etype (L))
            or else Is_Fixed_Point_Type (Etype (R)))
@@ -4897,7 +4897,7 @@ package body Sem_Res is
         and then
           not Nkind_In (Parent (N), N_Qualified_Expression, N_Type_Conversion)
       then
-         Check_Formal_Restriction
+         Check_SPARK_Restriction
            ("operation should be qualified or explicitly converted", N);
       end if;
 
@@ -5960,16 +5960,16 @@ package body Sem_Res is
       Generate_Operator_Reference (N, T);
       Check_Low_Bound_Tested (N);
 
-      --  In SPARK or ALFA, ordering operators <, <=, >, >= are not defined
-      --  for Boolean types or array types except String.
+      --  In SPARK, ordering operators <, <=, >, >= are not defined for Boolean
+      --  types or array types except String.
 
       if Is_Boolean_Type (T) then
-         Check_Formal_Restriction
+         Check_SPARK_Restriction
            ("comparison is not defined on Boolean type", N);
       elsif Is_Array_Type (T)
         and then Base_Type (T) /= Standard_String
       then
-         Check_Formal_Restriction
+         Check_SPARK_Restriction
            ("comparison is not defined on array types other than String", N);
       else
          null;
@@ -6817,9 +6817,9 @@ package body Sem_Res is
          Resolve (L, T);
          Resolve (R, T);
 
-         --  In SPARK or ALFA, equality operators = and /= for array types
-         --  other than String are only defined when, for each index position,
-         --  the operands have equal static bounds.
+         --  In SPARK, equality operators = and /= for array types other than
+         --  String are only defined when, for each index position, the
+         --  operands have equal static bounds.
 
          if Is_Array_Type (T)
            and then Base_Type (T) /= Standard_String
@@ -6828,7 +6828,7 @@ package body Sem_Res is
            and then Etype (R) /= Any_Composite  --  or else R in error
            and then not Matching_Static_Array_Bounds (Etype (L), Etype (R))
          then
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("array types should have matching static bounds", N);
          end if;
 
@@ -7357,10 +7357,10 @@ package body Sem_Res is
       Generate_Operator_Reference (N, B_Typ);
       Eval_Logical_Op (N);
 
-      --  In SPARK or ALFA, logical operations AND, OR and XOR for arrays are
-      --  defined only when both operands have same static lower and higher
-      --  bounds. Of course the types have to match, so only check if operands
-      --  are compatible and the node itself has no errors.
+      --  In SPARK, logical operations AND, OR and XOR for arrays are defined
+      --  only when both operands have same static lower and higher bounds. Of
+      --  course the types have to match, so only check if operands are
+      --  compatible and the node itself has no errors.
 
       if Is_Array_Type (B_Typ)
         and then Nkind (N) in N_Binary_Op
@@ -7374,7 +7374,7 @@ package body Sem_Res is
               and then Right_Typ /= Any_Composite  --  or Right_Opnd in error
               and then not Matching_Static_Array_Bounds (Left_Typ, Right_Typ)
             then
-               Check_Formal_Restriction
+               Check_SPARK_Restriction
                  ("array types should have matching static bounds", N);
             end if;
          end;
@@ -7627,7 +7627,7 @@ package body Sem_Res is
       end loop;
 
       if Base_Type (Etype (N)) /= Standard_String then
-         Check_Formal_Restriction
+         Check_SPARK_Restriction
            ("result of concatenation should have type String", N);
       end if;
    end Resolve_Op_Concat;
@@ -7734,21 +7734,21 @@ package body Sem_Res is
          Resolve (Arg, Btyp);
       end if;
 
-      --  Concatenation is restricted in SPARK or ALFA: each operand must be
-      --  either a string literal, a static character expression, or another
+      --  Concatenation is restricted in SPARK: each operand must be either a
+      --  string literal, a static character expression, or another
       --  concatenation. Arg cannot be a concatenation here as callers of
       --  Resolve_Op_Concat_Arg call it separately on each final operand, past
       --  concatenation operations.
 
       if Is_Character_Type (Etype (Arg)) then
          if not Is_Static_Expression (Arg) then
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("character operand for concatenation should be static", N);
          end if;
 
       elsif Is_String_Type (Etype (Arg)) then
          if not Is_Static_Expression (Arg) then
-            Check_Formal_Restriction
+            Check_SPARK_Restriction
               ("string operand for concatenation should be static", N);
          end if;
 
@@ -8032,7 +8032,7 @@ package body Sem_Res is
         and then Etype (Expr) /= Any_Composite  --  or else Expr in error
         and then not Matching_Static_Array_Bounds (Target_Typ, Etype (Expr))
       then
-         Check_Formal_Restriction
+         Check_SPARK_Restriction
            ("array types should have matching static bounds", N);
       end if;
 
@@ -9150,15 +9150,15 @@ package body Sem_Res is
 
       Resolve (Operand);
 
-      --  In SPARK or ALFA, a type conversion between array types should be
-      --  restricted to types which have matching static bounds.
+      --  In SPARK, a type conversion between array types should be restricted
+      --  to types which have matching static bounds.
 
       if Is_Array_Type (Target_Typ)
         and then Is_Array_Type (Operand_Typ)
         and then Operand_Typ /= Any_Composite  --  or else Operand in error
         and then not Matching_Static_Array_Bounds (Target_Typ, Operand_Typ)
       then
-         Check_Formal_Restriction
+         Check_SPARK_Restriction
            ("array types should have matching static bounds", N);
       end if;
 
@@ -9172,7 +9172,7 @@ package body Sem_Res is
         and then Is_Ancestor (Target_Typ, Operand_Typ)
         and then not Is_SPARK_Object_Reference (Operand)
       then
-         Check_Formal_Restriction ("object required", Operand);
+         Check_SPARK_Restriction ("object required", Operand);
       end if;
 
       --  Note: we do the Eval_Type_Conversion call before applying the
@@ -9414,7 +9414,7 @@ package body Sem_Res is
    begin
       if Is_Modular_Integer_Type (Typ) and then Nkind (N) /= N_Op_Not then
          Error_Msg_Name_1 := Chars (Typ);
-         Check_Formal_Restriction
+         Check_SPARK_Restriction
            ("unary operator not defined for modular type%", N);
       end if;
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index ef65040..b69bada 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -1179,7 +1179,7 @@ package body Sem_Util is
                      end if;
                   else
                      Error_Msg_Sloc := Body_Sloc;
-                     Check_Formal_Restriction
+                     Check_SPARK_Restriction
                        ("decl cannot appear after body#", Decl);
                   end if;
                end if;
@@ -3315,11 +3315,10 @@ package body Sem_Util is
       Append_Entity     (Def_Id, S);
       Set_Public_Status (Def_Id);
 
-      --  Declaring a homonym is not allowed in SPARK or ALFA ...
+      --  Declaring a homonym is not allowed in SPARK ...
 
       if Present (C)
-        and then (Restriction_Check_Required (SPARK)
-                   or else Formal_Verification_Mode)
+        and then Restriction_Check_Required (SPARK)
       then
 
          declare
@@ -3359,7 +3358,7 @@ package body Sem_Util is
               and then Comes_From_Source (C)
             then
                Error_Msg_Sloc := Sloc (C);
-               Check_Formal_Restriction
+               Check_SPARK_Restriction
                  ("redeclaration of identifier &#", Def_Id);
             end if;
          end;
@@ -10789,7 +10788,7 @@ package body Sem_Util is
            and then (Typ = 't' or else Ekind (Ent) = E_Package)
          then
             Error_Msg_Node_1 := Endl;
-            Check_Formal_Restriction ("`END &` required", Endl, Force => True);
+            Check_SPARK_Restriction ("`END &` required", Endl, Force => True);
          end if;
       end if;