]> git.ipfire.org Git - thirdparty/gcc.git/commitdiff
[multiple changes]
authorArnaud Charlet <charlet@gcc.gnu.org>
Thu, 27 Apr 2017 10:17:42 +0000 (12:17 +0200)
committerArnaud Charlet <charlet@gcc.gnu.org>
Thu, 27 Apr 2017 10:17:42 +0000 (12:17 +0200)
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

gcc/ada/ChangeLog
gcc/ada/debug.adb
gcc/ada/exp_util.adb
gcc/ada/sem_ch13.adb
gcc/ada/sem_ch6.adb
gcc/ada/sem_res.adb

index 2362ccf55c206b0ce12d05caa6cd1c89827635ba..cfcf449ffb6db3644e01ebe11ec5eb150ff24577 100644 (file)
@@ -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
index 46f19ca2e0621dd701cea4bc32af56793453e66d..c289c98e6044fefc488fb5c086662af7ad7279fe 100644 (file)
@@ -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
index c80cd39a885e0519b6ec5d5e376d0431d0ad5dc1..4da91dad397d57ae1e0d576a5d4a92e7f52997f9 100644 (file)
@@ -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 /
index 34fd7a53b52c5d1aafc8fde8bce0450858192885..2c2366d21920097296be948067e0cf1c69623ce5 100644 (file)
@@ -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;
index 020ffb8400a1d27666c6d78cf6a7cc0b6b572c4b..49bcc9b606402ecf13f01c4adb26d4dbce2fc7a6 100644 (file)
@@ -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;
index 0595b0b08355f23ea08b92717f622a3db0830fce..383a5a955195bec4bf510c48b0e77bbaf62e36a6 100644 (file)
@@ -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;