Patchwork [Ada] Contracts on imported subprograms

mail settings
Submitter Arnaud Charlet
Date July 17, 2012, 10:14 a.m.
Message ID <>
Download mbox | patch
Permalink /patch/171386/
State New
Headers show


Arnaud Charlet - July 17, 2012, 10:14 a.m.
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

must yield:
      warning: pre/post conditions on imported subprogram are not enforced
      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 : return
   with Pre => I /= 10,
   Post => F2'Result /= 0;
   pragma Import (C, F2, "f");

   function F (I : return
   with Pre => I /= 10,
   Post => F'Result /= 0,
   Convention => C,
   External_Name => "f";
end Hello;

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

2012-07-17  Ed Schonberg  <>

	* 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;
+               --  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