diff options
| author | Yannick Moy <moy@adacore.com> | 2021-01-06 11:31:28 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-05-04 05:17:32 -0400 |
| commit | f5a7c656e5ffde112fdcf122bc6b4ca5ed31643e (patch) | |
| tree | c507bac1d4eb7a417ecdfccebae7b2489c86c010 | |
| parent | 0964be0713f6c9a9e6a2a0a3efe869b7570dc9ce (diff) | |
| download | gcc-f5a7c656e5ffde112fdcf122bc6b4ca5ed31643e.zip gcc-f5a7c656e5ffde112fdcf122bc6b4ca5ed31643e.tar.gz gcc-f5a7c656e5ffde112fdcf122bc6b4ca5ed31643e.tar.bz2 | |
[Ada] Use error marker for messages in GNATprove mode
gcc/ada/
* gnat1drv.adb (Adjust_Global_Switches): Force error marker in
GNATprove mode.
| -rw-r--r-- | gcc/ada/gnat1drv.adb | 4 |
1 files changed, 4 insertions, 0 deletions
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. |