diff mbox

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

Message ID 20110901110025.GA29467@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Sept. 1, 2011, 11 a.m. UTC 
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  <moy@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.
diff mbox

Patch

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