From: Arnaud Charlet Date: Mon, 1 Aug 2011 15:17:35 +0000 (+0200) Subject: [multiple changes] X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=38171f43f1339cf9d2f02ded8b41f5c4a3828b42;p=gcc.git [multiple changes] 2011-08-01 Javier Miranda * 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 * s-poosiz.ads: Additional overriding indicators. 2011-08-01 Yannick Moy * 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 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index bc668042bc7..0c0b22f7e1f 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,47 @@ +2011-08-01 Javier Miranda + + * 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 + + * s-poosiz.ads: Additional overriding indicators. + +2011-08-01 Yannick Moy + + * 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 * sem_ch6.adb (Enter_Overloaded_Entity): Do not warn about a diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index a8b5913dd51..8d65e9e7513 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 1c1de932df4..a451ddcd45c 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 c336a97d676..871de86154d 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 ecbb9a3a974..4ee02b78041 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 2213ec5840b..34e49247835 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 9cf300fd96a..f2d5ccd88d5 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 974e7b6ecfc..e04414c16ea 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 da7e05e3242..ce71e7fc91b 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 96c778d3f83..3556590e7a7 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 2633fca0275..338eae56149 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 82ff0fc45a5..255edbe1b94 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 a88b2d8874e..e25c92f4e59 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;