From e949ee225e28fe925e872c1beaea1532bb9e2328 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 23 Jan 2014 17:54:50 +0100 Subject: [PATCH] [multiple changes] 2014-01-23 Robert Dewar * gnatlink.adb (Gnatlink): Fix problem of generating bad name msg on VMS. 2014-01-23 Bob Duff * g-dynhta.ads: Minor comment fix. 2014-01-23 Yannick Moy * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Inherit SPARK_Mode from spec on body only when not already inherited on spec. Set SPARK_Mode from context on body without previous spec. * * sem_prag.adb (Analyze_Pragma): Check placement of pragma on library-level entities. Correct retrieval of entity from declaration, for cases where the declaration is not a unit. * sem_ch12.adb (Instantiate_Object): Avoid calling Is_Volatile_Object on an empty node. From-SVN: r206987 --- gcc/ada/ChangeLog | 20 ++++++++++++++++++ gcc/ada/g-dynhta.ads | 2 +- gcc/ada/gnatlink.adb | 7 ++++--- gcc/ada/sem_ch12.adb | 5 ++++- gcc/ada/sem_ch6.adb | 10 ++++++++- gcc/ada/sem_prag.adb | 49 +++++++++++++++++++++++++++++++++++++++----- 6 files changed, 82 insertions(+), 11 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index ee7e846f541..a8851565ead 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,23 @@ +2014-01-23 Robert Dewar + + * gnatlink.adb (Gnatlink): Fix problem of generating bad name + msg on VMS. + +2014-01-23 Bob Duff + + * g-dynhta.ads: Minor comment fix. + +2014-01-23 Yannick Moy + + * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Inherit SPARK_Mode + from spec on body only when not already inherited on spec. Set + SPARK_Mode from context on body without previous spec. * + * sem_prag.adb (Analyze_Pragma): Check placement of pragma on + library-level entities. Correct retrieval of entity from + declaration, for cases where the declaration is not a unit. + * sem_ch12.adb (Instantiate_Object): Avoid + calling Is_Volatile_Object on an empty node. + 2014-01-23 Robert Dewar * gnatlink.adb (Gnatlink): Check for suspicious executable file diff --git a/gcc/ada/g-dynhta.ads b/gcc/ada/g-dynhta.ads index 13692446f96..e731ed359b3 100644 --- a/gcc/ada/g-dynhta.ads +++ b/gcc/ada/g-dynhta.ads @@ -56,7 +56,7 @@ package GNAT.Dynamic_HTables is -- A low-level Hash-Table abstraction, not as easy to instantiate as -- Simple_HTable. This mirrors the interface of GNAT.HTable.Static_HTable, -- but does require dynamic allocation (since we allow multiple instances - -- of the table. The model is that each Element contains its own Key that + -- of the table). The model is that each Element contains its own Key that -- can be retrieved by Get_Key. Furthermore, Element provides a link that -- can be used by the HTable for linking elements with same hash codes: diff --git a/gcc/ada/gnatlink.adb b/gcc/ada/gnatlink.adb index 1746bcd8533..ea679d9d25c 100644 --- a/gcc/ada/gnatlink.adb +++ b/gcc/ada/gnatlink.adb @@ -1101,9 +1101,9 @@ procedure Gnatlink is -- The following test needs comments, why is it VMS specific. -- The above comment looks out of date ??? - elsif not (OpenVMS_On_Target - and then - Is_Option_Present (Next_Line (Nfirst .. Nlast))) + elsif not + (OpenVMS_On_Target + and then Is_Option_Present (Next_Line (Nfirst .. Nlast))) then if Nlast > Nfirst + 2 and then Next_Line (Nfirst .. Nfirst + 1) = "-L" @@ -1832,6 +1832,7 @@ begin if FN'Length > 5 and then FN (FN'Last - 3 .. FN'Last) = ".exe" + and then not OpenVMS_On_Target then Check_File_Name ("install"); Check_File_Name ("setup"); diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 6b9c5feffc7..22b153764b6 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -9844,7 +9844,10 @@ package body Sem_Ch12 is -- The following check is only relevant when SPARK_Mode is on as it is -- not a standard Ada legality rule. - if SPARK_Mode = On and then Is_Volatile_Object (Actual) then + if SPARK_Mode = On + and then Present (Actual) + and then Is_Volatile_Object (Actual) + then Error_Msg_N ("volatile object cannot act as actual in generic instantiation " & "(SPARK RM 7.1.3(4))", Actual); diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 62dd8898760..f46f2e967b9 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -2997,7 +2997,9 @@ package body Sem_Ch6 is -- Set SPARK_Mode from spec if spec had a SPARK_Mode pragma - if Present (SPARK_Pragma (Spec_Id)) then + if Present (SPARK_Pragma (Spec_Id)) + and then not SPARK_Pragma_Inherited (Spec_Id) + then SPARK_Mode_Pragma := SPARK_Pragma (Spec_Id); SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragma); Set_SPARK_Pragma (Body_Id, SPARK_Pragma (Spec_Id)); @@ -3055,6 +3057,12 @@ package body Sem_Ch6 is Generate_Reference (Body_Id, Body_Id, 'b', Set_Ref => False, Force => True); Install_Formals (Body_Id); + + -- Set SPARK_Mode from context + + Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma); + Set_SPARK_Pragma_Inherited (Body_Id, True); + Push_Scope (Body_Id); end if; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 555a7887ff6..1a847fd03d4 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -18485,6 +18485,9 @@ package body Sem_Prag is -- anything. But if the old mode is OFF, then the only allowed -- new mode is also OFF. + procedure Check_Library_Level_Entity (E : Entity_Id); + -- Verify that pragma is applied to library-level entity E + function Get_SPARK_Mode_Name (Id : SPARK_Mode_Type) return Name_Id; -- Convert a value of type SPARK_Mode_Type to corresponding name @@ -18513,6 +18516,34 @@ package body Sem_Prag is end if; end Check_Pragma_Conformance; + -------------------------------- + -- Check_Library_Level_Entity -- + -------------------------------- + + procedure Check_Library_Level_Entity (E : Entity_Id) is + MsgF : String := "incorrect placement of pragma%"; + + begin + if not Is_Library_Level_Entity (E) then + Error_Msg_Name_1 := Pname; + Fix_Error (MsgF); + Error_Msg_N (MsgF, N); + + if Ekind_In (E, E_Generic_Package, + E_Package, + E_Package_Body) + then + Error_Msg_NE + ("\& is not a library-level package", N, E); + else + Error_Msg_NE + ("\& is not a library-level subprogram", N, E); + end if; + + raise Pragma_Exit; + end if; + end Check_Library_Level_Entity; + ------------------------- -- Get_SPARK_Mode_Name -- ------------------------- @@ -18614,7 +18645,8 @@ package body Sem_Prag is elsif Nkind_In (Stmt, N_Generic_Package_Declaration, N_Package_Declaration) then - Spec_Id := Defining_Unit_Name (Specification (Stmt)); + Spec_Id := Defining_Entity (Stmt); + Check_Library_Level_Entity (Spec_Id); Check_Pragma_Conformance (SPARK_Pragma (Spec_Id)); Set_SPARK_Pragma (Spec_Id, N); @@ -18628,7 +18660,8 @@ package body Sem_Prag is elsif Nkind_In (Stmt, N_Generic_Subprogram_Declaration, N_Subprogram_Declaration) then - Spec_Id := Defining_Unit_Name (Specification (Stmt)); + Spec_Id := Defining_Entity (Stmt); + Check_Library_Level_Entity (Spec_Id); Check_Pragma_Conformance (SPARK_Pragma (Spec_Id)); Set_SPARK_Pragma (Spec_Id, N); @@ -18679,11 +18712,12 @@ package body Sem_Prag is -- pragma SPARK_Mode; if Nkind (Context) = N_Package_Specification then - Spec_Id := Defining_Unit_Name (Context); + Spec_Id := Defining_Entity (Context); -- Pragma applies to private part if List_Containing (N) = Private_Declarations (Context) then + Check_Library_Level_Entity (Spec_Id); Check_Pragma_Conformance (SPARK_Aux_Pragma (Spec_Id)); SPARK_Mode_Pragma := N; SPARK_Mode := Mode_Id; @@ -18694,6 +18728,7 @@ package body Sem_Prag is -- Pragma applies to public part else + Check_Library_Level_Entity (Spec_Id); Check_Pragma_Conformance (SPARK_Pragma (Spec_Id)); SPARK_Mode_Pragma := N; SPARK_Mode := Mode_Id; @@ -18711,7 +18746,8 @@ package body Sem_Prag is elsif Nkind_In (Context, N_Function_Specification, N_Procedure_Specification) then - Spec_Id := Defining_Unit_Name (Context); + Spec_Id := Defining_Entity (Context); + Check_Library_Level_Entity (Spec_Id); Check_Pragma_Conformance (SPARK_Pragma (Spec_Id)); Set_SPARK_Pragma (Spec_Id, N); @@ -18725,6 +18761,7 @@ package body Sem_Prag is elsif Nkind (Context) = N_Package_Body then Spec_Id := Corresponding_Spec (Context); Body_Id := Defining_Entity (Context); + Check_Library_Level_Entity (Body_Id); Check_Pragma_Conformance (SPARK_Pragma (Body_Id)); SPARK_Mode_Pragma := N; SPARK_Mode := Mode_Id; @@ -18743,6 +18780,7 @@ package body Sem_Prag is Spec_Id := Corresponding_Spec (Context); Context := Specification (Context); Body_Id := Defining_Entity (Context); + Check_Library_Level_Entity (Body_Id); Check_Pragma_Conformance (SPARK_Pragma (Body_Id)); SPARK_Mode_Pragma := N; SPARK_Mode := Mode_Id; @@ -18761,7 +18799,8 @@ package body Sem_Prag is then Context := Parent (Context); Spec_Id := Corresponding_Spec (Context); - Body_Id := Defining_Unit_Name (Context); + Body_Id := Defining_Entity (Context); + Check_Library_Level_Entity (Body_Id); Check_Pragma_Conformance (SPARK_Aux_Pragma (Body_Id)); SPARK_Mode_Pragma := N; SPARK_Mode := Mode_Id;