The unit file name is needed when processing Alfa references from subunits,
in the formal verification backend of GNAT. Thus, add the unit file name
information for subunits in the line of the Alfa section that gives the
subunit file name.

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

2012-03-15  Yannick Moy  <m...@adacore.com>

        * alfa.ads Update the decription of ALI sections.
        (Alfa_File_Record): Add a component Unit_File_Name to store the
        unit file name for subunits.
        * get_alfa.adb, put_alfa.adb Adapt to the possible presence of
        a unit file name.
        * lib-xref-alfa.adb (Add_Alfa_File): For subunits, retrieve the
        file name of the unit.

Index: alfa.ads
===================================================================
--- alfa.ads    (revision 185390)
+++ alfa.ads    (working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---             Copyright (C) 2011, Free Software Foundation, Inc.           --
+--          Copyright (C) 2011-2012, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -70,7 +70,7 @@
    --  subprogram declaration and body, when both present, define two different
    --  scopes.
 
-   --    FD dependency-number filename
+   --    FD dependency-number filename (-> unit-filename)?
 
    --      This header precedes scope information for the unit identified by
    --      dependency number and file name. The dependency number is the index
@@ -89,6 +89,8 @@
    --      reading of the Alfa information, and means that the Alfa information
    --      can stand on its own without needing other parts of the ALI file.
 
+   --      The optional unit filename is given only for subunits.
+
    --    FS . scope line type col entity (-> spec-file . spec-scope)?
 
    --      (The ? mark stands for an optional entry in the syntax)
@@ -314,6 +316,10 @@
       File_Name : String_Ptr;
       --  Pointer to file name in ALI file
 
+      Unit_File_Name : String_Ptr;
+      --  Pointer to file name for unit in ALI file, when File_Name refers to a
+      --  subunit. Otherwise null.
+
       File_Num : Nat;
       --  Dependency number in ALI file
 
Index: put_alfa.adb
===================================================================
--- put_alfa.adb        (revision 185390)
+++ put_alfa.adb        (working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---             Copyright (C) 2011, Free Software Foundation, Inc.           --
+--          Copyright (C) 2011-2012, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -49,6 +49,18 @@
             Write_Info_Char (F.File_Name (N));
          end loop;
 
+         --  If file is a subunit, print the file name for the unit
+
+         if F.Unit_File_Name /= null then
+            Write_Info_Char (' ');
+            Write_Info_Char ('-');
+            Write_Info_Char ('>');
+            Write_Info_Char (' ');
+            for N in F.Unit_File_Name'Range loop
+               Write_Info_Char (F.Unit_File_Name (N));
+            end loop;
+         end if;
+
          Write_Info_Terminate;
 
          --  Loop through scope entries for this file
Index: lib-xref-alfa.adb
===================================================================
--- lib-xref-alfa.adb   (revision 185390)
+++ lib-xref-alfa.adb   (working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---             Copyright (C) 2011, Free Software Foundation, Inc.           --
+--          Copyright (C) 2011-2012, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -214,6 +214,8 @@
 
       S : constant Source_File_Index := Source_Index (U);
 
+      File_Name, Unit_File_Name : String_Ptr;
+
    begin
       --  Source file could be inexistant as a result of an error, if option
       --  gnatQ is used.
@@ -275,12 +277,23 @@
       --  Make entry for new file in file table
 
       Get_Name_String (Reference_Name (S));
+      File_Name := new String'(Name_Buffer (1 .. Name_Len));
 
+      --  For subunits, also retrieve the file name of the unit
+
+      if Present (Cunit (Unit (S)))
+        and then Nkind (Unit (Cunit (Unit (S)))) = N_Subunit
+      then
+         Get_Name_String (Reference_Name (Main_Source_File));
+         Unit_File_Name := new String'(Name_Buffer (1 .. Name_Len));
+      end if;
+
       Alfa_File_Table.Append (
-        (File_Name  => new String'(Name_Buffer (1 .. Name_Len)),
-         File_Num   => D,
-         From_Scope => From,
-         To_Scope   => Alfa_Scope_Table.Last));
+        (File_Name      => File_Name,
+         Unit_File_Name => Unit_File_Name,
+         File_Num       => D,
+         From_Scope     => From,
+         To_Scope       => Alfa_Scope_Table.Last));
    end Add_Alfa_File;
 
    --------------------
Index: get_alfa.adb
===================================================================
--- get_alfa.adb        (revision 185390)
+++ get_alfa.adb        (working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---             Copyright (C) 2011, Free Software Foundation, Inc.           --
+--          Copyright (C) 2011-2012, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -51,6 +51,9 @@
    --  Local string used to store name of File/entity scanned as
    --  Name_Str (1 .. Name_Len).
 
+   File_Name : String_Ptr;
+   Unit_File_Name : String_Ptr;
+
    -----------------------
    -- Local Subprograms --
    -----------------------
@@ -236,15 +239,32 @@
             Skip_Spaces;
             Cur_File := Get_Nat;
             Skip_Spaces;
+
             Get_Name;
+            File_Name := new String'(Name_Str (1 .. Name_Len));
+            Skip_Spaces;
 
+            --  Scan out unit file name when present (for subunits)
+
+            if Nextc = '-' then
+               Skipc;
+               Check ('>');
+               Skip_Spaces;
+               Get_Name;
+               Unit_File_Name := new String'(Name_Str (1 .. Name_Len));
+
+            else
+               Unit_File_Name := null;
+            end if;
+
             --  Make new File table entry (will fill in To_Scope later)
 
             Alfa_File_Table.Append (
-              (File_Name  => new String'(Name_Str (1 .. Name_Len)),
-               File_Num   => Cur_File,
-               From_Scope => Alfa_Scope_Table.Last + 1,
-               To_Scope   => 0));
+              (File_Name      => File_Name,
+               Unit_File_Name => Unit_File_Name,
+               File_Num       => Cur_File,
+               From_Scope     => Alfa_Scope_Table.Last + 1,
+               To_Scope       => 0));
 
             --  Initialize counter for scopes
 

Reply via email to