diff options
Diffstat (limited to 'gcc/ada/sem_prag.adb')
| -rw-r--r-- | gcc/ada/sem_prag.adb | 35 |
1 files changed, 22 insertions, 13 deletions
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 5ef1010e3ca..df8ec80b142 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -14894,12 +14894,21 @@ package body Sem_Prag is when Pragma_Inline => - -- Inline status is Enabled if inlining option is active + -- Pragma always active unless in GNATprove mode. It is disabled + -- in GNATprove mode because frontend inlining is applied + -- independently of pragmas Inline and Inline_Always for + -- formal verification, see Can_Be_Inlined_In_GNATprove_Mode + -- in inline.ads. - if Inline_Active then - Process_Inline (Enabled); - else - Process_Inline (Disabled); + if not GNATprove_Mode then + + -- Inline status is Enabled if inlining option is active + + if Inline_Active then + Process_Inline (Enabled); + else + Process_Inline (Disabled); + end if; end if; ------------------- @@ -14911,15 +14920,15 @@ package body Sem_Prag is when Pragma_Inline_Always => GNAT_Pragma; - -- Pragma always active unless in CodePeer mode. It is disabled - -- in CodePeer mode because inlining is not helpful, and enabling - -- if caused walk order issues. - - -- Historical note: this pragma used to be disabled in GNATprove - -- mode as well, but that was odd since walk order should not be - -- an issue in that case. + -- Pragma always active unless in CodePeer mode or GNATprove + -- mode. It is disabled in CodePeer mode because inlining is + -- not helpful, and enabling it caused walk order issues. It + -- is disabled in GNATprove mode because frontend inlining is + -- applied independently of pragmas Inline and Inline_Always for + -- formal verification, see Can_Be_Inlined_In_GNATprove_Mode in + -- inline.ads. - if not CodePeer_Mode then + if not CodePeer_Mode and not GNATprove_Mode then Process_Inline (Enabled); end if; |