[Ada] Detect returning procedures annotated with No_Return

[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