Usually a wrapper is generated in the case of a classwide type as actual of a
generic package. In Gnatprove_Mode, and when the generic has external
axiomatizations, This wrapper is not only useless but confuses gnatprove, so
it is disabled here.

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

2015-01-07  Johannes Kanig  <ka...@adacore.com>

        * sem_ch8.adb (Analyze_Subprogram_Renaming) do
        not build function wrapper in gnatprove mode when the package
        is externally axiomatized.

Index: sem_ch8.adb
===================================================================
--- sem_ch8.adb (revision 219282)
+++ sem_ch8.adb (working copy)
@@ -2710,7 +2710,17 @@
          --  Check whether the renaming is for a defaulted actual subprogram
          --  with a class-wide actual.
 
-         if CW_Actual and then Box_Present (Inst_Node) then
+         --  The class-wide wrapper is not needed when we are in
+         --  GNATprove_Mode and there is an external axiomatization on the
+         --  package.
+
+         if CW_Actual
+            and then Box_Present (Inst_Node)
+            and then not (GNATprove_Mode
+                          and then
+                          Present (Containing_Package_With_Ext_Axioms
+                                     (Formal_Spec)))
+         then
             Build_Class_Wide_Wrapper (New_S, Old_S);
 
          elsif Is_Entity_Name (Nam)

Reply via email to