From f5a7c656e5ffde112fdcf122bc6b4ca5ed31643e Mon Sep 17 00:00:00 2001
From: Yannick Moy <moy@adacore.com>
Date: Wed, 6 Jan 2021 11:31:28 +0100
Subject: [PATCH] [Ada] Use error marker for messages in GNATprove mode
gcc/ada/
* gnat1drv.adb (Adjust_Global_Switches): Force error marker in
GNATprove mode.
---
gcc/ada/gnat1drv.adb | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 3afe801efaa6..40f9228dd5c4 100644
--- 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.
--
GitLab