[Ada] Regression in partial compilation of RCI units
[gcc.git] / gcc / ada / lib-writ.adb
index 94d4b45552671af6dcc94d9f27b6bef28c969ef7..f035b45e913315d76b2588a3f801b1a1bfaa7512 100644 (file)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2009, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2018, 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- --
@@ -26,6 +26,7 @@
 with ALI;      use ALI;
 with Atree;    use Atree;
 with Casing;   use Casing;
+with Debug;    use Debug;
 with Einfo;    use Einfo;
 with Errout;   use Errout;
 with Fname;    use Fname;
@@ -37,11 +38,14 @@ with Gnatvsn;  use Gnatvsn;
 with Opt;      use Opt;
 with Osint;    use Osint;
 with Osint.C;  use Osint.C;
+with Output;   use Output;
 with Par;
 with Par_SCO;  use Par_SCO;
 with Restrict; use Restrict;
 with Rident;   use Rident;
+with Stand;    use Stand;
 with Scn;      use Scn;
+with Sem_Eval; use Sem_Eval;
 with Sinfo;    use Sinfo;
 with Sinput;   use Sinput;
 with Snames;   use Snames;
@@ -70,26 +74,34 @@ package body Lib.Writ is
    begin
       Units.Increment_Last;
       Units.Table (Units.Last) :=
-        (Unit_File_Name   => File_Name (S),
-         Unit_Name        => No_Unit_Name,
-         Expected_Unit    => No_Unit_Name,
-         Source_Index     => S,
-         Cunit            => Empty,
-         Cunit_Entity     => Empty,
-         Dependency_Num   => 0,
-         Dynamic_Elab     => False,
-         Fatal_Error      => False,
-         Generate_Code    => False,
-         Has_RACW         => False,
-         Is_Compiler_Unit => False,
-         Ident_String     => Empty,
-         Loading          => False,
-         Main_Priority    => -1,
-         Munit_Index      => 0,
-         Serial_Number    => 0,
-         Version          => 0,
-         Error_Location   => No_Location,
-         OA_Setting       => 'O');
+        (Unit_File_Name         => File_Name (S),
+         Unit_Name              => No_Unit_Name,
+         Expected_Unit          => No_Unit_Name,
+         Source_Index           => S,
+         Cunit                  => Empty,
+         Cunit_Entity           => Empty,
+         Dependency_Num         => 0,
+         Dynamic_Elab           => False,
+         Fatal_Error            => None,
+         Generate_Code          => False,
+         Has_RACW               => False,
+         Filler                 => False,
+         Ident_String           => Empty,
+         Is_Predefined_Renaming => False,
+         Is_Internal_Unit       => False,
+         Is_Predefined_Unit     => False,
+         Filler2                => False,
+         Loading                => False,
+         Main_Priority          => -1,
+         Main_CPU               => -1,
+         Munit_Index            => 0,
+         No_Elab_Code_All       => False,
+         Primary_Stack_Count    => 0,
+         Sec_Stack_Count        => 0,
+         Serial_Number          => 0,
+         Version                => 0,
+         Error_Location         => No_Location,
+         OA_Setting             => 'O');
    end Add_Preprocessing_Dependency;
 
    ------------------------------
@@ -124,30 +136,39 @@ package body Lib.Writ is
       System_Fname := File_Name (System_Source_File_Index);
 
       Units.Increment_Last;
-      Units.Table (Units.Last) := (
-        Unit_File_Name   => System_Fname,
-        Unit_Name        => System_Uname,
-        Expected_Unit    => System_Uname,
-        Source_Index     => System_Source_File_Index,
-        Cunit            => Empty,
-        Cunit_Entity     => Empty,
-        Dependency_Num   => 0,
-        Dynamic_Elab     => False,
-        Fatal_Error      => False,
-        Generate_Code    => False,
-        Has_RACW         => False,
-        Is_Compiler_Unit => False,
-        Ident_String     => Empty,
-        Loading          => False,
-        Main_Priority    => -1,
-        Munit_Index      => 0,
-        Serial_Number    => 0,
-        Version          => 0,
-        Error_Location   => No_Location,
-        OA_Setting       => 'O');
-
-      --  Parse system.ads so that the checksum is set right
-      --  Style checks are not applied.
+      Units.Table (Units.Last) :=
+        (Unit_File_Name         => System_Fname,
+         Unit_Name              => System_Uname,
+         Expected_Unit          => System_Uname,
+         Source_Index           => System_Source_File_Index,
+         Cunit                  => Empty,
+         Cunit_Entity           => Empty,
+         Dependency_Num         => 0,
+         Dynamic_Elab           => False,
+         Fatal_Error            => None,
+         Generate_Code          => False,
+         Has_RACW               => False,
+         Filler                 => False,
+         Ident_String           => Empty,
+         Is_Predefined_Renaming => False,
+         Is_Internal_Unit       => True,
+         Is_Predefined_Unit     => True,
+         Filler2                => False,
+         Loading                => False,
+         Main_Priority          => -1,
+         Main_CPU               => -1,
+         Munit_Index            => 0,
+         No_Elab_Code_All       => False,
+         Primary_Stack_Count    => 0,
+         Sec_Stack_Count        => 0,
+         Serial_Number          => 0,
+         Version                => 0,
+         Error_Location         => No_Location,
+         OA_Setting             => 'O');
+
+      --  Parse system.ads so that the checksum is set right. Style checks are
+      --  not applied. The Ekind is set to ensure that this reference is always
+      --  present in the ali file.
 
       declare
          Save_Mindex : constant Nat := Multiple_Unit_Index;
@@ -157,6 +178,8 @@ package body Lib.Writ is
          Style_Check := False;
          Initialize_Scanner (Units.Last, System_Source_File_Index);
          Discard_List (Par (Configuration_Pragmas => False));
+         Set_Ekind (Cunit_Entity (Units.Last), E_Package);
+         Set_Scope (Cunit_Entity (Units.Last), Standard_Standard);
          Style_Check := Save_Style;
          Multiple_Unit_Index := Save_Mindex;
       end;
@@ -191,6 +214,11 @@ package body Lib.Writ is
       Elab_All_Des_Flags : array (Units.First .. Last_Unit) of Boolean;
       --  Array of flags to show which units have Elaborate_All_Desirable set
 
+      type Yes_No is (Unknown, Yes, No);
+      Has_Implicit_With : array (Units.First .. Last_Unit) of Yes_No;
+      --  Indicates if an implicit with has been given for the unit. Yes if
+      --  certainly present, No if certainly absent, Unknown if not known.
+
       Sdep_Table : Unit_Ref_Table (1 .. Pos (Last_Unit - Units.First + 2));
       --  Sorted table of source dependencies. One extra entry in case we
       --  have to add a dummy entry for System.
@@ -207,8 +235,8 @@ package body Lib.Writ is
       -----------------------
 
       procedure Collect_Withs (Cunit : Node_Id);
-      --  Collect with lines for entries in the context clause of the
-      --  given compilation unit, Cunit.
+      --  Collect with lines for entries in the context clause of the given
+      --  compilation unit, Cunit.
 
       procedure Update_Tables_From_ALI_File;
       --  Given an up to date ALI file (see Up_To_Date_ALI_file_Exists
@@ -233,9 +261,47 @@ package body Lib.Writ is
       -------------------
 
       procedure Collect_Withs (Cunit : Node_Id) is
+         function Is_Implicit_With_Clause (Clause : Node_Id) return Boolean;
+         pragma Inline (Is_Implicit_With_Clause);
+         --  Determine whether a with clause denoted by Clause is implicit
+
+         -----------------------------
+         -- Is_Implicit_With_Clause --
+         -----------------------------
+
+         function Is_Implicit_With_Clause (Clause : Node_Id) return Boolean is
+         begin
+            --  With clauses created for ancestor units are marked as internal,
+            --  however, they emulate the semantics in Ada RM 10.1.2 (6/2),
+            --  where
+            --
+            --    with A.B;
+            --
+            --  is almost equivalent to
+            --
+            --    with A;
+            --    with A.B;
+            --
+            --  For ALI encoding purposes, they are considered to be explicit.
+            --  Note that the clauses cannot be marked as explicit because they
+            --  will be subjected to various checks related to with clauses and
+            --  possibly cause false positives.
+
+            if Parent_With (Clause) then
+               return False;
+
+            else
+               return Implicit_With (Clause);
+            end if;
+         end Is_Implicit_With_Clause;
+
+         --  Local variables
+
          Item : Node_Id;
          Unum : Unit_Number_Type;
 
+      --  Start of processing for Collect_Withs
+
       begin
          Item := First (Context_Items (Cunit));
          while Present (Item) loop
@@ -269,7 +335,31 @@ package body Lib.Writ is
                   end if;
 
                else
-                  Set_From_With_Type (Cunit_Entity (Unum));
+                  Set_From_Limited_With (Cunit_Entity (Unum));
+               end if;
+
+               if Is_Implicit_With_Clause (Item) then
+
+                  --  A previous explicit with clause withs the unit. Retain
+                  --  this classification, as it reflects the source relations
+                  --  between units.
+
+                  if Has_Implicit_With (Unum) = No then
+                     null;
+
+                  --  Otherwise this is either the first time any clause withs
+                  --  the unit, or the unit is already implicitly withed.
+
+                  else
+                     Has_Implicit_With (Unum) := Yes;
+                  end if;
+
+               --  Otherwise the current with clause is explicit. Such clauses
+               --  take precedence over existing implicit clauses because they
+               --  reflect the source relations between unit.
+
+               else
+                  Has_Implicit_With (Unum) := No;
                end if;
             end if;
 
@@ -407,10 +497,8 @@ package body Lib.Writ is
          --  If this is a spec ...
 
          if (Is_Subprogram (Uent)
-               or else
-             Ekind (Uent) = E_Package
-               or else
-             Is_Generic_Unit (Uent))
+              or else Ekind (Uent) = E_Package
+              or else Is_Generic_Unit (Uent))
 
             --  and an elaboration entity was declared ...
 
@@ -418,8 +506,7 @@ package body Lib.Writ is
 
             --  and either the elaboration flag is required ...
 
-            and then
-              (Elaboration_Entity_Required (Uent)
+            and then (Elaboration_Entity_Required (Uent)
 
                --  or this unit has elaboration code ...
 
@@ -433,20 +520,9 @@ package body Lib.Writ is
                    and then Present (Body_Entity (Uent))
                    and then
                      not Has_No_Elaboration_Code
-                           (Parent
-                             (Declaration_Node
-                               (Body_Entity (Uent))))))
+                           (Parent (Declaration_Node (Body_Entity (Uent))))))
          then
-            if Convention (Uent) = Convention_CIL then
-
-               --  Special case for generic CIL packages which never have
-               --  elaboration code
-
-               Write_Info_Str (" NE");
-
-            else
-               Write_Info_Str (" EE");
-            end if;
+            Write_Info_Str (" EE");
          end if;
 
          if Has_No_Elaboration_Code (Unode) then
@@ -456,6 +532,12 @@ package body Lib.Writ is
          Write_Info_Str (" O");
          Write_Info_Char (OA_Setting (Unit_Num));
 
+         if Ekind_In (Uent, E_Package, E_Package_Body)
+           and then Present (Finalizer (Uent))
+         then
+            Write_Info_Str (" PF");
+         end if;
+
          if Is_Preelaborated (Uent) then
             Write_Info_Str (" PR");
          end if;
@@ -476,6 +558,10 @@ package body Lib.Writ is
             Write_Info_Str (" RT");
          end if;
 
+         if Serious_Errors_Detected /= 0 then
+            Write_Info_Str (" SE");
+         end if;
+
          if Is_Shared_Passive (Uent) then
             Write_Info_Str (" SP");
          end if;
@@ -508,12 +594,12 @@ package body Lib.Writ is
            or else
              (Present (Library_Unit (Unode))
                 and then
-              Nkind (Unit (Library_Unit (Unode))) in N_Generic_Declaration)
+                  Nkind (Unit (Library_Unit (Unode))) in N_Generic_Declaration)
          then
             Write_Info_Str (" GE");
          end if;
 
-         if not Is_Internal_File_Name (Unit_File_Name (Unit_Num), True) then
+         if not Is_Internal_Unit (Unit_Num) then
             case Identifier_Casing (Source_Index (Unit_Num)) is
                when All_Lower_Case => Write_Info_Str (" IL");
                when All_Upper_Case => Write_Info_Str (" IU");
@@ -541,6 +627,7 @@ package body Lib.Writ is
             Elab_All_Flags     (J) := False;
             Elab_Des_Flags     (J) := False;
             Elab_All_Des_Flags (J) := False;
+            Has_Implicit_With  (J) := Unknown;
          end loop;
 
          Collect_Withs (Unode);
@@ -552,19 +639,18 @@ package body Lib.Writ is
          if Nkind (Unit (Unode)) in N_Unit_Body then
             for S in Units.First .. Last_Unit loop
 
-               --  We are only interested in subunits.
-               --  For preproc. data and def. files, Cunit is Empty, so
-               --  we need to test that first.
+               --  We are only interested in subunits. For preproc. data and
+               --  def. files, Cunit is Empty, so we need to test that first.
 
                if Cunit (S) /= Empty
                  and then Nkind (Unit (Cunit (S))) = N_Subunit
                then
                   Pnode := Library_Unit (Cunit (S));
 
-                  --  In gnatc mode, the errors in the subunits will not
-                  --  have been recorded, but the analysis of the subunit
-                  --  may have failed. There is no information to add to
-                  --  ALI file in this case.
+                  --  In gnatc mode, the errors in the subunits will not have
+                  --  been recorded, but the analysis of the subunit may have
+                  --  failed. There is no information to add to ALI file in
+                  --  this case.
 
                   if No (Pnode) then
                      exit;
@@ -588,46 +674,155 @@ package body Lib.Writ is
 
          Write_With_Lines;
 
-         --  Output linker option lines
+         --  Generate task stack lines
+
+         if Primary_Stack_Count (Unit_Num) > 0
+           or else Sec_Stack_Count (Unit_Num) > 0
+         then
+            Write_Info_Initiate ('T');
+            Write_Info_Char (' ');
+            Write_Info_Int (Primary_Stack_Count (Unit_Num));
+            Write_Info_Char (' ');
+            Write_Info_Int (Sec_Stack_Count (Unit_Num));
+            Write_Info_EOL;
+         end if;
+
+         --  Generate the linker option lines
 
          for J in 1 .. Linker_Option_Lines.Last loop
-            declare
-               S : constant Linker_Option_Entry :=
-                     Linker_Option_Lines.Table (J);
-               C : Character;
 
+            --  Pragma Linker_Options is not allowed in predefined generic
+            --  units. This is because they won't be read, due to the fact that
+            --  with lines for generic units lack the file name and lib name
+            --  parameters (see Lib_Writ spec for an explanation).
+
+            if Is_Generic_Unit (Cunit_Entity (Main_Unit))
+              and then Is_Predefined_Unit (Current_Sem_Unit)
+              and then Linker_Option_Lines.Table (J).Unit = Unit_Num
+            then
+               Set_Standard_Error;
+               Write_Line
+                 ("linker options not allowed in predefined generic unit");
+               raise Unrecoverable_Error;
+            end if;
+
+            --  Output one linker option line
+
+            declare
+               S : Linker_Option_Entry renames Linker_Option_Lines.Table (J);
             begin
                if S.Unit = Unit_Num then
                   Write_Info_Initiate ('L');
-                  Write_Info_Str (" """);
+                  Write_Info_Char (' ');
+                  Write_Info_Slit (S.Option);
+                  Write_Info_EOL;
+               end if;
+            end;
+         end loop;
+
+         --  Output notes
+
+         for J in 1 .. Notes.Last loop
+            declare
+               N : constant Node_Id          := Notes.Table (J);
+               L : constant Source_Ptr       := Sloc (N);
+               U : constant Unit_Number_Type :=
+                     Unit (Get_Source_File_Index (L));
+               C : Character;
+
+               Note_Unit : Unit_Number_Type;
+               --  The unit in whose U section this note must be emitted:
+               --  notes for subunits are emitted along with the main unit;
+               --  all other notes are emitted as part of the enclosing
+               --  compilation unit.
+
+            begin
+               if U /= No_Unit and then Nkind (Unit (Cunit (U))) = N_Subunit
+               then
+                  Note_Unit := Main_Unit;
+               else
+                  Note_Unit := U;
+               end if;
+
+               --  No action needed for pragmas removed by the expander (for
+               --  example, pragmas of ignored ghost entities).
+
+               if Nkind (N) = N_Null_Statement then
+                  pragma Assert (Nkind (Original_Node (N)) = N_Pragma);
+                  null;
 
-                  for J in 1 .. String_Length (S.Option) loop
-                     C := Get_Character (Get_String_Char (S.Option, J));
+               elsif Note_Unit = Unit_Num then
+                  Write_Info_Initiate ('N');
+                  Write_Info_Char (' ');
+
+                  case Pragma_Name (N) is
+                     when Name_Annotate =>
+                        C := 'A';
+                     when Name_Comment =>
+                        C := 'C';
+                     when Name_Ident =>
+                        C := 'I';
+                     when Name_Title =>
+                        C := 'T';
+                     when Name_Subtitle =>
+                        C := 'S';
+                     when others =>
+                        raise Program_Error;
+                  end case;
+
+                  Write_Info_Char (C);
+                  Write_Info_Int (Int (Get_Logical_Line_Number (L)));
+                  Write_Info_Char (':');
+                  Write_Info_Int (Int (Get_Column_Number (L)));
+
+                  --  Indicate source file of annotation if different from
+                  --  compilation unit source file (case of annotation coming
+                  --  from a separate).
+
+                  if Get_Source_File_Index (L) /= Source_Index (Unit_Num) then
+                     Write_Info_Char (':');
+                     Write_Info_Name (File_Name (Get_Source_File_Index (L)));
+                  end if;
+
+                  declare
+                     A : Node_Id;
 
-                     if C in Character'Val (16#20#) .. Character'Val (16#7E#)
-                       and then C /= '{'
-                     then
-                        Write_Info_Char (C);
+                  begin
+                     A := First (Pragma_Argument_Associations (N));
+                     while Present (A) loop
+                        Write_Info_Char (' ');
 
-                        if C = '"' then
-                           Write_Info_Char (C);
+                        if Chars (A) /= No_Name then
+                           Write_Info_Name (Chars (A));
+                           Write_Info_Char (':');
                         end if;
 
-                     else
                         declare
-                           Hex : constant array (0 .. 15) of Character :=
-                                   "0123456789ABCDEF";
+                           Expr : constant Node_Id := Expression (A);
 
                         begin
-                           Write_Info_Char ('{');
-                           Write_Info_Char (Hex (Character'Pos (C) / 16));
-                           Write_Info_Char (Hex (Character'Pos (C) mod 16));
-                           Write_Info_Char ('}');
+                           if Nkind (Expr) = N_Identifier then
+                              Write_Info_Name (Chars (Expr));
+
+                           elsif Nkind (Expr) = N_Integer_Literal
+                             and then Is_OK_Static_Expression (Expr)
+                           then
+                              Write_Info_Uint (Intval (Expr));
+
+                           elsif Nkind (Expr) = N_String_Literal
+                             and then Is_OK_Static_Expression (Expr)
+                           then
+                              Write_Info_Slit (Strval (Expr));
+
+                           else
+                              Write_Info_Str ("<expr>");
+                           end if;
                         end;
-                     end if;
-                  end loop;
 
-                  Write_Info_Char ('"');
+                        Next (A);
+                     end loop;
+                  end;
+
                   Write_Info_EOL;
                end if;
             end;
@@ -639,16 +834,16 @@ package body Lib.Writ is
       ----------------------
 
       procedure Write_With_Lines is
-         With_Table : Unit_Ref_Table (1 .. Pos (Last_Unit - Units.First + 1));
-         Num_Withs  : Int := 0;
-         Unum       : Unit_Number_Type;
-         Cunit      : Node_Id;
-         Uname      : Unit_Name_Type;
-         Fname      : File_Name_Type;
          Pname      : constant Unit_Name_Type :=
                         Get_Parent_Spec_Name (Unit_Name (Main_Unit));
          Body_Fname : File_Name_Type;
          Body_Index : Nat;
+         Cunit      : Node_Id;
+         Fname      : File_Name_Type;
+         Num_Withs  : Int := 0;
+         Unum       : Unit_Number_Type;
+         Uname      : Unit_Name_Type;
+         With_Table : Unit_Ref_Table (1 .. Pos (Last_Unit - Units.First + 1));
 
          procedure Write_With_File_Names
            (Nam : in out File_Name_Type;
@@ -656,9 +851,9 @@ package body Lib.Writ is
          --  Write source file name Nam and ALI file name for unit index Idx.
          --  Possibly change Nam to lowercase (generating a new file name).
 
-         --------------------------
-         -- Write_With_File_Name --
-         --------------------------
+         ---------------------------
+         -- Write_With_File_Names --
+         ---------------------------
 
          procedure Write_With_File_Names
            (Nam : in out File_Name_Type;
@@ -689,8 +884,8 @@ package body Lib.Writ is
             --  Add element to with table if it is with'ed or if it is the
             --  parent spec of the main unit (case of main unit is a child
             --  unit). The latter with is not needed for semantic purposes,
-            --  but is required by the binder for elaboration purposes.
-            --  For preproc. data and def. files, there is no Unit_Name,
+            --  but is required by the binder for elaboration purposes. For
+            --  preprocessing data and definition files, there is no Unit_Name,
             --  check for that first.
 
             if Unit_Name (J) /= No_Unit_Name
@@ -706,15 +901,30 @@ package body Lib.Writ is
          Sort (With_Table (1 .. Num_Withs));
 
          for J in 1 .. Num_Withs loop
-            Unum   := With_Table (J);
-            Cunit  := Units.Table (Unum).Cunit;
-            Uname  := Units.Table (Unum).Unit_Name;
-            Fname  := Units.Table (Unum).Unit_File_Name;
+            Unum := With_Table (J);
+
+            --  Do not generate a with line for an ignored Ghost unit because
+            --  the unit does not have an ALI file.
+
+            if Is_Ignored_Ghost_Entity (Cunit_Entity (Unum)) then
+               goto Next_With_Line;
+            end if;
+
+            Cunit := Units.Table (Unum).Cunit;
+            Uname := Units.Table (Unum).Unit_Name;
+            Fname := Units.Table (Unum).Unit_File_Name;
+
+            --  Limited with clauses must be processed first because they are
+            --  the most specific among the three kinds.
 
             if Ekind (Cunit_Entity (Unum)) = E_Package
-              and then From_With_Type (Cunit_Entity (Unum))
+              and then From_Limited_With (Cunit_Entity (Unum))
             then
                Write_Info_Initiate ('Y');
+
+            elsif Has_Implicit_With (Unum) = Yes then
+               Write_Info_Initiate ('Z');
+
             else
                Write_Info_Initiate ('W');
             end if;
@@ -736,25 +946,54 @@ package body Lib.Writ is
             if not ((Nkind (Unit (Cunit)) in N_Generic_Declaration
                       or else
                      Nkind (Unit (Cunit)) in N_Generic_Renaming_Declaration)
-                    and then Generic_May_Lack_ALI (Fname))
+                    and then Generic_May_Lack_ALI (Unum))
+
+              --  In SPARK mode, always generate the dependencies on ALI
+              --  files, which are required to compute frame conditions
+              --  of subprograms.
+
+              or else GNATprove_Mode
             then
                Write_Info_Tab (25);
 
                if Is_Spec_Name (Uname) then
-                  Body_Fname :=
-                    Get_File_Name
-                      (Get_Body_Name (Uname),
-                       Subunit => False, May_Fail => True);
-
-                  Body_Index :=
-                    Get_Unit_Index
-                      (Get_Body_Name (Uname));
-
-                  if Body_Fname = No_File then
-                     Body_Fname := Get_File_Name (Uname, Subunit => False);
-                     Body_Index := Get_Unit_Index (Uname);
-                  end if;
 
+                  --  In GNATprove mode we must write the spec of a unit which
+                  --  requires a body if that body is not found. This will
+                  --  allow partial analysis on incomplete sources. Also, in
+                  --  the case of a unit that is a remote call interface, the
+                  --  bodies of packages may not exist but still may form a
+                  --  valid program - so we handle that here as well.
+
+                  if GNATprove_Mode
+                    or else Is_Remote_Call_Interface (Cunit_Entity (Unum))
+                  then
+                     Body_Fname :=
+                       Get_File_Name
+                         (Uname    => Get_Body_Name (Uname),
+                          Subunit  => False,
+                          May_Fail => True);
+
+                     Body_Index := Get_Unit_Index (Get_Body_Name (Uname));
+
+                     if Body_Fname = No_File then
+                        Body_Fname := Get_File_Name (Uname, Subunit => False);
+                        Body_Index := Get_Unit_Index (Uname);
+                     end if;
+
+                  --  In the normal path we don't allow failure in fetching the
+                  --  name of the desired body unit so that it may be properly
+                  --  referenced in the output ali - even if it is missing.
+
+                  else
+                     Body_Fname :=
+                       Get_File_Name
+                         (Uname    => Get_Body_Name (Uname),
+                          Subunit  => False,
+                          May_Fail => False);
+
+                     Body_Index := Get_Unit_Index (Get_Body_Name (Uname));
+                  end if;
                else
                   Body_Fname := Get_File_Name (Uname, Subunit => False);
                   Body_Index := Get_Unit_Index (Uname);
@@ -773,7 +1012,7 @@ package body Lib.Writ is
                end if;
 
                if Ekind (Cunit_Entity (Unum)) = E_Package
-                  and then From_With_Type (Cunit_Entity (Unum))
+                  and then From_Limited_With (Cunit_Entity (Unum))
                then
                   null;
                else
@@ -796,7 +1035,42 @@ package body Lib.Writ is
             end if;
 
             Write_Info_EOL;
+
+         <<Next_With_Line>>
+            null;
          end loop;
+
+         --  Finally generate the special lines for cases of Restriction_Set
+         --  with No_Dependence and no restriction present.
+
+         declare
+            Unam : Unit_Name_Type;
+
+         begin
+            for J in Restriction_Set_Dependences.First ..
+                     Restriction_Set_Dependences.Last
+            loop
+               Unam := Restriction_Set_Dependences.Table (J);
+
+               --  Don't need an entry if already in the unit table
+
+               for U in 0 .. Last_Unit loop
+                  if Unit_Name (U) = Unam then
+                     goto Next_Restriction_Set;
+                  end if;
+               end loop;
+
+               --  Otherwise generate the entry
+
+               Write_Info_Initiate ('W');
+               Write_Info_Char (' ');
+               Write_Info_Name (Unam);
+               Write_Info_EOL;
+
+            <<Next_Restriction_Set>>
+               null;
+            end loop;
+         end;
       end Write_With_Lines;
 
    --  Start of processing for Write_ALI
@@ -811,15 +1085,41 @@ package body Lib.Writ is
          return;
       end if;
 
-      --  Build sorted source dependency table. We do this right away,
-      --  because it is referenced by Up_To_Date_ALI_File_Exists.
+      --  Generation of ALI files may be disabled, e.g. for formal verification
+      --  back-end.
+
+      if Disable_ALI_File then
+         return;
+      end if;
+
+      --  Build sorted source dependency table. We do this right away, because
+      --  it is referenced by Up_To_Date_ALI_File_Exists.
 
       for Unum in Units.First .. Last_Unit loop
          if Cunit_Entity (Unum) = Empty
-           or else not From_With_Type (Cunit_Entity (Unum))
+           or else not From_Limited_With (Cunit_Entity (Unum))
          then
-            Num_Sdep := Num_Sdep + 1;
-            Sdep_Table (Num_Sdep) := Unum;
+            --  Units that are not analyzed need not appear in the dependency
+            --  list. These units are either units appearing in limited_with
+            --  clauses of other units, or units loaded for inlining that end
+            --  up not inlined by a later decision of the inlining code, to
+            --  prevent circularities. We want to exclude these files from the
+            --  list of dependencies, so that the dependency number of other
+            --  is correctly set, as that number is used by cross-reference
+            --  tools to relate entity information to the unit in which they
+            --  are declared.
+
+            if Present (Cunit_Entity (Unum))
+              and then Ekind (Cunit_Entity (Unum)) = E_Void
+              and then Nkind (Unit (Cunit (Unum))) /= N_Subunit
+              and then Serious_Errors_Detected = 0
+            then
+               null;
+
+            else
+               Num_Sdep := Num_Sdep + 1;
+               Sdep_Table (Num_Sdep) := Unum;
+            end if;
          end if;
       end loop;
 
@@ -827,19 +1127,20 @@ package body Lib.Writ is
 
       Lib.Sort (Sdep_Table (1 .. Num_Sdep));
 
-      --  If we are not generating code, and there is an up to date
-      --  ali file accessible, read it, and acquire the compilation
-      --  arguments from this file.
+      --  If we are not generating code, and there is an up to date ALI file
+      --  file accessible, read it, and acquire the compilation arguments from
+      --  this file. In GNATprove mode, always generate the ALI file, which
+      --  contains a special section for formal verification.
 
-      if Operating_Mode /= Generate_Code then
+      if Operating_Mode /= Generate_Code and then not GNATprove_Mode then
          if Up_To_Date_ALI_File_Exists then
             Update_Tables_From_ALI_File;
             return;
          end if;
       end if;
 
-      --  Otherwise acquire compilation arguments and prepare to write
-      --  out a new ali file.
+      --  Otherwise acquire compilation arguments and prepare to write out a
+      --  new ali file.
 
       Create_Output_Library_Info;
 
@@ -877,6 +1178,11 @@ package body Lib.Writ is
                Write_Info_Nat (Opt.Time_Slice_Value);
             end if;
 
+            if Main_CPU (Main_Unit) /= Default_Main_CPU then
+               Write_Info_Str (" C=");
+               Write_Info_Nat (Main_CPU (Main_Unit));
+            end if;
+
             Write_Info_Str (" W=");
             Write_Info_Char
               (WC_Encoding_Letters (Wide_Character_Encoding_Method));
@@ -906,7 +1212,17 @@ package body Lib.Writ is
 
             S := Specification (U);
 
-            if No (Parameter_Specifications (S)) then
+            --  A generic subprogram is never a main program
+
+            if Nkind (U) = N_Subprogram_Body
+              and then Present (Corresponding_Spec (U))
+              and then
+                Ekind_In (Corresponding_Spec (U), E_Generic_Procedure,
+                                                  E_Generic_Function)
+            then
+               null;
+
+            elsif No (Parameter_Specifications (S)) then
                if Nkind (S) = N_Procedure_Specification then
                   Write_Info_Initiate ('M');
                   Write_Info_Str (" P");
@@ -955,23 +1271,7 @@ package body Lib.Writ is
          Write_Info_Str (" DB");
       end if;
 
-      if Opt.Float_Format /= ' ' then
-         Write_Info_Str (" F");
-
-         if Opt.Float_Format = 'I' then
-            Write_Info_Char ('I');
-
-         elsif Opt.Float_Format_Long = 'D' then
-            Write_Info_Char ('D');
-
-         else
-            Write_Info_Char ('G');
-         end if;
-      end if;
-
-      if Tasking_Used
-        and then not Is_Predefined_File_Name (Unit_File_Name (Main_Unit))
-      then
+      if Tasking_Used and then not Is_Predefined_Unit (Main_Unit) then
          if Locking_Policy /= ' ' then
             Write_Info_Str  (" L");
             Write_Info_Char (Locking_Policy);
@@ -989,6 +1289,19 @@ package body Lib.Writ is
          end if;
       end if;
 
+      if GNATprove_Mode then
+         Write_Info_Str (" GP");
+      end if;
+
+      if Partition_Elaboration_Policy /= ' ' then
+         Write_Info_Str  (" E");
+         Write_Info_Char (Partition_Elaboration_Policy);
+      end if;
+
+      if No_Component_Reordering_Config then
+         Write_Info_Str (" NC");
+      end if;
+
       if not Object then
          Write_Info_Str (" NO");
       end if;
@@ -1001,6 +1314,11 @@ package body Lib.Writ is
          Write_Info_Str (" NS");
       end if;
 
+      if Default_SSO_Config /= ' ' then
+         Write_Info_Str (" O");
+         Write_Info_Char (Default_SSO_Config);
+      end if;
+
       if Sec_Stack_Used then
          Write_Info_Str (" SS");
       end if;
@@ -1009,7 +1327,11 @@ package body Lib.Writ is
          Write_Info_Str (" UA");
       end if;
 
-      if Exception_Mechanism = Back_End_Exceptions then
+      if Front_End_Exceptions then
+         Write_Info_Str (" FX");
+      end if;
+
+      if ZCX_Exceptions then
          Write_Info_Str (" ZX");
       end if;
 
@@ -1022,71 +1344,145 @@ package body Lib.Writ is
       --  for which we have generated code
 
       for Unit in Units.First .. Last_Unit loop
-         if Units.Table (Unit).Generate_Code
-           or else Unit = Main_Unit
-         then
+         if Units.Table (Unit).Generate_Code or else Unit = Main_Unit then
             if not Has_No_Elaboration_Code (Cunit (Unit)) then
                Main_Restrictions.Violated (No_Elaboration_Code) := True;
             end if;
          end if;
       end loop;
 
-      --  Output first restrictions line
+      --  Positional case (only if debug flag -gnatd.R is set)
 
-      Write_Info_Initiate ('R');
-      Write_Info_Char (' ');
+      if Debug_Flag_Dot_RR then
 
-      --  First the information for the boolean restrictions
+         --  Output first restrictions line
 
-      for R in All_Boolean_Restrictions loop
-         if Main_Restrictions.Set (R)
-           and then not Restriction_Warnings (R)
-         then
-            Write_Info_Char ('r');
-         elsif Main_Restrictions.Violated (R) then
-            Write_Info_Char ('v');
-         else
-            Write_Info_Char ('n');
-         end if;
-      end loop;
+         Write_Info_Initiate ('R');
+         Write_Info_Char (' ');
 
-      --  And now the information for the parameter restrictions
+         --  First the information for the boolean restrictions
 
-      for RP in All_Parameter_Restrictions loop
-         if Main_Restrictions.Set (RP)
-           and then not Restriction_Warnings (RP)
-         then
-            Write_Info_Char ('r');
-            Write_Info_Nat (Nat (Main_Restrictions.Value (RP)));
-         else
-            Write_Info_Char ('n');
-         end if;
+         for R in All_Boolean_Restrictions loop
+            if Main_Restrictions.Set (R)
+              and then not Restriction_Warnings (R)
+            then
+               Write_Info_Char ('r');
+            elsif Main_Restrictions.Violated (R) then
+               Write_Info_Char ('v');
+            else
+               Write_Info_Char ('n');
+            end if;
+         end loop;
 
-         if not Main_Restrictions.Violated (RP)
-           or else RP not in Checked_Parameter_Restrictions
-         then
-            Write_Info_Char ('n');
-         else
-            Write_Info_Char ('v');
-            Write_Info_Nat (Nat (Main_Restrictions.Count (RP)));
+         --  And now the information for the parameter restrictions
 
-            if Main_Restrictions.Unknown (RP) then
-               Write_Info_Char ('+');
+         for RP in All_Parameter_Restrictions loop
+            if Main_Restrictions.Set (RP)
+              and then not Restriction_Warnings (RP)
+            then
+               Write_Info_Char ('r');
+               Write_Info_Nat (Nat (Main_Restrictions.Value (RP)));
+            else
+               Write_Info_Char ('n');
             end if;
-         end if;
-      end loop;
 
-      Write_Info_EOL;
+            if not Main_Restrictions.Violated (RP)
+              or else RP not in Checked_Parameter_Restrictions
+            then
+               Write_Info_Char ('n');
+            else
+               Write_Info_Char ('v');
+               Write_Info_Nat (Nat (Main_Restrictions.Count (RP)));
+
+               if Main_Restrictions.Unknown (RP) then
+                  Write_Info_Char ('+');
+               end if;
+            end if;
+         end loop;
+
+         Write_Info_EOL;
+
+      --  Named case (if debug flag -gnatd.R is not set)
+
+      else
+         declare
+            C : Character;
+
+         begin
+            --  Write RN header line with preceding blank line
+
+            Write_Info_EOL;
+            Write_Info_Initiate ('R');
+            Write_Info_Char ('N');
+            Write_Info_EOL;
+
+            --  First the lines for the boolean restrictions
+
+            for R in All_Boolean_Restrictions loop
+               if Main_Restrictions.Set (R)
+                 and then not Restriction_Warnings (R)
+               then
+                  C := 'R';
+               elsif Main_Restrictions.Violated (R) then
+                  C := 'V';
+               else
+                  goto Continue;
+               end if;
+
+               Write_Info_Initiate ('R');
+               Write_Info_Char (C);
+               Write_Info_Char (' ');
+               Write_Info_Str (All_Boolean_Restrictions'Image (R));
+               Write_Info_EOL;
+
+            <<Continue>>
+               null;
+            end loop;
+         end;
+
+         --  And now the lines for the parameter restrictions
+
+         for RP in All_Parameter_Restrictions loop
+            if Main_Restrictions.Set (RP)
+              and then not Restriction_Warnings (RP)
+            then
+               Write_Info_Initiate ('R');
+               Write_Info_Str ("R ");
+               Write_Info_Str (All_Parameter_Restrictions'Image (RP));
+               Write_Info_Char ('=');
+               Write_Info_Nat (Nat (Main_Restrictions.Value (RP)));
+               Write_Info_EOL;
+            end if;
+
+            if not Main_Restrictions.Violated (RP)
+              or else RP not in Checked_Parameter_Restrictions
+            then
+               null;
+            else
+               Write_Info_Initiate ('R');
+               Write_Info_Str ("V ");
+               Write_Info_Str (All_Parameter_Restrictions'Image (RP));
+               Write_Info_Char ('=');
+               Write_Info_Nat (Nat (Main_Restrictions.Count (RP)));
+
+               if Main_Restrictions.Unknown (RP) then
+                  Write_Info_Char ('+');
+               end if;
+
+               Write_Info_EOL;
+            end if;
+         end loop;
+      end if;
 
       --  Output R lines for No_Dependence entries
 
-      for J in No_Dependence.First .. No_Dependence.Last loop
-         if In_Extended_Main_Source_Unit (No_Dependence.Table (J).Unit)
-           and then not No_Dependence.Table (J).Warn
+      for J in No_Dependences.First .. No_Dependences.Last loop
+         if In_Extended_Main_Source_Unit (No_Dependences.Table (J).Unit)
+           and then not No_Dependences.Table (J).Warn
          then
             Write_Info_Initiate ('R');
             Write_Info_Char (' ');
-            Write_Unit_Name (No_Dependence.Table (J).Unit);
+            Write_Unit_Name (No_Dependences.Table (J).Unit);
             Write_Info_EOL;
          end if;
       end loop;
@@ -1172,8 +1568,16 @@ package body Lib.Writ is
 
             --  Normal case of a unit entry with a source index
 
-            if Sind /= No_Source_File then
-               Fname := File_Name (Sind);
+            if Sind > No_Source_File then
+               --  We never want directory information in ALI files
+               --  ???But back out this change temporarily until
+               --  gprbuild is fixed.
+
+               if False then
+                  Fname := Strip_Directory (File_Name (Sind));
+               else
+                  Fname := File_Name (Sind);
+               end if;
 
                --  Ensure that on platforms where the file names are not
                --  case sensitive, the recorded file name is in lower case.
@@ -1184,23 +1588,38 @@ package body Lib.Writ is
                   Fname := Name_Find;
                end if;
 
-               Write_Info_Name (Fname);
+               Write_Info_Name_May_Be_Quoted (Fname);
                Write_Info_Tab (25);
                Write_Info_Str (String (Time_Stamp (Sind)));
                Write_Info_Char (' ');
                Write_Info_Str (Get_Hex_String (Source_Checksum (Sind)));
 
+               --  If the dependency comes from a limited_with clause, record
+               --  limited_checksum. This is disabled until full checksum
+               --  changes are checked.
+
+               --  if Present (Cunit_Entity (Unum))
+               --    and then From_Limited_With (Cunit_Entity (Unum))
+               --  then
+               --     Write_Info_Char (' ');
+               --     Write_Info_Char ('Y');
+               --     Write_Info_Str (Get_Hex_String (Limited_Chk_Sum (Sind)));
+               --  end if;
+
                --  If subunit, add unit name, omitting the %b at the end
 
-               if Present (Cunit (Unum))
-                 and then Nkind (Unit (Cunit (Unum))) = N_Subunit
-               then
+               if Present (Cunit (Unum)) then
                   Get_Decoded_Name_String (Unit_Name (Unum));
                   Write_Info_Char (' ');
-                  Write_Info_Str (Name_Buffer (1 .. Name_Len - 2));
+
+                  if Nkind (Unit (Cunit (Unum))) = N_Subunit then
+                     Write_Info_Str (Name_Buffer (1 .. Name_Len - 2));
+                  else
+                     Write_Info_Str (Name_Buffer (1 .. Name_Len));
+                  end if;
                end if;
 
-               --  If Source_Reference pragma used output information
+               --  If Source_Reference pragma used, output information
 
                if Num_SRef_Pragmas (Sind) > 0 then
                   Write_Info_Char (' ');
@@ -1232,16 +1651,19 @@ package body Lib.Writ is
 
       --  Output cross-references
 
-      Output_References;
+      if Opt.Xref_Active then
+         Output_References;
+      end if;
 
       --  Output SCO information if present
 
       if Generate_SCO then
+         SCO_Record_Filtered;
          SCO_Output;
       end if;
 
       --  Output final blank line and we are done. This final blank line is
-      --  probably junk, but we don't feel like making an incompatible change!
+      --  probably junk, but we don't feel like making an incompatible change.
 
       Write_Info_Terminate;
       Close_Output_Library_Info;