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 <m...@adacore.com> * 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;