From: Yannick Moy Date: Tue, 2 Aug 2011 15:15:07 +0000 (+0000) Subject: einfo.adb, einfo.ads (Body_Is_In_ALFA, [...]): get/set for new flag denoting which... X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=975c689678295f3c614f55a84a62c49bdd866a6a;p=gcc.git 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 * 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 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index ece9717f063..8777494989c 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,24 @@ +2011-08-02 Yannick Moy + + * 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 * inline.adb, stand.ads, sem_ch6.adb, sem_ch8.adb: Minor reformatting. diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 062e1fd445d..ff07cfc4d1f 100644 --- a/gcc/ada/einfo.adb +++ b/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)); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index aa5b0e2961d..d666b5f85fb 100644 --- a/gcc/ada/einfo.ads +++ b/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); diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb index c68475bb907..b37a593b8be 100644 --- a/gcc/ada/restrict.adb +++ b/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 diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb index 357b3f1046a..73926faa4bb 100644 --- a/gcc/ada/sem_ch11.adb +++ b/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 diff --git a/gcc/ada/sem_ch2.adb b/gcc/ada/sem_ch2.adb index 3a3bbf9d245..2a021d2d787 100644 --- a/gcc/ada/sem_ch2.adb +++ b/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; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 55d4c3b3583..0f585a8d098 100644 --- a/gcc/ada/sem_ch3.adb +++ b/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 diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index ae169c2b5be..7fd0d9b04df 100644 --- a/gcc/ada/sem_ch4.adb +++ b/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))); diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index bfd41d0619b..d0d34431855 100644 --- a/gcc/ada/sem_ch5.adb +++ b/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 diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 87b6a0c2e88..1c0a3d96393 100644 --- a/gcc/ada/sem_ch6.adb +++ b/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 diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 46d63dc7ab4..474f39c830e 100644 --- a/gcc/ada/sem_ch7.adb +++ b/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 diff --git a/gcc/ada/sem_ch9.adb b/gcc/ada/sem_ch9.adb index 399d36e8771..4392949dcbb 100644 --- a/gcc/ada/sem_ch9.adb +++ b/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)); diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 1f0cc13f5f6..6ff32af98cc 100644 --- a/gcc/ada/sem_res.adb +++ b/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)); diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index b69badad644..a0a0e28397b 100644 --- a/gcc/ada/sem_util.adb +++ b/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 -- --------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 163e6470431..9fcd6c1dcff 100644 --- a/gcc/ada/sem_util.ads +++ b/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