diff mbox

[Ada] Disable wrapper for SPARK in the case of External Axiomatization

Message ID 20150107095308.GA6497@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Jan. 7, 2015, 9:53 a.m. UTC 
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  <kanig@adacore.com>

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

Patch

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)