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

	* einfo.adb, einfo.ads (Body_Is_In_ALFA, Set_Body_Is_In_ALFA): get/set
	for new flag denoting which subprogram bodies are in ALFA
	* restrict.adb, sem_ch7.adb: Update comment
	* sem_ch11.adb, sem_ch2.adb, sem_ch3.adb, sem_ch4.adb, sem_ch5.adb,
	sem_ch9.adb, sem_res.adb: Add calls to
	Current_Subprogram_Body_Is_Not_In_ALFA on unsupported constructs.
	* sem_ch6.adb (Analyze_Function_Return): add calls to
	Current_Subprogram_Body_Is_Not_In_ALFA on return statement in the
	middle of the body, and extended return.
	(Check_Missing_Return): add calls to Set_Body_Is_In_ALFA with argument
	False when missing return.
	(Analyze_Subprogram_Body_Helper): initialize the flag Body_Is_In_ALFA
	to True for subprograms whose spec is in ALFA. Remove later on the flag
	on the entity used for a subprogram body when there exists a separate
	declaration.
	* sem_util.adb, sem_util.ads (Current_Subprogram_Body_Is_Not_In_ALFA):
	if Current_Subprogram is not Empty, set its flag Body_Is_In_ALFA to
	False, otherwise do nothing.



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

15 files changed, 202 insertions, 29 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index ece9717f063..8777494989c 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,24 @@
+2011-08-02  Yannick Moy  <moy@adacore.com>
+
+	* einfo.adb, einfo.ads (Body_Is_In_ALFA, Set_Body_Is_In_ALFA): get/set
+	for new flag denoting which subprogram bodies are in ALFA
+	* restrict.adb, sem_ch7.adb: Update comment
+	* sem_ch11.adb, sem_ch2.adb, sem_ch3.adb, sem_ch4.adb, sem_ch5.adb,
+	sem_ch9.adb, sem_res.adb: Add calls to
+	Current_Subprogram_Body_Is_Not_In_ALFA on unsupported constructs.
+	* sem_ch6.adb (Analyze_Function_Return): add calls to
+	Current_Subprogram_Body_Is_Not_In_ALFA on return statement in the
+	middle of the body, and extended return.
+	(Check_Missing_Return): add calls to Set_Body_Is_In_ALFA with argument
+	False when missing return.
+	(Analyze_Subprogram_Body_Helper): initialize the flag Body_Is_In_ALFA
+	to True for subprograms whose spec is in ALFA. Remove later on the flag
+	on the entity used for a subprogram body when there exists a separate
+	declaration.
+	* sem_util.adb, sem_util.ads (Current_Subprogram_Body_Is_Not_In_ALFA):
+	if Current_Subprogram is not Empty, set its flag Body_Is_In_ALFA to
+	False, otherwise do nothing.
+
 2011-08-02  Robert Dewar  <dewar@adacore.com>
 
 	* inline.adb, stand.ads, sem_ch6.adb, sem_ch8.adb: Minor reformatting.
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 062e1fd445d..ff07cfc4d1f 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -518,7 +518,7 @@ package body Einfo is
    --    Is_Safe_To_Reevaluate           Flag249
    --    Has_Predicates                  Flag250
 
-   --    (unused)                        Flag251
+   --    Body_Is_In_ALFA                 Flag251
    --    (unused)                        Flag252
    --    (unused)                        Flag253
    --    (unused)                        Flag254
@@ -651,6 +651,12 @@ package body Einfo is
       return Node19 (Id);
    end Body_Entity;
 
+   function Body_Is_In_ALFA (Id : E) return B is
+   begin
+      pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
+      return Flag251 (Id);
+   end Body_Is_In_ALFA;
+
    function Body_Needed_For_SAL (Id : E) return B is
    begin
       pragma Assert
@@ -3098,6 +3104,12 @@ package body Einfo is
       Set_Node19 (Id, V);
    end Set_Body_Entity;
 
+   procedure Set_Body_Is_In_ALFA (Id : E; V : B := True) is
+   begin
+      pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
+      Set_Flag251 (Id, V);
+   end Set_Body_Is_In_ALFA;
+
    procedure Set_Body_Needed_For_SAL (Id : E; V : B := True) is
    begin
       pragma Assert
@@ -7349,6 +7361,7 @@ package body Einfo is
       end if;
 
       W ("Address_Taken",                   Flag104 (Id));
+      W ("Body_Is_In_ALFA",                 Flag251 (Id));
       W ("Body_Needed_For_SAL",             Flag40  (Id));
       W ("C_Pass_By_Copy",                  Flag125 (Id));
       W ("Can_Never_Be_Null",               Flag38  (Id));
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index aa5b0e2961d..d666b5f85fb 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -7,7 +7,7 @@
 --                                 S p e c                                  --
 --                                                                          --
 --          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- --
 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
@@ -486,6 +486,11 @@ package Einfo is
 --       Present in package and generic package entities, points to the
 --       corresponding package body entity if one is present.
 
+--    Body_Is_In_ALFA (Flag251)
+--       Present in subprogram entities. Set for subprograms whose body belongs
+--       to the ALFA subset, which are eligible for formal verification through
+--       SPARK or Why tool-sets.
+
 --    Body_Needed_For_SAL (Flag40)
 --       Present in package and subprogram entities that are compilation
 --       units. Indicates that the source for the body must be included
@@ -2273,7 +2278,9 @@ package Einfo is
 --    Is_In_ALFA (Flag151)
 --       Present in all entities. Set for entities that belong to the ALFA
 --       subset, which are eligible for formal verification through SPARK or
---       Why tool-sets.
+--       Why tool-sets. For a subprogram, this only means that a call to the
+--       subprogram can be formally analyzed. Another flag, Body_Is_In_ALFA,
+--       defines which subprograms can be formally analyzed.
 
 --    Is_Inlined (Flag11)
 --       Present in all entities. Set for functions and procedures which are
@@ -4336,7 +4343,7 @@ package Einfo is
    --  E_Anonymous_Access_Protected_Subprogram_Type
        E_Anonymous_Access_Type;
 
-   subtype Access_Subprogram_Kind is Entity_Kind range
+   subtype Access_Subprogram_Kind      is Entity_Kind range
        E_Access_Subprogram_Type ..
    --  E_Anonymous_Access_Subprogram_Type
    --  E_Access_Protected_Subprogram_Type
@@ -4536,7 +4543,7 @@ package Einfo is
    --  E_Floating_Point_Type
        E_Floating_Point_Subtype;
 
-   subtype Object_Kind                is Entity_Kind range
+   subtype Object_Kind                 is Entity_Kind range
        E_Component ..
    --  E_Constant
    --  E_Discriminant
@@ -5933,6 +5940,7 @@ package Einfo is
    function Barrier_Function                    (Id : E) return N;
    function Block_Node                          (Id : E) return N;
    function Body_Entity                         (Id : E) return E;
+   function Body_Is_In_ALFA                     (Id : E) return B;
    function Body_Needed_For_SAL                 (Id : E) return B;
    function CR_Discriminant                     (Id : E) return E;
    function C_Pass_By_Copy                      (Id : E) return B;
@@ -6519,6 +6527,7 @@ package Einfo is
    procedure Set_Barrier_Function                (Id : E; V : N);
    procedure Set_Block_Node                      (Id : E; V : N);
    procedure Set_Body_Entity                     (Id : E; V : E);
+   procedure Set_Body_Is_In_ALFA                 (Id : E; V : B := True);
    procedure Set_Body_Needed_For_SAL             (Id : E; V : B := True);
    procedure Set_CR_Discriminant                 (Id : E; V : E);
    procedure Set_C_Pass_By_Copy                  (Id : E; V : B := True);
@@ -7212,6 +7221,7 @@ package Einfo is
    pragma Inline (Barrier_Function);
    pragma Inline (Block_Node);
    pragma Inline (Body_Entity);
+   pragma Inline (Body_Is_In_ALFA);
    pragma Inline (Body_Needed_For_SAL);
    pragma Inline (CR_Discriminant);
    pragma Inline (C_Pass_By_Copy);
@@ -7653,6 +7663,7 @@ package Einfo is
    pragma Inline (Set_Barrier_Function);
    pragma Inline (Set_Block_Node);
    pragma Inline (Set_Body_Entity);
+   pragma Inline (Set_Body_Is_In_ALFA);
    pragma Inline (Set_Body_Needed_For_SAL);
    pragma Inline (Set_CR_Discriminant);
    pragma Inline (Set_C_Pass_By_Copy);
diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb
index c68475bb907..b37a593b8be 100644
--- a/gcc/ada/restrict.adb
+++ b/gcc/ada/restrict.adb
@@ -371,7 +371,7 @@ package body Restrict is
          return;
       end if;
 
-      --  In formal mode, issue an error for any use of class-wide, even if the
+      --  In SPARK mode, issue an error for any use of class-wide, even if the
       --  No_Dispatch restriction is not set.
 
       if R = No_Dispatch then
diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb
index 357b3f1046a..73926faa4bb 100644
--- a/gcc/ada/sem_ch11.adb
+++ b/gcc/ada/sem_ch11.adb
@@ -443,6 +443,7 @@ package body Sem_Ch11 is
       P              : Node_Id;
 
    begin
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("raise statement is not allowed", N);
       Check_Unreachable_Code (N);
 
@@ -610,6 +611,7 @@ package body Sem_Ch11 is
    --  Start of processing for Analyze_Raise_xxx_Error
 
    begin
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("raise statement is not allowed", N);
 
       if No (Etype (N)) then
diff --git a/gcc/ada/sem_ch2.adb b/gcc/ada/sem_ch2.adb
index 3a3bbf9d245..2a021d2d787 100644
--- a/gcc/ada/sem_ch2.adb
+++ b/gcc/ada/sem_ch2.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2007, 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- --
@@ -24,12 +24,14 @@
 ------------------------------------------------------------------------------
 
 with Atree;    use Atree;
+with Einfo;    use Einfo;
 with Errout;   use Errout;
 with Namet;    use Namet;
 with Opt;      use Opt;
 with Restrict; use Restrict;
 with Rident;   use Rident;
 with Sem_Ch8;  use Sem_Ch8;
+with Sem_Util; use Sem_Util;
 with Sinfo;    use Sinfo;
 with Stand;    use Stand;
 with Uintp;    use Uintp;
@@ -74,6 +76,13 @@ package body Sem_Ch2 is
          return;
       else
          Find_Direct_Name (N);
+
+         if Present (Entity (N))
+           and then Is_Object (Entity (N))
+           and then not Is_In_ALFA (Entity (N))
+         then
+            Current_Subprogram_Body_Is_Not_In_ALFA;
+         end if;
       end if;
    end Analyze_Identifier;
 
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 55d4c3b3583..0f585a8d098 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -3030,10 +3030,13 @@ package body Sem_Ch3 is
 
       Act_T := T;
 
-      --  The object is in ALFA if-and-only-if its type is in ALFA
+      --  The object is in ALFA if-and-only-if its type is in ALFA and it is
+      --  not aliased.
 
-      if Is_In_ALFA (T) then
+      if Is_In_ALFA (T) and then not Aliased_Present (N) then
          Set_Is_In_ALFA (Id);
+      else
+         Current_Subprogram_Body_Is_Not_In_ALFA;
       end if;
 
       --  These checks should be performed before the initialization expression
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb
index ae169c2b5be..7fd0d9b04df 100644
--- a/gcc/ada/sem_ch4.adb
+++ b/gcc/ada/sem_ch4.adb
@@ -350,6 +350,8 @@ package body Sem_Ch4 is
 
    procedure Analyze_Aggregate (N : Node_Id) is
    begin
+      Current_Subprogram_Body_Is_Not_In_ALFA;
+
       if No (Etype (N)) then
          Set_Etype (N, Any_Composite);
       end if;
@@ -369,6 +371,7 @@ package body Sem_Ch4 is
       C        : Node_Id;
 
    begin
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("allocator is not allowed", N);
 
       --  Deal with allocator restrictions
@@ -982,6 +985,15 @@ package body Sem_Ch4 is
             return;
          end if;
 
+         --  If this is an indirect call, or the subprogram called is not in
+         --  ALFA, then the call is not in ALFA.
+
+         if not Is_Subprogram (Nam_Ent)
+           or else not Is_In_ALFA (Nam_Ent)
+         then
+            Current_Subprogram_Body_Is_Not_In_ALFA;
+         end if;
+
          Analyze_One_Call (N, Nam_Ent, True, Success);
 
          --  If this is an indirect call, the return type of the access_to
@@ -1358,6 +1370,8 @@ package body Sem_Ch4 is
       L  : Node_Id;
 
    begin
+      Current_Subprogram_Body_Is_Not_In_ALFA;
+
       Candidate_Type := Empty;
 
       --  The following code is equivalent to:
@@ -1506,6 +1520,7 @@ package body Sem_Ch4 is
          return;
       end if;
 
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("conditional expression is not allowed", N);
 
       Else_Expr := Next (Then_Expr);
@@ -1706,6 +1721,7 @@ package body Sem_Ch4 is
    --  Start of processing for Analyze_Explicit_Dereference
 
    begin
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("explicit dereference is not allowed", N);
 
       Analyze (P);
@@ -2467,6 +2483,8 @@ package body Sem_Ch4 is
    --  Start of processing for Analyze_Membership_Op
 
    begin
+      Current_Subprogram_Body_Is_Not_In_ALFA;
+
       Analyze_Expression (L);
 
       if No (R)
@@ -2588,6 +2606,7 @@ package body Sem_Ch4 is
 
    procedure Analyze_Null (N : Node_Id) is
    begin
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("null is not allowed", N);
 
       Set_Etype (N, Any_Access);
@@ -3216,6 +3235,8 @@ package body Sem_Ch4 is
       T    : Entity_Id;
 
    begin
+      Current_Subprogram_Body_Is_Not_In_ALFA;
+
       Analyze_Expression (Expr);
 
       Set_Etype (N, Any_Type);
@@ -3274,6 +3295,7 @@ package body Sem_Ch4 is
       Iterator : Node_Id;
 
    begin
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("quantified expression is not allowed", N);
 
       Set_Etype  (Ent,  Standard_Void_Type);
@@ -3439,6 +3461,8 @@ package body Sem_Ch4 is
       Acc_Type : Entity_Id;
 
    begin
+      Current_Subprogram_Body_Is_Not_In_ALFA;
+
       Analyze (P);
 
       --  An interesting error check, if we take the 'Reference of an object
@@ -4302,6 +4326,7 @@ package body Sem_Ch4 is
    --  Start of processing for Analyze_Slice
 
    begin
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("slice is not allowed", N);
 
       Analyze (P);
@@ -4346,6 +4371,8 @@ package body Sem_Ch4 is
       T    : Entity_Id;
 
    begin
+      Current_Subprogram_Body_Is_Not_In_ALFA;
+
       --  If Conversion_OK is set, then the Etype is already set, and the
       --  only processing required is to analyze the expression. This is
       --  used to construct certain "illegal" conversions which are not
@@ -4476,6 +4503,7 @@ package body Sem_Ch4 is
 
    procedure Analyze_Unchecked_Type_Conversion (N : Node_Id) is
    begin
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Find_Type (Subtype_Mark (N));
       Analyze_Expression (Expression (N));
       Set_Etype (N, Entity (Subtype_Mark (N)));
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index bfd41d0619b..d0d34431855 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -815,7 +815,7 @@ package body Sem_Ch5 is
       HSS   : constant Node_Id := Handled_Statement_Sequence (N);
 
    begin
-      --  In formal mode, we reject block statements. Note that the case of
+      --  In SPARK mode, we reject block statements. Note that the case of
       --  block statements generated by the expander is fine.
 
       if Nkind (Original_Node (N)) = N_Block_Statement then
@@ -1113,6 +1113,7 @@ package body Sem_Ch5 is
       if Others_Present
         and then List_Length (Alternatives (N)) = 1
       then
+         Current_Subprogram_Body_Is_Not_In_ALFA;
          Check_SPARK_Restriction
            ("OTHERS as unique case alternative is not allowed", N);
       end if;
@@ -1194,6 +1195,7 @@ package body Sem_Ch5 is
 
          else
             if Has_Loop_In_Inner_Open_Scopes (U_Name) then
+               Current_Subprogram_Body_Is_Not_In_ALFA;
                Check_SPARK_Restriction
                  ("exit label must name the closest enclosing loop", N);
             end if;
@@ -1235,17 +1237,19 @@ package body Sem_Ch5 is
          Check_Unset_Reference (Cond);
       end if;
 
-      --  In formal mode, verify that the exit statement respects the SPARK
+      --  In SPARK mode, verify that the exit statement respects the SPARK
       --  restrictions.
 
       if Present (Cond) then
          if Nkind (Parent (N)) /= N_Loop_Statement then
+            Current_Subprogram_Body_Is_Not_In_ALFA;
             Check_SPARK_Restriction
               ("exit with when clause must be directly in loop", N);
          end if;
 
       else
          if Nkind (Parent (N)) /= N_If_Statement then
+            Current_Subprogram_Body_Is_Not_In_ALFA;
             if Nkind (Parent (N)) = N_Elsif_Part then
                Check_SPARK_Restriction
                  ("exit must be in IF without ELSIF", N);
@@ -1254,6 +1258,7 @@ package body Sem_Ch5 is
             end if;
 
          elsif Nkind (Parent (Parent (N))) /= N_Loop_Statement then
+            Current_Subprogram_Body_Is_Not_In_ALFA;
             Check_SPARK_Restriction
               ("exit must be in IF directly in loop", N);
 
@@ -1261,12 +1266,14 @@ package body Sem_Ch5 is
             --  leads to an error mentioning the ELSE.
 
          elsif Present (Else_Statements (Parent (N))) then
+            Current_Subprogram_Body_Is_Not_In_ALFA;
             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
+            Current_Subprogram_Body_Is_Not_In_ALFA;
             Check_SPARK_Restriction ("exit must be in IF without ELSIF", N);
          end if;
       end if;
@@ -1295,6 +1302,7 @@ package body Sem_Ch5 is
       Label_Ent   : Entity_Id;
 
    begin
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("goto statement is not allowed", N);
 
       --  Actual semantic checks
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 87b6a0c2e88..1c0a3d96393 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -638,11 +638,13 @@ package body Sem_Ch6 is
              (Nkind (Parent (Parent (N))) /= N_Subprogram_Body
                or else Present (Next (N)))
          then
+            Current_Subprogram_Body_Is_Not_In_ALFA;
             Check_SPARK_Restriction
               ("RETURN should be the last statement in function", N);
          end if;
 
       else
+         Current_Subprogram_Body_Is_Not_In_ALFA;
          Check_SPARK_Restriction ("extended RETURN is not allowed", N);
 
          --  Analyze parts specific to extended_return_statement:
@@ -1909,6 +1911,7 @@ package body Sem_Ch6 is
                  and then not Nkind_In (Stat, N_Simple_Return_Statement,
                                               N_Extended_Return_Statement)
                then
+                  Set_Body_Is_In_ALFA (Id, False);
                   Check_SPARK_Restriction
                     ("last statement in function should be RETURN", Stat);
                end if;
@@ -1927,6 +1930,7 @@ package body Sem_Ch6 is
             --  borrow the Check_Returns procedure here ???
 
             if Return_Present (Id) then
+               Set_Body_Is_In_ALFA (Id, False);
                Check_SPARK_Restriction
                  ("procedure should not have RETURN", N);
             end if;
@@ -2236,6 +2240,24 @@ package body Sem_Ch6 is
          end if;
       end if;
 
+      --  By default, consider that the subprogram body is in ALFA if the spec
+      --  is in ALFA. This is reversed later if some expression or statement is
+      --  not in ALFA.
+
+      declare
+         Id : Entity_Id;
+      begin
+         if Present (Spec_Id) then
+            Id := Spec_Id;
+         else
+            Id := Body_Id;
+         end if;
+
+         if Is_In_ALFA (Id) then
+            Set_Body_Is_In_ALFA (Id);
+         end if;
+      end;
+
       --  Do not inline any subprogram that contains nested subprograms, since
       --  the backend inlining circuit seems to generate uninitialized
       --  references in this case. We know this happens in the case of front
@@ -2467,6 +2489,7 @@ package body Sem_Ch6 is
          Set_Ekind (Body_Id, E_Subprogram_Body);
          Set_Scope (Body_Id, Scope (Spec_Id));
          Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Spec_Id));
+         Set_Is_In_ALFA (Body_Id, False);
 
       --  Case of subprogram body with no previous spec
 
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index 46d63dc7ab4..474f39c830e 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.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- --
@@ -875,9 +875,8 @@ package body Sem_Ch7 is
       --  package.
 
       procedure Check_One_Tagged_Type_Or_Extension_At_Most;
-      --  Issue an error in formal mode if a package specification contains
-      --  more than one tagged type or type extension. This is a restriction of
-      --  SPARK.
+      --  Issue an error in SPARK mode if a package specification contains
+      --  more than one tagged type or type extension.
 
       procedure Clear_Constants (Id : Entity_Id; FE : Entity_Id);
       --  Clears constant indications (Never_Set_In_Source, Constant_Value, and
diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb
index 399d36e8771..4392949dcbb 100644
--- a/gcc/ada/sem_ch9.adb
+++ b/gcc/ada/sem_ch9.adb
@@ -101,6 +101,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("abort statement is not allowed", N);
 
       T_Name := First (Names (N));
@@ -139,6 +140,7 @@ package body Sem_Ch9 is
    procedure Analyze_Accept_Alternative (N : Node_Id) is
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
 
       if Present (Pragmas_Before (N)) then
          Analyze_List (Pragmas_Before (N));
@@ -172,6 +174,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("accept statement is not allowed", N);
 
       --  Entry name is initialized to Any_Id. It should get reset to the
@@ -403,6 +406,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (Max_Asynchronous_Select_Nesting, N);
       Check_Restriction (No_Select_Statements, N);
@@ -449,6 +453,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (No_Select_Statements, N);
 
@@ -495,6 +500,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_Restriction (No_Delay, N);
 
       if Present (Pragmas_Before (N)) then
@@ -546,6 +552,7 @@ package body Sem_Ch9 is
       E : constant Node_Id := Expression (N);
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("delay statement is not allowed", N);
       Check_Restriction (No_Relative_Delay, N);
       Check_Restriction (No_Delay, N);
@@ -564,6 +571,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("delay statement is not allowed", N);
       Check_Restriction (No_Delay, N);
       Check_Potentially_Blocking_Operation (N);
@@ -592,6 +600,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
 
       --  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
@@ -824,6 +833,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
 
       if Present (Index) then
          Analyze (Index);
@@ -851,6 +861,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("entry call is not allowed", N);
 
       if Present (Pragmas_Before (N)) then
@@ -886,6 +897,7 @@ package body Sem_Ch9 is
    begin
       Generate_Definition (Def_Id);
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
 
       --  Case of no discrete subtype definition
 
@@ -955,6 +967,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Analyze (Def);
 
       --  There is no elaboration of the entry index specification. Therefore,
@@ -996,6 +1009,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Set_Ekind (Body_Id, E_Protected_Body);
       Spec_Id := Find_Concurrent_Spec (Body_Id);
 
@@ -1114,6 +1128,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("protected definition is not allowed", N);
       Analyze_Declarations (Visible_Declarations (N));
 
@@ -1167,6 +1182,7 @@ package body Sem_Ch9 is
       end if;
 
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_Restriction (No_Protected_Types, N);
 
       T := Find_Type_Name (N);
@@ -1308,6 +1324,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("requeue statement is not allowed", N);
       Check_Restriction (No_Requeue_Statements, N);
       Check_Unreachable_Code (N);
@@ -1582,6 +1599,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (No_Select_Statements, N);
 
@@ -1702,6 +1720,7 @@ package body Sem_Ch9 is
    begin
       Generate_Definition (Id);
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
 
       --  The node is rewritten as a protected type declaration, in exact
       --  analogy with what is done with single tasks.
@@ -1763,6 +1782,7 @@ package body Sem_Ch9 is
    begin
       Generate_Definition (Id);
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
 
       --  The node is rewritten as a task type declaration, followed by an
       --  object declaration of that anonymous task type.
@@ -1840,6 +1860,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Set_Ekind (Body_Id, E_Task_Body);
       Set_Scope (Body_Id, Current_Scope);
       Spec_Id := Find_Concurrent_Spec (Body_Id);
@@ -1960,6 +1981,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("task definition is not allowed", N);
 
       if Present (Visible_Declarations (N)) then
@@ -1994,6 +2016,7 @@ package body Sem_Ch9 is
    begin
       Check_Restriction (No_Tasking, N);
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       T := Find_Type_Name (N);
       Generate_Definition (T);
 
@@ -2099,6 +2122,7 @@ package body Sem_Ch9 is
    procedure Analyze_Terminate_Alternative (N : Node_Id) is
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
 
       if Present (Pragmas_Before (N)) then
          Analyze_List (Pragmas_Before (N));
@@ -2120,6 +2144,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
       Check_SPARK_Restriction ("select statement is not allowed", N);
       Check_Restriction (No_Select_Statements, N);
 
@@ -2156,6 +2181,7 @@ package body Sem_Ch9 is
 
    begin
       Tasking_Used := True;
+      Current_Subprogram_Body_Is_Not_In_ALFA;
 
       if Present (Pragmas_Before (N)) then
          Analyze_List (Pragmas_Before (N));
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 1f0cc13f5f6..6ff32af98cc 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -5964,13 +5964,19 @@ package body Sem_Res is
       --  types or array types except String.
 
       if Is_Boolean_Type (T) then
+         Current_Subprogram_Body_Is_Not_In_ALFA;
          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_SPARK_Restriction
-           ("comparison is not defined on array types other than String", N);
+
+      elsif Is_Array_Type (T) then
+         Current_Subprogram_Body_Is_Not_In_ALFA;
+
+         if Base_Type (T) /= Standard_String then
+            Check_SPARK_Restriction
+              ("comparison is not defined on array types other than String",
+               N);
+         end if;
+
       else
          null;
       end if;
@@ -6821,15 +6827,18 @@ package body Sem_Res is
          --  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
-           and then Base_Type (Etype (L)) = Base_Type (Etype (R))
-           and then Etype (L) /= Any_Composite  --  or else L in error
-           and then Etype (R) /= Any_Composite  --  or else R in error
-           and then not Matching_Static_Array_Bounds (Etype (L), Etype (R))
-         then
-            Check_SPARK_Restriction
-              ("array types should have matching static bounds", N);
+         if Is_Array_Type (T) then
+            Current_Subprogram_Body_Is_Not_In_ALFA;
+
+            if Base_Type (T) /= Standard_String
+              and then Base_Type (Etype (L)) = Base_Type (Etype (R))
+              and then Etype (L) /= Any_Composite  --  or else L in error
+              and then Etype (R) /= Any_Composite  --  or else R in error
+              and then not Matching_Static_Array_Bounds (Etype (L), Etype (R))
+            then
+               Check_SPARK_Restriction
+                 ("array types should have matching static bounds", N);
+            end if;
          end if;
 
          --  If the unique type is a class-wide type then it will be expanded
@@ -7365,6 +7374,8 @@ package body Sem_Res is
       if Is_Array_Type (B_Typ)
         and then Nkind (N) in N_Binary_Op
       then
+         Current_Subprogram_Body_Is_Not_In_ALFA;
+
          declare
             Left_Typ  : constant Node_Id := Etype (Left_Opnd (N));
             Right_Typ : constant Node_Id := Etype (Right_Opnd (N));
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index b69badad644..a0a0e28397b 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -2311,6 +2311,21 @@ package body Sem_Util is
       end if;
    end Current_Subprogram;
 
+   --------------------------------------------
+   -- Current_Subprogram_Body_Is_Not_In_ALFA --
+   --------------------------------------------
+
+   procedure Current_Subprogram_Body_Is_Not_In_ALFA is
+      Cur_Subp : constant Entity_Id := Current_Subprogram;
+   begin
+      if Present (Cur_Subp)
+        and then (Is_Subprogram (Cur_Subp)
+                   or else Is_Generic_Subprogram (Cur_Subp))
+      then
+         Set_Body_Is_In_ALFA (Cur_Subp, False);
+      end if;
+   end Current_Subprogram_Body_Is_Not_In_ALFA;
+
    ---------------------
    -- Defining_Entity --
    ---------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 163e6470431..9fcd6c1dcff 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -277,6 +277,10 @@ package Sem_Util is
    --  Current_Scope is returned. The returned value is Empty if this is called
    --  from a library package which is not within any subprogram.
 
+   procedure Current_Subprogram_Body_Is_Not_In_ALFA;
+   --  If Current_Subprogram is not Empty, set its flag Body_Is_In_ALFA to
+   --  False, otherwise do nothing.
+
    function Defining_Entity (N : Node_Id) return Entity_Id;
    --  Given a declaration N, returns the associated defining entity. If the
    --  declaration has a specification, the entity is obtained from the