From patchwork Mon Oct 1 08:39:53 2012 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 188242 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 8D3DB2C00E5 for ; Mon, 1 Oct 2012 18:40:06 +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=1349685606; 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=I7mLB4P4+iCRaLUSK5p/ iH/xvFk=; b=O2qq5Dxg+uApYPXcuQdJmgVNPrYDPcM/nC7Xeeq1HTOv764dPw18 W8PusfXBtsfTgMhT0oT52mmEfK/CHLDrKxsai3si7b2zZcJE/3Ekk6sPHLOoSqqC 0dZ/8EBJUJwKjNZDttRyvtHlwlqdkiNCHDAEu/AO0MmNTeHPCRbM+a8= 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=LHxRkp/leMpWAZCFLb4PR/cxfyBe2133+T9o0AtD/vV9Jdw3fvwSnzptovSus8 LErZZnui1qVRVk4ugX+3L7bTcXYMy7D0Ll4eXBxK7wYfKp0qzmFTQ2vgZ/Kk2/et IJcyyXJGh/Y3RhrGiVkqLRwMF5aXhQ9fGAoyexISqCq7s=; Received: (qmail 20471 invoked by alias); 1 Oct 2012 08:39:59 -0000 Received: (qmail 20461 invoked by uid 22791); 1 Oct 2012 08:39:58 -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; Mon, 01 Oct 2012 08:39:54 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id A29B81C754C; Mon, 1 Oct 2012 04:39:53 -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 bzUZ0WjBab1s; Mon, 1 Oct 2012 04:39:53 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 75DC61C7540; Mon, 1 Oct 2012 04:39:53 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 7143D3FF09; Mon, 1 Oct 2012 04:39:53 -0400 (EDT) Date: Mon, 1 Oct 2012 04:39:53 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Ed Schonberg Subject: [Ada] Invariant checks and multiple inheritance Message-ID: <20121001083953.GA4163@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 This patch fixes some problems involving the use of Type_Invariant'Class on the ancestor of a derived type that also implements an interface. The following command: gnatmake -q -gnat12 -gnata test_invariant test_invariant must yield: raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed inherited invariant from invariants.ads:5 --- with Carrier.Next; use Carrier.Next; procedure Test_Invariant is THing : NT; begin HeHe (Thing); end; --- package Carrier is type PT is tagged private; function Invariant(X: PT) return Boolean; procedure Do_AandB(X: out PT); private type PT is tagged record A,B: Integer; end record; procedure Do_A(X: out PT; V: Integer); procedure Do_B(X: out PT; V: Integer); end Carrier; --- Package body Carrier is procedure Do_AandB(X: out PT) is begin Do_A(X,42); Do_B(X,42); end Do_AandB; function Invariant(X: PT) return Boolean is begin return X.A=X.B; end Invariant; procedure Do_A(X: out PT; V: Integer) is begin X.A := V; end Do_A; procedure Do_B(X: out PT; V: Integer) is begin X.B := V; end do_B; end Carrier; --- with Carrier; use Carrier; Package Invariants is type T is new PT with private with Type_Invariant'class => Invariant(PT(T)); -- type T introduced by my ignorance about visibility rules inside -- of type invariants; maybe could be on Carrier.PT already, or -- only on I below. The conclusion applies in all cases and -- combinations. private type T is new PT with null record; end Invariants; --- package Interf is type I is Interface -- if you want: with Type_Invariant'Class => Invariant(I); -- maybe with the same "carrier detour" because of visibility? function Invariant(X: I) return boolean is abstract; procedure HeHe(X: out I) is abstract; end Interf; --- with Invariants; with Interf; package Carrier.Next is type NT is new Invariants.T and Interf.I with null record; procedure HeHe(X: out NT); -- newly added op; definitely needs -- to check the invariant, or else.... end Carrier.Next; --- package body Carrier.Next is procedure HeHe(X: out NT) is begin DO_A(PT(X),666); -- BREAKS THE INVARIANT end Hehe; -- HeHe BETTER RAISE ASSERTION_ERROR end Carrier.Next; Tested on x86_64-pc-linux-gnu, committed on trunk 2012-10-01 Ed Schonberg * aspects.ads: Type_Invariant'class is a valid aspect. * sem_ch6.adb (Is_Public_Subprogram_For): with the exception of initialization procedures, subprograms that do not come from source are not public for the purpose of invariant checking. * sem_ch13.adb (Build_Invariant_Procedure): Handle properly the case of a non-private type in a package without a private part, when the type inherits invariants from its ancestor. Index: aspects.ads =================================================================== --- aspects.ads (revision 191888) +++ aspects.ads (working copy) @@ -191,11 +191,12 @@ -- The following array indicates aspects that accept 'Class Class_Aspect_OK : constant array (Aspect_Id) of Boolean := - (Aspect_Invariant => True, - Aspect_Pre => True, - Aspect_Predicate => True, - Aspect_Post => True, - others => False); + (Aspect_Invariant => True, + Aspect_Pre => True, + Aspect_Predicate => True, + Aspect_Post => True, + Aspect_Type_Invariant => True, + others => False); -- The following array indicates aspects that a subtype inherits from -- its base type. True means that the subtype inherits the aspect from Index: sem_ch6.adb =================================================================== --- sem_ch6.adb (revision 191888) +++ sem_ch6.adb (working copy) @@ -11342,10 +11342,16 @@ -- If the subprogram declaration is not a list member, it must be -- an Init_Proc, in which case we want to consider it to be a -- public subprogram, since we do get initializations to deal with. + -- Other internally generated subprograms are not public. - if not Is_List_Member (DD) then + if not Is_List_Member (DD) + and then Is_Init_Proc (DD) + then return True; + elsif not Comes_From_Source (DD) then + return False; + -- Otherwise we test whether the subprogram is declared in the -- visible declarations of the package containing the type. Index: sem_ch13.adb =================================================================== --- sem_ch13.adb (revision 191900) +++ sem_ch13.adb (working copy) @@ -5188,9 +5188,6 @@ Statements => Stmts)); -- Insert procedure declaration and spec at the appropriate points. - -- Skip this if there are no private declarations (that's an error - -- that will be diagnosed elsewhere, and there is no point in having - -- an invariant procedure set if the full declaration is missing). if Present (Private_Decls) then @@ -5214,6 +5211,19 @@ if In_Private_Part (Current_Scope) then Analyze (PBody); end if; + + -- If there are no private declarations this may be an error that + -- will be diagnosed elsewhere. However, if this is a non-private + -- type that inherits invariants, it needs no completion and there + -- may be no private part. In this case insert invariant procedure + -- at end of current declarative list, and analyze at once, given + -- that the type is about to be frozen. + + elsif not Is_Private_Type (Typ) then + Append_To (Visible_Decls, PDecl); + Append_To (Visible_Decls, PBody); + Analyze (PDecl); + Analyze (PBody); end if; end if; end Build_Invariant_Procedure;