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)
