===================================================================
@@ -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;