In GNATprove mode, a warning on ignored pre/post on imported
subprograms was misleading, as it was meant for compilation only,
while formal verification does take these into account. Hence, we
do not generate this warning in GNATprove mode anymore.
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-02-24 Yannick Moy <m...@adacore.com>
* freeze.adb (Freeze_Entity): Do not issue warning
for pre/post being ignored on imported subprogram in GNATprove
mode.
Index: freeze.adb
===================================================================
--- freeze.adb (revision 208067)
+++ freeze.adb (working copy)
@@ -3868,9 +3868,12 @@
end if;
end;
- -- Pre/post conditions are implemented through a subprogram in
- -- the corresponding body, and therefore are not checked on an
- -- imported subprogram for which the body is not available.
+ -- Pre/post conditions are implemented through a subprogram
+ -- in the corresponding body, and therefore are not checked on
+ -- an imported subprogram for which the body is not available.
+ -- This warning is not issued in GNATprove mode, as these
+ -- contracts are handled in formal verification, so the
+ -- warning would be misleading in that case.
-- Could consider generating a wrapper to take care of this???
@@ -3878,6 +3881,7 @@
and then Is_Imported (E)
and then Present (Contract (E))
and then Present (Pre_Post_Conditions (Contract (E)))
+ and then not GNATprove_Mode
then
Error_Msg_NE
("pre/post conditions on imported subprogram are not "
