git
/
gcc
mirror of git://gcc.gnu.org/git/gcc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

[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
This commit is contained in:
Arnaud Charlet 2011-08-01 17:17:35 +02:00
parent 1f25038381
commit 38171f43f1
13 changed files with 299 additions and 117 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
gcc/ada/ChangeLog
View File

@ -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

27
gcc/ada/einfo.adb
View File

@ -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;

17
gcc/ada/einfo.ads
View File

@ -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)

35
gcc/ada/exp_aggr.adb
View File

@ -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)),
declare
Full_Typ : constant Entity_Id := Underlying_Type (Comp_Type);
Expression =>
Unchecked_Convert_To (RTE (RE_Tag),
New_Reference_To
(Node (First_Elmt (Access_Disp_Table (Comp_Type))),
Loc)));
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)),
Append_To (L, A);
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),

46
gcc/ada/exp_ch3.adb
View File

@ -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.
declare
Full_Typ : constant Entity_Id := Underlying_Type (Typ);
New_Ref :=
Make_Selected_Component (Loc,
Prefix => New_Reference_To (Def_Id, Loc),
Selector_Name =>
New_Reference_To (First_Tag_Component (Typ), Loc));
begin
-- The re-assignment of the tag has to be done even if the
-- object is a constant.
Set_Assignment_OK (New_Ref);
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 (Base_Type (Typ)))),
Loc))));
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)

44
gcc/ada/exp_ch4.adb
View File

@ -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;

6
gcc/ada/exp_disp.adb
View File

@ -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.

10
gcc/ada/s-poosiz.ads
View File

@ -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;

18
gcc/ada/sem_ch11.adb
View File

@ -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;

11
gcc/ada/sem_ch5.adb
View File

@ -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.

35
gcc/ada/sem_ch6.adb
View File

@ -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",

33
gcc/ada/sem_ch7.adb
View File

@ -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

90
gcc/ada/sem_ch9.adb
View File

@ -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;