[Ada] ALI lines for with'ed units should be complete in Alfa mode

[Arnaud Charlet]

In Alfa mode, complete information is required so that back-end can retrieve
Alfa information from suitable ALI files.

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-09-01  Yannick Moy  <m...@adacore.com>

        * lib-writ.adb (Write_With_Lines): Always output complete information
        on "with" line in Alfa mode, as this is required by formal verification
        back-end.


Index: lib-writ.adb
===================================================================
--- lib-writ.adb        (revision 178381)
+++ lib-writ.adb        (working copy)
@@ -796,6 +796,12 @@
                       or else
                      Nkind (Unit (Cunit)) in N_Generic_Renaming_Declaration)
                     and then Generic_May_Lack_ALI (Fname))
+
+              --  In Alfa mode, always generate the dependencies on ALI
+              --  files, which are required to compute frame conditions
+              --  of subprograms.
+
+              or else Alfa_Mode
             then
                Write_Info_Tab (25);