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