Patchwork [Ada] Contracts on imported subprograms

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

Comments

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 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.

Patch

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