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;
 

Reply via email to