[Ada] Detect returning procedures annotated with No_Return

GNAT was emitting a warning about procedures with No_Return aspect on the
spec and a returning body, but failed to handle similar procedures with
no explicit spec. Now fixed.

This was also affecting GNATprove, where an undetected mismatch between
No_Return aspect and the body was a soundness bug, i.e. GNATprove was
silently accept code that raise a runtime exception.

------------
-- Source --
------------

procedure P (X : Boolean) with No_Return is
begin
   if X then
      raise Program_Error;
   end if;
end;

-----------------
-- Compilation --
-----------------

$ gcc -c p.adb
p.adb:3:04: warning: implied return after this statement will raise
                     Program_Error
p.adb:3:04: warning: procedure "P" is marked as No_Return

2018-05-31  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* sem_ch6.adb (Check_Missing_Return): Handle procedures with no
	explicit spec.

From-SVN: r261012

gcc/ada/ChangeLog

+2018-05-31  Piotr Trojanek  <trojanek@adacore.com>
+
+	* sem_ch6.adb (Check_Missing_Return): Handle procedures with no
+	explicit spec.
+
 2018-05-31  Eric Botcazou  <ebotcazou@adacore.com>
 
 	* gcc-interface/trans.c (Call_to_gnu): In the by-reference case, if

gcc/ada/sem_ch6.adb

@@ -3040,11 +3040,16 @@ package body Sem_Ch6 is
 
          --  If procedure with No_Return, check returns
 
-         elsif Nkind (Body_Spec) = N_Procedure_Specification
-           and then Present (Spec_Id)
-           and then No_Return (Spec_Id)
-         then
-            Check_Returns (HSS, 'P', Missing_Ret, Spec_Id);
+         elsif Nkind (Body_Spec) = N_Procedure_Specification then
+            if Present (Spec_Id) then
+               Id := Spec_Id;
+            else
+               Id := Body_Id;
+            end if;
+
+            if No_Return (Id) then
+               Check_Returns (HSS, 'P', Missing_Ret, Id);
+            end if;
          end if;
 
          --  Special checks in SPARK mode