[Ada] GNATmake fails to detect missing body

This patch corrects an issue whereby building a multi-unit compilation with
missing sources resulted in a cryptic "code generation" error instead of the
appropriate file not found error.

------------
-- Source --
------------

--  main.adb

with Types;
procedure Main is
begin
   null;
end;

--  types.ads

package Types is
  procedure Force;
end;

----------------------------
-- Compilation and output --
----------------------------

& gnatmake -q main.adb
gnatmake: "types.adb" not found

2018-07-31  Justin Squirek  <squirek@adacore.com>

gcc/ada/

	* lib-writ.adb (Write_With_Lines): Modfiy the generation of
	dependencies within ali files so that source unit bodies are
	properly listed even if said bodies are missing.  Perform legacy
	behavior in GNATprove mode.
	* lib-writ.ads: Modify documentation to reflect current behavior.

From-SVN: r263100

gcc/ada/ChangeLog

+2018-07-31  Justin Squirek  <squirek@adacore.com>
+
+	* lib-writ.adb (Write_With_Lines): Modfiy the generation of
+	dependencies within ali files so that source unit bodies are
+	properly listed even if said bodies are missing.  Perform legacy
+	behavior in GNATprove mode.
+	* lib-writ.ads: Modify documentation to reflect current behavior.
+
 2018-07-31  Eric Botcazou  <ebotcazou@adacore.com>
 
 	*  libgnarl/s-osinte__solaris.ads (upad64_t): New private type.

gcc/ada/lib-writ.adb

@@ -950,20 +950,35 @@ package body Lib.Writ is
                Write_Info_Tab (25);
 
                if Is_Spec_Name (Uname) then
-                  Body_Fname :=
-                    Get_File_Name
-                      (Get_Body_Name (Uname),
-                       Subunit => False, May_Fail => True);
-
-                  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 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.
+
+                  if GNATprove_Mode then
+
+                     Body_Fname :=
+                       Get_File_Name (Get_Body_Name (Uname),
+                                       Subunit => False, May_Fail => True);
+
+                     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.
+
+                  else
+                     Body_Fname :=
+                       Get_File_Name (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);

gcc/ada/lib-writ.ads

@@ -629,13 +629,13 @@ package Lib.Writ is
    --      by the current unit. One Z line is present for each unit that is
    --      only implicitly withed by the current unit. The first parameter is
    --      the unit name in internal format. The second parameter is the file
-   --      name of the file that must be compiled to compile this unit. It is
-   --      usually the file for the body, except for packages which have no
-   --      body. For units that need a body, if the source file for the body
-   --      cannot be found, the file name of the spec is used instead. The
-   --      third parameter is the file name of the library information file
-   --      that contains the results of compiling this unit. The optional
-   --      modifiers are used as follows:
+   --      name of the body unit on which the current compliation depends -
+   --      except when in GNATprove mode. In GNATprove mode, when packages
+   --      which require a body have no associated source file, the file name
+   --      of the spec is used instead to allow partial analysis of incomplete
+   --      sources. The third parameter is the file name of the library
+   --      information file that contains the results of compiling this unit.
+   --      The optional modifiers are used as follows:
 
    --        E   pragma Elaborate applies to this unit