[Ada] Allow multiple units per file in GNATprove

For analysis tools that rely on information generated in ALI files, but
do not generate object files, the frontend did not generate the special
extension names like file~2.ali for unit 2 in the file. This is needed
to be able to analyze files with multiple units. Now fixed.

There is no impact on compilation.

2019-07-10  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* osint-c.adb (Set_File_Name): Always add extension for multiple
	units per file mode.

From-SVN: r273339

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 61afaff4ad9422b5ff9fc84e0a8601f09ab81255..2e5739892570f7b7cd4eae2e0a930e1d5e8bfeeb 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-07-10  Yannick Moy  <moy@adacore.com>
+
+       * osint-c.adb (Set_File_Name): Always add extension for multiple
+       units per file mode.
+
 2019-07-10  Corentin Gay  <gay@adacore.com>
 
        * sysdep.c: Put include directive for 'vxWorks.h' before any

diff --git a/gcc/ada/osint-c.adb b/gcc/ada/osint-c.adb
index 8af5aa0d2f12ce5fcdf199c8b2a75780afe35335..9fb9ee3c170938ec7c1c5bdf1f132f338d08b4ea 100644 (file)
--- a/gcc/ada/osint-c.adb
+++ b/gcc/ada/osint-c.adb
@@ -385,6 +385,21 @@ package body Osint.C is
          end if;
       end loop;
 
+      --  If we are in multiple-units-per-file mode, then add a ~nnn extension
+      --  to the name.
+
+      if Multiple_Unit_Index /= 0 then
+         declare
+            Exten : constant String := Name_Buffer (Dot_Index .. Name_Len);
+         begin
+            Name_Len := Dot_Index - 1;
+            Add_Char_To_Name_Buffer (Multi_Unit_Index_Character);
+            Add_Nat_To_Name_Buffer (Multiple_Unit_Index);
+            Dot_Index := Name_Len + 1;
+            Add_Str_To_Name_Buffer (Exten);
+         end;
+      end if;
+
       --  Make sure that the output file name matches the source file name.
       --  To compare them, remove file name directories and extensions.
 
@@ -395,21 +410,6 @@ package body Osint.C is
 
          Name_Buffer (Dot_Index) := '.';
 
-         --  If we are in multiple unit per file mode, then add ~nnn
-         --  extension to the name before doing the comparison.
-
-         if Multiple_Unit_Index /= 0 then
-            declare
-               Exten : constant String := Name_Buffer (Dot_Index .. Name_Len);
-            begin
-               Name_Len := Dot_Index - 1;
-               Add_Char_To_Name_Buffer (Multi_Unit_Index_Character);
-               Add_Nat_To_Name_Buffer (Multiple_Unit_Index);
-               Dot_Index := Name_Len + 1;
-               Add_Str_To_Name_Buffer (Exten);
-            end;
-         end if;
-
          --  Remove extension preparing to replace it
 
          declare