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 cbad1e0f19e8c56a0b33708089eaca529a94d9b8..03cbb30b5f591104e4fbe6d0bdf25ddec8ca5888 100644 (file)
--- 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.