Currently pre/postconditions are enforced by means of expansions in the body
of the corresponding subprogram. If the subprogram is imported there is no
available body on which to insert the checking code, and thr user should be
warned that the contracts will not be enforced.
THe command:
gcc -c -gnat12 -gnata hello.ads
must yield:
hello.ads:7:13:
warning: pre/post conditions on imported subprogram are not enforced
hello.ads:12:13:
warning: pre/post conditions on imported subprogram are not enforced
---
with Ada.Containers.Indefinite_Doubly_Linked_Lists;
with Ada.Finalization; use Ada.Finalization;
with Interfaces.C; use Interfaces.C;
package Hello is
function F2 (I : Interfaces.C.int) return Interfaces.C.int
with Pre => I /= 10,
Post => F2'Result /= 0;
pragma Import (C, F2, "f");
function F (I : Interfaces.C.int) return Interfaces.C.int
with Pre => I /= 10,
Post => F'Result /= 0,
Import,
Convention => C,
External_Name => "f";
end Hello;
Tested on x86_64-pc-linux-gnu, committed on trunk
2012-07-17 Ed Schonberg <schonb...@adacore.com>
* freeze.adb (Freeze_Entity): Warn if an imported subprogram
has pre/post conditions, because these will not be enforced.
Index: freeze.adb
===================================================================
--- freeze.adb (revision 189565)
+++ freeze.adb (working copy)
@@ -3026,6 +3026,21 @@
end if;
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.
+
+ if Is_Subprogram (E)
+ and then Is_Imported (E)
+ and then Present (Contract (E))
+ and then Present (Spec_PPC_List (Contract (E)))
+ then
+ Error_Msg_NE ("pre/post conditions on imported subprogram "
+ & "are not enforced?",
+ E, Spec_PPC_List (Contract (E)));
+ end if;
+
end if;
-- Must freeze its parent first if it is a derived subprogram
