diff mbox

[Ada] Do not perform tagged type expansion in Alfa mode

Message ID 20110919083256.GA16477@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Sept. 19, 2011, 8:32 a.m. UTC 
Tagged type expansion should not be performed in the formal verification mode.
It was previously performed, to avoid some errors, which are now corrected.

Tested on x86_64-pc-linux-gnu, committed on trunk

2011-09-19  Yannick Moy  <moy@adacore.com>

	* gnat1drv.adb (Adjust_Global_Switches): Set tagged type
	expansion to False in mode Alfa
diff mbox

Patch

Index: gnat1drv.adb
===================================================================
--- gnat1drv.adb	(revision 178955)
+++ gnat1drv.adb	(working copy)
@@ -477,12 +477,9 @@ 
 
          Global_Discard_Names := True;
 
-         --  We would prefer to suppress the expansion of tagged types and
-         --  dispatching calls, so that one day GNATprove can handle them
-         --  directly. Unfortunately, this is causing problems in some cases,
-         --  so keep this expansion for the time being. To be investigated ???
+         --  Suppress the expansion of tagged types and dispatching calls
 
-         Tagged_Type_Expansion := True;
+         Tagged_Type_Expansion := False;
       end if;
    end Adjust_Global_Switches;