diff options
Diffstat (limited to 'gcc/ada/sem_res.adb')
| -rw-r--r-- | gcc/ada/sem_res.adb | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index d81a5af..cfcbb94 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -7193,7 +7193,7 @@ package body Sem_Res is -- In GNATprove mode, expansion is disabled, but we want to inline some -- subprograms to facilitate formal verification. Indirect calls through -- a subprogram type or within a generic cannot be inlined. Inlining is - -- performed only for calls subject to SPARK_Mode on. + -- performed only for calls subject to SPARK_Mode => On. elsif GNATprove_Mode and then SPARK_Mode = On @@ -7206,10 +7206,13 @@ package body Sem_Res is if Nkind (Nam_Decl) = N_Subprogram_Declaration then Body_Id := Corresponding_Body (Nam_Decl); - -- Nothing to do if the subprogram is not eligible for inlining in - -- GNATprove mode, or inlining is disabled with switch -gnatdm + -- Nothing to do if the subprogram is not inlined (because it is + -- recursive, directly or indirectly), or is not eligible for + -- inlining GNATprove mode (because of properties of the + -- subprogram itself), or inlining has been disabled with switch + -- -gnatdm. - if not Is_Inlined_Always (Nam_UA) + if not Is_Inlined (Nam_UA) or else not Can_Be_Inlined_In_GNATprove_Mode (Nam_UA, Body_Id) or else Debug_Flag_M then |