From 0562ed3104a26738bda3828e2cbe7e4711e9e666 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Thu, 31 May 2018 10:47:19 +0000 Subject: [PATCH] [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 gcc/ada/ * sem_ch6.adb (Check_Missing_Return): Handle procedures with no explicit spec. From-SVN: r261012 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/sem_ch6.adb | 15 ++++++++++----- 2 files changed, 15 insertions(+), 5 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8e7eb118140..546e0d853a6 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2018-05-31 Piotr Trojanek + + * sem_ch6.adb (Check_Missing_Return): Handle procedures with no + explicit spec. + 2018-05-31 Eric Botcazou * gcc-interface/trans.c (Call_to_gnu): In the by-reference case, if diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index f000f71a3a9..3413e2185b5 100644 --- a/gcc/ada/sem_ch6.adb +++ b/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