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 <[email protected]>
* gnat1drv.adb (Adjust_Global_Switches): Set tagged type
expansion to False in mode Alfa
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;