From patchwork Tue Jul 17 10:14:54 2012 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 171386 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) by ozlabs.org (Postfix) with SMTP id 8458F2C0170 for ; Tue, 17 Jul 2012 20:15:17 +1000 (EST) Comment: DKIM? See http://www.dkim.org DKIM-Signature: v=1; a=rsa-sha1; c=relaxed/relaxed; d=gcc.gnu.org; s=default; x=1343124917; h=Comment: DomainKey-Signature:Received:Received:Received:Received:Received: Received:Received:Date:From:To:Cc:Subject:Message-ID: MIME-Version:Content-Type:Content-Disposition:User-Agent: Mailing-List:Precedence:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:Sender:Delivered-To; bh=89tgxxLa/S0A2ivG0ckY PnyaqFM=; b=wVjLK2bEEOd3fVTQnZEPtWxr2DWQSVAeCYxg2A4RaJX1D5cUV/d8 bsaiVlDxz5G+p9rb9aHkxj4UzCYDV77tmDgo2zt0sYVDIvcl5ZR+wfD7JOgixAov JAGBi9rJsqMWoBc73UYRPEsj7JyKX0CAys3qaF6OwEf/bNWgjM4H7jE= Comment: DomainKeys? See http://antispam.yahoo.com/domainkeys DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=default; d=gcc.gnu.org; h=Received:Received:X-SWARE-Spam-Status:X-Spam-Check-By:Received:Received:Received:Received:Received:Date:From:To:Cc:Subject:Message-ID:MIME-Version:Content-Type:Content-Disposition:User-Agent:Mailing-List:Precedence:List-Id:List-Unsubscribe:List-Archive:List-Post:List-Help:Sender:Delivered-To; b=H1Uh9tEvPG1brZTx6Jvc50i6OLKpmEv/5Mfu7qfONSLr/N7caCrlIyQSGmrWfS bROkWtUen0UdJD1AIFtotVooNVjzM6/2rrG3nH0HXVlLItmHvkGy7fUm2K4iGJJk vb16WyJCoIbbj5rRBRVK8CXkGJFXIN4XVPdxeD37lC0ts=; Received: (qmail 29819 invoked by alias); 17 Jul 2012 10:15:08 -0000 Received: (qmail 29739 invoked by uid 22791); 17 Jul 2012 10:15:07 -0000 X-SWARE-Spam-Status: No, hits=-1.9 required=5.0 tests=AWL, BAYES_00, RCVD_IN_HOSTKARMA_NO X-Spam-Check-By: sourceware.org Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.43rc1) with ESMTP; Tue, 17 Jul 2012 10:14:55 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 8AEC81C6E54; Tue, 17 Jul 2012 06:14:54 -0400 (EDT) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id 1mhi6FAezoRA; Tue, 17 Jul 2012 06:14:54 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 729CC1C6280; Tue, 17 Jul 2012 06:14:54 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 6F98A3FF09; Tue, 17 Jul 2012 06:14:54 -0400 (EDT) Date: Tue, 17 Jul 2012 06:14:54 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Ed Schonberg Subject: [Ada] Contracts on imported subprograms Message-ID: <20120717101454.GA25905@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org 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 * 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