From patchwork Mon Apr 22 10:45:04 2013 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 238434 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]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (Client CN "localhost", Issuer "www.qmailtoaster.com" (not verified)) by ozlabs.org (Postfix) with ESMTPS id 287132C1172 for ; Mon, 22 Apr 2013 20:45:13 +1000 (EST) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=Jc4f4P7L9njjQzRVJagRBpcBnA1otpa5EtpdjkSfEsj10yZZnt V2roP7heSgRvHrAbxmEHlOSFkIj7K7jlMo+xIxpSh/ybMoP/krYiXh3NSL4IUMM7 sf1Y3xOyE+XBwmsTHc42d9omeHNFGozQF2XYP7U/khGw1m0qHTQF39moQ= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=o9BgZcSQRXNVKMEZAWDGSFUtRvA=; b=buxjeUgmveCIoFZeEK/z ZlLs/qF0/DxBsc04REWN6/PNKqRoN4meTVmgaRUm5aIrV9ngtIXW/ExanmnwBopJ S8qFT4ar2O1u2/Pi53G2VRHg1TxhDeu73BpOesY3l1hK5CPi+unJW4Roo3apztus AgomoaiEMZ9aC/Gf1xxiHvw= Received: (qmail 30623 invoked by alias); 22 Apr 2013 10:45:07 -0000 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 Received: (qmail 30613 invoked by uid 89); 22 Apr 2013 10:45:06 -0000 X-Spam-SWARE-Status: No, score=-0.9 required=5.0 tests=AWL, BAYES_20, RCVD_IN_HOSTKARMA_NO autolearn=ham version=3.3.1 Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.84/v0.84-167-ge50287c) with ESMTP; Mon, 22 Apr 2013 10:45:06 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 4BA702EBF7; Mon, 22 Apr 2013 06:45:04 -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 iY8536Ob0aLr; Mon, 22 Apr 2013 06:45:04 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 2FEB62EB3D; Mon, 22 Apr 2013 06:45:04 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 267E73FF09; Mon, 22 Apr 2013 06:45:04 -0400 (EDT) Date: Mon, 22 Apr 2013 06:45:04 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Ed Schonberg Subject: [Ada] Ada 2012 predicate checks on (in-) out parameters Message-ID: <20130422104504.GA12385@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) X-Virus-Found: No RM 3.2.4 (23/3) stipulates that predicates are checked on out and in-out by-reference parameters on return from a call. If the call is to a primitive of the type the predicate call is inserted in the postcondition subprogram. However, if the call is to an inherited operation, the check must be performed explicitly on exit from the call. Executing the following: gnatmake -q -gnata -gnat12 main.adb main --- must yield: raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : predicate failed at main.adb:6 --- with Derived; use Derived; procedure Main is A : T0 := (X => 0); B : T0 := (X => A.X); begin P (A); B := A; end Main; --- with Parent; use Parent; package Derived is type T0 is new T with null record with Dynamic_Predicate => T0.X = 0; procedure Change (x : in out T0); end Derived; --- package Parent is type T is tagged record X : Integer; end record; procedure P (A : in out T); end Parent; --- package body Parent is procedure P (A : in out T) is begin A.X := 1; end P; end Parent; Tested on x86_64-pc-linux-gnu, committed on trunk 2013-04-22 Ed Schonberg * exp_ch6.adb (Expand_Actuals): If the call is to an inherited operation and the actual is a by-reference type with predicates, add predicate call to post-call actions. * sem_util.adb (Is_Inherited_Operation_For_Type): Fix coding error: a type declaration has a defining identifier, not an Etype. * sem_res.adb: Restore code removed because of above error. Index: sem_util.adb =================================================================== --- sem_util.adb (revision 198126) +++ sem_util.adb (working copy) @@ -8462,8 +8462,11 @@ Typ : Entity_Id) return Boolean is begin + -- Check that the operation has been created by the declaration for + -- the type. + return Is_Inherited_Operation (E) - and then Etype (Parent (E)) = Typ; + and then Defining_Identifier (Parent (E)) = Typ; end Is_Inherited_Operation_For_Type; ----------------- Index: sem_res.adb =================================================================== --- sem_res.adb (revision 198126) +++ sem_res.adb (working copy) @@ -5896,20 +5896,15 @@ -- In formal mode, the primitive operations of a tagged type or type -- extension do not include functions that return the tagged type. - -- Commented out as the call to Is_Inherited_Operation_For_Type may - -- cause an error because the type entity of the parent node of - -- Entity (Name (N) may not be set. ??? - -- So why not just add a guard ??? + if Nkind (N) = N_Function_Call + and then Is_Tagged_Type (Etype (N)) + and then Is_Entity_Name (Name (N)) + and then Is_Inherited_Operation_For_Type + (Entity (Name (N)), Etype (N)) + then + Check_SPARK_Restriction ("function not inherited", N); + end if; --- if Nkind (N) = N_Function_Call --- and then Is_Tagged_Type (Etype (N)) --- and then Is_Entity_Name (Name (N)) --- and then Is_Inherited_Operation_For_Type --- (Entity (Name (N)), Etype (N)) --- then --- Check_SPARK_Restriction ("function not inherited", N); --- end if; - -- Implement rule in 12.5.1 (23.3/2): In an instance, if the actual is -- class-wide and the call dispatches on result in a context that does -- not provide a tag, the call raises Program_Error. Index: exp_ch6.adb =================================================================== --- exp_ch6.adb (revision 198126) +++ exp_ch6.adb (working copy) @@ -942,6 +942,7 @@ Formal : Entity_Id; N_Node : Node_Id; Post_Call : List_Id; + E_Actual : Entity_Id; E_Formal : Entity_Id; procedure Add_Call_By_Copy_Code; @@ -1508,6 +1509,7 @@ Actual := First_Actual (N); while Present (Formal) loop E_Formal := Etype (Formal); + E_Actual := Etype (Actual); if Is_Scalar_Type (E_Formal) or else Nkind (Actual) = N_Slice @@ -1645,7 +1647,7 @@ -- conversion" errors. elsif Is_Access_Type (E_Formal) - and then not Same_Type (E_Formal, Etype (Actual)) + and then not Same_Type (E_Formal, E_Actual) and then not Is_Tagged_Type (Designated_Type (E_Formal)) then Add_Call_By_Copy_Code; @@ -1661,7 +1663,7 @@ elsif Is_Entity_Name (Actual) and then Is_Volatile (Entity (Actual)) - and then not Is_By_Reference_Type (Etype (Actual)) + and then not Is_By_Reference_Type (E_Actual) and then not Is_Scalar_Type (Etype (Entity (Actual))) and then not Is_Volatile (E_Formal) then @@ -1682,10 +1684,10 @@ elsif Is_Scalar_Type (E_Formal) and then - (not In_Subrange_Of (E_Formal, Etype (Actual)) + (not In_Subrange_Of (E_Formal, E_Actual) or else (Ekind (Formal) = E_In_Out_Parameter - and then not In_Subrange_Of (Etype (Actual), E_Formal))) + and then not In_Subrange_Of (E_Actual, E_Formal))) then -- Perhaps the setting back to False should be done within -- Add_Call_By_Copy_Code, since it could get set on other @@ -1698,6 +1700,28 @@ Add_Call_By_Copy_Code; end if; + -- RM 3.2.4 (23/3) : A predicate is checked on in-out and out + -- by-reference parameters on exit from the call. If the actual + -- is a derived type and the operation is inherited, the body + -- of the operation will not contain a call to the predicate + -- function, so it must be done explicitly after the call. Ditto + -- if the actual is an entity of a predicated subtype. + + if Is_By_Reference_Type (E_Formal) + and then Has_Predicates (E_Actual) + then + if Is_Derived_Type (E_Actual) + and then Is_Inherited_Operation_For_Type (Subp, E_Actual) + then + Append_To + (Post_Call, Make_Predicate_Check (E_Actual, Actual)); + + elsif Is_Entity_Name (Actual) then + Append_To + (Post_Call, Make_Predicate_Check (E_Actual, Actual)); + end if; + end if; + -- Processing for IN parameters else