diff mbox

[Ada] Fix handling of wrappers for some primitives in GNATprove

Message ID 20170427105252.GA133044@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet April 27, 2017, 10:52 a.m. UTC 
The wrappers introduced to handle correctly calls to overridden primitives
in class-wide contracts of inherited primitives need to be introduced for
compilation (whether SPARK_Mode is On or Off) but not formal verification
(when GNATprove_Mode is True).

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

2017-04-27  Yannick Moy  <moy@adacore.com>

	* sem_prag.adb (Analyze_Pre_Post_In_Decl_Part):
	Use correct test to detect call in GNATprove mode instead of
	compilation.
diff mbox

Patch

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 247315)
+++ sem_prag.adb	(working copy)
@@ -24007,16 +24007,20 @@ 
                         & "of &", Nod, Disp_Typ);
                   end if;
 
-               --  Otherwise we have a call to an overridden primitive, and
-               --  we will create a common class-wide clone for the body of
-               --  original operation and its eventual inherited versions.
-               --  If the original operation dispatches on result it is
-               --  never inherited and there is no need for a clone.
+               --  Otherwise we have a call to an overridden primitive, and we
+               --  will create a common class-wide clone for the body of
+               --  original operation and its eventual inherited versions.  If
+               --  the original operation dispatches on result it is never
+               --  inherited and there is no need for a clone. There is not
+               --  need for a clone either in GNATprove mode, as cases that
+               --  would require it are rejected (when an inherited primitive
+               --  calls an overridden operation in a class-wide contract), and
+               --  the clone would make proof impossible in some cases.
 
                elsif not Is_Abstract_Subprogram (Spec_Id)
                  and then No (Class_Wide_Clone (Spec_Id))
                  and then not Has_Controlling_Result (Spec_Id)
-                 and then SPARK_Mode /= On
+                 and then not GNATprove_Mode
                then
                   Build_Class_Wide_Clone_Decl (Spec_Id);
                end if;