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
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-05-31 Piotr Trojanek <troja...@adacore.com>
gcc/ada/
* sem_ch6.adb (Check_Missing_Return): Handle procedures with no
explicit spec.--- gcc/ada/sem_ch6.adb
+++ 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
