+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.
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);
-- 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