From: Arnaud Charlet Date: Wed, 18 Nov 2015 10:08:00 +0000 (+0100) Subject: [multiple changes] X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2f54ef3d56ff1e68036e389bb50a654474fe1a00;p=gcc.git [multiple changes] 2015-11-18 Hristian Kirtchev * einfo.adb (Has_Non_Null_Refinement): Rename to Has_Non_Null_Visible_Refinement. (Has_Null_Refinement): Rename to Has_Null_Visible_Refinement. * einfo.ads Update the documentation of attribute Has_Non_Null_Refinement and attribute Has_Null_Refinement. (Has_Non_Null_Refinement): Rename to Has_Non_Null_Visible_Refinement and update occurrences in entities. (Has_Null_Refinement): Rename to Has_Null_Visible_Refinement and update occurrences in entities. * sem_prag.adb (Check_In_Out_States): Update the calls to Has_[Non_]Null_Refinement. (Check_Input_States): Update the calls to Has_[Non_]Null_Refinement. (Check_Output_States): Update the calls to Has_[Non_]Null_Refinement. (Check_Proof_In_States): Update the calls to Has_[Non_]Null_Refinement. (Collect_Global_Item): Update the calls to Has_[Non_]Null_Refinement. (Is_Null_Refined_State): Update the calls to Has_[Non_]Null_Refinement. (Match_Item): Update the calls to Has_[Non_]Null_Refinement. * sem_util.adb (Has_Non_Null_Refinement): New routine. (Has_Null_Refinement): New routine. * sem_util.ads (Has_Non_Null_Refinement): New routine. (Has_Null_Refinement): New routine. 2015-11-18 Gary Dismukes * exp_util.adb: Minor reformatting and typo fixes. From-SVN: r230525 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 1393a92c0be..87dce3b86f0 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,32 @@ +2015-11-18 Hristian Kirtchev + + * einfo.adb (Has_Non_Null_Refinement): Rename to + Has_Non_Null_Visible_Refinement. + (Has_Null_Refinement): Rename to Has_Null_Visible_Refinement. + * einfo.ads Update the documentation of + attribute Has_Non_Null_Refinement and attribute Has_Null_Refinement. + (Has_Non_Null_Refinement): Rename to Has_Non_Null_Visible_Refinement + and update occurrences in entities. + (Has_Null_Refinement): Rename to Has_Null_Visible_Refinement and update + occurrences in entities. + * sem_prag.adb (Check_In_Out_States): Update the calls to + Has_[Non_]Null_Refinement. + (Check_Input_States): Update the + calls to Has_[Non_]Null_Refinement. + (Check_Output_States): Update the calls to Has_[Non_]Null_Refinement. + (Check_Proof_In_States): Update the calls to Has_[Non_]Null_Refinement. + (Collect_Global_Item): Update the calls to Has_[Non_]Null_Refinement. + (Is_Null_Refined_State): Update the calls to Has_[Non_]Null_Refinement. + (Match_Item): Update the calls to Has_[Non_]Null_Refinement. + * sem_util.adb (Has_Non_Null_Refinement): New routine. + (Has_Null_Refinement): New routine. + * sem_util.ads (Has_Non_Null_Refinement): New routine. + (Has_Null_Refinement): New routine. + +2015-11-18 Gary Dismukes + + * exp_util.adb: Minor reformatting and typo fixes. + 2015-11-18 Hristian Kirtchev * sem_ch4.adb: Minor reformatting. diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index e8ee8730f9c..b7c2732837d 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -7301,11 +7301,11 @@ package body Einfo is and then Present (Non_Limited_View (Id)); end Has_Non_Limited_View; - ----------------------------- - -- Has_Non_Null_Refinement -- - ----------------------------- + ------------------------------------- + -- Has_Non_Null_Visible_Refinement -- + ------------------------------------- - function Has_Non_Null_Refinement (Id : E) return B is + function Has_Non_Null_Visible_Refinement (Id : E) return B is begin -- "Refinement" is a concept applicable only to abstract states @@ -7322,7 +7322,7 @@ package body Einfo is end if; return False; - end Has_Non_Null_Refinement; + end Has_Non_Null_Visible_Refinement; ----------------------------- -- Has_Null_Abstract_State -- @@ -7337,11 +7337,11 @@ package body Einfo is and then Is_Null_State (Node (First_Elmt (Abstract_States (Id)))); end Has_Null_Abstract_State; - ------------------------- - -- Has_Null_Refinement -- - ------------------------- + --------------------------------- + -- Has_Null_Visible_Refinement -- + --------------------------------- - function Has_Null_Refinement (Id : E) return B is + function Has_Null_Visible_Refinement (Id : E) return B is begin -- "Refinement" is a concept applicable only to abstract states @@ -7358,7 +7358,7 @@ package body Einfo is end if; return False; - end Has_Null_Refinement; + end Has_Null_Visible_Refinement; -------------------- -- Has_Unmodified -- diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 31059fd2bc6..28fa5d6115d 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -1761,9 +1761,10 @@ package Einfo is -- E_Abstract_State entities. True if their Non_Limited_View attribute -- is present. --- Has_Non_Null_Refinement (synth) --- Defined in E_Abstract_State entities. True if the state has at least --- one variable or state constituent in aspect/pragma Refined_State. +-- Has_Non_Null_Visible_Refinement (synth) +-- Defined in E_Abstract_State entities. True if the state has a visible +-- refinement of at least one variable or state constituent as expressed +-- in aspect/pragma Refined_State. -- Has_Non_Standard_Rep (Flag75) [implementation base type only] -- Defined in all type entities. Set when some representation clause @@ -1779,9 +1780,9 @@ package Einfo is -- Defined in package entities. True if the package is subject to a null -- Abstract_State aspect/pragma. --- Has_Null_Refinement (synth) --- Defined in E_Abstract_State entities. True if the state has a null --- refinement in aspect/pragma Refined_State. +-- Has_Null_Visible_Refinement (synth) +-- Defined in E_Abstract_State entities. True if the state has a visible +-- null refinement as expressed in aspect/pragma Refined_State. -- Has_Object_Size_Clause (Flag172) -- Defined in entities for types and subtypes. Set if an Object_Size @@ -5525,8 +5526,8 @@ package Einfo is -- From_Limited_With (Flag159) -- Has_Visible_Refinement (Flag263) -- Has_Non_Limited_View (synth) - -- Has_Non_Null_Refinement (synth) - -- Has_Null_Refinement (synth) + -- Has_Non_Null_Visible_Refinement (synth) + -- Has_Null_Visible_Refinement (synth) -- Is_External_State (synth) -- Is_Null_State (synth) -- Is_Synchronized_State (synth) @@ -7255,9 +7256,9 @@ package Einfo is function Has_Entries (Id : E) return B; function Has_Foreign_Convention (Id : E) return B; function Has_Non_Limited_View (Id : E) return B; - function Has_Non_Null_Refinement (Id : E) return B; + function Has_Non_Null_Visible_Refinement (Id : E) return B; function Has_Null_Abstract_State (Id : E) return B; - function Has_Null_Refinement (Id : E) return B; + function Has_Null_Visible_Refinement (Id : E) return B; function Implementation_Base_Type (Id : E) return E; function Is_Base_Type (Id : E) return B; function Is_Boolean_Type (Id : E) return B; diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 3f10b9573fd..5810dd58636 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -6586,8 +6586,8 @@ package body Exp_Util is if Is_Private_Type (Unc_Typ) and then Has_Unknown_Discriminants (Unc_Typ) then - -- The caller requests a unque external name for both the private and - -- the full subtype. + -- The caller requests a unique external name for both the private + -- and the full subtype. if Present (Related_Id) then Full_Subtyp := diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index be42aaa390c..d113a2c2654 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -23308,7 +23308,7 @@ package body Sem_Prag is return Ekind (Item_Id) = E_Abstract_State - and then Has_Null_Refinement (Item_Id); + and then Has_Null_Visible_Refinement (Item_Id); else return False; end if; @@ -23359,7 +23359,7 @@ package body Sem_Prag is -- An abstract state with visible null refinement matches -- null or Empty (special case). - if Has_Null_Refinement (Dep_Item_Id) + if Has_Null_Visible_Refinement (Dep_Item_Id) and then (No (Ref_Item) or else Nkind (Ref_Item) = N_Null) then Record_Item (Dep_Item_Id); @@ -23368,7 +23368,7 @@ package body Sem_Prag is -- An abstract state with visible non-null refinement -- matches one of its constituents. - elsif Has_Non_Null_Refinement (Dep_Item_Id) then + elsif Has_Non_Null_Visible_Refinement (Dep_Item_Id) then if Is_Entity_Name (Ref_Item) then Ref_Item_Id := Entity_Of (Ref_Item); @@ -23698,7 +23698,7 @@ package body Sem_Prag is -- Ensure that all of the constituents are utilized as -- outputs in pragma Refined_Depends. - elsif Has_Non_Null_Refinement (Item_Id) then + elsif Has_Non_Null_Visible_Refinement (Item_Id) then Check_Constituent_Usage (Item_Id); end if; end if; @@ -24270,7 +24270,7 @@ package body Sem_Prag is -- Ensure that one of the three coverage variants is satisfied if Ekind (Item_Id) = E_Abstract_State - and then Has_Non_Null_Refinement (Item_Id) + and then Has_Non_Null_Visible_Refinement (Item_Id) then Check_Constituent_Usage (Item_Id); end if; @@ -24361,7 +24361,7 @@ package body Sem_Prag is -- is of mode Input. if Ekind (Item_Id) = E_Abstract_State - and then Has_Non_Null_Refinement (Item_Id) + and then Has_Non_Null_Visible_Refinement (Item_Id) then Check_Constituent_Usage (Item_Id); end if; @@ -24455,7 +24455,7 @@ package body Sem_Prag is -- have mode Output. if Ekind (Item_Id) = E_Abstract_State - and then Has_Non_Null_Refinement (Item_Id) + and then Has_Non_Null_Visible_Refinement (Item_Id) then Check_Constituent_Usage (Item_Id); end if; @@ -24545,7 +24545,7 @@ package body Sem_Prag is -- is of mode Proof_In if Ekind (Item_Id) = E_Abstract_State - and then Has_Non_Null_Refinement (Item_Id) + and then Has_Non_Null_Visible_Refinement (Item_Id) then Check_Constituent_Usage (Item_Id); end if; @@ -24750,10 +24750,10 @@ package body Sem_Prag is -- be null in which case there are no constituents. if Ekind (Item_Id) = E_Abstract_State then - if Has_Null_Refinement (Item_Id) then + if Has_Null_Visible_Refinement (Item_Id) then Has_Null_State := True; - elsif Has_Non_Null_Refinement (Item_Id) then + elsif Has_Non_Null_Visible_Refinement (Item_Id) then Append_New_Elmt (Item_Id, States); if Item_Mode = Name_Input then diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 036cc0cfe48..9a000ae7dc6 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -9078,6 +9078,25 @@ package body Sem_Util is end if; end Has_No_Obvious_Side_Effects; + ----------------------------- + -- Has_Non_Null_Refinement -- + ----------------------------- + + function Has_Non_Null_Refinement (Id : Entity_Id) return Boolean is + begin + pragma Assert (Ekind (Id) = E_Abstract_State); + + -- For a refinement to be non-null, the first constituent must be + -- anything other than null. + + if Present (Refinement_Constituents (Id)) then + return + Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) /= N_Null; + end if; + + return False; + end Has_Non_Null_Refinement; + ------------------------ -- Has_Null_Exclusion -- ------------------------ @@ -9168,6 +9187,25 @@ package body Sem_Util is end if; end Has_Null_Extension; + ------------------------- + -- Has_Null_Refinement -- + ------------------------- + + function Has_Null_Refinement (Id : Entity_Id) return Boolean is + begin + pragma Assert (Ekind (Id) = E_Abstract_State); + + -- For a refinement to be null, the state's sole constituent must be a + -- null. + + if Present (Refinement_Constituents (Id)) then + return + Nkind (Node (First_Elmt (Refinement_Constituents (Id)))) = N_Null; + end if; + + return False; + end Has_Null_Refinement; + ------------------------------- -- Has_Overriding_Initialize -- ------------------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 838546b91dc..cc53a57bb51 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1059,9 +1059,19 @@ package Sem_Util is -- routine in Remove_Side_Effects is much more extensive and perhaps could -- be shared, so that this routine would be more accurate. + function Has_Non_Null_Refinement (Id : Entity_Id) return Boolean; + -- Determine whether abstract state Id has at least one nonnull constituent + -- as expressed in pragma Refined_State. This function does not take into + -- account the visible refinement region of abstract state Id. + function Has_Null_Exclusion (N : Node_Id) return Boolean; -- Determine whether node N has a null exclusion + function Has_Null_Refinement (Id : Entity_Id) return Boolean; + -- Determine whether abstract state Id has a null refinement as expressed + -- in pragma Refined_State. This function does not take into account the + -- visible refinement region of abstract state Id. + function Has_Overriding_Initialize (T : Entity_Id) return Boolean; -- Predicate to determine whether a controlled type has a user-defined -- Initialize primitive (and, in Ada 2012, whether that primitive is