sem_prag.adb (Analyze_Depends_In_Decl_Part): Add continuation message for missing input.

2017-09-06  Yannick Moy  <moy@adacore.com>

	* sem_prag.adb (Analyze_Depends_In_Decl_Part): Add continuation
	message for missing input.

2017-09-06  Yannick Moy  <moy@adacore.com>

	* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Prevent inlining
	of protected subprograms and entries.
	* sem_util.adb, sem_util.ads (Is_Subp_Or_Entry_Inside_Protected):
	New function to detect when a subprogram of entry is defined
	inside a protected object.

From-SVN: r251778

gcc/ada/ChangeLog

+2017-09-06  Yannick Moy  <moy@adacore.com>
+
+	* sem_prag.adb (Analyze_Depends_In_Decl_Part): Add continuation
+	message for missing input.
+
+2017-09-06  Yannick Moy  <moy@adacore.com>
+
+	* inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Prevent inlining
+	of protected subprograms and entries.
+	* sem_util.adb, sem_util.ads (Is_Subp_Or_Entry_Inside_Protected):
+	New function to detect when a subprogram of entry is defined
+	inside a protected object.
+
 2017-09-06  Bob Duff  <duff@adacore.com>
 
 	* sysdep.c (__gnat_has_cap_sys_nice): New function to determine

gcc/ada/inline.adb

@@ -1406,6 +1406,13 @@ package body Inline is
       elsif Instantiation_Location (Sloc (Id)) /= No_Location then
          return False;
 
+      --  Do not inline subprograms and entries defined inside protected types,
+      --  which typically are not helper subprograms, which also avoids getting
+      --  spurious messages on calls that cannot be inlined.
+
+      elsif Is_Subp_Or_Entry_Inside_Protected (Id) then
+         return False;
+
       --  Do not inline predicate functions (treated specially by GNATprove)
 
       elsif Is_Predicate_Function (Id) then

gcc/ada/sem_prag.adb

@@ -1457,6 +1457,9 @@ package body Sem_Prag is
 
                   Error_Msg := Name_Find;
                   SPARK_Msg_NE (Get_Name_String (Error_Msg), N, Item_Id);
+                  SPARK_Msg_NE
+                    ("\add `null ='> &` dependency to ignore this input",
+                     N, Item_Id);
                end if;
 
             --  Output case (SPARK RM 6.1.5(10))

gcc/ada/sem_util.adb

@@ -15539,6 +15539,32 @@ package body Sem_Util is
         and then Ekind (Defining_Entity (N)) /= E_Subprogram_Body;
    end Is_Subprogram_Stub_Without_Prior_Declaration;
 
+   ---------------------------------------
+   -- Is_Subp_Or_Entry_Inside_Protected --
+   ---------------------------------------
+
+   function Is_Subp_Or_Entry_Inside_Protected (E : Entity_Id) return Boolean is
+      Scop : Entity_Id;
+
+   begin
+      case Ekind (E) is
+         when Entry_Kind | Subprogram_Kind =>
+            Scop := Scope (E);
+
+            while Present (Scop) loop
+               if Ekind (Scop) = E_Protected_Type then
+                  return True;
+               end if;
+               Scop := Scope (Scop);
+            end loop;
+
+            return False;
+
+         when others =>
+            return False;
+      end case;
+   end Is_Subp_Or_Entry_Inside_Protected;
+
    --------------------------
    -- Is_Suspension_Object --
    --------------------------

gcc/ada/sem_util.ads

@@ -1842,6 +1842,10 @@ package Sem_Util is
    --  Return True if N is a subprogram stub with no prior subprogram
    --  declaration.
 
+   function Is_Subp_Or_Entry_Inside_Protected (E : Entity_Id) return Boolean;
+   --  Return True if E is an entry or a subprogram that is part (directly or
+   --  in a nested way) of a protected type.
+
    function Is_Suspension_Object (Id : Entity_Id) return Boolean;
    --  Determine whether arbitrary entity Id denotes Suspension_Object defined
    --  in Ada.Synchronous_Task_Control.