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 <m...@adacore.com>
* sem_prag.adb (Analyze_Pre_Post_In_Decl_Part):
Use correct test to detect call in GNATprove mode instead of
compilation.
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;
