r261012 - in /trunk/gcc/ada: ChangeLog sem_ch6.adb

[pmderodat at gcc dot gnu dot org]

Author: pmderodat
Date: Thu May 31 10:47:19 2018
New Revision: 261012

URL: https://gcc.gnu.org/viewcvs?rev=261012&root=gcc&view=rev
Log:
[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.

Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/sem_ch6.adb