From patchwork Tue Oct 27 11:53:19 2015 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 536576 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.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 41C80141365 for ; Tue, 27 Oct 2015 22:53:41 +1100 (AEDT) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b=mgBliKr9; dkim-atps=neutral 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=sEdIXXMfYxBIdZRgnTbXhqZiyZcoUxGD+/mGJxzE23J7xiY1ne umwnEhAbN0HRZuk16Z+At+kJz1LHTVO2PoRnDPa8FHvMFJPJ6ixd4zeoMmDigKWk osb79PiCD9zOglsjnvTO1KOR9e8mqMEvID4qcJiQ10yevOpRFpRJp0OsA= 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=enwO0dP02mKfK6WR78WpQWDEIac=; b=mgBliKr9A1FpkjLMpqo+ WcLawM6YzHYW0H0PO+Ks9ZDMwAtGTaTAuQwMuNSKqHfBT7kH+Y+vUUGu3K1RGSEQ 0m1yirEkagMlji5y8cH26P3sajccDHjkSqTMG6UWSUe9cNRXkL0Wmw6XR/aExjx4 w9B7gQYn7isWvkmhNVc/exU= Received: (qmail 63868 invoked by alias); 27 Oct 2015 11:53:28 -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 63747 invoked by uid 89); 27 Oct 2015 11:53:27 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-0.1 required=5.0 tests=AWL, BAYES_50, KAM_LAZY_DOMAIN_SECURITY, RCVD_IN_DNSWL_LOW autolearn=no version=3.3.2 X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with (AES256-SHA encrypted) ESMTPS; Tue, 27 Oct 2015 11:53:21 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id D1BEF11826F; Tue, 27 Oct 2015 07:53:19 -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 dOV-T5reiWhz; Tue, 27 Oct 2015 07:53:19 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id C193511826A; Tue, 27 Oct 2015 07:53:19 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4192) id C042E184; Tue, 27 Oct 2015 07:53:19 -0400 (EDT) Date: Tue, 27 Oct 2015 07:53:19 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Spurious error on legal use of abstract state constituent Message-ID: <20151027115319.GA66719@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) This patch modifies the analysis of pragma Refined_Global to treat objects and states as constituents only when their encapsulating state appears in pragma Global. ------------ -- Source -- ------------ -- pack.ads package Pack with Abstract_State => (State1, State2), Initializes => (Var, State1, State2) is Var : Integer := 0; procedure Initialize_State with Global => (Output => State1), Depends => (State1 => null); end Pack; -- pack.adb package body Pack with Refined_State => (State1 => (A, B), State2 => (Inner.Inner_Var, Inner.Inner_State)) is A, B : Integer; package Inner with Abstract_State => Inner_State, Initializes => (Inner_State, Inner_Var => Var) is Inner_Var : Integer; procedure Initialize_Inner with Global => (Output => (Inner_State, Inner_Var), Input => Var), Depends => (Inner_State => null, Inner_Var => Var); end Inner; procedure Initialize_State is separate with Refined_Global => (Output => (A, B)), Refined_Depends => ((A, B) => null); procedure Double_B is separate with Global => (In_Out => B), Depends => (B => B); package body Inner is separate; begin Initialize_State; Double_B; end Pack; -- pack-double_b.adb separate (Pack) procedure Double_B is begin B := B * 2; end Double_B; -- pack-initialize_state.adb separate (Pack) procedure Initialize_State is begin A := 0; B := 0; end Initialize_State; -- pack-inner.adb separate (Pack) package body Inner with Refined_State => (Inner_State => Inner_Body_Var) is Inner_Body_Var : Integer; procedure Initialize_Inner with Refined_Global => (Output => (Inner_Body_Var, Inner_Var), Input => Var), Refined_Depends => (Inner_Body_Var => null, Inner_Var => Var) is begin Inner_Body_Var := 0; Inner_Var := Var; end Initialize_Inner; begin Initialize_Inner; end Inner; ----------------- -- Compilation -- ----------------- $ gcc -c pack.adb Tested on x86_64-pc-linux-gnu, committed on trunk 2015-10-27 Hristian Kirtchev * sem_prag.adb (Analyze_Refined_Global_In_Decl_Part): Add variable States. (Check_Refined_Global_Item): An object or state acts as a constituent only when the corresponding encapsulating state appears in pragma Global. (Collect_Global_Item): Add a state with non-null visible refinement to list States. Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 229414) +++ sem_prag.adb (working copy) @@ -527,7 +527,7 @@ -- E_Constant - "constant" -- E_Discriminant - "discriminant" -- E_Generic_In_Out_Parameter - "generic parameter" - -- E_Generic_Out_Parameter - "generic parameter" + -- E_Generic_In_Parameter - "generic parameter" -- E_In_Parameter - "parameter" -- E_In_Out_Parameter - "parameter" -- E_Loop_Parameter - "loop parameter" @@ -24057,6 +24057,9 @@ Spec_Id : Entity_Id; -- The entity of the subprogram subject to pragma Refined_Global + States : Elist_Id := No_Elist; + -- A list of all states with visible refinement found in pragma Global + procedure Check_In_Out_States; -- Determine whether the corresponding Global pragma mentions In_Out -- states with visible refinement and if so, ensure that one of the @@ -24566,11 +24569,14 @@ begin -- When the state or object acts as a constituent of another -- state with a visible refinement, collect it for the state - -- completeness checks performed later on. + -- completeness checks performed later on. Note that the item + -- acts as a constituent only when the encapsulating state is + -- present in pragma Global. if Ekind_In (Item_Id, E_Abstract_State, E_Constant, E_Variable) and then Present (Encapsulating_State (Item_Id)) and then Has_Visible_Refinement (Encapsulating_State (Item_Id)) + and then Contains (States, Encapsulating_State (Item_Id)) then if Global_Mode = Name_Input then Append_New_Elmt (Item_Id, In_Constits); @@ -24715,6 +24721,8 @@ Has_Null_State := True; elsif Has_Non_Null_Refinement (Item_Id) then + Append_New_Elmt (Item_Id, States); + if Item_Mode = Name_Input then Has_In_State := True; elsif Item_Mode = Name_In_Out then