From patchwork Tue Aug 2 14:28:40 2011 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 107929 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 7D460B71D4 for ; Wed, 3 Aug 2011 00:29:02 +1000 (EST) Received: (qmail 325 invoked by alias); 2 Aug 2011 14:29:00 -0000 Received: (qmail 317 invoked by uid 22791); 2 Aug 2011 14:28:59 -0000 X-SWARE-Spam-Status: No, hits=-1.8 required=5.0 tests=AWL,BAYES_00 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, 02 Aug 2011 14:28:42 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id AD4BC2BAEDE; Tue, 2 Aug 2011 10:28:41 -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 ulT9nxijUlgG; Tue, 2 Aug 2011 10:28:41 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 61FC12BAEA5; Tue, 2 Aug 2011 10:28:40 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 52AD73FEE8; Tue, 2 Aug 2011 10:28:40 -0400 (EDT) Date: Tue, 2 Aug 2011 10:28:40 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Ed Schonberg Subject: [Ada] Implementation of Ada2012 rules on preconditions for null procedures Message-ID: <20110802142840.GA1415@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 Ada Issue AI05-0230 specifies that null procedures can only have inheritable 'Class preconditions. For compatibility with the earlier GNAT pragmas for preconditions, this rule only applies to Ada2012 aspect specifications. Compilation of p.ads must yield: p.ads:5:06: aspect "Pre" requires 'Class for null procedure p.ads:17:05: aspect "Pre" requires 'Class for abstract subprogram --- package P is type I is interface; procedure Proc (Obj : I) is null with Pre => False; -- ERROR procedure Proc2 (Obj : in out I) is null with Pre'Class => False; -- OK procedure Proc3 (Obj : in out I) is abstract with Pre'Class => False; -- OK procedure Proc4 (Obj : in out I) is abstract with Pre => False; -- ERROR procedure Proc5 (Obj : out I) is null; pragma Precondition (False); -- OK. GNAT pragma end P; Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-02 Ed Schonberg * sem_prag.adb (Chain_PPC): Implement AI04-0230: null procedures can only have inheritable classwide pre/postconditions. Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 177157) +++ sem_prag.adb (working copy) @@ -1595,6 +1595,19 @@ ("aspect % requires ''Class for abstract subprogram"); end if; + -- AI05-0230: the same restriction applies to null procedures. + -- For compatibility with earlier uses of the Ada pragma, apply + -- this rule only to aspect specifications. + + elsif Nkind (PO) = N_Subprogram_Declaration + and then Nkind (Specification (PO)) = N_Procedure_Specification + and then Null_Present (Specification (PO)) + and then From_Aspect_Specification (N) + and then not Class_Present (N) + then + Error_Pragma + ("aspect % requires ''Class for null procedure"); + elsif not Nkind_In (PO, N_Subprogram_Declaration, N_Generic_Subprogram_Declaration, N_Entry_Declaration)