* 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.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@177047
138bc75d-0d04-0410-961f-
82ee72b054a4
+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
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;
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;
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;
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;
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;
-- 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
-- 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
-- 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
-- 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)
-- 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)
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
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),
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
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)
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
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;
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),
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
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);
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;
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);
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.
-- --
-- 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- --
(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;
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
-- 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;
then
Formal_Error_Msg_N
("exit label must name the closest enclosing loop", N);
+ return;
else
Set_Has_Exit (U_Name);
end if;
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.
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);
-- 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
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",
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
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
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
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);
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;
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);
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);
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
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;
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;
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;
projects / platform / upstream / linaro-gcc.git / commitdiff