[multiple changes]

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

	* exp_ch9.adb (Expand_N_Asynchronous_Select): Initialize the Cancel
	flag when it is declared in order to avoid confusing CodePeer about
	the possibility of an uninitialized variable read.

2017-04-27  Ed Schonberg  <schonberg@adacore.com>

	* sem_dim.adb (Analyze_Dimension_Object_Declaration): There is
	no dimensionality error if the subtype of the expression is
	identical to the nominal subtype in the declaration, even though
	the expression itself may have been constant-folded and lack a
	dimension vector.
	* sem_dim.ads: Add comments on setting of dimension vectors and
	its interaction with node rewritings and side-effect removal.

2017-04-27  Bob Duff  <duff@adacore.com>

	* debug.adb: Minor comment correction.
	* sem_dim.ads: Minor reformatting and typo fixes.

2017-04-27  Bob Duff  <duff@adacore.com>

	* g-table.adb, g-table.adsa, scos.h: From the C side, access First and
	Last of the tables via function calls, rather than relying on layout
	of data structures.

2017-04-27  Ed Schonberg  <schonberg@adacore.com>

	* exp_util.adb: No wrapper in GNATprove mode.

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

	* sem_res.adb (Resolve_Comparison_Op): Always
	evaluate comparisons between values of universal types.

2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_elab.adb (Check_Internal_Call_Continue): Do not generate
	an elaboration counter nor a check when in GNATprove mode.
	* sem_util.adb (Build_Elaboration_Entity): Do not create an
	elaboration counter when in GNATprove mode.

From-SVN: r247317

12 files changed, 124 insertions, 24 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index f06d94e..3e64117 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,46 @@
+2017-04-27  Steve Baird  <baird@adacore.com>
+
+	* exp_ch9.adb (Expand_N_Asynchronous_Select): Initialize the Cancel
+	flag when it is declared in order to avoid confusing CodePeer about
+	the possibility of an uninitialized variable read.
+
+2017-04-27  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_dim.adb (Analyze_Dimension_Object_Declaration): There is
+	no dimensionality error if the subtype of the expression is
+	identical to the nominal subtype in the declaration, even though
+	the expression itself may have been constant-folded and lack a
+	dimension vector.
+	* sem_dim.ads: Add comments on setting of dimension vectors and
+	its interaction with node rewritings and side-effect removal.
+
+2017-04-27  Bob Duff  <duff@adacore.com>
+
+	* debug.adb: Minor comment correction.
+	* sem_dim.ads: Minor reformatting and typo fixes.
+
+2017-04-27  Bob Duff  <duff@adacore.com>
+
+	* g-table.adb, g-table.adsa, scos.h: From the C side, access First and
+	Last of the tables via function calls, rather than relying on layout
+	of data structures.
+
+2017-04-27  Ed Schonberg  <schonberg@adacore.com>
+
+	* exp_util.adb: No wrapper in GNATprove mode.
+
+2017-04-27  Yannick Moy  <moy@adacore.com>
+
+	* sem_res.adb (Resolve_Comparison_Op): Always
+	evaluate comparisons between values of universal types.
+
+2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_elab.adb (Check_Internal_Call_Continue): Do not generate
+	an elaboration counter nor a check when in GNATprove mode.
+	* sem_util.adb (Build_Elaboration_Entity): Do not create an
+	elaboration counter when in GNATprove mode.
+
 2017-04-27  Ed Schonberg  <schonberg@adacore.com>
 
 	* freeze.adb: copy-paste typo.
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index c289c98..8822265 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -848,8 +848,8 @@ package body Debug is
    --      prefer specs with no bodies to specs with bodies, and between two
    --      specs with bodies, prefers the one whose body is closer to being
    --      able to be elaborated. This is a clear improvement, but we provide
-   --      this debug flag in case of regressions. Note: -gnatdo is even older
-   --      than -gnatdp.
+   --      this debug flag in case of regressions. Note: -do is even older
+   --      than -dp.
 
    --  dp  Use old elaboration order preference. The new preference rules
    --      elaborate all units within a strongly connected component together,
diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb
index 89f9e71..6a6766d 100644
--- a/gcc/ada/exp_ch9.adb
+++ b/gcc/ada/exp_ch9.adb
@@ -7515,7 +7515,16 @@ package body Exp_Ch9 is
            Make_Object_Declaration (Loc,
              Defining_Identifier => Cancel_Param,
              Object_Definition   =>
-               New_Occurrence_Of (Standard_Boolean, Loc)));
+               New_Occurrence_Of (Standard_Boolean, Loc),
+             Expression          =>
+               New_Occurrence_Of (Standard_False, Loc),
+               --  True would work equally well here. This initialization
+               --  should be dead, but only because of things (e.g.,
+               --  abortion deferral) that CodePeer doesn't know about.
+               --  We want to avoid CodePeer complaints about a possible read
+               --  of an uninitialized variable when this variable is read,
+               --  so we initialize it here.
+             Has_Init_Expression => True));
 
          --  Remove and save the call to Call_Simple
 
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 8c05d99..c9e099e 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -1114,10 +1114,13 @@ package body Exp_Util is
             if Present (New_E) then
                Rewrite (N, New_Occurrence_Of (New_E, Sloc (N)));
 
-               --  If the entity is an overridden primitive, we must build a
-               --  wrapper for the current inherited operation.
+               --  If the entity is an overridden primitive and we are not
+               --  in proof mode, we must build a wrapper for the current
+               --  inherited operation.
 
-               if Is_Subprogram (New_E) then
+               if Is_Subprogram (New_E)
+                 and then not GNATprove_Mode
+               then
                   Needs_Wrapper := True;
                end if;
             end if;
diff --git a/gcc/ada/g-table.adb b/gcc/ada/g-table.adb
index e12e84f..c5c5891 100644
--- a/gcc/ada/g-table.adb
+++ b/gcc/ada/g-table.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---                     Copyright (C) 1998-2014, AdaCore                     --
+--                     Copyright (C) 1998-2017, AdaCore                     --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -116,6 +116,15 @@ package body GNAT.Table is
       Last_Val := Last_Val - 1;
    end Decrement_Last;
 
+   -----------
+   -- First --
+   -----------
+
+   function First return Table_Index_Type is
+   begin
+      return Table_Low_Bound;
+   end First;
+
    --------------
    -- For_Each --
    --------------
diff --git a/gcc/ada/g-table.ads b/gcc/ada/g-table.ads
index 1b4b04c4..d27b322 100644
--- a/gcc/ada/g-table.ads
+++ b/gcc/ada/g-table.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---                     Copyright (C) 1998-2015, AdaCore                     --
+--                     Copyright (C) 1998-2017, AdaCore                     --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -154,8 +154,9 @@ package GNAT.Table is
    --  Free all allocated memory for the table. A call to Init is required
    --  before any use of this table after calling Free.
 
-   First : constant Table_Index_Type := Table_Low_Bound;
-   --  Export First as synonym for Low_Bound (parallel with use of Last)
+   function First return Table_Index_Type;
+   pragma Inline (First);
+   --  Export First as synonym for Table_Low_Bound (parallel with use of Last)
 
    procedure Set_Last (New_Val : Table_Index_Type);
    pragma Inline (Set_Last);
diff --git a/gcc/ada/scos.h b/gcc/ada/scos.h
index f7b4aba..6c1f545 100644
--- a/gcc/ada/scos.h
+++ b/gcc/ada/scos.h
@@ -6,7 +6,7 @@
  *                                                                          *
  *                              C Header File                               *
  *                                                                          *
- *            Copyright (C) 2014, Free Software Foundation, Inc.            *
+ *           Copyright (C) 2014-2017, Free Software Foundation, Inc.        *
  *                                                                          *
  * GNAT is free software;  you can  redistribute it  and/or modify it under *
  * terms of the  GNU General Public License as published  by the Free Soft- *
@@ -48,11 +48,11 @@ typedef struct SCO_Unit_Table_Entry *SCO_Unit_Table_Type;
 extern SCO_Unit_Table_Type scos__sco_unit_table__table;
 #define SCO_Unit_Table scos__sco_unit_table__table
 
-extern Int scos__sco_unit_table__min;
-#define SCO_Unit_Table_Min scos__sco_unit_table__min
+extern Int scos__sco_unit_table__first(void);
+#define SCO_Unit_Table_First scos__sco_unit_table__first
 
-extern Int scos__sco_unit_table__last_val;
-#define SCO_Unit_Table_Last_Val scos__sco_unit_table__last_val
+extern Int scos__sco_unit_table__last(void);
+#define SCO_Unit_Table_Last scos__sco_unit_table__last
 
 
 /* SCOs table:  */
@@ -77,11 +77,11 @@ typedef struct SCO_Table_Entry *SCO_Table_Type;
 extern SCO_Table_Type scos__sco_table__table;
 #define SCO_Table scos__sco_table__table
 
-extern Int scos__sco_table__min;
-#define SCO_Table_Min scos__sco_table__min
+extern Int scos__sco_table__first(void);
+#define SCO_Table_First scos__sco_table__first
 
-extern Int scos__sco_table__last_val;
-#define SCO_Table_Last_Val scos__sco_table__last_val
+extern Int scos__sco_table__last(void);
+#define SCO_Table_Last scos__sco_table__last
 
 #ifdef __cplusplus
 }
diff --git a/gcc/ada/sem_dim.adb b/gcc/ada/sem_dim.adb
index 01689bf..cac2af5 100644
--- a/gcc/ada/sem_dim.adb
+++ b/gcc/ada/sem_dim.adb
@@ -2171,6 +2171,12 @@ package body Sem_Dim is
 
                Set_Dimensions (Id, Dim_Of_Expr);
 
+            --  Expression may have been constant-folded. If nominal type
+            --  has dimensions, verify that expression has same type.
+
+            elsif Exists (Dim_Of_Etyp) and then Etype (Expr) = Etyp then
+               null;
+
             --  For all other cases, issue an error message
 
             else
diff --git a/gcc/ada/sem_dim.ads b/gcc/ada/sem_dim.ads
index fc484ea..bad3bf2 100644
--- a/gcc/ada/sem_dim.ads
+++ b/gcc/ada/sem_dim.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2011-2016, Free Software Foundation, Inc.         --
+--          Copyright (C) 2011-2017, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -83,6 +83,16 @@
 --  Phase 2 is called only when the node allows a dimension (see body of
 --  Sem_Dim to get the list of nodes that permit dimensions).
 
+--  In principle every node that is a component of a floating-point expression
+--  may have a dimension vector. However, the dimensionality checking is for
+--  the most part a bottom-up tree traversal, and the dimensions of operands
+--  become irrelevant once the dimensions of an operation have been computed.
+--  To minimize space use, the dimensions of operands are removed after the
+--  computation of the dimensions of the parent operation. This may complicate
+--  the analysis of nodes that have been constant-folded or otherwise rewritten
+--  when removing side effects. In such cases, the (sub)type of the expression
+--  is used to determine the applicable dimensions.
+
 with Types; use Types;
 
 package Sem_Dim is
diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index 676c146..6bf6dfd 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -2573,9 +2573,15 @@ package body Sem_Elab is
       --  Call is not at outer level
 
       else
+         --  Do not generate elaboration checks in GNATprove mode because the
+         --  elaboration counter and the check are both forms of expansion.
+
+         if GNATprove_Mode then
+            null;
+
          --  Deal with dynamic elaboration check
 
-         if not Elaboration_Checks_Suppressed (E) then
+         elsif not Elaboration_Checks_Suppressed (E) then
             Set_Elaboration_Entity_Required (E);
 
             --  Case of no elaboration entity allocated yet
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index 383a5a9..132fe67 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6927,8 +6927,15 @@ package body Sem_Res is
       --  this Eval call may change N to True/False. Skip this evaluation
       --  inside assertions, in order to keep assertions as written by users
       --  for tools that rely on these, e.g. GNATprove for loop invariants.
-
-      if In_Assertion_Expr = 0 then
+      --  Except evaluation is still performed even inside assertions for
+      --  comparisons between values of universal type, which are useless
+      --  for static analysis tools, and not supported even by GNATprove.
+
+      if In_Assertion_Expr = 0
+        or else (Is_Universal_Numeric_Type (Etype (L))
+                   and then
+                 Is_Universal_Numeric_Type (Etype (R)))
+      then
          Eval_Relational_Op (N);
       end if;
    end Resolve_Comparison_Op;
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index e158905..200417a 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -1584,7 +1584,13 @@ package body Sem_Util is
       elsif ASIS_Mode then
          return;
 
-      --  See if we need elaboration entity.
+      --  Do not generate an elaboration entity in GNATprove move because the
+      --  elaboration counter is a form of expansion.
+
+      elsif GNATprove_Mode then
+         return;
+
+      --  See if we need elaboration entity
 
       --  We always need an elaboration entity when preserving control flow, as
       --  we want to remain explicit about the unit's elaboration order.