[Ada] Use error marker for messages in GNATprove mode

Message ID 20210504095222.GA90434@adacore.com
State New
Headers show
  • [Ada] Use error marker for messages in GNATprove mode
Related show

Commit Message

Pierre-Marie de Rodat May 4, 2021, 9:52 a.m.
Force the use of the "error:" marker for error messages in GNATprove.
This helps distinguishing these messages from others like warnings,
check messages and info messages, in particular when colored output is

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


	* gnat1drv.adb (Adjust_Global_Switches): Force error marker in
	GNATprove mode.


diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -565,6 +565,10 @@  procedure Gnat1drv is
          Tagged_Type_Expansion := False;
+         --  Force the use of "error:" prefix for error messages
+         Unique_Error_Tag := True;
          --  Detect that the runtime library support for floating-point numbers
          --  may not be compatible with SPARK analysis of IEEE-754 floats.