[Ada] Display source code pointing at locations in messages for GNATprove

gcc/ada/

	* errout.adb: (Error_Msg-Internal): Pass the location for a line
	insertion if any in the message.
	(Output_Messages: Add display of source code lines if -gnatdF is
	set.
	(Write_Source_Code_Line): Code clean up.
	* erroutc.adb (Prescan_Message): Apply prescan for continuation
	lines when -gnatdF is set, and record presence of line
	insertion.
	* erroutc.ads (Has_Insertion_Line): New global for prescan.
	(Error_Msg_Object): Add field to record line insertion if
	present.
	* errutil.adb (Error_Msg): Pass no location for Insertion_Sloc.

4 files changed, 114 insertions, 11 deletions

diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index 36e8f6a..1326cdc 100644
--- a/gcc/ada/errout.adb
+++ b/gcc/ada/errout.adb
@@ -1119,6 +1119,8 @@ package body Errout is
           Prev                => No_Error_Msg,
           Sptr                => Sptr,
           Optr                => Optr,
+          Insertion_Sloc      => (if Has_Insertion_Line then Error_Msg_Sloc
+                                  else No_Location),
           Sfile               => Get_Source_File_Index (Sptr),
           Line                => Get_Physical_Line_Number (Sptr),
           Col                 => Get_Column_Number (Sptr),
@@ -1823,8 +1825,8 @@ package body Errout is
    ---------------------
 
    procedure Output_Messages is
-      E        : Error_Msg_Id;
-      Err_Flag : Boolean;
+
+      --  Local subprograms
 
       procedure Write_Error_Summary;
       --  Write error summary
@@ -1835,6 +1837,15 @@ package body Errout is
       procedure Write_Max_Errors;
       --  Write message if max errors reached
 
+      procedure Write_Source_Code_Line (Loc : Source_Ptr);
+      --  Write the source code line corresponding to Loc, as follows:
+      --
+      --       |
+      --  line |  actual code line here with Loc somewhere
+      --       |                             ^ here
+      --
+      --  where the carret on the last line points to location Loc.
+
       -------------------------
       -- Write_Error_Summary --
       -------------------------
@@ -2025,6 +2036,59 @@ package body Errout is
          end if;
       end Write_Max_Errors;
 
+      ----------------------------
+      -- Write_Source_Code_Line --
+      ----------------------------
+
+      procedure Write_Source_Code_Line (Loc : Source_Ptr) is
+         Line    : constant Pos := Pos (Get_Physical_Line_Number (Loc));
+         Col     : constant Natural := Natural (Get_Column_Number (Loc));
+         Padding : constant String (1 .. Int'Image (Line)'Length) :=
+                              (others => ' ');
+
+         Buf     : Source_Buffer_Ptr;
+         Cur_Loc : Source_Ptr := Loc;
+      begin
+         if Loc >= First_Source_Ptr then
+            Buf := Source_Text (Get_Source_File_Index (Loc));
+
+            --  First line
+
+            Write_Str (Padding);
+            Write_Char ('|');
+            Write_Eol;
+
+            --  Second line with the actual source code line
+
+            Write_Int (Line);
+            Write_Str (" |");
+            Write_Str (String (Buf (Loc - Source_Ptr (Col) + 1  .. Loc - 1)));
+
+            while Cur_Loc <= Buf'Last
+              and then Buf (Cur_Loc) /= ASCII.LF
+            loop
+               Write_Char (Buf (Cur_Loc));
+               Cur_Loc := Cur_Loc + 1;
+            end loop;
+
+            Write_Eol;
+
+            --  Third line with carret sign pointing to location Loc
+
+            Write_Str (Padding);
+            Write_Char ('|');
+            Write_Str (String'(1 .. Col - 1 => ' '));
+            Write_Str ("^ here");
+            Write_Eol;
+         end if;
+      end Write_Source_Code_Line;
+
+      --  Local variables
+
+      E          : Error_Msg_Id;
+      Err_Flag   : Boolean;
+      Use_Prefix : Boolean;
+
    --  Start of processing for Output_Messages
 
    begin
@@ -2051,12 +2115,16 @@ package body Errout is
 
          E := First_Error_Msg;
          while E /= No_Error_Msg loop
-            if not Errors.Table (E).Deleted and then not Debug_Flag_KK then
 
-               --  If -gnatdF is used, separate main messages from previous
-               --  messages with a newline and make continuation messages
-               --  follow the main message with only an indentation of two
-               --  space characters, without repeating file:line:col: prefix.
+            --  If -gnatdF is used, separate main messages from previous
+            --  messages with a newline and make continuation messages
+            --  follow the main message with only an indentation of two
+            --  space characters, without repeating file:line:col: prefix.
+
+            Use_Prefix :=
+              not (Debug_Flag_FF and then Errors.Table (E).Msg_Cont);
+
+            if not Errors.Table (E).Deleted and then not Debug_Flag_KK then
 
                if Debug_Flag_FF then
                   if Errors.Table (E).Msg_Cont then
@@ -2066,7 +2134,7 @@ package body Errout is
                   end if;
                end if;
 
-               if not (Debug_Flag_FF and then Errors.Table (E).Msg_Cont) then
+               if Use_Prefix then
                   if Full_Path_Name_For_Brief_Errors then
                      Write_Name (Full_Ref_Name (Errors.Table (E).Sfile));
                   else
@@ -2089,6 +2157,22 @@ package body Errout is
 
                Output_Msg_Text (E);
                Write_Eol;
+
+               if Debug_Flag_FF then
+                  if Errors.Table (E).Msg_Cont then
+                     declare
+                        Loc : constant Source_Ptr :=
+                          Errors.Table (E).Insertion_Sloc;
+                     begin
+                        if Loc /= No_Location then
+                           Write_Source_Code_Line (Loc);
+                        end if;
+                     end;
+
+                  else
+                     Write_Source_Code_Line (Errors.Table (E).Sptr);
+                  end if;
+               end if;
             end if;
 
             E := Errors.Table (E).Next;
diff --git a/gcc/ada/erroutc.adb b/gcc/ada/erroutc.adb
index df174f6..93f53bb 100644
--- a/gcc/ada/erroutc.adb
+++ b/gcc/ada/erroutc.adb
@@ -814,9 +814,9 @@ package body Erroutc is
       J : Natural;
 
    begin
-      --  Nothing to do for continuation line
+      --  Nothing to do for continuation line, unless -gnatdF is set
 
-      if Msg (Msg'First) = '\' then
+      if not Debug_Flag_FF and then Msg (Msg'First) = '\' then
          return;
       end if;
 
@@ -826,6 +826,7 @@ package body Erroutc is
       Is_Unconditional_Msg := False;
       Is_Warning_Msg       := False;
       Has_Double_Exclam    := False;
+      Has_Insertion_Line   := False;
 
       --  Check style message
 
@@ -903,6 +904,12 @@ package body Erroutc is
                J := J + 1;
             end if;
 
+         --  Insertion line (# insertion)
+
+         elsif Msg (J) = '#' then
+            Has_Insertion_Line := True;
+            J := J + 1;
+
          --  Non-serious error (| insertion)
 
          elsif Msg (J) = '|' then
diff --git a/gcc/ada/erroutc.ads b/gcc/ada/erroutc.ads
index 8472ee5..4c0e68a 100644
--- a/gcc/ada/erroutc.ads
+++ b/gcc/ada/erroutc.ads
@@ -51,6 +51,10 @@ package Erroutc is
    --  Set true to indicate that the current message contains the insertion
    --  sequence !! (force warnings even in non-main unit source files).
 
+   Has_Insertion_Line : Boolean := False;
+   --  Set True to indicate that the current message contains the insertion
+   --  character # (insert line number reference).
+
    Is_Compile_Time_Msg : Boolean := False;
    --  Set true to indicate that the current message originates from a
    --  Compile_Time_Warning or Compile_Time_Error pragma.
@@ -209,6 +213,9 @@ package Erroutc is
       --  instantiation copy corresponding to the instantiation referenced by
       --  Sptr).
 
+      Insertion_Sloc : Source_Ptr;
+      --  Location in message for insertion character # when used
+
       Line : Physical_Line_Number;
       --  Line number for error message
 
@@ -470,11 +477,15 @@ package Erroutc is
    --    Has_Double_Exclam is set True if the message contains the sequence !!
    --    and is otherwise set False.
    --
+   --    Has_Insertion_Line is set True if the message contains the character #
+   --    and is otherwise set False.
+   --
    --  We need to know right away these aspects of a message, since we will
    --  test these values before doing the full error scan.
    --
    --  Note that the call has no effect for continuation messages (those whose
-   --  first character is '\'), and all variables are left unchanged.
+   --  first character is '\'), and all variables are left unchanged, unless
+   --  -gnatdF is set.
 
    procedure Purge_Messages (From : Source_Ptr; To : Source_Ptr);
    --  All error messages whose location is in the range From .. To (not
diff --git a/gcc/ada/errutil.adb b/gcc/ada/errutil.adb
index 75d29a9..d4821fc 100644
--- a/gcc/ada/errutil.adb
+++ b/gcc/ada/errutil.adb
@@ -209,6 +209,7 @@ package body Errutil is
             Sfile               => Get_Source_File_Index (Sptr),
             Sptr                => Sptr,
             Optr                => Optr,
+            Insertion_Sloc      => No_Location,
             Line                => Get_Physical_Line_Number (Sptr),
             Col                 => Get_Column_Number (Sptr),
             Compile_Time_Pragma => Is_Compile_Time_Msg,