[Ada] Allow multiple units per file in GNATprove

Message ID 20190710090330.GA81243@adacore.com
State New
Headers show
Series
  • [Ada] Allow multiple units per file in GNATprove
Related show

Commit Message

Pierre-Marie de Rodat July 10, 2019, 9:03 a.m.
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.

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

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.

Patch

--- gcc/ada/osint-c.adb
+++ 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