[multiple changes]

2014-01-22  Robert Dewar  <dewar@adacore.com>

	* sem_ch3.adb, exp_util.adb, sem_dim.adb, sem_elab.adb, sem_ch8.adb,
	sem_eval.ads: Minor reformatting.

2014-01-22  Thomas Quinot  <quinot@adacore.com>

	* sem_eval.adb (Compile_Time_Known_Bounds): Return False for
	Any_Composite to prevent cascaded errors.

2014-01-22  Yannick Moy  <moy@adacore.com>

	* errout.adb (Initialize): Do not insert special entry in Warnings
	table in GNATprove_Mode.
	* erroutc.adb (Set_Warnings_Mode_On): Add info in Warnings table in
	GNATprove_Mode.
	* gnat1drv.adb (Adjust_Global_Switches): Do not suppress frontend
	warnings anymore.

From-SVN: r206922

11 files changed, 60 insertions, 41 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 1cff347..2dca6e3 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,24 @@
 2014-01-22  Robert Dewar  <dewar@adacore.com>
 
+	* sem_ch3.adb, exp_util.adb, sem_dim.adb, sem_elab.adb, sem_ch8.adb,
+	sem_eval.ads: Minor reformatting.
+
+2014-01-22  Thomas Quinot  <quinot@adacore.com>
+
+	* sem_eval.adb (Compile_Time_Known_Bounds): Return False for
+	Any_Composite to prevent cascaded errors.
+
+2014-01-22  Yannick Moy  <moy@adacore.com>
+
+	* errout.adb (Initialize): Do not insert special entry in Warnings
+	table in GNATprove_Mode.
+	* erroutc.adb (Set_Warnings_Mode_On): Add info in Warnings table in
+	GNATprove_Mode.
+	* gnat1drv.adb (Adjust_Global_Switches): Do not suppress frontend
+	warnings anymore.
+
+2014-01-22  Robert Dewar  <dewar@adacore.com>
+
 	* sem_prag.adb (Analyze_Initializes_In_Decl_Part): Handle null
 	initializes case.
 
diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index 4d4a9f8..70a770a 100644
--- a/gcc/ada/errout.adb
+++ b/gcc/ada/errout.adb
@@ -1499,13 +1499,19 @@ package body Errout is
       Cur_Msg := No_Error_Msg;
       List_Pragmas.Init;
 
-      --  Initialize warnings table, if all warnings are suppressed, supply an
-      --  initial dummy entry covering all possible source locations.
+      --  Initialize warnings table. As an optimization, if all warnings are
+      --  suppressed, we supply an initial dummy entry covering all possible
+      --  source locations, which avoids taking into account pragma Warnings
+      --  in the source. In GNATprove_Mode, this optimization is disabled, as
+      --  we rely on the Warnings table to be correctly filled for back-end
+      --  warnings.
 
       Warnings.Init;
       Specific_Warnings.Init;
 
-      if Warning_Mode = Suppress then
+      if not GNATprove_Mode
+        and then Warning_Mode = Suppress
+      then
          Warnings.Append
            ((Start => Source_Ptr'First, Stop => Source_Ptr'Last));
       end if;
diff --git a/gcc/ada/erroutc.adb b/gcc/ada/erroutc.adb
index e2631f8..81a3c6d 100644
--- a/gcc/ada/erroutc.adb
+++ b/gcc/ada/erroutc.adb
@@ -1207,14 +1207,18 @@ package body Erroutc is
          return;
       end if;
 
-      --  Nothing to do unless command line switch to suppress all warnings
-      --  is off, and the last entry in the warnings table covers this
-      --  pragma Warnings (On), in which case adjust the end point.
+      --  Nothing to do unless command line switch to suppress all warnings is
+      --  off or we are in GNATprove_Mode, and the last entry in the warnings
+      --  table covers this pragma Warnings (On), in which case adjust the end
+      --  point.
 
       if (Warnings.Last >= Warnings.First
            and then Warnings.Table (Warnings.Last).Start <= Loc
            and then Loc <= Warnings.Table (Warnings.Last).Stop)
-        and then Warning_Mode /= Suppress
+        and then
+          (Warning_Mode /= Suppress
+             or else
+           GNATprove_Mode)
       then
          Warnings.Table (Warnings.Last).Stop := Loc;
       end if;
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index d97146c..1c5c63c 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -3422,8 +3422,8 @@ package body Exp_Util is
             --  actions, they must be added to the existing actions. The other
             --  alternative is when the new actions are related to one of the
             --  existing actions of the expression with actions, and should
-            --  never reach here: if actions are inserted on a statement within
-            --  the Actions of an expression with actions, or on some
+            --  never reach here: if actions are inserted on a statement
+            --  within the Actions of an expression with actions, or on some
             --  sub-expression of such a statement, then the outermost proper
             --  insertion point is right before the statement, and we should
             --  never climb up as far as the N_Expression_With_Actions itself.
@@ -3437,6 +3437,7 @@ package body Exp_Util is
                      Insert_List_After_And_Analyze
                        (Last (Actions (P)), Ins_Actions);
                   end if;
+
                   return;
 
                else
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index e95cbb3..ba30b4c 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -383,11 +383,6 @@ procedure Gnat1drv is
 
          Reset_Style_Check_Options;
 
-         --  Suppress compiler warnings, since what we are interested in here
-         --  is what formal verification can find out.
-
-         Warning_Mode := Suppress;
-
          --  Suppress the generation of name tables for enumerations, which are
          --  not needed for formal verification, and fall outside the SPARK
          --  subset (use of pointers).
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 5d27710..b744873 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -3637,7 +3637,7 @@ package body Sem_Ch3 is
          if No (E) then
             Act_T := Build_Default_Subtype (T, N);
          else
-            --  Ada 2005:  a limited object may be initialized by means of an
+            --  Ada 2005: a limited object may be initialized by means of an
             --  aggregate. If the type has default discriminants it has an
             --  unconstrained nominal type, Its actual subtype will be obtained
             --  from the aggregate, and not from the default discriminants.
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index bcf06a7..a766866 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -5981,21 +5981,18 @@ package body Sem_Ch8 is
       begin
          Comp_Unit := N;
          while Present (Comp_Unit)
-            and then Nkind (Comp_Unit) /= N_Compilation_Unit
+           and then Nkind (Comp_Unit) /= N_Compilation_Unit
          loop
             Comp_Unit := Parent (Comp_Unit);
          end loop;
 
-         if No (Comp_Unit)
-           or else Nkind (Unit (Comp_Unit)) /= N_Subunit
-         then
+         if No (Comp_Unit) or else Nkind (Unit (Comp_Unit)) /= N_Subunit then
             return False;
          end if;
 
          --  Now check whether the package is in the context of the subunit
 
          Clause := First (Context_Items (Comp_Unit));
-
          while Present (Clause) loop
             if Nkind (Clause) = N_With_Clause
               and then Entity (Name (Clause)) = P_Name
@@ -6009,6 +6006,8 @@ package body Sem_Ch8 is
          return False;
       end Is_Reference_In_Subunit;
 
+   --  Start of processing for Find_Selected_Component
+
    begin
       Analyze (P);
 
@@ -6036,9 +6035,7 @@ package body Sem_Ch8 is
       --  in the expansion of record equality).
 
       if Present (Entity (Selector_Name (N))) then
-         if No (Etype (N))
-           or else Etype (N) = Any_Type
-         then
+         if No (Etype (N)) or else Etype (N) = Any_Type then
             declare
                Sel_Name : constant Node_Id   := Selector_Name (N);
                Selector : constant Entity_Id := Entity (Sel_Name);
@@ -6065,8 +6062,7 @@ package body Sem_Ch8 is
                      Save_Interps (P, Nam);
                   end if;
 
-                  Rewrite (P,
-                    Make_Function_Call (Sloc (P), Name => Nam));
+                  Rewrite (P, Make_Function_Call (Sloc (P), Name => Nam));
                   Analyze_Call (P);
                   Analyze_Selected_Component (N);
                   return;
@@ -6088,13 +6084,12 @@ package body Sem_Ch8 is
                       ((RTE_Available (RE_Dispatch_Table_Wrapper)
                          and then Scope (Selector) =
                                      RTE (RE_Dispatch_Table_Wrapper))
-                         or else
-                           (RTE_Available (RE_No_Dispatch_Table_Wrapper)
-                             and then Scope (Selector) =
-                                        RTE (RE_No_Dispatch_Table_Wrapper)))
+                        or else
+                          (RTE_Available (RE_No_Dispatch_Table_Wrapper)
+                            and then Scope (Selector) =
+                                     RTE (RE_No_Dispatch_Table_Wrapper)))
                   then
                      C_Etype := Empty;
-
                   else
                      C_Etype :=
                        Build_Actual_Subtype_Of_Component
@@ -6292,10 +6287,8 @@ package body Sem_Ch8 is
                      if Present (P_Name) then
                         if not Is_Reference_In_Subunit then
                            Error_Msg_Sloc := Sloc (Entity (Prefix (N)));
-
                            Error_Msg_NE
-                             ("package& is hidden by declaration#",
-                               N, P_Name);
+                             ("package& is hidden by declaration#", N, P_Name);
                         end if;
 
                         Set_Entity (Prefix (N), P_Name);
diff --git a/gcc/ada/sem_dim.adb b/gcc/ada/sem_dim.adb
index 3d010f7..7c29784 100644
--- a/gcc/ada/sem_dim.adb
+++ b/gcc/ada/sem_dim.adb
@@ -1908,10 +1908,11 @@ package body Sem_Dim is
       elsif Nkind (N) = N_Identifier then
          Analyze_Dimension_Identifier : declare
             Id : constant Entity_Id := Entity (N);
+
          begin
-            if No (Id) then
-               --  Abnormal tree, assume previous error
+            --  If Id is missing, abnormal tree, assume previous error
 
+            if No (Id) then
                Check_Error_Detected;
                return;
 
diff --git a/gcc/ada/sem_elab.adb b/gcc/ada/sem_elab.adb
index d3f9b91..b0b4534 100644
--- a/gcc/ada/sem_elab.adb
+++ b/gcc/ada/sem_elab.adb
@@ -2917,11 +2917,11 @@ package body Sem_Elab is
 
       --  Build check node, possibly with condition
 
-      Chk := Make_Raise_Program_Error (Loc,
-               Reason => PE_Access_Before_Elaboration);
+      Chk :=
+        Make_Raise_Program_Error (Loc, Reason => PE_Access_Before_Elaboration);
+
       if Present (C) then
-         Set_Condition (Chk,
-           Make_Op_Not (Loc, Right_Opnd => C));
+         Set_Condition (Chk, Make_Op_Not (Loc, Right_Opnd => C));
       end if;
 
       --  If we are inserting at the top level, insert in Aux_Decls
diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb
index 8f7eff4..920ee7c 100644
--- a/gcc/ada/sem_eval.adb
+++ b/gcc/ada/sem_eval.adb
@@ -1259,7 +1259,7 @@ package body Sem_Eval is
       Typ  : Entity_Id;
 
    begin
-      if not Is_Array_Type (T) then
+      if T = Any_Composite or else not Is_Array_Type (T) then
          return False;
       end if;
 
diff --git a/gcc/ada/sem_eval.ads b/gcc/ada/sem_eval.ads
index aee03d9..fb1ebfa 100644
--- a/gcc/ada/sem_eval.ads
+++ b/gcc/ada/sem_eval.ads
@@ -282,7 +282,7 @@ package Sem_Eval is
 
    function Compile_Time_Known_Bounds (T : Entity_Id) return Boolean;
    --  If T is an array whose index bounds are all known at compile time, then
-   --  True is returned, if T is not an array, or one or more of its index
+   --  True is returned. If T is not an array type, or one or more of its index
    --  bounds is not known at compile time, then False is returned.
 
    function Expr_Value (N : Node_Id) return Uint;