From patchwork Mon Aug 29 14:15:37 2011 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 112062 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 90503B6F95 for ; Tue, 30 Aug 2011 00:15:58 +1000 (EST) Received: (qmail 7947 invoked by alias); 29 Aug 2011 14:15:54 -0000 Received: (qmail 7936 invoked by uid 22791); 29 Aug 2011 14:15:52 -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; Mon, 29 Aug 2011 14:15:38 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 861312BAF11; Mon, 29 Aug 2011 10:15:37 -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 b15u4y97t6FB; Mon, 29 Aug 2011 10:15:37 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 70A7A2BAF0A; Mon, 29 Aug 2011 10:15:37 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 6E94692A55; Mon, 29 Aug 2011 10:15:37 -0400 (EDT) Date: Mon, 29 Aug 2011 10:15:37 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Add declaration for Itypes in Alfa mode Message-ID: <20110829141537.GA24255@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 The formal verification back-end expects declaration to be present for Itypes, even if they are not attached to the tree. Add such declarations in the case of Itypes introduced for index/component types of arrays and anonymous array types in object declaration. Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-29 Yannick Moy * sem_ch3.adb (Array_Type_Declaration): Create declarations for Itypes created in Alfa mode, instead of inserting artificial declarations of non-Itypes in the tree. * sem_util.adb, sem_util.ads (Itype_Has_Declaration): New function to know if an Itype has a corresponding declaration, as defined in itypes.ads. Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 178239) +++ sem_ch3.adb (working copy) @@ -4741,26 +4741,20 @@ Make_Index (Index, P, Related_Id, Nb_Index); - -- In formal verification mode, create an explicit subtype for every - -- index if not already a subtype_mark, and replace the existing type - -- of index by this new type. Having a declaration for all type + -- In formal verification mode, create an explicit declaration for + -- Itypes created for index types. Having a declaration for all type -- entities facilitates the task of the formal verification back-end. + -- Notice that this declaration is not attached to the tree. if ALFA_Mode - and then not Nkind_In (Index, N_Identifier, N_Expanded_Name) + and then Is_Itype (Etype (Index)) then declare Loc : constant Source_Ptr := Sloc (Def); - New_E : Entity_Id; + Sub_Ind : Node_Id; Decl : Entity_Id; - Sub_Ind : Node_Id; begin - New_E := - New_External_Entity - (E_Void, Current_Scope, Sloc (P), Related_Id, 'D', - Nb_Index, 'T'); - if Nkind (Index) = N_Subtype_Indication then Sub_Ind := Relocate_Node (Index); else @@ -4775,11 +4769,10 @@ Decl := Make_Subtype_Declaration (Loc, - Defining_Identifier => New_E, + Defining_Identifier => Etype (Index), Subtype_Indication => Sub_Ind); - Insert_Action (Parent (Def), Decl); - Set_Etype (Index, New_E); + Analyze (Decl); end; end if; @@ -4799,34 +4792,29 @@ if Present (Component_Typ) then - -- In formal verification mode, create an explicit subtype for the - -- component type if not already a subtype_mark. Having a declaration - -- for all type entities facilitates the task of the formal - -- verification back-end. + Element_Type := Process_Subtype (Component_Typ, P, Related_Id, 'C'); + -- In formal verification mode, create an explicit declaration for + -- the Itype created for a component type. Having a declaration for + -- all type entities facilitates the task of the formal verification + -- back-end. Notice that this declaration is not attached to the + -- tree. + if ALFA_Mode - and then Nkind (Component_Typ) = N_Subtype_Indication + and then Is_Itype (Element_Type) then declare Loc : constant Source_Ptr := Sloc (Def); Decl : Entity_Id; begin - Element_Type := - New_External_Entity - (E_Void, Current_Scope, Sloc (P), Related_Id, 'C', 0, 'T'); - Decl := Make_Subtype_Declaration (Loc, Defining_Identifier => Element_Type, Subtype_Indication => Relocate_Node (Component_Typ)); - Insert_Action (Parent (Def), Decl); + Analyze (Decl); end; - - else - Element_Type := - Process_Subtype (Component_Typ, P, Related_Id, 'C'); end if; Set_Etype (Component_Typ, Element_Type); @@ -4915,6 +4903,30 @@ (Implicit_Base, Finalize_Storage_Only (Element_Type)); + -- In ALFA mode, generate a declaration for Itype T, so that the + -- formal verification back-end can use it. + + if ALFA_Mode + and then Is_Itype (T) + then + declare + Loc : constant Source_Ptr := Sloc (Def); + Decl : Node_Id; + + begin + Decl := Make_Full_Type_Declaration (Loc, + Defining_Identifier => T, + Type_Definition => + Make_Constrained_Array_Definition (Loc, + Discrete_Subtype_Definitions => + New_Copy_List (Discrete_Subtype_Definitions (Def)), + Component_Definition => + Relocate_Node (Component_Definition (Def)))); + + Analyze (Decl); + end; + end if; + -- Unconstrained array case else Index: sem_util.adb =================================================================== --- sem_util.adb (revision 178239) +++ sem_util.adb (working copy) @@ -8507,6 +8507,20 @@ end if; end Is_Volatile_Object; + --------------------------- + -- Itype_Has_Declaration -- + --------------------------- + + function Itype_Has_Declaration (Id : Entity_Id) return Boolean is + begin + pragma Assert (Is_Itype (Id)); + return Present (Parent (Id)) + and then Nkind_In (Parent (Id), + N_Full_Type_Declaration, + N_Subtype_Declaration) + and then Defining_Entity (Parent (Id)) = Id; + end Itype_Has_Declaration; + ------------------------- -- Kill_Current_Values -- ------------------------- Index: sem_util.ads =================================================================== --- sem_util.ads (revision 178235) +++ sem_util.ads (working copy) @@ -969,6 +969,11 @@ -- for something actually declared as volatile, not for an object that gets -- treated as volatile (see Einfo.Treat_As_Volatile). + function Itype_Has_Declaration (Id : Entity_Id) return Boolean; + -- Applies to Itypes. True if the Itype is attached to a declaration for + -- the type through its Parent field, which may or not be present in the + -- tree. + procedure Kill_Current_Values (Last_Assignment_Only : Boolean := False); -- This procedure is called to clear all constant indications from all -- entities in the current scope and in any parent scopes if the current