[Ada] Contracts on imported subprograms

[Ada] Contracts on imported subprograms

[Arnaud Charlet]

[-- Attachment #1: Type: text/plain, Size: 1233 bytes --]

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  <schonberg@adacore.com>

	* freeze.adb (Freeze_Entity): Warn if an imported subprogram
	has pre/post conditions, because these will not be enforced.


[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 1013 bytes --]

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