--- a/gcc/ada/lib-writ.adb	Fri Oct 27 22:46:09 2017 +0900
+++ b/gcc/ada/lib-writ.adb	Thu Oct 25 07:37:49 2018 +0900
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2017, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2018, 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- --
@@ -215,9 +215,9 @@
       --  Array of flags to show which units have Elaborate_All_Desirable set
 
       type Yes_No is (Unknown, Yes, No);
-      Implicit_With : array (Units.First .. Last_Unit) of Yes_No;
+      Has_Implicit_With : array (Units.First .. Last_Unit) of Yes_No;
       --  Indicates if an implicit with has been given for the unit. Yes if
-      --  certainly present, no if certainly absent, unkonwn if not known.
+      --  certainly present, No if certainly absent, Unknown if not known.
 
       Sdep_Table : Unit_Ref_Table (1 .. Pos (Last_Unit - Units.First + 2));
       --  Sorted table of source dependencies. One extra entry in case we
@@ -226,17 +226,13 @@
       Num_Sdep : Nat := 0;
       --  Number of active entries in Sdep_Table
 
-      flag_compare_debug : Int;
-      pragma Import (C, flag_compare_debug);
-      --  Import from toplev.c
-
       -----------------------
       -- Local Subprograms --
       -----------------------
 
       procedure Collect_Withs (Cunit : Node_Id);
-      --  Collect with lines for entries in the context clause of the
-      --  given compilation unit, Cunit.
+      --  Collect with lines for entries in the context clause of the given
+      --  compilation unit, Cunit.
 
       procedure Update_Tables_From_ALI_File;
       --  Given an up to date ALI file (see Up_To_Date_ALI_file_Exists
@@ -261,9 +257,47 @@
       -------------------
 
       procedure Collect_Withs (Cunit : Node_Id) is
+         function Is_Implicit_With_Clause (Clause : Node_Id) return Boolean;
+         pragma Inline (Is_Implicit_With_Clause);
+         --  Determine whether a with clause denoted by Clause is implicit
+
+         -----------------------------
+         -- Is_Implicit_With_Clause --
+         -----------------------------
+
+         function Is_Implicit_With_Clause (Clause : Node_Id) return Boolean is
+         begin
+            --  With clauses created for ancestor units are marked as internal,
+            --  however, they emulate the semantics in Ada RM 10.1.2 (6/2),
+            --  where
+            --
+            --    with A.B;
+            --
+            --  is almost equivalent to
+            --
+            --    with A;
+            --    with A.B;
+            --
+            --  For ALI encoding purposes, they are considered to be explicit.
+            --  Note that the clauses cannot be marked as explicit because they
+            --  will be subjected to various checks related to with clauses and
+            --  possibly cause false positives.
+
+            if Parent_With (Clause) then
+               return False;
+
+            else
+               return Implicit_With (Clause);
+            end if;
+         end Is_Implicit_With_Clause;
+
+         --  Local variables
+
          Item : Node_Id;
          Unum : Unit_Number_Type;
 
+      --  Start of processing for Collect_Withs
+
       begin
          Item := First (Context_Items (Cunit));
          while Present (Item) loop
@@ -300,12 +334,28 @@
                   Set_From_Limited_With (Cunit_Entity (Unum));
                end if;
 
-               if Implicit_With (Unum) /= Yes then
-                  if Implicit_With_From_Instantiation (Item) then
-                     Implicit_With (Unum) := Yes;
+               if Is_Implicit_With_Clause (Item) then
+
+                  --  A previous explicit with clause withs the unit. Retain
+                  --  this classification, as it reflects the source relations
+                  --  between units.
+
+                  if Has_Implicit_With (Unum) = No then
+                     null;
+
+                  --  Otherwise this is either the first time any clause withs
+                  --  the unit, or the unit is already implicitly withed.
+
                   else
-                     Implicit_With (Unum) := No;
+                     Has_Implicit_With (Unum) := Yes;
                   end if;
+
+               --  Otherwise the current with clause is explicit. Such clauses
+               --  take precedence over existing implicit clauses because they
+               --  reflect the source relations between unit.
+
+               else
+                  Has_Implicit_With (Unum) := No;
                end if;
             end if;
 
@@ -573,7 +623,7 @@
             Elab_All_Flags     (J) := False;
             Elab_Des_Flags     (J) := False;
             Elab_All_Des_Flags (J) := False;
-            Implicit_With      (J) := Unknown;
+            Has_Implicit_With  (J) := Unknown;
          end loop;
 
          Collect_Withs (Unode);
@@ -690,11 +740,18 @@
                   Note_Unit := U;
                end if;
 
-               if Note_Unit = Unit_Num then
+               --  No action needed for pragmas removed by the expander (for
+               --  example, pragmas of ignored ghost entities).
+
+               if Nkind (N) = N_Null_Statement then
+                  pragma Assert (Nkind (Original_Node (N)) = N_Pragma);
+                  null;
+
+               elsif Note_Unit = Unit_Num then
                   Write_Info_Initiate ('N');
                   Write_Info_Char (' ');
 
-                  case Pragma_Name_Unmapped (N) is
+                  case Pragma_Name (N) is
                      when Name_Annotate =>
                         C := 'A';
                      when Name_Comment =>
@@ -790,9 +847,9 @@
          --  Write source file name Nam and ALI file name for unit index Idx.
          --  Possibly change Nam to lowercase (generating a new file name).
 
-         --------------------------
-         -- Write_With_File_Name --
-         --------------------------
+         ---------------------------
+         -- Write_With_File_Names --
+         ---------------------------
 
          procedure Write_With_File_Names
            (Nam : in out File_Name_Type;
@@ -853,14 +910,17 @@
             Uname := Units.Table (Unum).Unit_Name;
             Fname := Units.Table (Unum).Unit_File_Name;
 
-            if Implicit_With (Unum) = Yes then
-               Write_Info_Initiate ('Z');
+            --  Limited with clauses must be processed first because they are
+            --  the most specific among the three kinds.
 
-            elsif Ekind (Cunit_Entity (Unum)) = E_Package
+            if Ekind (Cunit_Entity (Unum)) = E_Package
               and then From_Limited_With (Cunit_Entity (Unum))
             then
                Write_Info_Initiate ('Y');
 
+            elsif Has_Implicit_With (Unum) = Yes then
+               Write_Info_Initiate ('Z');
+
             else
                Write_Info_Initiate ('W');
             end if;
@@ -893,20 +953,43 @@
                Write_Info_Tab (25);
 
                if Is_Spec_Name (Uname) then
-                  Body_Fname :=
-                    Get_File_Name
-                      (Get_Body_Name (Uname),
-                       Subunit => False, May_Fail => True);
+
+                  --  In GNATprove mode we must write the spec of a unit which
+                  --  requires a body if that body is not found. This will
+                  --  allow partial analysis on incomplete sources. Also, in
+                  --  the case of a unit that is a remote call interface, the
+                  --  bodies of packages may not exist but still may form a
+                  --  valid program - so we handle that here as well.
+
+                  if GNATprove_Mode
+                    or else Is_Remote_Call_Interface (Cunit_Entity (Unum))
+                  then
+                     Body_Fname :=
+                       Get_File_Name
+                         (Uname    => Get_Body_Name (Uname),
+                          Subunit  => False,
+                          May_Fail => True);
+
+                     Body_Index := Get_Unit_Index (Get_Body_Name (Uname));
 
-                  Body_Index :=
-                    Get_Unit_Index
-                      (Get_Body_Name (Uname));
+                     if Body_Fname = No_File then
+                        Body_Fname := Get_File_Name (Uname, Subunit => False);
+                        Body_Index := Get_Unit_Index (Uname);
+                     end if;
+
+                  --  In the normal path we don't allow failure in fetching the
+                  --  name of the desired body unit so that it may be properly
+                  --  referenced in the output ali - even if it is missing.
 
-                  if Body_Fname = No_File then
-                     Body_Fname := Get_File_Name (Uname, Subunit => False);
-                     Body_Index := Get_Unit_Index (Uname);
+                  else
+                     Body_Fname :=
+                       Get_File_Name
+                         (Uname    => Get_Body_Name (Uname),
+                          Subunit  => False,
+                          May_Fail => False);
+
+                     Body_Index := Get_Unit_Index (Get_Body_Name (Uname));
                   end if;
-
                else
                   Body_Fname := Get_File_Name (Uname, Subunit => False);
                   Body_Index := Get_Unit_Index (Uname);
@@ -992,9 +1075,7 @@
       --  We never write an ALI file if the original operating mode was
       --  syntax-only (-gnats switch used in compiler invocation line)
 
-      if Original_Operating_Mode = Check_Syntax
-        or flag_compare_debug /= 0
-      then
+      if Original_Operating_Mode = Check_Syntax then
          return;
       end if;
 
@@ -1482,10 +1563,18 @@
             --  Normal case of a unit entry with a source index
 
             if Sind > No_Source_File then
-               Fname := File_Name (Sind);
+               --  We never want directory information in ALI files
+               --  ???But back out this change temporarily until
+               --  gprbuild is fixed.
 
-               --  Ensure that on platforms where the file names are not case
-               --  sensitive, the recorded file name is in lower case.
+               if False then
+                  Fname := Strip_Directory (File_Name (Sind));
+               else
+                  Fname := File_Name (Sind);
+               end if;
+
+               --  Ensure that on platforms where the file names are not
+               --  case sensitive, the recorded file name is in lower case.
 
                if not File_Names_Case_Sensitive then
                   Get_Name_String (Fname);
@@ -1567,14 +1656,6 @@
          SCO_Output;
       end if;
 
-      --  Output SPARK cross-reference information if needed
-
-      if Opt.Xref_Active and then GNATprove_Mode then
-         SPARK_Specific.Collect_SPARK_Xrefs (Sdep_Table => Sdep_Table,
-                                             Num_Sdep   => Num_Sdep);
-         SPARK_Specific.Output_SPARK_Xrefs;
-      end if;
-
       --  Output final blank line and we are done. This final blank line is
       --  probably junk, but we don't feel like making an incompatible change.