From: Piotr Trojanek Date: Thu, 29 Apr 2021 22:29:33 +0000 (+0200) Subject: [Ada] Reject overlays in Global/Depends/Initializes contracts X-Git-Tag: basepoints/gcc-13~6279 X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=59748b7180590360d3608d30e707a27b0b2cb476;p=thirdparty%2Fgcc.git [Ada] Reject overlays in Global/Depends/Initializes contracts gcc/ada/ * sem_prag.adb (Analyze_Depends_In_Decl_Part): Reject overlays in Depends and Refined_Depends contracts. (Analyze_Global_In_Decl_Part): Likewise for Global and Refined_Global. (Analyze_Initializes_In_Decl_Part): Likewise for Initializes (when appearing both as a single item and as a initialization clause). * sem_util.ads (Ultimate_Overlaid_Entity): New routine. * sem_util.adb (Report_Unused_Body_States): Ignore overlays. (Ultimate_Overlaid_Entity): New routine. --- diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 0efdceff5e72..41e887d8f39f 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -1139,6 +1139,17 @@ package body Sem_Prag is (State_Id => Item_Id, Ref => Item); end if; + + elsif Ekind (Item_Id) in E_Constant | E_Variable + and then Present (Ultimate_Overlaid_Entity (Item_Id)) + then + SPARK_Msg_NE + ("overlaying object & cannot appear in Depends", + Item, Item_Id); + SPARK_Msg_NE + ("\use the overlaid object & instead", + Item, Ultimate_Overlaid_Entity (Item_Id)); + return; end if; -- When the item renames an entire object, replace the @@ -2387,6 +2398,17 @@ package body Sem_Prag is elsif Is_Formal_Object (Item_Id) then null; + elsif Ekind (Item_Id) in E_Constant | E_Variable + and then Present (Ultimate_Overlaid_Entity (Item_Id)) + then + SPARK_Msg_NE + ("overlaying object & cannot appear in Global", + Item, Item_Id); + SPARK_Msg_NE + ("\use the overlaid object & instead", + Item, Ultimate_Overlaid_Entity (Item_Id)); + return; + -- The only legal references are those to abstract states, -- objects and various kinds of constants (SPARK RM 6.1.4(4)). @@ -2984,6 +3006,16 @@ package body Sem_Prag is if Item_Id = Any_Id then null; + elsif Ekind (Item_Id) in E_Constant | E_Variable + and then Present (Ultimate_Overlaid_Entity (Item_Id)) + then + SPARK_Msg_NE + ("overlaying object & cannot appear in Initializes", + Item, Item_Id); + SPARK_Msg_NE + ("\use the overlaid object & instead", + Item, Ultimate_Overlaid_Entity (Item_Id)); + -- The state or variable must be declared in the visible -- declarations of the package (SPARK RM 7.1.5(7)). @@ -3126,6 +3158,18 @@ package body Sem_Prag is end if; end if; + if Ekind (Input_Id) in E_Constant | E_Variable + and then Present (Ultimate_Overlaid_Entity (Input_Id)) + then + SPARK_Msg_NE + ("overlaying object & cannot appear in Initializes", + Input, Input_Id); + SPARK_Msg_NE + ("\use the overlaid object & instead", + Input, Ultimate_Overlaid_Entity (Input_Id)); + return; + end if; + -- Detect a duplicate use of the same input item -- (SPARK RM 7.1.5(5)). diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 7ea809bf5a6a..038c1ee686b3 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -5708,6 +5708,13 @@ package body Sem_Util is if Ekind (State_Id) = E_Constant then null; + -- Overlays do not contribute to package state + + elsif Ekind (State_Id) = E_Variable + and then Present (Ultimate_Overlaid_Entity (State_Id)) + then + null; + -- Generate an error message of the form: -- body of package ... has unused hidden states @@ -29312,6 +29319,39 @@ package body Sem_Util is end if; end Type_Without_Stream_Operation; + ------------------------------ + -- Ultimate_Overlaid_Entity -- + ------------------------------ + + function Ultimate_Overlaid_Entity (E : Entity_Id) return Entity_Id is + Address : Node_Id; + Alias : Entity_Id := E; + Offset : Boolean; + + begin + -- Currently this routine is only called for stand-alone objects that + -- have been analysed, since the analysis of the Address aspect is often + -- delayed. + + pragma Assert (Ekind (E) in E_Constant | E_Variable); + + loop + Address := Address_Clause (Alias); + if Present (Address) then + Find_Overlaid_Entity (Address, Alias, Offset); + if Present (Alias) then + null; + else + return Empty; + end if; + elsif Alias = E then + return Empty; + else + return Alias; + end if; + end loop; + end Ultimate_Overlaid_Entity; + --------------------- -- Ultimate_Prefix -- --------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index a49272e080f2..7cacae2f9079 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -3275,6 +3275,15 @@ package Sem_Util is -- prevents the construction of a composite stream operation. If Op is -- specified we check only for the given stream operation. + function Ultimate_Overlaid_Entity (E : Entity_Id) return Entity_Id; + -- If entity E is overlaying some other entity via an Address clause (which + -- possibly overlays yet another entity via its own Address clause), then + -- return the ultimate overlaid entity. If entity E is not overlaying any + -- other entity (or the overlaid entity cannot be determined statically), + -- then return Empty. + -- + -- Subsidiary to the analysis of object overlays in SPARK. + function Ultimate_Prefix (N : Node_Id) return Node_Id; -- Obtain the "outermost" prefix of arbitrary node N. Return N if no such -- prefix exists.