diff options
Diffstat (limited to 'gcc/ada/lib-writ.adb')
| -rw-r--r-- | gcc/ada/lib-writ.adb | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/gcc/ada/lib-writ.adb b/gcc/ada/lib-writ.adb index 12664ee..e786f47 100644 --- a/gcc/ada/lib-writ.adb +++ b/gcc/ada/lib-writ.adb @@ -33,7 +33,6 @@ with Fname; use Fname; with Fname.UF; use Fname.UF; with Lib.Util; use Lib.Util; with Lib.Xref; use Lib.Xref; - use Lib.Xref.Alfa; with Nlists; use Nlists; with Gnatvsn; use Gnatvsn; with Opt; use Opt; @@ -816,11 +815,11 @@ package body Lib.Writ is Nkind (Unit (Cunit)) in N_Generic_Renaming_Declaration) and then Generic_May_Lack_ALI (Fname)) - -- In Alfa mode, always generate the dependencies on ALI + -- In SPARK mode, always generate the dependencies on ALI -- files, which are required to compute frame conditions -- of subprograms. - or else Alfa_Mode + or else SPARK_Mode then Write_Info_Tab (25); @@ -1433,11 +1432,12 @@ package body Lib.Writ is SCO_Output; end if; - -- Output Alfa information if needed + -- Output SPARK cross-reference information if needed - if Opt.Xref_Active and then Alfa_Mode then - Collect_Alfa (Sdep_Table => Sdep_Table, Num_Sdep => Num_Sdep); - Output_Alfa; + if Opt.Xref_Active and then SPARK_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 |