Skip to content

R
riscv-gcc-1
Commit 975c6896 by Yannick Moy Committed by Arnaud Charlet
Options

einfo.adb, einfo.ads (Body_Is_In_ALFA, [...]): get/set for new flag denoting… 

einfo.adb, einfo.ads (Body_Is_In_ALFA, [...]): get/set for new flag denoting which subprogram bodies are in ALFA

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

	* einfo.adb, einfo.ads (Body_Is_In_ALFA, Set_Body_Is_In_ALFA): get/set
	for new flag denoting which subprogram bodies are in ALFA
	* restrict.adb, sem_ch7.adb: Update comment
	* sem_ch11.adb, sem_ch2.adb, sem_ch3.adb, sem_ch4.adb, sem_ch5.adb,
	sem_ch9.adb, sem_res.adb: Add calls to
	Current_Subprogram_Body_Is_Not_In_ALFA on unsupported constructs.
	* sem_ch6.adb (Analyze_Function_Return): add calls to
	Current_Subprogram_Body_Is_Not_In_ALFA on return statement in the
	middle of the body, and extended return.
	(Check_Missing_Return): add calls to Set_Body_Is_In_ALFA with argument
	False when missing return.
	(Analyze_Subprogram_Body_Helper): initialize the flag Body_Is_In_ALFA
	to True for subprograms whose spec is in ALFA. Remove later on the flag
	on the entity used for a subprogram body when there exists a separate
	declaration.
	* sem_util.adb, sem_util.ads (Current_Subprogram_Body_Is_Not_In_ALFA):
	if Current_Subprogram is not Empty, set its flag Body_Is_In_ALFA to
	False, otherwise do nothing.

From-SVN: r177177
parent afc8324d
Showing with 202 additions and 29 deletions
gcc/ada/ChangeLog
2011-08-02 Yannick Moy <moy@adacore.com>
* einfo.adb, einfo.ads (Body_Is_In_ALFA, Set_Body_Is_In_ALFA): get/set
for new flag denoting which subprogram bodies are in ALFA
* restrict.adb, sem_ch7.adb: Update comment
* sem_ch11.adb, sem_ch2.adb, sem_ch3.adb, sem_ch4.adb, sem_ch5.adb,
sem_ch9.adb, sem_res.adb: Add calls to
Current_Subprogram_Body_Is_Not_In_ALFA on unsupported constructs.
* sem_ch6.adb (Analyze_Function_Return): add calls to
Current_Subprogram_Body_Is_Not_In_ALFA on return statement in the
middle of the body, and extended return.
(Check_Missing_Return): add calls to Set_Body_Is_In_ALFA with argument
False when missing return.
(Analyze_Subprogram_Body_Helper): initialize the flag Body_Is_In_ALFA
to True for subprograms whose spec is in ALFA. Remove later on the flag
on the entity used for a subprogram body when there exists a separate
declaration.
* sem_util.adb, sem_util.ads (Current_Subprogram_Body_Is_Not_In_ALFA):
if Current_Subprogram is not Empty, set its flag Body_Is_In_ALFA to
False, otherwise do nothing.
2011-08-02 Robert Dewar <dewar@adacore.com>
* inline.adb, stand.ads, sem_ch6.adb, sem_ch8.adb: Minor reformatting.
......
gcc/ada/einfo.adb
......@@ -518,7 +518,7 @@ package body Einfo is
-- Is_Safe_To_Reevaluate Flag249
-- Has_Predicates Flag250
-- (unused) Flag251
-- Body_Is_In_ALFA Flag251
-- (unused) Flag252
-- (unused) Flag253
-- (unused) Flag254
......@@ -651,6 +651,12 @@ package body Einfo is
return Node19 (Id);
end Body_Entity;
function Body_Is_In_ALFA (Id : E) return B is
begin
pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
return Flag251 (Id);
end Body_Is_In_ALFA;
function Body_Needed_For_SAL (Id : E) return B is
begin
pragma Assert
......@@ -3098,6 +3104,12 @@ package body Einfo is
Set_Node19 (Id, V);
end Set_Body_Entity;
procedure Set_Body_Is_In_ALFA (Id : E; V : B := True) is
begin
pragma Assert (Is_Subprogram (Id) or else Is_Generic_Subprogram (Id));
Set_Flag251 (Id, V);
end Set_Body_Is_In_ALFA;
procedure Set_Body_Needed_For_SAL (Id : E; V : B := True) is
begin
pragma Assert
......@@ -7349,6 +7361,7 @@ package body Einfo is
end if;
W ("Address_Taken", Flag104 (Id));
W ("Body_Is_In_ALFA", Flag251 (Id));
W ("Body_Needed_For_SAL", Flag40 (Id));
W ("C_Pass_By_Copy", Flag125 (Id));
W ("Can_Never_Be_Null", Flag38 (Id));
......
gcc/ada/einfo.ads
......@@ -7,7 +7,7 @@
-- S p e c --
-- --
-- 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- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
......@@ -486,6 +486,11 @@ package Einfo is
-- Present in package and generic package entities, points to the
-- corresponding package body entity if one is present.
-- Body_Is_In_ALFA (Flag251)
-- Present in subprogram entities. Set for subprograms whose body belongs
-- to the ALFA subset, which are eligible for formal verification through
-- SPARK or Why tool-sets.
-- Body_Needed_For_SAL (Flag40)
-- Present in package and subprogram entities that are compilation
-- units. Indicates that the source for the body must be included
......@@ -2273,7 +2278,9 @@ package Einfo is
-- Is_In_ALFA (Flag151)
-- Present in all entities. Set for entities that belong to the ALFA
-- subset, which are eligible for formal verification through SPARK or
-- Why tool-sets.
-- Why tool-sets. For a subprogram, this only means that a call to the
-- subprogram can be formally analyzed. Another flag, Body_Is_In_ALFA,
-- defines which subprograms can be formally analyzed.
-- Is_Inlined (Flag11)
-- Present in all entities. Set for functions and procedures which are
......@@ -4336,7 +4343,7 @@ package Einfo is
-- E_Anonymous_Access_Protected_Subprogram_Type
E_Anonymous_Access_Type;
subtype Access_Subprogram_Kind is Entity_Kind range
subtype Access_Subprogram_Kind is Entity_Kind range
E_Access_Subprogram_Type ..
-- E_Anonymous_Access_Subprogram_Type
-- E_Access_Protected_Subprogram_Type
......@@ -4536,7 +4543,7 @@ package Einfo is
-- E_Floating_Point_Type
E_Floating_Point_Subtype;
subtype Object_Kind is Entity_Kind range
subtype Object_Kind is Entity_Kind range
E_Component ..
-- E_Constant
-- E_Discriminant
......@@ -5933,6 +5940,7 @@ package Einfo is
function Barrier_Function (Id : E) return N;
function Block_Node (Id : E) return N;
function Body_Entity (Id : E) return E;
function Body_Is_In_ALFA (Id : E) return B;
function Body_Needed_For_SAL (Id : E) return B;
function CR_Discriminant (Id : E) return E;
function C_Pass_By_Copy (Id : E) return B;
......@@ -6519,6 +6527,7 @@ package Einfo is
procedure Set_Barrier_Function (Id : E; V : N);
procedure Set_Block_Node (Id : E; V : N);
procedure Set_Body_Entity (Id : E; V : E);
procedure Set_Body_Is_In_ALFA (Id : E; V : B := True);
procedure Set_Body_Needed_For_SAL (Id : E; V : B := True);
procedure Set_CR_Discriminant (Id : E; V : E);
procedure Set_C_Pass_By_Copy (Id : E; V : B := True);
......@@ -7212,6 +7221,7 @@ package Einfo is
pragma Inline (Barrier_Function);
pragma Inline (Block_Node);
pragma Inline (Body_Entity);
pragma Inline (Body_Is_In_ALFA);
pragma Inline (Body_Needed_For_SAL);
pragma Inline (CR_Discriminant);
pragma Inline (C_Pass_By_Copy);
......@@ -7653,6 +7663,7 @@ package Einfo is
pragma Inline (Set_Barrier_Function);
pragma Inline (Set_Block_Node);
pragma Inline (Set_Body_Entity);
pragma Inline (Set_Body_Is_In_ALFA);
pragma Inline (Set_Body_Needed_For_SAL);
pragma Inline (Set_CR_Discriminant);
pragma Inline (Set_C_Pass_By_Copy);
......
gcc/ada/restrict.adb
......@@ -371,7 +371,7 @@ package body Restrict is
return;
end if;
-- In formal mode, issue an error for any use of class-wide, even if the
-- In SPARK mode, issue an error for any use of class-wide, even if the
-- No_Dispatch restriction is not set.
if R = No_Dispatch then
......
gcc/ada/sem_ch11.adb
......@@ -443,6 +443,7 @@ package body Sem_Ch11 is
P : Node_Id;
begin
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("raise statement is not allowed", N);
Check_Unreachable_Code (N);
......@@ -610,6 +611,7 @@ package body Sem_Ch11 is
-- Start of processing for Analyze_Raise_xxx_Error
begin
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("raise statement is not allowed", N);
if No (Etype (N)) then
......
gcc/ada/sem_ch2.adb
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-2007, 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- --
......@@ -24,12 +24,14 @@
------------------------------------------------------------------------------
with Atree; use Atree;
with Einfo; use Einfo;
with Errout; use Errout;
with Namet; use Namet;
with Opt; use Opt;
with Restrict; use Restrict;
with Rident; use Rident;
with Sem_Ch8; use Sem_Ch8;
with Sem_Util; use Sem_Util;
with Sinfo; use Sinfo;
with Stand; use Stand;
with Uintp; use Uintp;
......@@ -74,6 +76,13 @@ package body Sem_Ch2 is
return;
else
Find_Direct_Name (N);
if Present (Entity (N))
and then Is_Object (Entity (N))
and then not Is_In_ALFA (Entity (N))
then
Current_Subprogram_Body_Is_Not_In_ALFA;
end if;
end if;
end Analyze_Identifier;
......
gcc/ada/sem_ch3.adb
......@@ -3030,10 +3030,13 @@ package body Sem_Ch3 is
Act_T := T;
-- The object is in ALFA if-and-only-if its type is in ALFA
-- The object is in ALFA if-and-only-if its type is in ALFA and it is
-- not aliased.
if Is_In_ALFA (T) then
if Is_In_ALFA (T) and then not Aliased_Present (N) then
Set_Is_In_ALFA (Id);
else
Current_Subprogram_Body_Is_Not_In_ALFA;
end if;
-- These checks should be performed before the initialization expression
......
gcc/ada/sem_ch4.adb
......@@ -350,6 +350,8 @@ package body Sem_Ch4 is
procedure Analyze_Aggregate (N : Node_Id) is
begin
Current_Subprogram_Body_Is_Not_In_ALFA;
if No (Etype (N)) then
Set_Etype (N, Any_Composite);
end if;
......@@ -369,6 +371,7 @@ package body Sem_Ch4 is
C : Node_Id;
begin
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("allocator is not allowed", N);
-- Deal with allocator restrictions
......@@ -982,6 +985,15 @@ package body Sem_Ch4 is
return;
end if;
-- If this is an indirect call, or the subprogram called is not in
-- ALFA, then the call is not in ALFA.
if not Is_Subprogram (Nam_Ent)
or else not Is_In_ALFA (Nam_Ent)
then
Current_Subprogram_Body_Is_Not_In_ALFA;
end if;
Analyze_One_Call (N, Nam_Ent, True, Success);
-- If this is an indirect call, the return type of the access_to
......@@ -1358,6 +1370,8 @@ package body Sem_Ch4 is
L : Node_Id;
begin
Current_Subprogram_Body_Is_Not_In_ALFA;
Candidate_Type := Empty;
-- The following code is equivalent to:
......@@ -1506,6 +1520,7 @@ package body Sem_Ch4 is
return;
end if;
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("conditional expression is not allowed", N);
Else_Expr := Next (Then_Expr);
......@@ -1706,6 +1721,7 @@ package body Sem_Ch4 is
-- Start of processing for Analyze_Explicit_Dereference
begin
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("explicit dereference is not allowed", N);
Analyze (P);
......@@ -2467,6 +2483,8 @@ package body Sem_Ch4 is
-- Start of processing for Analyze_Membership_Op
begin
Current_Subprogram_Body_Is_Not_In_ALFA;
Analyze_Expression (L);
if No (R)
......@@ -2588,6 +2606,7 @@ package body Sem_Ch4 is
procedure Analyze_Null (N : Node_Id) is
begin
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("null is not allowed", N);
Set_Etype (N, Any_Access);
......@@ -3216,6 +3235,8 @@ package body Sem_Ch4 is
T : Entity_Id;
begin
Current_Subprogram_Body_Is_Not_In_ALFA;
Analyze_Expression (Expr);
Set_Etype (N, Any_Type);
......@@ -3274,6 +3295,7 @@ package body Sem_Ch4 is
Iterator : Node_Id;
begin
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("quantified expression is not allowed", N);
Set_Etype (Ent, Standard_Void_Type);
......@@ -3439,6 +3461,8 @@ package body Sem_Ch4 is
Acc_Type : Entity_Id;
begin
Current_Subprogram_Body_Is_Not_In_ALFA;
Analyze (P);
-- An interesting error check, if we take the 'Reference of an object
......@@ -4302,6 +4326,7 @@ package body Sem_Ch4 is
-- Start of processing for Analyze_Slice
begin
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("slice is not allowed", N);
Analyze (P);
......@@ -4346,6 +4371,8 @@ package body Sem_Ch4 is
T : Entity_Id;
begin
Current_Subprogram_Body_Is_Not_In_ALFA;
-- If Conversion_OK is set, then the Etype is already set, and the
-- only processing required is to analyze the expression. This is
-- used to construct certain "illegal" conversions which are not
......@@ -4476,6 +4503,7 @@ package body Sem_Ch4 is
procedure Analyze_Unchecked_Type_Conversion (N : Node_Id) is
begin
Current_Subprogram_Body_Is_Not_In_ALFA;
Find_Type (Subtype_Mark (N));
Analyze_Expression (Expression (N));
Set_Etype (N, Entity (Subtype_Mark (N)));
......
gcc/ada/sem_ch5.adb
......@@ -815,7 +815,7 @@ package body Sem_Ch5 is
HSS : constant Node_Id := Handled_Statement_Sequence (N);
begin
-- In formal mode, we reject block statements. Note that the case of
-- In SPARK mode, we reject block statements. Note that the case of
-- block statements generated by the expander is fine.
if Nkind (Original_Node (N)) = N_Block_Statement then
......@@ -1113,6 +1113,7 @@ package body Sem_Ch5 is
if Others_Present
and then List_Length (Alternatives (N)) = 1
then
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction
("OTHERS as unique case alternative is not allowed", N);
end if;
......@@ -1194,6 +1195,7 @@ package body Sem_Ch5 is
else
if Has_Loop_In_Inner_Open_Scopes (U_Name) then
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction
("exit label must name the closest enclosing loop", N);
end if;
......@@ -1235,17 +1237,19 @@ package body Sem_Ch5 is
Check_Unset_Reference (Cond);
end if;
-- In formal mode, verify that the exit statement respects the SPARK
-- In SPARK mode, verify that the exit statement respects the SPARK
-- restrictions.
if Present (Cond) then
if Nkind (Parent (N)) /= N_Loop_Statement then
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction
("exit with when clause must be directly in loop", N);
end if;
else
if Nkind (Parent (N)) /= N_If_Statement then
Current_Subprogram_Body_Is_Not_In_ALFA;
if Nkind (Parent (N)) = N_Elsif_Part then
Check_SPARK_Restriction
("exit must be in IF without ELSIF", N);
......@@ -1254,6 +1258,7 @@ package body Sem_Ch5 is
end if;
elsif Nkind (Parent (Parent (N))) /= N_Loop_Statement then
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction
("exit must be in IF directly in loop", N);
......@@ -1261,12 +1266,14 @@ package body Sem_Ch5 is
-- leads to an error mentioning the ELSE.
elsif Present (Else_Statements (Parent (N))) then
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("exit must be in IF without ELSE", N);
-- An exit in an ELSIF does not reach here, as it would have been
-- detected in the case (Nkind (Parent (N)) /= N_If_Statement).
elsif Present (Elsif_Parts (Parent (N))) then
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("exit must be in IF without ELSIF", N);
end if;
end if;
......@@ -1295,6 +1302,7 @@ package body Sem_Ch5 is
Label_Ent : Entity_Id;
begin
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("goto statement is not allowed", N);
-- Actual semantic checks
......
gcc/ada/sem_ch6.adb
......@@ -638,11 +638,13 @@ package body Sem_Ch6 is
(Nkind (Parent (Parent (N))) /= N_Subprogram_Body
or else Present (Next (N)))
then
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction
("RETURN should be the last statement in function", N);
end if;
else
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("extended RETURN is not allowed", N);
-- Analyze parts specific to extended_return_statement:
......@@ -1909,6 +1911,7 @@ package body Sem_Ch6 is
and then not Nkind_In (Stat, N_Simple_Return_Statement,
N_Extended_Return_Statement)
then
Set_Body_Is_In_ALFA (Id, False);
Check_SPARK_Restriction
("last statement in function should be RETURN", Stat);
end if;
......@@ -1927,6 +1930,7 @@ package body Sem_Ch6 is
-- borrow the Check_Returns procedure here ???
if Return_Present (Id) then
Set_Body_Is_In_ALFA (Id, False);
Check_SPARK_Restriction
("procedure should not have RETURN", N);
end if;
......@@ -2236,6 +2240,24 @@ package body Sem_Ch6 is
end if;
end if;
-- By default, consider that the subprogram body is in ALFA if the spec
-- is in ALFA. This is reversed later if some expression or statement is
-- not in ALFA.
declare
Id : Entity_Id;
begin
if Present (Spec_Id) then
Id := Spec_Id;
else
Id := Body_Id;
end if;
if Is_In_ALFA (Id) then
Set_Body_Is_In_ALFA (Id);
end if;
end;
-- Do not inline any subprogram that contains nested subprograms, since
-- the backend inlining circuit seems to generate uninitialized
-- references in this case. We know this happens in the case of front
......@@ -2467,6 +2489,7 @@ package body Sem_Ch6 is
Set_Ekind (Body_Id, E_Subprogram_Body);
Set_Scope (Body_Id, Scope (Spec_Id));
Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Spec_Id));
Set_Is_In_ALFA (Body_Id, False);
-- Case of subprogram body with no previous spec
......
gcc/ada/sem_ch7.adb
......@@ -6,7 +6,7 @@
-- --
-- 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- --
......@@ -875,9 +875,8 @@ package body Sem_Ch7 is
-- package.
procedure Check_One_Tagged_Type_Or_Extension_At_Most;
-- Issue an error in formal mode if a package specification contains
-- more than one tagged type or type extension. This is a restriction of
-- SPARK.
-- Issue an error in SPARK mode if a package specification contains
-- more than one tagged type or type extension.
procedure Clear_Constants (Id : Entity_Id; FE : Entity_Id);
-- Clears constant indications (Never_Set_In_Source, Constant_Value, and
......
gcc/ada/sem_ch9.adb
......@@ -101,6 +101,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("abort statement is not allowed", N);
T_Name := First (Names (N));
......@@ -139,6 +140,7 @@ package body Sem_Ch9 is
procedure Analyze_Accept_Alternative (N : Node_Id) is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
if Present (Pragmas_Before (N)) then
Analyze_List (Pragmas_Before (N));
......@@ -172,6 +174,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("accept statement is not allowed", N);
-- Entry name is initialized to Any_Id. It should get reset to the
......@@ -403,6 +406,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("select statement is not allowed", N);
Check_Restriction (Max_Asynchronous_Select_Nesting, N);
Check_Restriction (No_Select_Statements, N);
......@@ -449,6 +453,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("select statement is not allowed", N);
Check_Restriction (No_Select_Statements, N);
......@@ -495,6 +500,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_Restriction (No_Delay, N);
if Present (Pragmas_Before (N)) then
......@@ -546,6 +552,7 @@ package body Sem_Ch9 is
E : constant Node_Id := Expression (N);
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("delay statement is not allowed", N);
Check_Restriction (No_Relative_Delay, N);
Check_Restriction (No_Delay, N);
......@@ -564,6 +571,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("delay statement is not allowed", N);
Check_Restriction (No_Delay, N);
Check_Potentially_Blocking_Operation (N);
......@@ -592,6 +600,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
-- 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
......@@ -824,6 +833,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
if Present (Index) then
Analyze (Index);
......@@ -851,6 +861,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("entry call is not allowed", N);
if Present (Pragmas_Before (N)) then
......@@ -886,6 +897,7 @@ package body Sem_Ch9 is
begin
Generate_Definition (Def_Id);
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
-- Case of no discrete subtype definition
......@@ -955,6 +967,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Analyze (Def);
-- There is no elaboration of the entry index specification. Therefore,
......@@ -996,6 +1009,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Set_Ekind (Body_Id, E_Protected_Body);
Spec_Id := Find_Concurrent_Spec (Body_Id);
......@@ -1114,6 +1128,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("protected definition is not allowed", N);
Analyze_Declarations (Visible_Declarations (N));
......@@ -1167,6 +1182,7 @@ package body Sem_Ch9 is
end if;
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_Restriction (No_Protected_Types, N);
T := Find_Type_Name (N);
......@@ -1308,6 +1324,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("requeue statement is not allowed", N);
Check_Restriction (No_Requeue_Statements, N);
Check_Unreachable_Code (N);
......@@ -1582,6 +1599,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("select statement is not allowed", N);
Check_Restriction (No_Select_Statements, N);
......@@ -1702,6 +1720,7 @@ package body Sem_Ch9 is
begin
Generate_Definition (Id);
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
-- The node is rewritten as a protected type declaration, in exact
-- analogy with what is done with single tasks.
......@@ -1763,6 +1782,7 @@ package body Sem_Ch9 is
begin
Generate_Definition (Id);
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
-- The node is rewritten as a task type declaration, followed by an
-- object declaration of that anonymous task type.
......@@ -1840,6 +1860,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Set_Ekind (Body_Id, E_Task_Body);
Set_Scope (Body_Id, Current_Scope);
Spec_Id := Find_Concurrent_Spec (Body_Id);
......@@ -1960,6 +1981,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("task definition is not allowed", N);
if Present (Visible_Declarations (N)) then
......@@ -1994,6 +2016,7 @@ package body Sem_Ch9 is
begin
Check_Restriction (No_Tasking, N);
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
T := Find_Type_Name (N);
Generate_Definition (T);
......@@ -2099,6 +2122,7 @@ package body Sem_Ch9 is
procedure Analyze_Terminate_Alternative (N : Node_Id) is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
if Present (Pragmas_Before (N)) then
Analyze_List (Pragmas_Before (N));
......@@ -2120,6 +2144,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction ("select statement is not allowed", N);
Check_Restriction (No_Select_Statements, N);
......@@ -2156,6 +2181,7 @@ package body Sem_Ch9 is
begin
Tasking_Used := True;
Current_Subprogram_Body_Is_Not_In_ALFA;
if Present (Pragmas_Before (N)) then
Analyze_List (Pragmas_Before (N));
......
gcc/ada/sem_res.adb
......@@ -5964,13 +5964,19 @@ package body Sem_Res is
-- types or array types except String.
if Is_Boolean_Type (T) then
Current_Subprogram_Body_Is_Not_In_ALFA;
Check_SPARK_Restriction
("comparison is not defined on Boolean type", N);
elsif Is_Array_Type (T)
and then Base_Type (T) /= Standard_String
then
Check_SPARK_Restriction
("comparison is not defined on array types other than String", N);
elsif Is_Array_Type (T) then
Current_Subprogram_Body_Is_Not_In_ALFA;
if Base_Type (T) /= Standard_String then
Check_SPARK_Restriction
("comparison is not defined on array types other than String",
N);
end if;
else
null;
end if;
......@@ -6821,15 +6827,18 @@ package body Sem_Res is
-- String are only defined when, for each index position, the
-- operands have equal static bounds.
if Is_Array_Type (T)
and then Base_Type (T) /= Standard_String
and then Base_Type (Etype (L)) = Base_Type (Etype (R))
and then Etype (L) /= Any_Composite -- or else L in error
and then Etype (R) /= Any_Composite -- or else R in error
and then not Matching_Static_Array_Bounds (Etype (L), Etype (R))
then
Check_SPARK_Restriction
("array types should have matching static bounds", N);
if Is_Array_Type (T) then
Current_Subprogram_Body_Is_Not_In_ALFA;
if Base_Type (T) /= Standard_String
and then Base_Type (Etype (L)) = Base_Type (Etype (R))
and then Etype (L) /= Any_Composite -- or else L in error
and then Etype (R) /= Any_Composite -- or else R in error
and then not Matching_Static_Array_Bounds (Etype (L), Etype (R))
then
Check_SPARK_Restriction
("array types should have matching static bounds", N);
end if;
end if;
-- If the unique type is a class-wide type then it will be expanded
......@@ -7365,6 +7374,8 @@ package body Sem_Res is
if Is_Array_Type (B_Typ)
and then Nkind (N) in N_Binary_Op
then
Current_Subprogram_Body_Is_Not_In_ALFA;
declare
Left_Typ : constant Node_Id := Etype (Left_Opnd (N));
Right_Typ : constant Node_Id := Etype (Right_Opnd (N));
......
gcc/ada/sem_util.adb
......@@ -2311,6 +2311,21 @@ package body Sem_Util is
end if;
end Current_Subprogram;
--------------------------------------------
-- Current_Subprogram_Body_Is_Not_In_ALFA --
--------------------------------------------
procedure Current_Subprogram_Body_Is_Not_In_ALFA is
Cur_Subp : constant Entity_Id := Current_Subprogram;
begin
if Present (Cur_Subp)
and then (Is_Subprogram (Cur_Subp)
or else Is_Generic_Subprogram (Cur_Subp))
then
Set_Body_Is_In_ALFA (Cur_Subp, False);
end if;
end Current_Subprogram_Body_Is_Not_In_ALFA;
---------------------
-- Defining_Entity --
---------------------
......
gcc/ada/sem_util.ads
......@@ -277,6 +277,10 @@ package Sem_Util is
-- Current_Scope is returned. The returned value is Empty if this is called
-- from a library package which is not within any subprogram.
procedure Current_Subprogram_Body_Is_Not_In_ALFA;
-- If Current_Subprogram is not Empty, set its flag Body_Is_In_ALFA to
-- False, otherwise do nothing.
function Defining_Entity (N : Node_Id) return Entity_Id;
-- Given a declaration N, returns the associated defining entity. If the
-- declaration has a specification, the entity is obtained from the
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment