From a98480ddbbe03479ae6606ed674de2999e24c022 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 7 Nov 2014 14:47:31 +0100 Subject: [PATCH] [multiple changes] 2014-11-07 Hristian Kirtchev * freeze.adb (Freeze_Entity): Issue an error regardless of the SPARK_Mode when a ghost type is effectively volatile. * sem_ch3.adb (Analyze_Object_Contract): Decouple the checks related to Ghost from SPARK_Mode. * sem_res.adb (Check_Ghost_Policy): Issue an error regardless of the SPARK_Mode when the Ghost policies do not match. * sem_util.adb (Check_Ghost_Completion): Issue an error regardless of the SPARK_Mode when the Ghost policies do not match. 2014-11-07 Ed Schonberg * sem_ch5.adb (Analyze_Iterator_Specification): return if name in iterator does not have any usable aspect for iteration. 2014-11-07 Ed Schonberg * sem_ch6.adb (Analyze_Null_Procedure): Reject a null procedure that there is a previous null procedure in scope with a matching profile. 2014-11-07 Hristian Kirtchev * atree.adb (Copy_Separate_Tree): Copy the aspect specifications. * inline.adb (Has_Some_Contract): Do the check only when the related entity has been analyzed. From-SVN: r217224 --- gcc/ada/ChangeLog | 28 +++++++++++++++++++++++ gcc/ada/atree.adb | 10 +++++++++ gcc/ada/freeze.adb | 53 ++++++++++++++++---------------------------- gcc/ada/inline.adb | 21 +++++++++++++----- gcc/ada/sem_ch3.adb | 28 ++++++++++------------- gcc/ada/sem_ch5.adb | 4 ++++ gcc/ada/sem_ch6.adb | 5 +++++ gcc/ada/sem_res.adb | 23 ++++++++++--------- gcc/ada/sem_util.adb | 20 ++++++++--------- 9 files changed, 116 insertions(+), 76 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index e7fedaa586b..3386f6a9911 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,31 @@ +2014-11-07 Hristian Kirtchev + + * freeze.adb (Freeze_Entity): Issue an error regardless of the + SPARK_Mode when a ghost type is effectively volatile. + * sem_ch3.adb (Analyze_Object_Contract): Decouple the checks + related to Ghost from SPARK_Mode. + * sem_res.adb (Check_Ghost_Policy): Issue an error regardless + of the SPARK_Mode when the Ghost policies do not match. + * sem_util.adb (Check_Ghost_Completion): Issue an error regardless + of the SPARK_Mode when the Ghost policies do not match. + +2014-11-07 Ed Schonberg + + * sem_ch5.adb (Analyze_Iterator_Specification): return if name + in iterator does not have any usable aspect for iteration. + +2014-11-07 Ed Schonberg + + * sem_ch6.adb (Analyze_Null_Procedure): Reject a null procedure + that there is a previous null procedure in scope with a matching + profile. + +2014-11-07 Hristian Kirtchev + + * atree.adb (Copy_Separate_Tree): Copy the aspect specifications. + * inline.adb (Has_Some_Contract): Do the check only when the + related entity has been analyzed. + 2014-11-07 Ed Schonberg * exp_fixd.adb (Expand_Multiply_Fixed_By_Fixed_Giving_Integer): diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index 2af7e2e48b9..eb196e4fa1c 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -892,6 +892,16 @@ package body Atree is Set_Field4 (New_Id, Possible_Copy (Field4 (New_Id))); Set_Field5 (New_Id, Possible_Copy (Field5 (New_Id))); + -- Explicitly copy the aspect specifications as those do not reside + -- in a node field. + + if Permits_Aspect_Specifications (Source) + and then Has_Aspects (Source) + then + Set_Aspect_Specifications + (New_Id, Copy_List (Aspect_Specifications (Source))); + end if; + -- Set Entity field to Empty to ensure that no entity references -- are shared between the two, if the source is already analyzed. diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index d98645c0cab..9ba6f24c734 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -2398,6 +2398,24 @@ package body Freeze is Set_Has_Non_Standard_Rep (Base_Type (Arr), True); Set_Is_Bit_Packed_Array (Base_Type (Arr), True); Set_Is_Packed (Base_Type (Arr), True); + + -- Make sure that we have the necessary routines to + -- implement the packing, and complain now if not. + + declare + CS : constant Int := UI_To_Int (Csiz); + RE : constant RE_Id := Get_Id (CS); + + begin + if RE /= RE_Null + and then not RTE_Available (RE) + then + Error_Msg_CRT + ("packing of " & UI_Image (Csiz) + & "-bit components", + First_Subtype (Etype (Arr))); + end if; + end; end if; end; end if; @@ -2650,37 +2668,6 @@ package body Freeze is Create_Packed_Array_Impl_Type (Arr); Freeze_And_Append (Packed_Array_Impl_Type (Arr), N, Result); - -- Make sure that we have the necessary routines to implement the - -- packing, and complain now if not. Note that we only test this - -- for constrained array types. - - if Is_Constrained (Arr) - and then Is_Bit_Packed_Array (Arr) - and then Present (Packed_Array_Impl_Type (Arr)) - and then Is_Array_Type (Packed_Array_Impl_Type (Arr)) - then - declare - CS : constant Uint := Component_Size (Arr); - RE : constant RE_Id := Get_Id (UI_To_Int (CS)); - - begin - if RE /= RE_Null - and then not RTE_Available (RE) - then - Error_Msg_CRT - ("packing of " & UI_Image (CS) & "-bit components", - First_Subtype (Etype (Arr))); - - -- Cancel the packing - - Set_Is_Packed (Base_Type (Arr), False); - Set_Is_Bit_Packed_Array (Base_Type (Arr), False); - Set_Packed_Array_Impl_Type (Arr, Empty); - goto Skip_Packed; - end if; - end; - end if; - -- Size information of packed array type is copied to the array -- type, since this is really the representation. But do not -- override explicit existing size values. If the ancestor subtype @@ -2702,8 +2689,6 @@ package body Freeze is end if; end if; - <> - -- For non-packed arrays set the alignment of the array to the -- alignment of the component type if it is unknown. Skip this -- in atomic case (atomic arrays may need larger alignments). @@ -4835,7 +4820,7 @@ package body Freeze is if Is_Ghost_Entity (E) and then Is_Effectively_Volatile (E) then - SPARK_Msg_N ("ghost type & cannot be volatile", E); + Error_Msg_N ("ghost type & cannot be volatile", E); end if; -- Deal with special cases of freezing for subtype diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 9646cc2fdc7..812002b4ed0 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1316,12 +1316,23 @@ package body Inline is ----------------------- function Has_Some_Contract (Id : Entity_Id) return Boolean is - Items : constant Node_Id := Contract (Id); + Items : Node_Id; + begin - return Present (Items) - and then (Present (Pre_Post_Conditions (Items)) or else - Present (Contract_Test_Cases (Items)) or else - Present (Classifications (Items))); + -- A call to an expression function may precede the actual body which + -- is inserted at the end of the enclosing declarations. Ensure that + -- the related entity is analyzed before inspecting the contract. + + if Analyzed (Id) then + Items := Contract (Id); + + return Present (Items) + and then (Present (Pre_Post_Conditions (Items)) or else + Present (Contract_Test_Cases (Items)) or else + Present (Classifications (Items))); + end if; + + return False; end Has_Some_Contract; ----------------------------- diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 8579e083313..969283251e8 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -3185,24 +3185,22 @@ package body Sem_Ch3 is Obj_Id); end if; end if; + end if; - if Is_Ghost_Entity (Obj_Id) then + if Is_Ghost_Entity (Obj_Id) then - -- A Ghost object cannot be effectively volatile - -- (SPARK RM 6.9(8)). + -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8)) - if Is_Effectively_Volatile (Obj_Id) then - SPARK_Msg_N ("ghost variable & cannot be volatile", Obj_Id); + if Is_Effectively_Volatile (Obj_Id) then + Error_Msg_N ("ghost variable & cannot be volatile", Obj_Id); - -- A Ghost object cannot be imported or exported - -- (SPARK RM 6.9(8)). + -- A Ghost object cannot be imported or exported (SPARK RM 6.9(8)) - elsif Is_Imported (Obj_Id) then - SPARK_Msg_N ("ghost object & cannot be imported", Obj_Id); + elsif Is_Imported (Obj_Id) then + Error_Msg_N ("ghost object & cannot be imported", Obj_Id); - elsif Is_Exported (Obj_Id) then - SPARK_Msg_N ("ghost object & cannot be exported", Obj_Id); - end if; + elsif Is_Exported (Obj_Id) then + Error_Msg_N ("ghost object & cannot be exported", Obj_Id); end if; end if; @@ -3256,10 +3254,10 @@ package body Sem_Ch3 is if Is_Ghost_Entity (Obj_Id) then if Is_Exported (Obj_Id) then - SPARK_Msg_N ("ghost object & cannot be exported", Obj_Id); + Error_Msg_N ("ghost object & cannot be exported", Obj_Id); elsif Is_Imported (Obj_Id) then - SPARK_Msg_N ("ghost object & cannot be imported", Obj_Id); + Error_Msg_N ("ghost object & cannot be imported", Obj_Id); end if; end if; end Analyze_Object_Contract; @@ -4788,8 +4786,6 @@ package body Sem_Ch3 is when Class_Wide_Kind => Set_Ekind (Id, E_Class_Wide_Subtype); - Set_First_Entity (Id, First_Entity (T)); - Set_Last_Entity (Id, Last_Entity (T)); Set_Class_Wide_Type (Id, Class_Wide_Type (T)); Set_Cloned_Subtype (Id, T); Set_Is_Tagged_Type (Id, True); diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 0e09a02acf7..2a809be40f4 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -2063,6 +2063,10 @@ package body Sem_Ch5 is Error_Msg_NE ("\to iterate directly over the elements of a container, " & "write `of &`", Name (N), Original_Node (Name (N))); + + -- No point in continuing analysis of iterator spec. + + return; end if; end if; diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 1ef29c55387..8536aa65007 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1453,6 +1453,11 @@ package body Sem_Ch6 is -- there are various error checks that are applied on this body -- when it is analyzed (e.g. correct aspect placement). + if Has_Completion (Prev) then + Error_Msg_Sloc := Sloc (Prev); + Error_Msg_NE ("duplicate body for & declared#", N, Prev); + end if; + Is_Completion := True; Rewrite (N, Null_Body); Analyze (N); diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 893e1e15ed8..0b295f9faa3 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -846,16 +846,16 @@ package body Sem_Res is if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then Error_Msg_Sloc := Sloc (Err_N); - SPARK_Msg_N ("incompatible ghost policies in effect", Err_N); - SPARK_Msg_NE ("\& declared with ghost policy Check", Err_N, Id); - SPARK_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id); + Error_Msg_N ("incompatible ghost policies in effect", Err_N); + Error_Msg_NE ("\& declared with ghost policy Check", Err_N, Id); + Error_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id); elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then Error_Msg_Sloc := Sloc (Err_N); - SPARK_Msg_N ("incompatible ghost policies in effect", Err_N); - SPARK_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id); - SPARK_Msg_NE ("\& used # with ghost policy Check", Err_N, Id); + Error_Msg_N ("incompatible ghost policies in effect", Err_N); + Error_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id); + Error_Msg_NE ("\& used # with ghost policy Check", Err_N, Id); end if; end Check_Ghost_Policy; @@ -873,7 +873,7 @@ package body Sem_Res is -- its behavior or value. else - SPARK_Msg_N + Error_Msg_N ("ghost entity cannot appear in this context (SPARK RM 6.9(12))", Ghost_Ref); end if; @@ -7089,12 +7089,13 @@ package body Sem_Res is ("volatile object cannot appear in this context " & "(SPARK RM 7.1.3(13))", N); end if; + end if; + end if; - -- A Ghost entity must appear in a specific context + -- A Ghost entity must appear in a specific context - elsif Is_Ghost_Entity (E) and then Comes_From_Source (N) then - Check_Ghost_Context (E, N); - end if; + if Is_Ghost_Entity (E) and then Comes_From_Source (N) then + Check_Ghost_Context (E, N); end if; end Resolve_Entity_Name; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 793120f0bf6..fc160e17d36 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -2688,18 +2688,18 @@ package body Sem_Util is then Error_Msg_Sloc := Sloc (Full_View); - SPARK_Msg_N ("incompatible ghost policies in effect", Partial_View); - SPARK_Msg_N ("\& declared with ghost policy Check", Partial_View); - SPARK_Msg_N ("\& completed # with ghost policy Ignore", Partial_View); + Error_Msg_N ("incompatible ghost policies in effect", Partial_View); + Error_Msg_N ("\& declared with ghost policy Check", Partial_View); + Error_Msg_N ("\& completed # with ghost policy Ignore", Partial_View); elsif Is_Ignored_Ghost_Entity (Partial_View) and then Policy = Name_Check then Error_Msg_Sloc := Sloc (Full_View); - SPARK_Msg_N ("incompatible ghost policies in effect", Partial_View); - SPARK_Msg_N ("\& declared with ghost policy Ignore", Partial_View); - SPARK_Msg_N ("\& completed # with ghost policy Check", Partial_View); + Error_Msg_N ("incompatible ghost policies in effect", Partial_View); + Error_Msg_N ("\& declared with ghost policy Ignore", Partial_View); + Error_Msg_N ("\& completed # with ghost policy Check", Partial_View); end if; end Check_Ghost_Completion; @@ -2722,8 +2722,8 @@ package body Sem_Util is -- The parent type of a Ghost type extension must be Ghost elsif not Is_Ghost_Entity (Parent_Typ) then - SPARK_Msg_N ("type extension & cannot be ghost", Typ); - SPARK_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ); + Error_Msg_N ("type extension & cannot be ghost", Typ); + Error_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ); return; end if; @@ -2735,8 +2735,8 @@ package body Sem_Util is Iface := Node (Iface_Elmt); if not Is_Ghost_Entity (Iface) then - SPARK_Msg_N ("type extension & cannot be ghost", Typ); - SPARK_Msg_NE ("\interface type & is not ghost", Typ, Iface); + Error_Msg_N ("type extension & cannot be ghost", Typ); + Error_Msg_NE ("\interface type & is not ghost", Typ, Iface); return; end if; -- 2.30.2