From f5a7c656e5ffde112fdcf122bc6b4ca5ed31643e Mon Sep 17 00:00:00 2001 From: Yannick Moy 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 3afe801..40f9228 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. -- 2.7.4