diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2018-05-31 10:47:19 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2018-05-31 10:47:19 +0000 |
| commit | 0562ed3104a26738bda3828e2cbe7e4711e9e666 (patch) | |
| tree | 12c711233bf0bc1c9559d8adbf1d6a7f7cf0a222 /gcc | |
| parent | 6e03839f3d5a26617da02a5d052451251486ede1 (diff) | |
| download | gcc-0562ed3104a26738bda3828e2cbe7e4711e9e666.zip gcc-0562ed3104a26738bda3828e2cbe7e4711e9e666.tar.gz gcc-0562ed3104a26738bda3828e2cbe7e4711e9e666.tar.bz2 | |
[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
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/sem_ch6.adb | 15 |
2 files changed, 15 insertions, 5 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 8e7eb11..546e0d8 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +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 diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index f000f71..3413e21 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 |