From: Johannes Kanig <[email protected]>
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.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/gnat1drv.adb | 17 +++++++++++++++++
1 file changed, 17 insertions(+)
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 03cbb30b5f5..e4357d5fc8d 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);
--
2.53.0
