Frontend inlining is applied independently of pragmas Inline or Inline_Always in GNATprove mode, to benefit from contextual analysis whenever possible. Hence, ignore such pragmas in GNATprove mode, to avoid getting useless errors on these when the corresponding subprogram is inlined by the frontend already.
Tested on x86_64-pc-linux-gnu, committed on trunk 2014-10-23 Yannick Moy <m...@adacore.com> * sem_prag.adb (Analyze_Pragma/Pragma_Inline & Pragma_Inline_Always): Disable analysis in GNATprove mode.
Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 216574) +++ sem_prag.adb (working copy) @@ -14894,12 +14894,21 @@ 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 @@ 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. + -- 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. - -- 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. - - if not CodePeer_Mode then + if not CodePeer_Mode and not GNATprove_Mode then Process_Inline (Enabled); end if;