[multiple changes]

2017-04-27  Steve Baird  <baird@adacore.com>

	* exp_util.adb (Build_Allocate_Deallocate_Proc):
	Add "Suppress => All_Checks" to avoid generating unnecessary
	checks.

2017-04-27  Yannick Moy  <moy@adacore.com>

	* debug.adb: Reserve debug flag 'm' for no inlining in GNATprove.
	* sem_ch6.adb (Anayze_Subprogram_Body_Helper): Skip creation of
	inlining body in GNATprove mode when switch -gnatdm used.
	* sem_res.adb (Resolve_Call): Skip detection of lack of inlining
	in GNATprove mode when switch -gnatdm used.

2017-04-27  Arnaud Charlet  <charlet@adacore.com>

	* sem_ch13.adb (Analyze_Attribute_Definition_Clause
	[Attribute_Address]): Call Set_Address_Taken when ignoring rep
	clauses, so that we keep an indication of the address clause
	before removing it from the tree.

From-SVN: r247312

6 files changed, 38 insertions, 4 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 2362ccf..cfcf449 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,24 @@
+2017-04-27  Steve Baird  <baird@adacore.com>
+
+	* exp_util.adb (Build_Allocate_Deallocate_Proc):
+	Add "Suppress => All_Checks" to avoid generating unnecessary
+	checks.
+
+2017-04-27  Yannick Moy  <moy@adacore.com>
+
+	* debug.adb: Reserve debug flag 'm' for no inlining in GNATprove.
+	* sem_ch6.adb (Anayze_Subprogram_Body_Helper): Skip creation of
+	inlining body in GNATprove mode when switch -gnatdm used.
+	* sem_res.adb (Resolve_Call): Skip detection of lack of inlining
+	in GNATprove mode when switch -gnatdm used.
+
+2017-04-27  Arnaud Charlet  <charlet@adacore.com>
+
+	* sem_ch13.adb (Analyze_Attribute_Definition_Clause
+	[Attribute_Address]): Call Set_Address_Taken when ignoring rep
+	clauses, so that we keep an indication of the address clause
+	before removing it from the tree.
+
 2017-04-27  Yannick Moy  <moy@adacore.com>
 
 	* exp_util.ads, exp_util.adb (Evaluate_Name): Force evaluation
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index 46f19ca..c289c98 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -49,7 +49,7 @@ package body Debug is
    --  dj   Suppress "junk null check" for access parameter values
    --  dk   Generate GNATBUG message on abort, even if previous errors
    --  dl   Generate unit load trace messages
-   --  dm
+   --  dm   Prevent special frontend inlining in GNATprove mode
    --  dn   Generate messages for node/list allocation
    --  do   Print source from tree (original code only)
    --  dp   Generate messages for parser scope stack push/pops
@@ -281,6 +281,11 @@ package body Debug is
    --       generated each time a request is made to the library manager to
    --       load a new unit.
 
+   --  dm   Prevent special frontend inlining in GNATprove mode. In some cases,
+   --       some subprogram calls are inlined in GNATprove mode in order to
+   --       facilitate formal verification. This debug switch prevents that
+   --       inlining to happen.
+
    --  dn   Generate messages for node/list allocation. Each time a node or
    --       list header is allocated, a line of output is generated. Certain
    --       other basic tree operations also cause a line of output to be
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index c80cd39..4da91da 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -991,7 +991,8 @@ package body Exp_Util is
                    Make_Procedure_Call_Statement (Loc,
                      Name                   =>
                        New_Occurrence_Of (Proc_To_Call, Loc),
-                     Parameter_Associations => Actuals)))));
+                     Parameter_Associations => Actuals)))),
+           Suppress => All_Checks);
 
          --  The newly generated Allocate / Deallocate becomes the default
          --  procedure to call when the back end processes the allocation /
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 34fd7a5..2c2366d 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -4701,7 +4701,7 @@ package body Sem_Ch13 is
 
             --  We do not do anything here with address clauses, they will be
             --  removed by Freeze later on, but for now, it works better to
-            --  keep then in the tree.
+            --  keep them in the tree.
 
             when Attribute_Address =>
                null;
@@ -4860,8 +4860,12 @@ package body Sem_Ch13 is
             --  Even when ignoring rep clauses we need to indicate that the
             --  entity has an address clause and thus it is legal to declare
             --  it imported. Freeze will get rid of the address clause later.
+            --  Also call Set_Address_Taken to indicate that an address clause
+            --  was present, even if we are about to remove it.
 
             if Ignore_Rep_Clauses then
+               Set_Address_Taken (U_Ent);
+
                if Ekind_In (U_Ent, E_Variable, E_Constant) then
                   Record_Rep_Item (U_Ent, N);
                end if;
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 020ffb8..49bcc9b 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -4050,6 +4050,7 @@ package body Sem_Ch6 is
       --  inlining. This inlining should occur after analysis of the body, so
       --  that it is known whether the value of SPARK_Mode, which can be
       --  defined by a pragma inside the body, is applicable to the body.
+      --  Inlining can be disabled with switch -gnatdm
 
       elsif GNATprove_Mode
         and then Full_Analysis
@@ -4060,6 +4061,7 @@ package body Sem_Ch6 is
         and then Body_Has_SPARK_Mode_On
         and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id)
         and then not Body_Has_Contract
+        and then not Debug_Flag_M
       then
          Build_Body_To_Inline (N, Spec_Id);
       end if;
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 0595b0b..383a5a9 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6621,10 +6621,11 @@ package body Sem_Res is
             Body_Id := Corresponding_Body (Nam_Decl);
 
             --  Nothing to do if the subprogram is not eligible for inlining in
-            --  GNATprove mode.
+            --  GNATprove mode, or inlining is disabled with switch -gnatdm
 
             if not Is_Inlined_Always (Nam_UA)
               or else not Can_Be_Inlined_In_GNATprove_Mode (Nam_UA, Body_Id)
+              or else Debug_Flag_M
             then
                null;