[multiple changes]

2011-08-01  Javier Miranda  <miranda@adacore.com>

	* sem_ch7.adb (Uninstall_Declarations): Remove useless code.
	* einfo.ads (Access_Disp_Table): Fix documentation.
	(Dispatch_Table_Wrappers): Fix documentation.
	* einfo.adb (Access_Disp_Table, Dispatch_Table_Wrappers,
	Set_Access_Disp_Table, Set_Dispatch_Table_Wrappers): Fix the assertions
	to enforce the documentation of this attribute.
	(Set_Is_Interface): Cleanup the assertion.
	* exp_ch4.adb (Expand_Allocator_Expression, Tagged_Membership): Locate
	the Underlying_Type entity before reading attribute Access_Disp_Table.
	* exp_disp.adb (Expand_Dispatching_Call, Expand_Interface_Conversion):
	Locate the Underlying_Type before reading attribute Access_Disp_Table.
	* exp_aggr.adb (Build_Array_Aggr_Code, Build_Record_Aggr_Code): Locate
	the Underlying_Type entity before reading attribute Access_Disp_Table.
	* exp_ch3.adb (Build_Record_Init_Proc, Expand_N_Object_Declaration):
	Locate the Underlying_Type entity before reading attribute
	Access_Disp_Table.

2011-08-01  Ed Schonberg  <schonberg@adacore.com>

	* s-poosiz.ads: Additional overriding indicators.

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

	* sem_ch5.adb (Analyze_Exit_Statement): add return after error in
	formal mode.
	(Analyze_Iteration_Scheme): issue error in formal mode when loop
	parameter specification does not include a subtype mark.
	* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): issue error in
	formal mode on abstract subprogram.
	(Analyze_Subprogram_Specification): issue error in formal mode on
	user-defined operator.
	(Process_Formals): issue error in formal mode on access parameter and
	default expression.
	* sem_ch9.adb (Analyze_Abort_Statement,
	Analyze_Accept_Statement, Analyze_Asynchronous_Select,
	Analyze_Conditional_Entry_Call, Analyze_Delay_Relative,
	Analyze_Delay_Until, Analyze_Entry_Call_Alternative,
	Analyze_Requeue, Analyze_Selective_Accept,
	Analyze_Timed_Entry_Call): issue error in formal mode on such constructs
	* sem_ch11.adb (Analyze_Raise_Statement, Analyze_Raise_xxx_Error):
	issue error in formal mode on user-defined raise statement.

From-SVN: r177047

13 files changed, 302 insertions, 120 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index bc66804..0c0b22f 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,47 @@
+2011-08-01  Javier Miranda  <miranda@adacore.com>
+
+	* sem_ch7.adb (Uninstall_Declarations): Remove useless code.
+	* einfo.ads (Access_Disp_Table): Fix documentation.
+	(Dispatch_Table_Wrappers): Fix documentation.
+	* einfo.adb (Access_Disp_Table, Dispatch_Table_Wrappers,
+	Set_Access_Disp_Table, Set_Dispatch_Table_Wrappers): Fix the assertions
+	to enforce the documentation of this attribute.
+	(Set_Is_Interface): Cleanup the assertion.
+	* exp_ch4.adb (Expand_Allocator_Expression, Tagged_Membership): Locate
+	the Underlying_Type entity before reading attribute Access_Disp_Table.
+	* exp_disp.adb (Expand_Dispatching_Call, Expand_Interface_Conversion):
+	Locate the Underlying_Type before reading attribute Access_Disp_Table.
+	* exp_aggr.adb (Build_Array_Aggr_Code, Build_Record_Aggr_Code): Locate
+	the Underlying_Type entity before reading attribute Access_Disp_Table.
+	* exp_ch3.adb (Build_Record_Init_Proc, Expand_N_Object_Declaration):
+	Locate the Underlying_Type entity before reading attribute
+	Access_Disp_Table.
+
+2011-08-01  Ed Schonberg  <schonberg@adacore.com>
+
+	* s-poosiz.ads: Additional overriding indicators.
+
+2011-08-01  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch5.adb (Analyze_Exit_Statement): add return after error in
+	formal mode.
+	(Analyze_Iteration_Scheme): issue error in formal mode when loop
+	parameter specification does not include a subtype mark.
+	* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): issue error in
+	formal mode on abstract subprogram.
+	(Analyze_Subprogram_Specification): issue error in formal mode on
+	user-defined operator.
+	(Process_Formals): issue error in formal mode on access parameter and
+	default expression.
+	* sem_ch9.adb (Analyze_Abort_Statement,
+	Analyze_Accept_Statement, Analyze_Asynchronous_Select,
+	Analyze_Conditional_Entry_Call, Analyze_Delay_Relative,
+	Analyze_Delay_Until, Analyze_Entry_Call_Alternative,
+	Analyze_Requeue, Analyze_Selective_Accept,
+	Analyze_Timed_Entry_Call): issue error in formal mode on such constructs
+	* sem_ch11.adb (Analyze_Raise_Statement, Analyze_Raise_xxx_Error):
+	issue error in formal mode on user-defined raise statement.
+
 2011-08-01  Thomas Quinot  <quinot@adacore.com>
 
 	* sem_ch6.adb (Enter_Overloaded_Entity): Do not warn about a
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index a8b5913..8d65e9e 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -573,7 +573,8 @@ package body Einfo is
 
    function Access_Disp_Table (Id : E) return L is
    begin
-      pragma Assert (Is_Tagged_Type (Id));
+      pragma Assert (Ekind_In (Id, E_Record_Type,
+                                   E_Record_Subtype));
       return Elist16 (Implementation_Base_Type (Id));
    end Access_Disp_Table;
 
@@ -882,7 +883,8 @@ package body Einfo is
 
    function Dispatch_Table_Wrappers (Id : E) return L is
    begin
-      pragma Assert (Is_Tagged_Type (Id));
+      pragma Assert (Ekind_In (Id, E_Record_Type,
+                                   E_Record_Subtype));
       return Elist26 (Implementation_Base_Type (Id));
    end Dispatch_Table_Wrappers;
 
@@ -2996,7 +2998,9 @@ package body Einfo is
 
    procedure Set_Access_Disp_Table (Id : E; V : L) is
    begin
-      pragma Assert (Is_Tagged_Type (Id) and then Is_Base_Type (Id));
+      pragma Assert (Ekind (Id) = E_Record_Type
+        and then Id = Implementation_Base_Type (Id));
+      pragma Assert (V = No_Elist or else Is_Tagged_Type (Id));
       Set_Elist16 (Id, V);
    end Set_Access_Disp_Table;
 
@@ -3302,12 +3306,9 @@ package body Einfo is
 
    procedure Set_Dispatch_Table_Wrappers (Id : E; V : L) is
    begin
-      pragma Assert (Is_Tagged_Type (Id)
-        and then Is_Base_Type (Id)
-        and then Ekind_In (Id, E_Record_Type,
-                               E_Record_Subtype,
-                               E_Record_Type_With_Private,
-                               E_Record_Subtype_With_Private));
+      pragma Assert (Ekind (Id) = E_Record_Type
+        and then Id = Implementation_Base_Type (Id));
+      pragma Assert (V = No_Elist or else Is_Tagged_Type (Id));
       Set_Elist26 (Id, V);
    end Set_Dispatch_Table_Wrappers;
 
@@ -4312,13 +4313,7 @@ package body Einfo is
 
    procedure Set_Is_Interface (Id : E; V : B := True) is
    begin
-      pragma Assert
-        (Ekind_In (Id, E_Record_Type,
-                       E_Record_Subtype,
-                       E_Record_Type_With_Private,
-                       E_Record_Subtype_With_Private,
-                       E_Class_Wide_Type,
-                       E_Class_Wide_Subtype));
+      pragma Assert (Is_Record_Type (Id));
       Set_Flag186 (Id, V);
    end Set_Is_Interface;
 
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 1c1de93..a451ddc 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -338,8 +338,8 @@ package Einfo is
 --       statements referencing the same entry.
 
 --    Access_Disp_Table (Elist16) [implementation base type only]
---       Present in record type entities. For a tagged type, points to the
---       dispatch tables associated with the tagged type. The first two
+--       Present in record types and subtypes. Set in tagged types to point to
+--       the dispatch tables associated with the tagged type. The first two
 --       entities correspond with the primary dispatch table: 1) primary
 --       dispatch table with user-defined primitives, 2) primary dispatch table
 --       with predefined primitives. For each interface type covered by the
@@ -349,7 +349,7 @@ package Einfo is
 --       dispatch table with user-defined primitives, and 6) secondary dispatch
 --       table with predefined primitives. The last entity of this list is an
 --       access type declaration used to expand dispatching calls through the
---       primary dispatch table. For a non-tagged record, contains Empty.
+--       primary dispatch table. For a non-tagged record, contains No_Elist.
 
 --    Actual_Subtype (Node17)
 --       Present in variables, constants, and formal parameters. This is the
@@ -855,11 +855,10 @@ package Einfo is
 --       index starting at 1 and ranging up to number of discriminants.
 
 --    Dispatch_Table_Wrappers (Elist26) [implementation base type only]
---       Present in record type [with private] entities. Set in library level
---       record type entities if we are generating statically allocated
---       dispatch tables. For a tagged type, points to the list of dispatch
---       table wrappers associated with the tagged type. For a non-tagged
---       record, contains No_Elist.
+--       Present in record types and subtypes. Set in library level tagged type
+--       entities if we are generating statically allocated dispatch tables.
+--       Points to the list of dispatch table wrappers associated with the
+--       tagged type. For a non-tagged record, contains No_Elist.
 
 --    DTC_Entity (Node16)
 --       Present in function and procedure entities. Set to Empty unless
@@ -5513,7 +5512,6 @@ package Einfo is
    --  E_Record_Type_With_Private
    --  E_Record_Subtype_With_Private
    --    Direct_Primitive_Operations         (Elist10)
-   --    Access_Disp_Table                   (Elist16)  (base type only)
    --    First_Entity                        (Node17)
    --    Private_Dependents                  (Elist18)
    --    Underlying_Full_View                (Node19)
@@ -5522,7 +5520,6 @@ package Einfo is
    --    Private_View                        (Node22)
    --    Stored_Constraint                   (Elist23)
    --    Interfaces                          (Elist25)
-   --    Dispatch_Table_Wrappers             (Elist26)  (base type only)
    --    Has_Completion                      (Flag26)
    --    Has_Record_Rep_Clause               (Flag65)   (base type only)
    --    Has_External_Tag_Rep_Clause         (Flag110)
diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb
index c336a97..871de86 100644
--- a/gcc/ada/exp_aggr.adb
+++ b/gcc/ada/exp_aggr.adb
@@ -1211,22 +1211,27 @@ package body Exp_Aggr is
               and then Is_Tagged_Type (Comp_Type)
               and then Tagged_Type_Expansion
             then
-               A :=
-                 Make_OK_Assignment_Statement (Loc,
-                   Name =>
-                     Make_Selected_Component (Loc,
-                       Prefix =>  New_Copy_Tree (Indexed_Comp),
-                       Selector_Name =>
-                         New_Reference_To
-                           (First_Tag_Component (Comp_Type), Loc)),
-
-                   Expression =>
-                     Unchecked_Convert_To (RTE (RE_Tag),
-                       New_Reference_To
-                         (Node (First_Elmt (Access_Disp_Table (Comp_Type))),
-                          Loc)));
-
-               Append_To (L, A);
+               declare
+                  Full_Typ : constant Entity_Id := Underlying_Type (Comp_Type);
+
+               begin
+                  A :=
+                    Make_OK_Assignment_Statement (Loc,
+                      Name =>
+                        Make_Selected_Component (Loc,
+                          Prefix =>  New_Copy_Tree (Indexed_Comp),
+                          Selector_Name =>
+                            New_Reference_To
+                              (First_Tag_Component (Full_Typ), Loc)),
+
+                      Expression =>
+                        Unchecked_Convert_To (RTE (RE_Tag),
+                          New_Reference_To
+                            (Node (First_Elmt (Access_Disp_Table (Full_Typ))),
+                             Loc)));
+
+                  Append_To (L, A);
+               end;
             end if;
 
             --  Adjust and attach the component to the proper final list, which
@@ -2982,7 +2987,7 @@ package body Exp_Aggr is
                Gen_Ctrl_Actions_For_Aggr;
             end if;
 
-            Comp_Type := Etype (Selector);
+            Comp_Type := Underlying_Type (Etype (Selector));
             Comp_Expr :=
               Make_Selected_Component (Loc,
                 Prefix        => New_Copy_Tree (Target),
diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb
index ecbb9a3..4ee02b7 100644
--- a/gcc/ada/exp_ch3.adb
+++ b/gcc/ada/exp_ch3.adb
@@ -1917,7 +1917,10 @@ package body Exp_Ch3 is
                 Expression =>
                   Unchecked_Convert_To (RTE (RE_Tag),
                     New_Reference_To
-                      (Node (First_Elmt (Access_Disp_Table (Typ))), Loc))));
+                      (Node
+                        (First_Elmt
+                          (Access_Disp_Table (Underlying_Type (Typ)))),
+                       Loc))));
          end if;
 
          --  Adjust the component if controlled except if it is an aggregate
@@ -5055,27 +5058,32 @@ package body Exp_Ch3 is
               and then Tagged_Type_Expansion
               and then Nkind (Expr) /= N_Aggregate
             then
-               --  The re-assignment of the tag has to be done even if the
-               --  object is a constant.
-
-               New_Ref :=
-                 Make_Selected_Component (Loc,
-                    Prefix => New_Reference_To (Def_Id, Loc),
-                    Selector_Name =>
-                      New_Reference_To (First_Tag_Component (Typ), Loc));
+               declare
+                  Full_Typ : constant Entity_Id := Underlying_Type (Typ);
 
-               Set_Assignment_OK (New_Ref);
+               begin
+                  --  The re-assignment of the tag has to be done even if the
+                  --  object is a constant.
 
-               Insert_After (Init_After,
-                 Make_Assignment_Statement (Loc,
-                   Name => New_Ref,
-                   Expression =>
-                     Unchecked_Convert_To (RTE (RE_Tag),
-                       New_Reference_To
-                         (Node
-                           (First_Elmt
-                             (Access_Disp_Table (Base_Type (Typ)))),
-                          Loc))));
+                  New_Ref :=
+                    Make_Selected_Component (Loc,
+                       Prefix => New_Reference_To (Def_Id, Loc),
+                       Selector_Name =>
+                         New_Reference_To (First_Tag_Component (Full_Typ),
+                                           Loc));
+                  Set_Assignment_OK (New_Ref);
+
+                  Insert_After (Init_After,
+                    Make_Assignment_Statement (Loc,
+                      Name => New_Ref,
+                      Expression =>
+                        Unchecked_Convert_To (RTE (RE_Tag),
+                          New_Reference_To
+                            (Node
+                              (First_Elmt
+                                (Access_Disp_Table (Full_Typ))),
+                             Loc))));
+               end;
 
             elsif Is_Tagged_Type (Typ)
               and then Is_CPP_Constructor_Call (Expr)
diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb
index 2213ec5..34e4924 100644
--- a/gcc/ada/exp_ch4.adb
+++ b/gcc/ada/exp_ch4.adb
@@ -874,19 +874,23 @@ package body Exp_Ch4 is
          end if;
 
          if Present (TagT) then
-            Tag_Assign :=
-              Make_Assignment_Statement (Loc,
-                Name =>
-                  Make_Selected_Component (Loc,
-                    Prefix => TagR,
-                    Selector_Name =>
-                      New_Reference_To (First_Tag_Component (TagT), Loc)),
+            declare
+               Full_T : constant Entity_Id := Underlying_Type (TagT);
 
-                Expression =>
-                  Unchecked_Convert_To (RTE (RE_Tag),
-                    New_Reference_To
-                      (Elists.Node (First_Elmt (Access_Disp_Table (TagT))),
-                       Loc)));
+            begin
+               Tag_Assign :=
+                 Make_Assignment_Statement (Loc,
+                   Name =>
+                     Make_Selected_Component (Loc,
+                       Prefix => TagR,
+                       Selector_Name =>
+                         New_Reference_To (First_Tag_Component (Full_T), Loc)),
+                   Expression =>
+                     Unchecked_Convert_To (RTE (RE_Tag),
+                       New_Reference_To
+                         (Elists.Node
+                           (First_Elmt (Access_Disp_Table (Full_T))), Loc)));
+            end;
 
             --  The previous assignment has to be done in any case
 
@@ -10397,6 +10401,7 @@ package body Exp_Ch4 is
       Right : constant Node_Id    := Right_Opnd (N);
       Loc   : constant Source_Ptr := Sloc (N);
 
+      Full_R_Typ : Entity_Id;
       Left_Type  : Entity_Id;
       New_Node   : Node_Id;
       Right_Type : Entity_Id;
@@ -10414,6 +10419,12 @@ package body Exp_Ch4 is
          Left_Type := Root_Type (Left_Type);
       end if;
 
+      if Is_Class_Wide_Type (Right_Type) then
+         Full_R_Typ := Underlying_Type (Root_Type (Right_Type));
+      else
+         Full_R_Typ := Underlying_Type (Right_Type);
+      end if;
+
       Obj_Tag :=
         Make_Selected_Component (Loc,
           Prefix        => Relocate_Node (Left),
@@ -10482,8 +10493,7 @@ package body Exp_Ch4 is
                      Prefix => Obj_Tag,
                      Attribute_Name => Name_Address),
                    New_Reference_To (
-                     Node (First_Elmt
-                            (Access_Disp_Table (Root_Type (Right_Type)))),
+                     Node (First_Elmt (Access_Disp_Table (Full_R_Typ))),
                      Loc)));
 
          --  Ada 95: Normal case
@@ -10493,9 +10503,7 @@ package body Exp_Ch4 is
               Obj_Tag_Node => Obj_Tag,
               Typ_Tag_Node =>
                  New_Reference_To (
-                   Node (First_Elmt
-                          (Access_Disp_Table (Root_Type (Right_Type)))),
-                   Loc),
+                   Node (First_Elmt (Access_Disp_Table (Full_R_Typ))),  Loc),
               Related_Nod => N,
               New_Node    => New_Node);
 
@@ -10526,7 +10534,7 @@ package body Exp_Ch4 is
                 Left_Opnd  => Obj_Tag,
                 Right_Opnd =>
                   New_Reference_To
-                    (Node (First_Elmt (Access_Disp_Table (Right_Type))), Loc));
+                    (Node (First_Elmt (Access_Disp_Table (Full_R_Typ))), Loc));
          end if;
       end if;
    end Tagged_Membership;
diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb
index 9cf300f..f2d5ccd 100644
--- a/gcc/ada/exp_disp.adb
+++ b/gcc/ada/exp_disp.adb
@@ -919,7 +919,7 @@ package body Exp_Disp is
 
       else
          Build_Get_Prim_Op_Address (Loc,
-           Typ      => Find_Dispatching_Type (Subp),
+           Typ      => Underlying_Type (Find_Dispatching_Type (Subp)),
            Tag_Node => Controlling_Tag,
            Position => DT_Position (Subp),
            New_Node => New_Node);
@@ -1107,6 +1107,10 @@ package body Exp_Disp is
          Iface_Typ := Corresponding_Record_Type (Iface_Typ);
       end if;
 
+      --  Handle private types
+
+      Iface_Typ := Underlying_Type (Iface_Typ);
+
       --  Freeze the entity associated with the target interface to have
       --  available the attribute Access_Disp_Table.
 
diff --git a/gcc/ada/s-poosiz.ads b/gcc/ada/s-poosiz.ads
index 974e7b6..e04414c 100644
--- a/gcc/ada/s-poosiz.ads
+++ b/gcc/ada/s-poosiz.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2009 Free Software Foundation, Inc.          --
+--          Copyright (C) 1992-2010, 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- --
@@ -62,21 +62,21 @@ package System.Pool_Size is
                                                        (1 .. Pool_Size);
       end record;
 
-   function Storage_Size
+   overriding function Storage_Size
      (Pool : Stack_Bounded_Pool) return System.Storage_Elements.Storage_Count;
 
-   procedure Allocate
+   overriding procedure Allocate
      (Pool         : in out Stack_Bounded_Pool;
       Address      : out System.Address;
       Storage_Size : System.Storage_Elements.Storage_Count;
       Alignment    : System.Storage_Elements.Storage_Count);
 
-   procedure Deallocate
+   overriding procedure Deallocate
      (Pool         : in out Stack_Bounded_Pool;
       Address      : System.Address;
       Storage_Size : System.Storage_Elements.Storage_Count;
       Alignment    : System.Storage_Elements.Storage_Count);
 
-   procedure Initialize (Pool : in out Stack_Bounded_Pool);
+   overriding procedure Initialize (Pool : in out Stack_Bounded_Pool);
 
 end System.Pool_Size;
diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb
index da7e05e..ce71e7f 100644
--- a/gcc/ada/sem_ch11.adb
+++ b/gcc/ada/sem_ch11.adb
@@ -441,6 +441,14 @@ package body Sem_Ch11 is
       P              : Node_Id;
 
    begin
+      --  Raise statement is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Formal_Error_Msg_N ("raise statement is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       Check_Unreachable_Code (N);
 
       --  Check exception restrictions on the original source
@@ -607,6 +615,16 @@ package body Sem_Ch11 is
    --  Start of processing for Analyze_Raise_xxx_Error
 
    begin
+      --  Source-code raise statement is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode
+        and then Comes_From_Source (N)
+      then
+         Formal_Error_Msg_N ("raise statement is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       if No (Etype (N)) then
          Set_Etype (N, Standard_Void_Type);
       end if;
diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb
index 96c778d..3556590 100644
--- a/gcc/ada/sem_ch5.adb
+++ b/gcc/ada/sem_ch5.adb
@@ -1186,6 +1186,7 @@ package body Sem_Ch5 is
          then
             Formal_Error_Msg_N
               ("exit label must name the closest enclosing loop", N);
+            return;
          else
             Set_Has_Exit (U_Name);
          end if;
@@ -1864,6 +1865,16 @@ package body Sem_Ch5 is
                   end if;
                end;
 
+               --  Loop parameter specification must include subtype mark in
+               --  SPARK or ALFA
+
+               if Formal_Verification_Mode
+                 and then Nkind (DS) = N_Range
+               then
+                  Formal_Error_Msg_N ("loop parameter specification must "
+                                      & "include subtype mark", N);
+               end if;
+
                --  Now analyze the subtype definition. If it is a range, create
                --  temporaries for bounds.
 
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 2633fca..338eae5 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -359,6 +359,14 @@ package body Sem_Ch6 is
       Scop       : constant Entity_Id := Current_Scope;
 
    begin
+      --  Abstract subprogram is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Formal_Error_Msg_N ("abstract subprogram is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       Generate_Definition (Designator);
       Set_Is_Abstract_Subprogram (Designator);
       New_Overloaded_Entity (Designator);
@@ -3034,6 +3042,16 @@ package body Sem_Ch6 is
    --  Start of processing for Analyze_Subprogram_Specification
 
    begin
+      --  User-defined operator is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode
+        and then Nkind (Defining_Unit_Name (N)) = N_Defining_Operator_Symbol
+      then
+         Formal_Error_Msg_N ("user-defined operator is not allowed", N);
+      end if;
+
+      --  Proceed with analysis
+
       Generate_Definition (Designator);
 
       if Nkind (N) = N_Function_Specification then
@@ -8662,7 +8680,24 @@ package body Sem_Ch6 is
          Set_Etype (Formal, Formal_Type);
          Default := Expression (Param_Spec);
 
+         --  Access parameter is not allowed in SPARK or ALFA
+
+         if Formal_Verification_Mode
+           and then Ekind (Formal_Type) = E_Anonymous_Access_Type
+         then
+            Formal_Error_Msg_N ("access parameter is not allowed", Param_Spec);
+         end if;
+
          if Present (Default) then
+            --  Default expression is not allowed in SPARK or ALFA
+
+            if Formal_Verification_Mode then
+               Formal_Error_Msg_N
+                 ("default expression is not allowed", Default);
+            end if;
+
+            --  Proceed with analysis
+
             if Out_Present (Param_Spec) then
                Error_Msg_N
                  ("default initialization only allowed for IN parameters",
diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb
index 82ff0fc..255edbe 100644
--- a/gcc/ada/sem_ch7.adb
+++ b/gcc/ada/sem_ch7.adb
@@ -2069,39 +2069,6 @@ package body Sem_Ch7 is
            and then Is_Tagged_Type (Full)
            and then not Error_Posted (Full)
          then
-            if Priv_Is_Base_Type then
-
-               --  Ada 2005 (AI-345): The full view of a type implementing an
-               --  interface can be a task type.
-
-               --    type T is new I with private;
-               --  private
-               --    task type T is new I with ...
-
-               if Is_Interface (Etype (Priv))
-                 and then Is_Concurrent_Type (Base_Type (Full))
-               then
-                  --  Protect the frontend against previous errors
-
-                  if Present (Corresponding_Record_Type
-                               (Base_Type (Full)))
-                  then
-                     Set_Access_Disp_Table
-                       (Priv, Access_Disp_Table
-                               (Corresponding_Record_Type (Base_Type (Full))));
-
-                  --  Generic context, or previous errors
-
-                  else
-                     null;
-                  end if;
-
-               else
-                  Set_Access_Disp_Table
-                    (Priv, Access_Disp_Table (Base_Type (Full)));
-               end if;
-            end if;
-
             if Is_Tagged_Type (Priv) then
 
                --  If the type is tagged, the tag itself must be available on
diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb
index a88b2d8..e25c92f 100644
--- a/gcc/ada/sem_ch9.adb
+++ b/gcc/ada/sem_ch9.adb
@@ -100,6 +100,15 @@ package body Sem_Ch9 is
       T_Name : Node_Id;
 
    begin
+      --  Abort statement is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Formal_Error_Msg_N ("abort statement is not allowed", N);
+         return;
+      end if;
+
+      --  Proceed with analysis
+
       Tasking_Used := True;
       T_Name := First (Names (N));
       while Present (T_Name) loop
@@ -169,6 +178,15 @@ package body Sem_Ch9 is
       Task_Nam  : Entity_Id;
 
    begin
+      --  Accept statement is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Formal_Error_Msg_N ("accept statement is not allowed", N);
+         return;
+      end if;
+
+      --  Proceed with analysis
+
       Tasking_Used := True;
 
       --  Entry name is initialized to Any_Id. It should get reset to the
@@ -399,6 +417,15 @@ package body Sem_Ch9 is
       Trigger        : Node_Id;
 
    begin
+      --  Select statement is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Formal_Error_Msg_N ("select statement is not allowed", N);
+         return;
+      end if;
+
+      --  Proceed with analysis
+
       Tasking_Used := True;
       Check_Restriction (Max_Asynchronous_Select_Nesting, N);
       Check_Restriction (No_Select_Statements, N);
@@ -444,6 +471,15 @@ package body Sem_Ch9 is
       Is_Disp_Select : Boolean := False;
 
    begin
+      --  Select statement is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Formal_Error_Msg_N ("select statement is not allowed", N);
+         return;
+      end if;
+
+      --  Proceed with analysis
+
       Check_Restriction (No_Select_Statements, N);
       Tasking_Used := True;
 
@@ -540,6 +576,15 @@ package body Sem_Ch9 is
    procedure Analyze_Delay_Relative (N : Node_Id) is
       E : constant Node_Id := Expression (N);
    begin
+      --  Delay statement is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Formal_Error_Msg_N ("delay statement is not allowed", N);
+         return;
+      end if;
+
+      --  Proceed with analysis
+
       Check_Restriction (No_Relative_Delay, N);
       Tasking_Used := True;
       Check_Restriction (No_Delay, N);
@@ -557,6 +602,15 @@ package body Sem_Ch9 is
       Typ : Entity_Id;
 
    begin
+      --  Delay statement is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Formal_Error_Msg_N ("delay statement is not allowed", N);
+         return;
+      end if;
+
+      --  Proceed with analysis
+
       Tasking_Used := True;
       Check_Restriction (No_Delay, N);
       Check_Potentially_Blocking_Operation (N);
@@ -843,6 +897,15 @@ package body Sem_Ch9 is
       Call : constant Node_Id := Entry_Call_Statement (N);
 
    begin
+      --  Entry call is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Formal_Error_Msg_N ("entry call is not allowed", N);
+         return;
+      end if;
+
+      --  Proceed with analysis
+
       Tasking_Used := True;
 
       if Present (Pragmas_Before (N)) then
@@ -1293,6 +1356,15 @@ package body Sem_Ch9 is
       Outer_Ent   : Entity_Id;
 
    begin
+      --  Requeue statement is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Formal_Error_Msg_N ("requeue statement is not allowed", N);
+         return;
+      end if;
+
+      --  Proceed with analysis
+
       Check_Restriction (No_Requeue_Statements, N);
       Check_Unreachable_Code (N);
       Tasking_Used := True;
@@ -1566,6 +1638,15 @@ package body Sem_Ch9 is
       Alt_Count         : Uint    := Uint_0;
 
    begin
+      --  Select statement is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Formal_Error_Msg_N ("select statement is not allowed", N);
+         return;
+      end if;
+
+      --  Proceed with analysis
+
       Check_Restriction (No_Select_Statements, N);
       Tasking_Used := True;
 
@@ -2094,6 +2175,15 @@ package body Sem_Ch9 is
       Is_Disp_Select : Boolean := False;
 
    begin
+      --  Select statement is not allowed in SPARK or ALFA
+
+      if Formal_Verification_Mode then
+         Formal_Error_Msg_N ("select statement is not allowed", N);
+         return;
+      end if;
+
+      --  Proceed with analysis
+
       Check_Restriction (No_Select_Statements, N);
       Tasking_Used := True;