2016-06-22 Hristian Kirtchev <kirtchev@adacore.com>

	* lib-xref-spark_specific.adb, checks.adb, sem_ch13.adb: Minor
	reformatting.
	* exp_ch7.adb: Minor typo fix.
	* lib.ads (Get_Top_Level_Code_Unit): Add comment.

2016-06-22  Bob Duff  <duff@adacore.com>

	* s-tassta.adb (Task_Wrapper): Fix handling of Fall_Back_Handler
	wrt independent tasks.

2016-06-22  Ed Schonberg  <schonberg@adacore.com>

	* sem_dim.adb (Analyze_Dimension): Propagate dimension for
	explicit_dereference nodes when they do not come from source,
	to handle correctly dimensional analysis on iterators over
	containers whose elements have declared dimensions.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@237691 138bc75d-0d04-0410-961f-82ee72b054a4

8 files changed, 260 insertions, 219 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index b6d23ea146e..6d4bf1ed76d 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,22 @@
+2016-06-22  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* lib-xref-spark_specific.adb, checks.adb, sem_ch13.adb: Minor
+	reformatting.
+	* exp_ch7.adb: Minor typo fix.
+	* lib.ads (Get_Top_Level_Code_Unit): Add comment.
+
+2016-06-22  Bob Duff  <duff@adacore.com>
+
+	* s-tassta.adb (Task_Wrapper): Fix handling of Fall_Back_Handler
+	wrt independent tasks.
+
+2016-06-22  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_dim.adb (Analyze_Dimension): Propagate dimension for
+	explicit_dereference nodes when they do not come from source,
+	to handle correctly dimensional analysis on iterators over
+	containers whose elements have declared dimensions.
+
 2016-06-22  Arnaud Charlet  <charlet@adacore.com>
 
 	* spark_xrefs.ads (Scope_Num): type refined to positive integers.
diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index 157bd065bd9..cde455f7b51 100644
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -635,17 +635,15 @@ package body Checks is
    procedure Apply_Address_Clause_Check (E : Entity_Id; N : Node_Id) is
       pragma Assert (Nkind (N) = N_Freeze_Entity);
 
-      AC   : constant Node_Id    := Address_Clause (E);
-      Loc  : constant Source_Ptr := Sloc (AC);
-      Typ  : constant Entity_Id  := Etype (E);
+      AC  : constant Node_Id    := Address_Clause (E);
+      Loc : constant Source_Ptr := Sloc (AC);
+      Typ : constant Entity_Id  := Etype (E);
 
       Expr : Node_Id;
       --  Address expression (not necessarily the same as Aexp, for example
       --  when Aexp is a reference to a constant, in which case Expr gets
       --  reset to reference the value expression of the constant).
 
-   --  Start of processing for Apply_Address_Clause_Check
-
    begin
       --  See if alignment check needed. Note that we never need a check if the
       --  maximum alignment is one, since the check will always succeed.
@@ -679,8 +677,8 @@ package body Checks is
             AL : Uint := Alignment (Typ);
 
          begin
-            --  The object alignment might be more restrictive than the
-            --  type alignment.
+            --  The object alignment might be more restrictive than the type
+            --  alignment.
 
             if Known_Alignment (E) then
                AL := Alignment (E);
@@ -718,9 +716,9 @@ package body Checks is
       --  Generate a check to raise PE if alignment may be inappropriate
 
       else
-         --  If the original expression is a non-static constant, use the
-         --  name of the constant itself rather than duplicating its
-         --  defining expression, which was extracted above.
+         --  If the original expression is a non-static constant, use the name
+         --  of the constant itself rather than duplicating its initialization
+         --  expression, which was extracted above.
 
          --  Note: Expr is empty if the address-clause is applied to in-mode
          --  actuals (allowed by 13.1(22)).
@@ -729,8 +727,8 @@ package body Checks is
            or else
              (Is_Entity_Name (Expression (AC))
                and then Ekind (Entity (Expression (AC))) = E_Constant
-               and then Nkind (Parent (Entity (Expression (AC))))
-                                 = N_Object_Declaration)
+               and then Nkind (Parent (Entity (Expression (AC)))) =
+                          N_Object_Declaration)
          then
             Expr := New_Copy_Tree (Expression (AC));
          else
@@ -745,9 +743,9 @@ package body Checks is
            Make_Raise_Program_Error (Loc,
              Condition =>
                Make_Op_Ne (Loc,
-                 Left_Opnd =>
+                 Left_Opnd  =>
                    Make_Op_Mod (Loc,
-                     Left_Opnd =>
+                     Left_Opnd  =>
                        Unchecked_Convert_To
                          (RTE (RE_Integer_Address), Expr),
                      Right_Opnd =>
@@ -755,7 +753,7 @@ package body Checks is
                          Prefix         => New_Occurrence_Of (E, Loc),
                          Attribute_Name => Name_Alignment)),
                  Right_Opnd => Make_Integer_Literal (Loc, Uint_0)),
-                       Reason    => PE_Misaligned_Address_Value));
+             Reason    => PE_Misaligned_Address_Value));
 
          Warning_Msg := No_Error_Msg;
          Analyze (First (Actions (N)), Suppress => All_Checks);
@@ -765,6 +763,7 @@ package body Checks is
          --  No_Exception_Propagation).
 
          if Warning_Msg /= No_Error_Msg then
+
             --  If the expression has a known at compile time value, then
             --  once we know the alignment of the type, we can check if the
             --  exception will be raised or not, and if not, we don't need
@@ -773,12 +772,13 @@ package body Checks is
             if Compile_Time_Known_Value (Expr) then
                Alignment_Warnings.Append
                  ((E => E, A => Expr_Value (Expr), W => Warning_Msg));
-            else
-               --  Add explanation of the warning generated by the check
 
+            --  Add explanation of the warning generated by the check
+
+            else
                Error_Msg_N
-                 ("\address value may be incompatible with alignment "
-                  & "of object?X?", AC);
+                 ("\address value may be incompatible with alignment of "
+                  & "object?X?", AC);
             end if;
          end if;
 
@@ -786,6 +786,7 @@ package body Checks is
       end if;
 
    exception
+
       --  If we have some missing run time component in configurable run time
       --  mode then just skip the check (it is not required in any case).
 
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 31522370058..f46f57ec321 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -4616,7 +4616,7 @@ package body Exp_Ch7 is
       Set_Ghost_Mode_From_Entity (Work_Typ);
 
       --  Emulate the environment of the invariant procedure by installing
-      --  its scope and formal parameters. Note that this is not need, but
+      --  its scope and formal parameters. Note that this is not needed, but
       --  having the scope of the invariant procedure installed helps with
       --  the detection of invariant-related errors.
 
diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb
index 3e5026bb1d1..28b167cea5a 100644
--- a/gcc/ada/lib-xref-spark_specific.adb
+++ b/gcc/ada/lib-xref-spark_specific.adb
@@ -54,9 +54,9 @@ package body SPARK_Specific is
    --  True for each reference type used in SPARK
 
    SPARK_References : constant array (Character) of Boolean :=
-     ('m' => True,
-      'r' => True,
-      's' => True,
+     ('m'    => True,
+      'r'    => True,
+      's'    => True,
       others => False);
 
    type Entity_Hashed_Range is range 0 .. 255;
@@ -102,9 +102,9 @@ package body SPARK_Specific is
    generic
       with procedure Process (N : Node_Id) is <>;
    procedure Traverse_Compilation_Unit (CU : Node_Id; Inside_Stubs : Boolean);
-   --  Call Process on all declarations in compilation unit CU. If
-   --  Inside_Stubs is True, then the body of stubs is also traversed.
-   --  Generic declarations are ignored.
+   --  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 --
@@ -114,9 +114,6 @@ package body SPARK_Specific is
       File : constant Source_File_Index := Source_Index (Uspec);
       From : constant Scope_Index       := SPARK_Scope_Table.Last + 1;
 
-      File_Name      : String_Ptr;
-      Unit_File_Name : String_Ptr;
-
       Scope_Id : Pos := 1;
 
       procedure Add_SPARK_Scope (N : Node_Id);
@@ -147,49 +144,46 @@ package body SPARK_Specific is
          end if;
 
          case Ekind (E) is
-         when E_Entry
-            | E_Entry_Family
-            | E_Generic_Function
-            | E_Generic_Package
-            | E_Generic_Procedure
-            | E_Package
-            | E_Protected_Type
-            | E_Task_Type
-            =>
-            Typ := Xref_Entity_Letters (Ekind (E));
-
-         when E_Function
-            | E_Procedure
-            =>
-            --  In SPARK we need to distinguish protected functions and
-            --  procedures from ordinary subprograms, but there are no special
-            --  Xref letters for them. Since this distiction is only needed to
-            --  detect protected calls, we pretend that such calls are entry
-            --  calls.
-
-            if Ekind (Scope (E)) = E_Protected_Type then
-               Typ := Xref_Entity_Letters (E_Entry);
-            else
+            when E_Entry             |
+                 E_Entry_Family      |
+                 E_Generic_Function  |
+                 E_Generic_Package   |
+                 E_Generic_Procedure |
+                 E_Package           |
+                 E_Protected_Type    |
+                 E_Task_Type         =>
                Typ := Xref_Entity_Letters (Ekind (E));
-            end if;
 
-         when E_Package_Body
-            | E_Protected_Body
-            | E_Subprogram_Body
-            | E_Task_Body
-            =>
-            Typ := Xref_Entity_Letters (Ekind (Unique_Entity (E)));
+            when E_Function | E_Procedure =>
 
-         when E_Void =>
+               --  In SPARK we need to distinguish protected functions and
+               --  procedures from ordinary subprograms, but there are no
+               --  special Xref letters for them. Since this distiction is
+               --  only needed to detect protected calls, we pretend that
+               --  such calls are entry calls.
 
-            --  Compilation of prj-attr.adb with -gnatn creates a node with
-            --  entity E_Void for the package defined at a-charac.ads16:13.
-            --  ??? TBD
+               if Ekind (Scope (E)) = E_Protected_Type then
+                  Typ := Xref_Entity_Letters (E_Entry);
+               else
+                  Typ := Xref_Entity_Letters (Ekind (E));
+               end if;
 
-            return;
+            when E_Package_Body    |
+                 E_Protected_Body  |
+                 E_Subprogram_Body |
+                 E_Task_Body       =>
+               Typ := Xref_Entity_Letters (Ekind (Unique_Entity (E)));
+
+            when E_Void =>
+
+               --  Compilation of prj-attr.adb with -gnatn creates a node with
+               --  entity E_Void for the package defined at a-charac.ads16:13.
+               --  ??? TBD
 
-         when others =>
-            raise Program_Error;
+               return;
+
+            when others =>
+               raise Program_Error;
          end case;
 
          --  File_Num and Scope_Num are filled later. From_Xref and To_Xref
@@ -218,24 +212,32 @@ package body SPARK_Specific is
 
       procedure Detect_And_Add_SPARK_Scope (N : Node_Id) is
       begin
-         if Nkind_In (N, N_Entry_Body,             --  entries
-                      N_Entry_Declaration)
-           or else
-             Nkind_In (N, N_Package_Body,           --  packages
-                       N_Package_Body_Stub,
-                       N_Package_Declaration)
-           or else
-             Nkind_In (N, N_Protected_Body,         --  protected objects
-                       N_Protected_Body_Stub,
-                       N_Protected_Type_Declaration)
-           or else
-             Nkind_In (N, N_Subprogram_Body,        --  subprograms
-                       N_Subprogram_Body_Stub,
-                       N_Subprogram_Declaration)
-           or else
-             Nkind_In (N, N_Task_Body,              --  tasks
-                       N_Task_Body_Stub,
-                       N_Task_Type_Declaration)
+         --  Entries
+
+         if Nkind_In (N, N_Entry_Body, N_Entry_Declaration)
+
+           --  Packages
+
+           or else Nkind_In (N, N_Package_Body,
+                                N_Package_Body_Stub,
+                                N_Package_Declaration)
+           --  Protected units
+
+           or else Nkind_In (N, N_Protected_Body,
+                                N_Protected_Body_Stub,
+                                N_Protected_Type_Declaration)
+
+           --  Subprograms
+
+           or else Nkind_In (N, N_Subprogram_Body,
+                                N_Subprogram_Body_Stub,
+                                N_Subprogram_Declaration)
+
+           --  Task units
+
+           or else Nkind_In (N, N_Task_Body,
+                                N_Task_Body_Stub,
+                                N_Task_Type_Declaration)
          then
             Add_SPARK_Scope (N);
          end if;
@@ -244,6 +246,11 @@ package body SPARK_Specific is
       procedure Traverse_Scopes is new
         Traverse_Compilation_Unit (Detect_And_Add_SPARK_Scope);
 
+      --  Local variables
+
+      File_Name      : String_Ptr;
+      Unit_File_Name : String_Ptr;
+
    --  Start of processing for Add_SPARK_File
 
    begin
@@ -307,6 +314,9 @@ package body SPARK_Specific is
       function Get_Entity_Type (E : Entity_Id) return Character;
       --  Return a character representing the type of entity
 
+      function Get_Scope_Num (N : Entity_Id) return Nat;
+      --  Return the scope number associated to entity N
+
       function Is_Constant_Object_Without_Variable_Input
         (E : Entity_Id) return Boolean;
       --  Return True if E is known to have no variable input, as defined in
@@ -333,6 +343,9 @@ package body SPARK_Specific is
       procedure Move (From : Natural; To : Natural);
       --  Move procedure for Sort call
 
+      procedure Set_Scope_Num (N : Entity_Id; Num : Nat);
+      --  Associate entity N to scope number Num
+
       procedure Update_Scope_Range
         (S    : Scope_Index;
          From : Xref_Index;
@@ -341,12 +354,6 @@ package body SPARK_Specific is
 
       package Sorting is new GNAT.Heap_Sort_G (Move, Lt);
 
-      function Get_Scope_Num (N : Entity_Id) return Nat;
-      --  Return the scope number associated to entity N
-
-      procedure Set_Scope_Num (N : Entity_Id; Num : Nat);
-      --  Associate entity N to scope number Num
-
       No_Scope : constant Nat := 0;
       --  Initial scope counter
 
@@ -551,7 +558,7 @@ package body SPARK_Specific is
       -- Lt --
       --------
 
-      function Lt (Op1, Op2 : Natural) return Boolean is
+      function Lt (Op1 : Natural; Op2 : Natural) return Boolean is
          T1 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op1)));
          T2 : constant Xref_Entry := Xrefs.Table (Rnums (Nat (Op2)));
 
@@ -767,9 +774,7 @@ package body SPARK_Specific is
          Nrefs     := 1;
 
          for Index in 2 .. Ref_Count loop
-            if Xrefs.Table (Rnums (Index)) /=
-               Xrefs.Table (Rnums (Nrefs))
-            then
+            if Xrefs.Table (Rnums (Index)) /= Xrefs.Table (Rnums (Nrefs)) then
                Nrefs := Nrefs + 1;
                Rnums (Nrefs) := Rnums (Index);
             end if;
@@ -900,7 +905,8 @@ package body SPARK_Specific is
      (Sdep_Table : Unit_Ref_Table;
       Num_Sdep   : Nat)
    is
-      Sdep, Sdep_Next : Pos;
+      Sdep      : Pos;
+      Sdep_Next : Pos;
       --  Index of the current and next source dependency
 
       Sdep_File : Pos;
@@ -908,7 +914,8 @@ package body SPARK_Specific is
       --  library-level instances of generic units this points to the unit
       --  of the body, because this is where references are assigned to.
 
-      Uspec, Ubody : Unit_Number_Type;
+      Ubody : Unit_Number_Type;
+      Uspec : Unit_Number_Type;
       --  Unit numbers for the dependency spec and possibly its body (only in
       --  the case of library-level instance of a generic package).
 
@@ -936,20 +943,22 @@ package body SPARK_Specific is
             declare
                Cunit1 : Node_Id renames Cunit (Sdep_Table (Sdep));
                Cunit2 : Node_Id renames Cunit (Sdep_Table (Sdep + 1));
+
             begin
                --  Both Cunit point to compilation unit nodes
-               pragma Assert (Nkind (Cunit1) = N_Compilation_Unit
-                                and then
-                              Nkind (Cunit2) = N_Compilation_Unit);
+
+               pragma Assert
+                 (Nkind (Cunit1) = N_Compilation_Unit
+                   and then Nkind (Cunit2) = N_Compilation_Unit);
 
                --  Do not depend on the sorting order, which is based on
                --  Unit_Name and for library-level instances of nested
                --  generic-packages they are equal.
 
                --  If declaration comes before the body
+
                if Nkind (Unit (Cunit1)) = N_Package_Declaration
-                 and then
-                  Nkind (Unit (Cunit2)) = N_Package_Body
+                 and then Nkind (Unit (Cunit2)) = N_Package_Body
                then
                   Uspec := Sdep_Table (Sdep);
                   Ubody := Sdep_Table (Sdep + 1);
@@ -959,8 +968,7 @@ package body SPARK_Specific is
                --  If body comes before declaration
 
                elsif Nkind (Unit (Cunit1)) = N_Package_Body
-                       and then
-                     Nkind (Unit (Cunit2)) = N_Package_Declaration
+                 and then Nkind (Unit (Cunit2)) = N_Package_Declaration
                then
                   Uspec := Sdep_Table (Sdep + 1);
                   Ubody := Sdep_Table (Sdep);
@@ -970,18 +978,19 @@ package body SPARK_Specific is
                --  Otherwise it is an error
 
                else
-
                   raise Program_Error;
                end if;
 
                Sdep_Next := Sdep + 2;
             end;
+
+         --  ??? otherwise?
+
          else
             Uspec := Sdep_Table (Sdep);
             Ubody := No_Unit;
 
             Sdep_File := Sdep;
-
             Sdep_Next := Sdep + 1;
          end if;
 
@@ -1191,7 +1200,6 @@ package body SPARK_Specific is
    --  Start of processing for Generate_Dereference
 
    begin
-
       if Loc > No_Location then
          Drefs.Increment_Last;
 
@@ -1234,11 +1242,9 @@ package body SPARK_Specific is
      (CU           : Node_Id;
       Inside_Stubs : Boolean)
    is
-      Lu : Node_Id;
-
       procedure Traverse_Block                      (N : Node_Id);
-      procedure Traverse_Declarations_And_HSS       (N : Node_Id);
       procedure Traverse_Declaration_Or_Statement   (N : Node_Id);
+      procedure Traverse_Declarations_And_HSS       (N : Node_Id);
       procedure Traverse_Declarations_Or_Statements (L : List_Id);
       procedure Traverse_Handled_Statement_Sequence (N : Node_Id);
       procedure Traverse_Package_Body               (N : Node_Id);
@@ -1260,133 +1266,129 @@ package body SPARK_Specific is
       -- Traverse_Declaration_Or_Statement --
       ---------------------------------------
 
-      procedure Traverse_Declaration_Or_Statement (N : Node_Id)
-      is
+      procedure Traverse_Declaration_Or_Statement (N : Node_Id) is
       begin
          case Nkind (N) is
-         when N_Package_Declaration =>
-            Traverse_Visible_And_Private_Parts (Specification (N));
+            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;
+            when N_Package_Body =>
+               if Ekind (Defining_Entity (N)) /= E_Generic_Package then
+                  Traverse_Package_Body (N);
+               end if;
 
-         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;
-            end if;
+            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;
+               end if;
 
-         when N_Subprogram_Body =>
-            if not Is_Generic_Subprogram (Defining_Entity (N)) then
-               Traverse_Subprogram_Body (N);
-            end if;
+            when N_Subprogram_Body =>
+               if not Is_Generic_Subprogram (Defining_Entity (N)) then
+                  Traverse_Subprogram_Body (N);
+               end if;
 
-         when N_Entry_Body =>
-            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;
-            end if;
+            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;
+               end if;
 
-         when N_Protected_Body =>
-            Traverse_Protected_Body (N);
+            when N_Protected_Body =>
+               Traverse_Protected_Body (N);
 
-         when N_Protected_Body_Stub =>
-            if Present (Library_Unit (N)) then
-               if Inside_Stubs then
+            when N_Protected_Body_Stub =>
+               if Present (Library_Unit (N)) and then Inside_Stubs then
                   Traverse_Protected_Body (Get_Body_From_Stub (N));
                end if;
-            end if;
 
-         when N_Protected_Type_Declaration | N_Single_Protected_Declaration =>
-            Traverse_Visible_And_Private_Parts (Protected_Definition (N));
+            when N_Protected_Type_Declaration   |
+                 N_Single_Protected_Declaration =>
+               Traverse_Visible_And_Private_Parts (Protected_Definition (N));
 
-         when N_Task_Definition =>
-            Traverse_Visible_And_Private_Parts (N);
+            when N_Task_Definition =>
+               Traverse_Visible_And_Private_Parts (N);
 
-         when N_Task_Body =>
-            Traverse_Task_Body (N);
+            when N_Task_Body =>
+               Traverse_Task_Body (N);
 
-         when N_Task_Body_Stub =>
-            if Present (Library_Unit (N)) then
-               if Inside_Stubs then
+            when N_Task_Body_Stub =>
+               if Present (Library_Unit (N)) and then Inside_Stubs then
                   Traverse_Task_Body (Get_Body_From_Stub (N));
                end if;
-            end if;
 
-         when N_Block_Statement =>
-            Traverse_Block (N);
+            when N_Block_Statement =>
+               Traverse_Block (N);
 
-         when N_If_Statement =>
+            when N_If_Statement =>
 
-            --  Traverse the statements in the THEN part
+               --  Traverse the statements in the THEN part
 
-            Traverse_Declarations_Or_Statements (Then_Statements (N));
+               Traverse_Declarations_Or_Statements (Then_Statements (N));
 
-            --  Loop through ELSIF parts if present
+               --  Loop through ELSIF parts if present
 
-            if Present (Elsif_Parts (N)) then
-               declare
-                  Elif : Node_Id := First (Elsif_Parts (N));
+               if Present (Elsif_Parts (N)) then
+                  declare
+                     Elif : Node_Id := First (Elsif_Parts (N));
 
-               begin
-                  while Present (Elif) loop
-                     Traverse_Declarations_Or_Statements
-                       (Then_Statements (Elif));
-                     Next (Elif);
-                  end loop;
-               end;
-            end if;
+                  begin
+                     while Present (Elif) loop
+                        Traverse_Declarations_Or_Statements
+                          (Then_Statements (Elif));
+                        Next (Elif);
+                     end loop;
+                  end;
+               end if;
 
-            --  Finally traverse the ELSE statements if present
+               --  Finally traverse the ELSE statements if present
 
-            Traverse_Declarations_Or_Statements (Else_Statements (N));
+               Traverse_Declarations_Or_Statements (Else_Statements (N));
 
-         when N_Case_Statement =>
+            when N_Case_Statement =>
 
-            --  Process case branches
+               --  Process case branches
 
-            declare
-               Alt : Node_Id;
-            begin
-               Alt := First (Alternatives (N));
-               while Present (Alt) loop
-                  Traverse_Declarations_Or_Statements (Statements (Alt));
-                  Next (Alt);
-               end loop;
-            end;
+               declare
+                  Alt : Node_Id;
+               begin
+                  Alt := First (Alternatives (N));
+                  while Present (Alt) loop
+                     Traverse_Declarations_Or_Statements (Statements (Alt));
+                     Next (Alt);
+                  end loop;
+               end;
 
-         when N_Extended_Return_Statement =>
-            Traverse_Handled_Statement_Sequence
-              (Handled_Statement_Sequence (N));
+            when N_Extended_Return_Statement =>
+               Traverse_Handled_Statement_Sequence
+                 (Handled_Statement_Sequence (N));
 
-         when N_Loop_Statement =>
-            Traverse_Declarations_Or_Statements (Statements (N));
+            when N_Loop_Statement =>
+               Traverse_Declarations_Or_Statements (Statements (N));
 
-            --  Generic declarations are ignored
+               --  Generic declarations are ignored
 
-         when others =>
-            null;
+            when others =>
+               null;
          end case;
       end Traverse_Declaration_Or_Statement;
 
@@ -1394,8 +1396,7 @@ package body SPARK_Specific is
       -- Traverse_Declarations_And_HSS --
       -----------------------------------
 
-      procedure Traverse_Declarations_And_HSS (N : Node_Id)
-      is
+      procedure Traverse_Declarations_And_HSS (N : Node_Id) is
       begin
          Traverse_Declarations_Or_Statements (Declarations (N));
          Traverse_Handled_Statement_Sequence (Handled_Statement_Sequence (N));
@@ -1405,8 +1406,7 @@ package body SPARK_Specific is
       -- Traverse_Declarations_Or_Statements --
       -----------------------------------------
 
-      procedure Traverse_Declarations_Or_Statements (L : List_Id)
-      is
+      procedure Traverse_Declarations_Or_Statements (L : List_Id) is
          N : Node_Id;
 
       begin
@@ -1414,13 +1414,12 @@ package body SPARK_Specific is
 
          N := First (L);
          while Present (N) loop
+
             --  Call Process on all declarations
 
             if Nkind (N) in N_Declaration
-              or else
-                Nkind (N) in N_Later_Decl_Item
-              or else
-                Nkind (N) = N_Entry_Body
+              or else Nkind (N) in N_Later_Decl_Item
+              or else Nkind (N) = N_Entry_Body
             then
                Process (N);
             end if;
@@ -1435,8 +1434,7 @@ package body SPARK_Specific is
       -- Traverse_Handled_Statement_Sequence --
       -----------------------------------------
 
-      procedure Traverse_Handled_Statement_Sequence (N : Node_Id)
-      is
+      procedure Traverse_Handled_Statement_Sequence (N : Node_Id) is
          Handler : Node_Id;
 
       begin
@@ -1483,12 +1481,20 @@ package body SPARK_Specific is
       procedure Traverse_Task_Body (N : Node_Id) renames
         Traverse_Declarations_And_HSS;
 
+      ----------------------------------------
+      -- Traverse_Visible_And_Private_Parts --
+      ----------------------------------------
+
       procedure Traverse_Visible_And_Private_Parts (N : Node_Id) is
       begin
          Traverse_Declarations_Or_Statements (Visible_Declarations (N));
          Traverse_Declarations_Or_Statements (Private_Declarations (N));
       end Traverse_Visible_And_Private_Parts;
 
+      --  Local variables
+
+      Lu : Node_Id;
+
    --  Start of processing for Traverse_Compilation_Unit
 
    begin
diff --git a/gcc/ada/lib.ads b/gcc/ada/lib.ads
index 4f8ffee3a29..c54e2ca180a 100644
--- a/gcc/ada/lib.ads
+++ b/gcc/ada/lib.ads
@@ -548,6 +548,12 @@ package Lib is
    --  This is like Get_Code_Unit, except that in the case of subunits, it
    --  returns the top-level unit to which the subunit belongs instead of
    --  the subunit.
+   --
+   --  Note: for nodes and slocs in declarations of library-level instances of
+   --  generics these routines wrongly return the unit number corresponding to
+   --  the body of the instance. In effect, locations of SPARK references in
+   --  ALI files are bogus. However, fixing this is not worth the effort, since
+   --  these references are only used for debugging.
 
    function In_Extended_Main_Code_Unit
      (N : Node_Or_Entity_Id) return Boolean;
diff --git a/gcc/ada/s-tassta.adb b/gcc/ada/s-tassta.adb
index 947e5aca994..7566629ebe0 100644
--- a/gcc/ada/s-tassta.adb
+++ b/gcc/ada/s-tassta.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                  B o d y                                 --
 --                                                                          --
---         Copyright (C) 1992-2014, Free Software Foundation, Inc.          --
+--         Copyright (C) 1992-2016, Free Software Foundation, Inc.          --
 --                                                                          --
 -- GNARL 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- --
@@ -1339,7 +1339,13 @@ package body System.Tasking.Stages is
 
       if Self_ID.Common.Specific_Handler /= null then
          TH := Self_ID.Common.Specific_Handler;
-      else
+
+      --  Independent tasks should not call the Fall_Back_Handler (of the
+      --  environment task), because they are implementation artifacts that
+      --  should be invisible to Ada programs.
+
+      elsif Self_ID.Master_of_Task /= Independent_Task_Level then
+
          --  Look for a fall-back handler following the master relationship
          --  for the task. As specified in ARM C.7.3 par. 9/2, "the fall-back
          --  handler applies only to the dependent tasks of the task". Hence,
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 3c1c1b69e1a..6896dac2586 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -13204,11 +13204,11 @@ package body Sem_Ch13 is
                --  Get alignments, sizes and offset, if any
 
                X_Alignment := Alignment (ACCR.X);
-               X_Size := Esize (ACCR.X);
+               X_Size      := Esize (ACCR.X);
 
                if Present (ACCR.Y) then
                   Y_Alignment := Alignment (ACCR.Y);
-                  Y_Size := Esize (ACCR.Y);
+                  Y_Size      := Esize (ACCR.Y);
                end if;
 
                if ACCR.Off
diff --git a/gcc/ada/sem_dim.adb b/gcc/ada/sem_dim.adb
index cabb01347fc..2bdf9e5a2c4 100644
--- a/gcc/ada/sem_dim.adb
+++ b/gcc/ada/sem_dim.adb
@@ -1121,13 +1121,15 @@ package body Sem_Dim is
    begin
       --  Aspect is an Ada 2012 feature. Note that there is no need to check
       --  dimensions for nodes that don't come from source, except for subtype
-      --  declarations where the dimensions are inherited from the base type.
+      --  declarations where the dimensions are inherited from the base type,
+      --  and for explicit dereferences generated when expanding iterators.
 
       if Ada_Version < Ada_2012 then
          return;
 
       elsif not Comes_From_Source (N)
         and then Nkind (N) /= N_Subtype_Declaration
+        and then Nkind (N) /= N_Explicit_Dereference
       then
          return;
       end if;
@@ -2015,7 +2017,8 @@ package body Sem_Dim is
          end if;
       end if;
 
-      --  Removal of dimensions in expression
+      --  Remove dimensions from inner expressions, to prevent dimensions
+      --  table from growing uselessly.
 
       case Nkind (N) is
          when N_Attribute_Reference |