https://gcc.gnu.org/g:8e3bcd151cc302de31736154e02bba29cf8d044d
commit r17-958-g8e3bcd151cc302de31736154e02bba29cf8d044d Author: Andres Toom <[email protected]> Date: Mon Mar 16 11:55:09 2026 +0200 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: --- gcc/ada/gnat1drv.adb | 6 ------ 1 file changed, 6 deletions(-) diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb index cbad1e0f19e8..03cbb30b5f59 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.
