-- --
-- B o d y --
-- --
--- Copyright (C) 1992-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- --
------------------------------------------------------------------------------
-with Aspects; use Aspects;
with Atree; use Atree;
with Checks; use Checks;
with Einfo; use Einfo;
T_Name : Node_Id;
begin
- -- Abort statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~abort statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
Tasking_Used := True;
+ Check_SPARK_Restriction ("abort statement is not allowed", N);
+
T_Name := First (Names (N));
while Present (T_Name) loop
Analyze (T_Name);
Task_Nam : Entity_Id;
begin
- -- Accept statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~accept statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
Tasking_Used := True;
+ Check_SPARK_Restriction ("accept statement is not allowed", N);
-- Entry name is initialized to Any_Id. It should get reset to the
-- matching entry entity. An error is signalled if it is not reset.
Trigger : Node_Id;
begin
- -- Select statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~select statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
Tasking_Used := True;
+ Check_SPARK_Restriction ("select statement is not allowed", N);
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
- Error_Msg_F ("|~~select statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
- Check_Restriction (No_Select_Statements, N);
Tasking_Used := True;
+ Check_SPARK_Restriction ("select statement is not allowed", N);
+ Check_Restriction (No_Select_Statements, N);
-- Ada 2005 (AI-345): The trigger may be a dispatching call
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
- Error_Msg_F ("|~~delay statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
- Check_Restriction (No_Relative_Delay, N);
Tasking_Used := True;
+ Check_SPARK_Restriction ("delay statement is not allowed", N);
+ Check_Restriction (No_Relative_Delay, N);
Check_Restriction (No_Delay, N);
Check_Potentially_Blocking_Operation (N);
Analyze_And_Resolve (E, Standard_Duration);
Typ : Entity_Id;
begin
- -- Delay statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~delay statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
Tasking_Used := True;
+ Check_SPARK_Restriction ("delay statement is not allowed", N);
Check_Restriction (No_Delay, N);
Check_Potentially_Blocking_Operation (N);
Analyze (E);
-- for the discriminals and privals and finally a declaration for the
-- entry family index (if applicable).
- if Expander_Active
+ if Full_Expander_Active
and then Is_Protected_Type (P_Type)
then
Install_Private_Data_Declarations
Call : constant Node_Id := Entry_Call_Statement (N);
begin
- -- Entry call is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~entry call is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
Tasking_Used := True;
+ Check_SPARK_Restriction ("entry call is not allowed", N);
if Present (Pragmas_Before (N)) then
Analyze_List (Pragmas_Before (N));
begin
Generate_Definition (Def_Id);
+ Set_Contract (Def_Id, Make_Contract (Sloc (Def_Id)));
Tasking_Used := True;
-- Case of no discrete subtype definition
Bad_Predicated_Subtype_Use
("subtype& has predicate, not allowed in entry family",
D_Sdef, Etype (D_Sdef));
+
+ -- Check entry family static bounds outside allowed limits
+
+ -- Note: originally this check was not performed here, but in that
+ -- case the check happens deep in the expander, and the message is
+ -- posted at the wrong location, and omitted in -gnatc mode.
+ -- If the type of the entry index is a generic formal, no check
+ -- is possible. In an instance, the check is not static and a run-
+ -- time exception will be raised if the bounds are unreasonable.
+
+ declare
+ PEI : constant Entity_Id := RTE (RE_Protected_Entry_Index);
+ LB : constant Uint := Expr_Value (Type_Low_Bound (PEI));
+ UB : constant Uint := Expr_Value (Type_High_Bound (PEI));
+
+ LBR : Node_Id;
+ UBR : Node_Id;
+
+ begin
+
+ -- No bounds checking if the type is generic or if previous error.
+ -- In an instance the check is dynamic.
+
+ if Is_Generic_Type (Etype (D_Sdef))
+ or else In_Instance
+ or else Error_Posted (D_Sdef)
+ then
+ goto Skip_LB;
+
+ elsif Nkind (D_Sdef) = N_Range then
+ LBR := Low_Bound (D_Sdef);
+
+ elsif Is_Entity_Name (D_Sdef)
+ and then Is_Type (Entity (D_Sdef))
+ then
+ LBR := Type_Low_Bound (Entity (D_Sdef));
+
+ else
+ goto Skip_LB;
+ end if;
+
+ if Is_Static_Expression (LBR)
+ and then Expr_Value (LBR) < LB
+ then
+ Error_Msg_Uint_1 := LB;
+ Error_Msg_N ("entry family low bound must be '>'= ^!", D_Sdef);
+ end if;
+
+ <<Skip_LB>>
+ if Is_Generic_Type (Etype (D_Sdef))
+ or else In_Instance
+ or else Error_Posted (D_Sdef)
+ then
+ goto Skip_UB;
+
+ elsif Nkind (D_Sdef) = N_Range then
+ UBR := High_Bound (D_Sdef);
+
+ elsif Is_Entity_Name (D_Sdef)
+ and then Is_Type (Entity (D_Sdef))
+ then
+ UBR := Type_High_Bound (Entity (D_Sdef));
+
+ else
+ goto Skip_UB;
+ end if;
+
+ if Is_Static_Expression (UBR)
+ and then Expr_Value (UBR) > UB
+ then
+ Error_Msg_Uint_1 := UB;
+ Error_Msg_N ("entry family high bound must be '<'= ^!", D_Sdef);
+ end if;
+
+ <<Skip_UB>>
+ null;
+ end;
end if;
-- Decorate Def_Id
end if;
Generate_Reference_To_Formals (Def_Id);
- Analyze_Aspect_Specifications (N, Def_Id, Aspect_Specifications (N));
+
+ if Has_Aspects (N) then
+ Analyze_Aspect_Specifications (N, Def_Id);
+ end if;
end Analyze_Entry_Declaration;
---------------------------------------
begin
Tasking_Used := True;
+ Check_SPARK_Restriction ("protected definition is not allowed", N);
Analyze_Declarations (Visible_Declarations (N));
if Present (Private_Declarations (N))
begin
if No_Run_Time_Mode then
Error_Msg_CRT ("protected type", N);
- goto Leave;
+
+ if Has_Aspects (N) then
+ Analyze_Aspect_Specifications (N, Def_Id);
+ end if;
+
+ return;
end if;
Tasking_Used := True;
Set_Is_Constrained (T, not Has_Discriminants (T));
+ -- If aspects are present, analyze them now. They can make references
+ -- to the discriminants of the type, but not to any components.
+
+ if Has_Aspects (N) then
+ Analyze_Aspect_Specifications (N, Def_Id);
+ end if;
+
Analyze (Protected_Definition (N));
-- In the case where the protected type is declared at a nested level
end if;
-- Create corresponding record now, because some private dependents
- -- may be subtypes of the partial view. Skip if errors are present,
- -- to prevent cascaded messages.
+ -- may be subtypes of the partial view.
+
+ -- Skip if errors are present, to prevent cascaded messages
if Serious_Errors_Detected = 0
- and then Expander_Active
+
+ -- Also skip if expander is not active
+
+ and then Full_Expander_Active
then
Expand_N_Protected_Type_Declaration (N);
Process_Full_View (N, T, Def_Id);
end if;
end if;
-
- <<Leave>>
- Analyze_Aspect_Specifications (N, Def_Id, Aspect_Specifications (N));
end Analyze_Protected_Type_Declaration;
---------------------
Outer_Ent : Entity_Id;
begin
- -- Requeue statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~requeue statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
+ Tasking_Used := True;
+ Check_SPARK_Restriction ("requeue statement is not allowed", N);
Check_Restriction (No_Requeue_Statements, N);
Check_Unreachable_Code (N);
- Tasking_Used := True;
Enclosing := Empty;
for J in reverse 0 .. Scope_Stack.Last loop
Alt_Count : Uint := Uint_0;
begin
- -- Select statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~select statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
- Check_Restriction (No_Select_Statements, N);
Tasking_Used := True;
+ Check_SPARK_Restriction ("select statement is not allowed", N);
+ Check_Restriction (No_Select_Statements, N);
-- Loop to analyze alternatives
Defining_Identifier => O_Name,
Object_Definition => Make_Identifier (Loc, Chars (T)));
- Move_Aspects (N, O_Decl);
Rewrite (N, T_Decl);
Insert_After (N, O_Decl);
Mark_Rewrite_Insertion (O_Decl);
-- disastrous result.
Analyze_Protected_Type_Declaration (N);
- Analyze_Aspect_Specifications (N, Id, Aspect_Specifications (N));
+
+ if Has_Aspects (N) then
+ Analyze_Aspect_Specifications (N, Id);
+ end if;
end Analyze_Single_Protected_Declaration;
-------------------------------------
Defining_Identifier => O_Name,
Object_Definition => Make_Identifier (Loc, Chars (T)));
- Move_Aspects (N, O_Decl);
Rewrite (N, T_Decl);
Insert_After (N, O_Decl);
Mark_Rewrite_Insertion (O_Decl);
-- disastrous result.
Analyze_Task_Type_Declaration (N);
- Analyze_Aspect_Specifications (N, Id, Aspect_Specifications (N));
+
+ if Has_Aspects (N) then
+ Analyze_Aspect_Specifications (N, Id);
+ end if;
end Analyze_Single_Task_Declaration;
-----------------------
begin
Tasking_Used := True;
+ Check_SPARK_Restriction ("task definition is not allowed", N);
if Present (Visible_Declarations (N)) then
Analyze_Declarations (Visible_Declarations (N));
-- In the case of an incomplete type, use the full view, unless it's not
-- present (as can occur for an incomplete view from a limited with).
+ -- Initialize the Corresponding_Record_Type (which overlays the Private
+ -- Dependents field of the incomplete view).
- if Ekind (T) = E_Incomplete_Type and then Present (Full_View (T)) then
- T := Full_View (T);
- Set_Completion_Referenced (T);
+ if Ekind (T) = E_Incomplete_Type then
+ if Present (Full_View (T)) then
+ T := Full_View (T);
+ Set_Completion_Referenced (T);
+
+ else
+ Set_Ekind (T, E_Task_Type);
+ Set_Corresponding_Record_Type (T, Empty);
+ end if;
end if;
Set_Ekind (T, E_Task_Type);
Set_Is_Constrained (T, not Has_Discriminants (T));
+ if Has_Aspects (N) then
+ Analyze_Aspect_Specifications (N, Def_Id);
+ end if;
+
if Present (Task_Definition (N)) then
Analyze_Task_Definition (Task_Definition (N));
end if;
end if;
-- Create corresponding record now, because some private dependents
- -- may be subtypes of the partial view. Skip if errors are present,
- -- to prevent cascaded messages.
+ -- may be subtypes of the partial view.
+
+ -- Skip if errors are present, to prevent cascaded messages
if Serious_Errors_Detected = 0
- and then Expander_Active
+
+ -- Also skip if expander is not active
+
+ and then Full_Expander_Active
then
Expand_N_Task_Type_Declaration (N);
Process_Full_View (N, T, Def_Id);
end if;
end if;
-
- Analyze_Aspect_Specifications (N, Def_Id, Aspect_Specifications (N));
end Analyze_Task_Type_Declaration;
-----------------------------------
Is_Disp_Select : Boolean := False;
begin
- -- Select statement is not allowed in SPARK or ALFA
-
- if Formal_Verification_Mode then
- Error_Msg_F ("|~~select statement is not allowed", N);
- end if;
-
- -- Proceed with analysis
-
- Check_Restriction (No_Select_Statements, N);
Tasking_Used := True;
+ Check_SPARK_Restriction ("select statement is not allowed", N);
+ Check_Restriction (No_Select_Statements, N);
-- Ada 2005 (AI-345): The trigger may be a dispatching call
-- declaration must be limited.
if Present (Interface_List (N))
- and then not Is_Limited_Record (Priv_T)
+ and then not Is_Limited_Type (Priv_T)
then
Error_Msg_Sloc := Sloc (Priv_T);
Error_Msg_N ("(Ada 2005) limited type declaration expected for " &
OSDN Git Service
