[gcc r17-1285] ada: Call back-end even in case of errors

[Marc Poulhies via Gcc-cvs]

https://gcc.gnu.org/g:65feeb215dd8f81964708b7c1efd1af03b12139b

commit r17-1285-g65feeb215dd8f81964708b7c1efd1af03b12139b
Author: Johannes Kanig <ka...@adacore.com>
Date:   Fri Apr 10 00:06:45 2026 +0000

    ada: Call back-end even in case of errors
    
    In GNATprove mode, still invoke the back end when frontend compilation
    errors are present, so the back-end has a chance to emit error messages
    for SARIF report generation.
    
    gcc/ada/ChangeLog:
    
            * gnat1drv.adb (Gnat1drv): In GNATprove mode, call the
            back end before exiting on compilation errors.

Diff:
---
 gcc/ada/gnat1drv.adb | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 03cbb30b5f59..e4357d5fc8d8 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -1194,6 +1194,23 @@ begin
 
       if Compilation_Errors then
          Ecode := E_Errors;
+
+         if GNATprove_Mode then
+            Atree.Lock;
+            Elists.Lock;
+            Fname.UF.Lock;
+            Ghost.Lock;
+            Inline.Lock;
+            Lib.Lock;
+            Namet.Lock;
+            Nlists.Lock;
+            Sem.Lock;
+            Sinput.Lock;
+            Stringt.Lock;
+
+            Back_End.Call_Back_End (Declarations_Only);
+         end if;
+
          Treepr.Tree_Dump;
          Errout.Finalize (Last_Call => True);
          Errout.Output_Messages (Ecode);