[Ada] Ignore pragmas Inline/Inline_Always in GNATprove mode

[Arnaud Charlet]

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  <moy@adacore.com>

	* sem_prag.adb (Analyze_Pragma/Pragma_Inline & Pragma_Inline_Always):
	Disable analysis in GNATprove mode.

-------------- next part --------------
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;