[multiple changes]

2014-01-23  Robert Dewar  <dewar@adacore.com>

	* gnatlink.adb (Gnatlink): Fix problem of generating bad name
	msg on VMS.

2014-01-23  Bob Duff  <duff@adacore.com>

	* g-dynhta.ads: Minor comment fix.

2014-01-23  Yannick Moy  <moy@adacore.com>

	* 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

6 files changed, 82 insertions, 11 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index ee7e846..a885156 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,25 @@
 2014-01-23  Robert Dewar  <dewar@adacore.com>
 
+	* gnatlink.adb (Gnatlink): Fix problem of generating bad name
+	msg on VMS.
+
+2014-01-23  Bob Duff  <duff@adacore.com>
+
+	* g-dynhta.ads: Minor comment fix.
+
+2014-01-23  Yannick Moy  <moy@adacore.com>
+
+	* 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  <dewar@adacore.com>
+
 	* gnatlink.adb (Gnatlink): Check for suspicious executable file
 	names on windows.
 
diff --git a/gcc/ada/g-dynhta.ads b/gcc/ada/g-dynhta.ads
index 1369244..e731ed3 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 1746bcd..ea679d9 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 6b9c5fe..22b1537 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 62dd889..f46f2e9 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 555a788..1a847fd 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;