From: Andres Toom <toom@adacore.com>
Date: Mon, 16 Mar 2026 09:55:09 +0000 (+0200)
Subject: ada: Do not set Global_Discard_Names in GNATprove_Mode
X-Git-Url: http://git.ipfire.org/gitweb.cgi?a=commitdiff_plain;h=8e3bcd151cc302de31736154e02bba29cf8d044d;p=thirdparty%2Fgcc.git

ada: Do not set Global_Discard_Names in GNATprove_Mode

GNATprove now supports the Image attribute of enumerated types. Hence,
it is important to keep the names of the enumeration literals to be able
to properly reason about them.

gcc/ada/ChangeLog:

	* gnat1drv.adb (Adjust_Global_Switches): Do not set
	Global_Discard_Names in GNATprove_Mode.
---

diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index cbad1e0f19e..03cbb30b5f5 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -527,12 +527,6 @@ procedure Gnat1drv is
                Warnsw.Warning_Doc_Switch,
              others => False));
 
-         --  Suppress the generation of name tables for enumerations, which are
-         --  not needed for formal verification, and fall outside the SPARK
-         --  subset (use of pointers).
-
-         Global_Discard_Names := True;
-
          --  Suppress the expansion of tagged types and dispatching calls,
          --  which lead to the generation of non-SPARK code (use of pointers),
          --  which is more complex to formally verify than the original source.