From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-wm1-x335.google.com (mail-wm1-x335.google.com [IPv6:2a00:1450:4864:20::335]) by sourceware.org (Postfix) with ESMTPS id 8ABC63857B81 for ; Wed, 6 Jul 2022 13:31:30 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 8ABC63857B81 Received: by mail-wm1-x335.google.com with SMTP id v67-20020a1cac46000000b003a1888b9d36so9180993wme.0 for ; Wed, 06 Jul 2022 06:31:30 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=b96QqF2XPMtkCVIcTQC+92E+hd6pUizMtji9n4gKM2E=; b=KLdr4qW7kkIMCbGsRePrUBtKknDXZTO/sgqMnrMfvPMj0qhE1Fxi9aPbiOEjnOBaK6 0HKiN4AnZ6GvKxdBJMISo+eEc+l4WJvREW8dadacJJg3xUMSKechLGAjfTdwByn3iSgy OniyMt2E4OYwCMEK/ogET0P9DKOAa4sr9/sG2P0Wk4ly1PFE8hll0oXTo7f3FjNyftcb xDOGGOGuNDhiRgThWU8n0aDxzkLY+dBXaYXJDuf77ZefCJSIOyhEBdBttlx6w6Uuk2Ht lt7EcOEahZ4YWrVxrQqVgYSXd6N/HyyYKPwCi6d6OBS7KBVXynVMOYCML4us1zeQs4y4 vYCg== X-Gm-Message-State: AJIora+fAIn5QOnqE14FMBDn3cOg6WL67khC1Foe7ZptANfYz1SBbUD8 FNNWq5JUln55QJukHRGA3zzEe621Tl+O5Q== X-Google-Smtp-Source: AGRyM1ts4JwDwDdJAJsD8nyLLi7eJqAaaClFb17gbP924n4qDVGADpYmxmPxy6FZMEtAnJbnjPA3ow== X-Received: by 2002:a05:600c:4f55:b0:3a1:f1c5:2107 with SMTP id m21-20020a05600c4f5500b003a1f1c52107mr16898757wmq.114.1657114289248; Wed, 06 Jul 2022 06:31:29 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id p2-20020a056000018200b002103cfd2fbasm35951252wrx.65.2022.07.06.06.31.28 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 06 Jul 2022 06:31:28 -0700 (PDT) Date: Wed, 6 Jul 2022 13:31:28 +0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Support ghost generic formal parameters Message-ID: <20220706133128.GA2205007@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="mYCpIKhGyMATD0i+" Content-Disposition: inline X-Spam-Status: No, score=-12.9 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 06 Jul 2022 13:31:34 -0000 --mYCpIKhGyMATD0i+ Content-Type: text/plain; charset=us-ascii Content-Disposition: inline This adds support in GNAT for ghost generic formal parameters, as included in SPARK RM 6.9. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * ghost.adb (Check_Ghost_Context): Delay checking for generic associations. (Check_Ghost_Context_In_Generic_Association): Perform ghost checking in analyzed generic associations. (Check_Ghost_Formal_Procedure_Or_Package): Check SPARK RM 6.9(13-14) for formal procedures and packages. (Check_Ghost_Formal_Variable): Check SPARK RM 6.9(13-14) for variables. * ghost.ads: Declarations for the above. * sem_ch12.adb (Analyze_Associations): Apply delayed checking for generic associations. (Analyze_Formal_Object_Declaration): Same. (Analyze_Formal_Subprogram_Declaration): Same. (Instantiate_Formal_Package): Same. (Instantiate_Formal_Subprogram): Same. (Instantiate_Object): Same. Copy ghost aspect to newly declared object for actual for IN formal object. Use new function Get_Enclosing_Deep_Object to retrieve root object. (Instantiate_Type): Copy ghost aspect to declared subtype for actual for formal type. * sem_prag.adb (Analyze_Pragma): Recognize new allowed declarations. * sem_util.adb (Copy_Ghost_Aspect): Copy the ghost aspect between nodes. (Get_Enclosing_Deep_Object): New function to return enclosing deep object (or root for reachable part). * sem_util.ads (Copy_Ghost_Aspect): Same. (Get_Enclosing_Deep_Object): Same. * libgnat/s-imageu.ads: Declare formal subprograms as ghost. * libgnat/s-valuei.ads: Same. * libgnat/s-valuti.ads: Same. --mYCpIKhGyMATD0i+ Content-Type: text/x-diff; charset=us-ascii Content-Disposition: attachment; filename="patch.diff" diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -472,6 +472,13 @@ package body Ghost is if Is_Ignored_Ghost_Node (Par) then return True; + -- It is not possible to check correct use of Ghost entities + -- in generic instantiations until after the generic has been + -- resolved. Postpone that verification to after resolution. + + elsif Nkind (Par) = N_Generic_Association then + return True; + -- A reference to a Ghost entity can appear within an aspect -- specification (SPARK RM 6.9(10)). The precise checking will -- occur when analyzing the corresponding pragma. We make an @@ -521,19 +528,6 @@ package body Ghost is then return True; - -- In the context of an instantiation, accept currently Ghost - -- arguments for formal subprograms, as SPARK does not provide - -- a way to distinguish Ghost formal parameters from non-Ghost - -- ones. Illegal use of such arguments in a non-Ghost context - -- will lead to errors inside the instantiation. - - elsif Nkind (Parent (Par)) = N_Generic_Association - and then (Nkind (Par) in N_Has_Entity - and then Present (Entity (Par)) - and then Is_Subprogram (Entity (Par))) - then - return True; - elsif Is_OK_Declaration (Par) then return True; @@ -680,6 +674,128 @@ package body Ghost is end if; end Check_Ghost_Context; + ------------------------------------------------ + -- Check_Ghost_Context_In_Generic_Association -- + ------------------------------------------------ + + procedure Check_Ghost_Context_In_Generic_Association + (Actual : Node_Id; + Formal : Entity_Id) + is + function Emit_Error_On_Ghost_Reference + (N : Node_Id) + return Traverse_Result; + -- Determine wether N denotes a reference to a ghost entity, and if so + -- issue an error. + + ----------------------------------- + -- Emit_Error_On_Ghost_Reference -- + ----------------------------------- + + function Emit_Error_On_Ghost_Reference + (N : Node_Id) + return Traverse_Result + is + begin + if Is_Entity_Name (N) + and then Present (Entity (N)) + and then Is_Ghost_Entity (Entity (N)) + then + Error_Msg_N ("ghost entity cannot appear in this context", N); + Error_Msg_Sloc := Sloc (Formal); + Error_Msg_NE ("\formal & was not declared as ghost #", N, Formal); + return Abandon; + end if; + + return OK; + end Emit_Error_On_Ghost_Reference; + + procedure Check_Ghost_References is + new Traverse_Proc (Emit_Error_On_Ghost_Reference); + + -- Start of processing for Check_Ghost_Context_In_Generic_Association + + begin + -- The context is ghost when it appears within a Ghost package or + -- subprogram. + + if Ghost_Mode > None then + return; + + -- The context is ghost if Formal is explicitly marked as ghost + + elsif Is_Ghost_Entity (Formal) then + return; + + else + Check_Ghost_References (Actual); + end if; + end Check_Ghost_Context_In_Generic_Association; + + --------------------------------------------- + -- Check_Ghost_Formal_Procedure_Or_Package -- + --------------------------------------------- + + procedure Check_Ghost_Formal_Procedure_Or_Package + (N : Node_Id; + Actual : Entity_Id; + Formal : Entity_Id; + Is_Default : Boolean := False) + is + begin + if not Is_Ghost_Entity (Formal) then + return; + end if; + + if Present (Actual) and then Is_Ghost_Entity (Actual) then + return; + end if; + + if Is_Default then + Error_Msg_N ("ghost procedure expected as default", N); + Error_Msg_NE ("\formal & is declared as ghost", N, Formal); + + else + if Ekind (Formal) = E_Procedure then + Error_Msg_N ("ghost procedure expected for actual", N); + else + Error_Msg_N ("ghost package expected for actual", N); + end if; + + Error_Msg_Sloc := Sloc (Formal); + Error_Msg_NE ("\formal & was declared as ghost #", N, Formal); + end if; + end Check_Ghost_Formal_Procedure_Or_Package; + + --------------------------------- + -- Check_Ghost_Formal_Variable -- + --------------------------------- + + procedure Check_Ghost_Formal_Variable + (Actual : Node_Id; + Formal : Entity_Id; + Is_Default : Boolean := False) + is + Actual_Obj : constant Entity_Id := Get_Enclosing_Deep_Object (Actual); + begin + if not Is_Ghost_Entity (Formal) then + return; + end if; + + if No (Actual_Obj) + or else not Is_Ghost_Entity (Actual_Obj) + then + if Is_Default then + Error_Msg_N ("ghost object expected as default", Actual); + Error_Msg_NE ("\formal & is declared as ghost", Actual, Formal); + else + Error_Msg_N ("ghost object expected for mutable actual", Actual); + Error_Msg_Sloc := Sloc (Formal); + Error_Msg_NE ("\formal & was declared as ghost #", Actual, Formal); + end if; + end if; + end Check_Ghost_Formal_Variable; + ---------------------------- -- Check_Ghost_Overriding -- ---------------------------- diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads --- a/gcc/ada/ghost.ads +++ b/gcc/ada/ghost.ads @@ -44,6 +44,33 @@ package Ghost is -- Determine whether node Ghost_Ref appears within a Ghost-friendly context -- where Ghost entity Ghost_Id can safely reside. + procedure Check_Ghost_Context_In_Generic_Association + (Actual : Node_Id; + Formal : Entity_Id); + -- Check that if Actual contains references to ghost entities, generic + -- formal parameter Formal is ghost (SPARK RM 6.9(10)). + + procedure Check_Ghost_Formal_Procedure_Or_Package + (N : Node_Id; + Actual : Entity_Id; + Formal : Entity_Id; + Is_Default : Boolean := False); + -- Verify that if generic formal procedure (resp. package) Formal is ghost, + -- then Actual is not Empty and also a ghost procedure (resp. package) + -- (SPARK RM 6.9(13-14)). The error if any is located on N. If + -- Is_Default is False, N and Actual represent the actual parameter in an + -- instantiation. Otherwise, they represent the default subprogram of a + -- formal subprogram declaration. + + procedure Check_Ghost_Formal_Variable + (Actual : Node_Id; + Formal : Entity_Id; + Is_Default : Boolean := False); + -- Verify that if Formal (either an IN OUT generic formal parameter, or an + -- IN generic formal parameter of access-to-variable type) is ghost, then + -- Actual is a ghost object (SPARK RM 6.9(13-14)). Is_Default is True when + -- Actual is the default expression of the formal object declaration. + procedure Check_Ghost_Overriding (Subp : Entity_Id; Overridden_Subp : Entity_Id); diff --git a/gcc/ada/libgnat/s-imageu.ads b/gcc/ada/libgnat/s-imageu.ads --- a/gcc/ada/libgnat/s-imageu.ads +++ b/gcc/ada/libgnat/s-imageu.ads @@ -54,27 +54,34 @@ generic Unsigned_Width_Ghost : Natural; - with function Wrap_Option (Value : Uns) return Uns_Option; + with function Wrap_Option (Value : Uns) return Uns_Option + with Ghost; with function Only_Decimal_Ghost (Str : String; From, To : Integer) - return Boolean; - with function Hexa_To_Unsigned_Ghost (X : Character) return Uns; + return Boolean + with Ghost; + with function Hexa_To_Unsigned_Ghost (X : Character) return Uns + with Ghost; with function Scan_Based_Number_Ghost (Str : String; From, To : Integer; Base : Uns := 10; - Acc : Uns := 0) return Uns_Option; - with function Is_Unsigned_Ghost (Str : String) return Boolean; + Acc : Uns := 0) return Uns_Option + with Ghost; + with function Is_Unsigned_Ghost (Str : String) return Boolean + with Ghost; with function Value_Unsigned (Str : String) return Uns; with procedure Prove_Iter_Scan_Based_Number_Ghost (Str1, Str2 : String; From, To : Integer; Base : Uns := 10; - Acc : Uns := 0); + Acc : Uns := 0) + with Ghost; with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; - Val : Uns); + Val : Uns) + with Ghost; package System.Image_U is diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads --- a/gcc/ada/libgnat/s-valuei.ads +++ b/gcc/ada/libgnat/s-valuei.ads @@ -55,30 +55,37 @@ generic -- Additional parameters for ghost subprograms used inside contracts type Uns_Option is private; - with function Wrap_Option (Value : Uns) return Uns_Option; - with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean; + with function Wrap_Option (Value : Uns) return Uns_Option + with Ghost; + with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean + with Ghost; with function Raw_Unsigned_Overflows_Ghost (Str : String; From, To : Integer) - return Boolean; + return Boolean + with Ghost; with function Scan_Raw_Unsigned_Ghost (Str : String; From, To : Integer) - return Uns; + return Uns + with Ghost; with function Raw_Unsigned_Last_Ghost (Str : String; From, To : Integer) - return Positive; + return Positive + with Ghost; with function Only_Decimal_Ghost (Str : String; From, To : Integer) - return Boolean; + return Boolean + with Ghost; with function Scan_Based_Number_Ghost (Str : String; From, To : Integer; Base : Uns := 10; Acc : Uns := 0) - return Uns_Option; + return Uns_Option + with Ghost; package System.Value_I is pragma Preelaborate; diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads --- a/gcc/ada/libgnat/s-valuti.ads +++ b/gcc/ada/libgnat/s-valuti.ads @@ -384,27 +384,36 @@ is Unsigned_Width_Ghost : Natural; - with function Wrap_Option (Value : Uns) return Uns_Option; + with function Wrap_Option (Value : Uns) return Uns_Option + with Ghost; with function Only_Decimal_Ghost (Str : String; From, To : Integer) - return Boolean; - with function Hexa_To_Unsigned_Ghost (X : Character) return Uns; + return Boolean + with Ghost; + with function Hexa_To_Unsigned_Ghost (X : Character) return Uns + with Ghost; with function Scan_Based_Number_Ghost (Str : String; From, To : Integer; Base : Uns := 10; Acc : Uns := 0) - return Uns_Option; - with function Is_Integer_Ghost (Str : String) return Boolean; + return Uns_Option + with Ghost; + with function Is_Integer_Ghost (Str : String) return Boolean + with Ghost; with procedure Prove_Iter_Scan_Based_Number_Ghost (Str1, Str2 : String; From, To : Integer; Base : Uns := 10; - Acc : Uns := 0); - with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int); - with function Abs_Uns_Of_Int (Val : Int) return Uns; - with function Value_Integer (Str : String) return Int; + Acc : Uns := 0) + with Ghost; + with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) + with Ghost; + with function Abs_Uns_Of_Int (Val : Int) return Uns + with Ghost; + with function Value_Integer (Str : String) return Int + with Ghost; package Int_Params is end Int_Params; diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -2204,6 +2204,19 @@ package body Sem_Ch12 is raise Program_Error; end case; + -- Check here the correct use of Ghost entities in generic + -- instantiations, as now the generic has been resolved and + -- we know which formal generic parameters are ghost (SPARK + -- RM 6.9(10)). + + if Nkind (Formal) not in N_Use_Package_Clause + | N_Use_Type_Clause + then + Check_Ghost_Context_In_Generic_Association + (Actual => Match, + Formal => Defining_Entity (Analyzed_Formal)); + end if; + Formal := Saved_Formal; Next_Non_Pragma (Analyzed_Formal); end loop; @@ -2715,6 +2728,17 @@ package body Sem_Ch12 is if Present (E) then Preanalyze_Spec_Expression (E, T); + -- The default for a ghost generic formal IN parameter of + -- access-to-variable type should be a ghost object (SPARK + -- RM 6.9(13)). + + if Is_Access_Variable (T) then + Check_Ghost_Formal_Variable + (Actual => E, + Formal => Id, + Is_Default => True); + end if; + if Is_Limited_Type (T) and then not OK_For_Limited_Init (T, E) then Error_Msg_N ("initialization not allowed for limited types", E); @@ -3398,6 +3422,25 @@ package body Sem_Ch12 is goto Leave; end if; + -- The default for a ghost generic formal procedure should be a ghost + -- procedure (SPARK RM 6.9(13)). + + if Ekind (Nam) = E_Procedure then + declare + Def_E : Entity_Id := Empty; + begin + if Nkind (Def) in N_Has_Entity then + Def_E := Entity (Def); + end if; + + Check_Ghost_Formal_Procedure_Or_Package + (N => Def, + Actual => Def_E, + Formal => Nam, + Is_Default => True); + end; + end if; + -- Default name may be overloaded, in which case the interpretation -- with the correct profile must be selected, as for a renaming. -- If the definition is an indexed component, it must denote a @@ -10594,6 +10637,14 @@ package body Sem_Ch12 is Gen_Parent := Generic_Parent (Specification (Analyzed_Formal)); Formal_Pack := Defining_Unit_Name (Specification (Analyzed_Formal)); + -- The actual for a ghost generic formal package should be a ghost + -- package (SPARK RM 6.9(14)). + + Check_Ghost_Formal_Procedure_Or_Package + (N => Actual, + Actual => Actual_Pack, + Formal => Formal_Pack); + if Nkind (Parent (Actual_Pack)) = N_Defining_Program_Unit_Name then Parent_Spec := Package_Specification (Actual_Pack); else @@ -10881,6 +10932,18 @@ package body Sem_Ch12 is Act_E := Empty; end if; + -- The actual for a ghost generic formal procedure should be a ghost + -- procedure (SPARK RM 6.9(14)). + + if Present (Act_E) + and then Ekind (Act_E) = E_Procedure + then + Check_Ghost_Formal_Procedure_Or_Package + (N => Act, + Actual => Act_E, + Formal => Analyzed_S); + end if; + if (Present (Act_E) and then Is_Overloadable (Act_E)) or else Nkind (Act) in N_Attribute_Reference | N_Indexed_Component @@ -11400,40 +11463,22 @@ package body Sem_Ch12 is -- volatility refinement aspects. declare - Actual_Obj : Entity_Id; - N : Node_Id := Actual; + Actual_Obj : constant Entity_Id := + Get_Enclosing_Deep_Object (Actual); begin - -- Similar to Sem_Util.Get_Enclosing_Object, but treat - -- pointer dereference like component selection. - loop - if Is_Entity_Name (N) then - Actual_Obj := Entity (N); - exit; - end if; - - case Nkind (N) is - when N_Indexed_Component - | N_Selected_Component - | N_Slice - | N_Explicit_Dereference - => - N := Prefix (N); - - when N_Type_Conversion => - N := Expression (N); - - when others => - Actual_Obj := Etype (N); - exit; - end case; - end loop; - Check_Volatility_Compatibility (Actual_Obj, A_Gen_Obj, "actual object", "its corresponding formal object of mode in out", Srcpos_Bearer => Actual); end; + -- The actual for a ghost generic formal IN OUT parameter should be a + -- ghost object (SPARK RM 6.9(14)). + + Check_Ghost_Formal_Variable + (Actual => Actual, + Formal => A_Gen_Obj); + -- Formal in-parameter else @@ -11459,6 +11504,7 @@ package body Sem_Ch12 is Object_Definition => Def, Expression => Actual); + Copy_Ghost_Aspect (Formal, To => Decl_Node); Set_Corresponding_Generic_Association (Decl_Node, Act_Assoc); -- A generic formal object of a tagged type is defined to be @@ -11470,6 +11516,16 @@ package body Sem_Ch12 is Append (Decl_Node, List); + -- The actual for a ghost generic formal IN parameter of + -- access-to-variable type should be a ghost object (SPARK + -- RM 6.9(14)). + + if Is_Access_Variable (Etype (A_Gen_Obj)) then + Check_Ghost_Formal_Variable + (Actual => Actual, + Formal => A_Gen_Obj); + end if; + -- No need to repeat (pre-)analysis of some expression nodes -- already handled in Preanalyze_Actuals. @@ -11543,6 +11599,7 @@ package body Sem_Ch12 is Expression => New_Copy_Tree (Default_Expression (Formal))); + Copy_Ghost_Aspect (Formal, To => Decl_Node); Set_Corresponding_Generic_Association (Decl_Node, Expression (Decl_Node)); @@ -14199,6 +14256,8 @@ package body Sem_Ch12 is Defining_Identifier => Subt, Subtype_Indication => New_Occurrence_Of (Act_T, Loc)); + Copy_Ghost_Aspect (Formal, To => Decl_Node); + -- Record whether the actual is private at this point, so that -- Check_Generic_Actuals can restore its proper view before the -- semantic analysis of the instance. diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -17002,6 +17002,9 @@ package body Sem_Prag is -- The pragma applies to a legal construct, stop the traversal elsif Nkind (Stmt) in N_Abstract_Subprogram_Declaration + | N_Formal_Object_Declaration + | N_Formal_Subprogram_Declaration + | N_Formal_Type_Declaration | N_Full_Type_Declaration | N_Generic_Subprogram_Declaration | N_Object_Declaration diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -7024,6 +7024,25 @@ package body Sem_Util is return Comps; end Copy_Component_List; + ----------------------- + -- Copy_Ghost_Aspect -- + ----------------------- + + procedure Copy_Ghost_Aspect (From : Node_Id; To : Node_Id) is + pragma Assert (not Has_Aspects (To)); + Asp : Node_Id; + + begin + if Has_Aspects (From) then + Asp := Find_Aspect (Defining_Entity (From), Aspect_Ghost); + + if Present (Asp) then + Set_Aspect_Specifications (To, New_List (New_Copy_Tree (Asp))); + Set_Has_Aspects (To, True); + end if; + end if; + end Copy_Ghost_Aspect; + ------------------------- -- Copy_Parameter_List -- ------------------------- @@ -11004,6 +11023,32 @@ package body Sem_Util is end if; end Get_Enclosing_Object; + ------------------------------- + -- Get_Enclosing_Deep_Object -- + ------------------------------- + + function Get_Enclosing_Deep_Object (N : Node_Id) return Entity_Id is + begin + if Is_Entity_Name (N) then + return Entity (N); + else + case Nkind (N) is + when N_Explicit_Dereference + | N_Indexed_Component + | N_Selected_Component + | N_Slice + => + return Get_Enclosing_Deep_Object (Prefix (N)); + + when N_Type_Conversion => + return Get_Enclosing_Deep_Object (Expression (N)); + + when others => + return Empty; + end case; + end if; + end Get_Enclosing_Deep_Object; + --------------------------- -- Get_Enum_Lit_From_Pos -- --------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -625,6 +625,11 @@ package Sem_Util is -- create a new compatible record type. Loc is the source location assigned -- to the created nodes. + procedure Copy_Ghost_Aspect (From : Node_Id; To : Node_Id); + -- Copy the Ghost aspect if present in the aspect specifications of node + -- From to node To. On entry it is assumed that To does not have aspect + -- specifications. If From has no aspects, the routine has no effect. + function Copy_Parameter_List (Subp_Id : Entity_Id) return List_Id; -- Utility to create a parameter profile for a new subprogram spec, when -- the subprogram has a body that acts as spec. This is done for some cases @@ -1183,6 +1188,12 @@ package Sem_Util is -- If expression N references a part of an object, return this object. -- Otherwise return Empty. Expression N should have been resolved already. + function Get_Enclosing_Deep_Object (N : Node_Id) return Entity_Id; + -- If expression N references a reachable part of an object (as defined in + -- SPARK RM 6.9), return this object. Otherwise return Empty. It is similar + -- to Get_Enclosing_Object, but treats pointer dereference like component + -- selection. Expression N should have been resolved already. + function Get_Generic_Entity (N : Node_Id) return Entity_Id; -- Returns the true generic entity in an instantiation. If the name in the -- instantiation is a renaming, the function returns the renamed generic. --mYCpIKhGyMATD0i+--