[multiple changes]

2017-01-19  Steve Baird  <baird@adacore.com>

	* sem_util.ads: Add new Use_Full_View Boolean parameter to
	Get_Index_Bounds.
	* sem_util.adb (Get_Index_Bounds): replace calls to Scalar_Range with
	calls to a newly-defined Scalar_Range_Of_Right_View function.

2017-01-19  Arnaud Charlet  <charlet@adacore.com>

	* gnat1drv.adb: minor fix of unbalanced parens in comment
	* lib-xref.ads (Traverse_Compilation_Unit): declaration moved
	to visible part of the package to allow re-use in GNATprove.
	* lib-xref-spark_specific.adb (Traverse_Stub): routine refactored
	from repeated code of Traverse_Compilation_Unit.
	(Traverse_Declaration_Or_Statement): fixed detection of
	generic subprograms and packages; also, iteration over case
	statement alternatives rewritten to avoid testing if the first
	alternative is present (since it must be present due to Ada
	syntax restrictions).

From-SVN: r244617

6 files changed, 115 insertions, 55 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index ee40173..55f5b1f 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,23 @@
+2017-01-19  Steve Baird  <baird@adacore.com>
+
+	* sem_util.ads: Add new Use_Full_View Boolean parameter to
+	Get_Index_Bounds.
+	* sem_util.adb (Get_Index_Bounds): replace calls to Scalar_Range with
+	calls to a newly-defined Scalar_Range_Of_Right_View function.
+
+2017-01-19  Arnaud Charlet  <charlet@adacore.com>
+
+	* gnat1drv.adb: minor fix of unbalanced parens in comment
+	* lib-xref.ads (Traverse_Compilation_Unit): declaration moved
+	to visible part of the package to allow re-use in GNATprove.
+	* lib-xref-spark_specific.adb (Traverse_Stub): routine refactored
+	from repeated code of Traverse_Compilation_Unit.
+	(Traverse_Declaration_Or_Statement): fixed detection of
+	generic subprograms and packages; also, iteration over case
+	statement alternatives rewritten to avoid testing if the first
+	alternative is present (since it must be present due to Ada
+	syntax restrictions).
+
 2017-01-19  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* exp_ch6.adb (Expand_N_Subprogram_Body): Mark the spec as
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 34aea34..057dc9e 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -1439,7 +1439,7 @@ begin
       --  are delayed till now, since it is perfectly possible for gigi to
       --  generate errors, modify the tree (in particular by setting flags
       --  indicating that elaboration is required, and also to back annotate
-      --  representation information for List_Rep_Info.
+      --  representation information for List_Rep_Info).
 
       Errout.Finalize (Last_Call => True);
       Errout.Output_Messages;
diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb
index b74489f..e7239ec 100644
--- a/gcc/ada/lib-xref-spark_specific.adb
+++ b/gcc/ada/lib-xref-spark_specific.adb
@@ -99,13 +99,6 @@ package body SPARK_Specific is
    function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range;
    --  Hash function for hash table
 
-   generic
-      with procedure Process (N : Node_Id) is <>;
-   procedure Traverse_Compilation_Unit (CU : Node_Id; Inside_Stubs : Boolean);
-   --  Call Process on all declarations within compilation unit CU. If flag
-   --  Inside_Stubs is True, then the body of stubs is also traversed. Generic
-   --  declarations are ignored.
-
    --------------------
    -- Add_SPARK_File --
    --------------------
@@ -1269,63 +1262,54 @@ package body SPARK_Specific is
       ---------------------------------------
 
       procedure Traverse_Declaration_Or_Statement (N : Node_Id) is
+         function Traverse_Stub (N : Node_Id) return Boolean;
+         --  Returns True iff stub N should be traversed
+
+         function Traverse_Stub (N : Node_Id) return Boolean is
+         begin
+            pragma Assert (Nkind_In (N, N_Package_Body_Stub,
+                                        N_Protected_Body_Stub,
+                                        N_Subprogram_Body_Stub,
+                                        N_Task_Body_Stub));
+
+            return Inside_Stubs and then Present (Library_Unit (N));
+         end Traverse_Stub;
+
+      --  Start of processing for Traverse_Declaration_Or_Statement
+
       begin
          case Nkind (N) is
             when N_Package_Declaration =>
                Traverse_Visible_And_Private_Parts (Specification (N));
 
             when N_Package_Body =>
-               if Ekind (Defining_Entity (N)) /= E_Generic_Package then
-                  Traverse_Package_Body (N);
-               end if;
+               Traverse_Package_Body (N);
 
             when N_Package_Body_Stub =>
-               if Present (Library_Unit (N)) then
-                  declare
-                     Body_N : constant Node_Id := Get_Body_From_Stub (N);
-                  begin
-                     if Inside_Stubs
-                       and then Ekind (Defining_Entity (Body_N)) /=
-                                  E_Generic_Package
-                     then
-                        Traverse_Package_Body (Body_N);
-                     end if;
-                  end;
+               if Traverse_Stub (N) then
+                  Traverse_Package_Body (Get_Body_From_Stub (N));
                end if;
 
             when N_Subprogram_Body =>
-               if not Is_Generic_Subprogram (Defining_Entity (N)) then
-                  Traverse_Subprogram_Body (N);
-               end if;
+               Traverse_Subprogram_Body (N);
 
             when N_Entry_Body =>
                Traverse_Subprogram_Body (N);
 
             when N_Subprogram_Body_Stub =>
-               if Present (Library_Unit (N)) then
-                  declare
-                     Body_N : constant Node_Id := Get_Body_From_Stub (N);
-                  begin
-                     if Inside_Stubs
-                       and then
-                         not Is_Generic_Subprogram (Defining_Entity (Body_N))
-                     then
-                        Traverse_Subprogram_Body (Body_N);
-                     end if;
-                  end;
+               if Traverse_Stub (N) then
+                  Traverse_Subprogram_Body (Get_Body_From_Stub (N));
                end if;
 
             when N_Protected_Body =>
                Traverse_Protected_Body (N);
 
             when N_Protected_Body_Stub =>
-               if Present (Library_Unit (N)) and then Inside_Stubs then
+               if Traverse_Stub (N) then
                   Traverse_Protected_Body (Get_Body_From_Stub (N));
                end if;
 
-            when N_Protected_Type_Declaration
-               | N_Single_Protected_Declaration
-            =>
+            when N_Protected_Type_Declaration =>
                Traverse_Visible_And_Private_Parts (Protected_Definition (N));
 
             when N_Task_Definition =>
@@ -1335,7 +1319,7 @@ package body SPARK_Specific is
                Traverse_Task_Body (N);
 
             when N_Task_Body_Stub =>
-               if Present (Library_Unit (N)) and then Inside_Stubs then
+               if Traverse_Stub (N) then
                   Traverse_Task_Body (Get_Body_From_Stub (N));
                end if;
 
@@ -1372,12 +1356,12 @@ package body SPARK_Specific is
                --  Process case branches
 
                declare
-                  Alt : Node_Id;
+                  Alt : Node_Id := First (Alternatives (N));
                begin
-                  Alt := First (Alternatives (N));
-                  while Present (Alt) loop
+                  loop
                      Traverse_Declarations_Or_Statements (Statements (Alt));
                      Next (Alt);
+                     exit when No (Alt);
                   end loop;
                end;
 
@@ -1458,8 +1442,18 @@ package body SPARK_Specific is
       -- Traverse_Package_Body --
       ---------------------------
 
-      procedure Traverse_Package_Body (N : Node_Id) renames
-        Traverse_Declarations_And_HSS;
+      procedure Traverse_Package_Body (N : Node_Id) is
+         Spec_E : constant Entity_Id := Unique_Defining_Entity (N);
+      begin
+         case Ekind (Spec_E) is
+            when E_Package =>
+               Traverse_Declarations_And_HSS (N);
+            when E_Generic_Package =>
+               null;
+            when others =>
+               raise Program_Error;
+         end case;
+      end Traverse_Package_Body;
 
       -----------------------------
       -- Traverse_Protected_Body --
@@ -1474,8 +1468,18 @@ package body SPARK_Specific is
       -- Traverse_Subprogram_Body --
       ------------------------------
 
-      procedure Traverse_Subprogram_Body (N : Node_Id) renames
-        Traverse_Declarations_And_HSS;
+      procedure Traverse_Subprogram_Body (N : Node_Id) is
+         Spec_E : constant Entity_Id := Unique_Defining_Entity (N);
+      begin
+         case Ekind (Spec_E) is
+            when E_Function | E_Procedure | Entry_Kind =>
+               Traverse_Declarations_And_HSS (N);
+            when Generic_Subprogram_Kind =>
+               null;
+            when others =>
+               raise Program_Error;
+         end case;
+      end Traverse_Subprogram_Body;
 
       ------------------------
       -- Traverse_Task_Body --
diff --git a/gcc/ada/lib-xref.ads b/gcc/ada/lib-xref.ads
index 4694853..3713bdb 100644
--- a/gcc/ada/lib-xref.ads
+++ b/gcc/ada/lib-xref.ads
@@ -651,6 +651,14 @@ package Lib.Xref is
       --  the information collected in the tables in library package called
       --  SPARK_Xrefs, and using routines in Lib.Util.
 
+      generic
+         with procedure Process (N : Node_Id) is <>;
+      procedure Traverse_Compilation_Unit (CU           : Node_Id;
+                                           Inside_Stubs : Boolean);
+      --  Call Process on all declarations within compilation unit CU. If
+      --  Inside_Stubs is True, then the body of stubs is also traversed.
+      --  Generic declarations are ignored.
+
    end SPARK_Specific;
 
    -----------------
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index b3a6b5b..56171e2 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -8037,10 +8037,31 @@ package body Sem_Util is
    -- Get_Index_Bounds --
    ----------------------
 
-   procedure Get_Index_Bounds (N : Node_Id; L, H : out Node_Id) is
+   procedure Get_Index_Bounds
+     (N : Node_Id;
+      L, H : out Node_Id;
+      Use_Full_View : Boolean := False)
+   is
       Kind : constant Node_Kind := Nkind (N);
       R    : Node_Id;
 
+      function Scalar_Range_Of_Right_View return Node_Id;
+      --  Call Scalar_Range with argument determined by Use_Full_View
+      --  parameter.
+
+      --------------------------------
+      -- Scalar_Range_Of_Right_View --
+      --------------------------------
+
+      function Scalar_Range_Of_Right_View return Node_Id is
+         E : Entity_Id := Entity (N);
+      begin
+         if Use_Full_View and then Present (Full_View (E)) then
+            E := Full_View (E);
+         end if;
+         return Scalar_Range (E);
+      end Scalar_Range_Of_Right_View;
+
    begin
       if Kind = N_Range then
          L := Low_Bound (N);
@@ -8060,16 +8081,16 @@ package body Sem_Util is
          end if;
 
       elsif Is_Entity_Name (N) and then Is_Type (Entity (N)) then
-         if Error_Posted (Scalar_Range (Entity (N))) then
+         if Error_Posted (Scalar_Range_Of_Right_View) then
             L := Error;
             H := Error;
 
-         elsif Nkind (Scalar_Range (Entity (N))) = N_Subtype_Indication then
-            Get_Index_Bounds (Scalar_Range (Entity (N)), L, H);
+         elsif Nkind (Scalar_Range_Of_Right_View) = N_Subtype_Indication then
+            Get_Index_Bounds (Scalar_Range_Of_Right_View, L, H);
 
          else
-            L := Low_Bound  (Scalar_Range (Entity (N)));
-            H := High_Bound (Scalar_Range (Entity (N)));
+            L := Low_Bound  (Scalar_Range_Of_Right_View);
+            H := High_Bound (Scalar_Range_Of_Right_View);
          end if;
 
       else
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index b5d1e4a..5b661c9 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -891,11 +891,18 @@ package Sem_Util is
    --  ancestor declared in a parent unit, even if there is an intermediate
    --  derivation that does not see the full view of that ancestor.
 
-   procedure Get_Index_Bounds (N : Node_Id; L, H : out Node_Id);
+   procedure Get_Index_Bounds
+     (N : Node_Id;
+      L, H : out Node_Id;
+      Use_Full_View : Boolean := False);
    --  This procedure assigns to L and H respectively the values of the low and
    --  high bounds of node N, which must be a range, subtype indication, or the
    --  name of a scalar subtype. The result in L, H may be set to Error if
    --  there was an earlier error in the range.
+   --  Use_Full_View is intended for use by clients other than the compiler
+   --  (specifically, gnat2scil) to indicate that we want the full view if
+   --  the index type turns out to be a partial view; this case should
+   --  not arise during normal compilation of semantically correct programs.
 
    function Get_Enum_Lit_From_Pos
      (T   : Entity_Id;