From patchwork Mon Aug 29 08:30:21 2011 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 111975 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 F0466B6F7F for ; Mon, 29 Aug 2011 18:30:46 +1000 (EST) Received: (qmail 3211 invoked by alias); 29 Aug 2011 08:30:39 -0000 Received: (qmail 3197 invoked by uid 22791); 29 Aug 2011 08:30:35 -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 08:30:22 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id AAFD92BAECF; Mon, 29 Aug 2011 04:30:21 -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 Vmta6KVw5kJj; Mon, 29 Aug 2011 04:30:21 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 84EF42BAEAD; Mon, 29 Aug 2011 04:30:21 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 83B203FEE8; Mon, 29 Aug 2011 04:30:21 -0400 (EDT) Date: Mon, 29 Aug 2011 04:30:21 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Insert subtypes for array index/component in formal verification mode Message-ID: <20110829083021.GA30543@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 In formal verification mode, it is expected that subtypes are declared before use, hence these additional declarations. Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-29 Yannick Moy * sem_ch3.adb (Array_Type_Declaration): Insert a subtype declaration for every index type and component type that is not a subtype_mark. (Process_Subtype): Set Etype of subtype. Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 178155) +++ sem_ch3.adb (working copy) @@ -4741,6 +4741,47 @@ 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. Why are we doing this ??? + + if ALFA_Mode + and then not Nkind_In (Index, N_Identifier, N_Expanded_Name) + then + declare + Loc : constant Source_Ptr := Sloc (Def); + New_E : Entity_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 + Sub_Ind := + Make_Subtype_Indication (Loc, + Subtype_Mark => + New_Occurrence_Of (Base_Type (Etype (Index)), Loc), + Constraint => + Make_Range_Constraint (Loc, + Range_Expression => Relocate_Node (Index))); + end if; + + Decl := + Make_Subtype_Declaration (Loc, + Defining_Identifier => New_E, + Subtype_Indication => Sub_Ind); + + Insert_Action (Parent (Def), Decl); + Set_Etype (Index, New_E); + end; + end if; + -- Check error of subtype with predicate for index type Bad_Predicated_Subtype_Use @@ -4756,8 +4797,37 @@ -- Process subtype indication if one is present if Present (Component_Typ) then - Element_Type := Process_Subtype (Component_Typ, P, Related_Id, 'C'); + -- In formal verification mode, create an explicit subtype for the + -- component type if not already a subtype_mark. Why do this ??? + + if ALFA_Mode + and then Nkind (Component_Typ) = N_Subtype_Indication + 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); + end; + + else + Element_Type := + Process_Subtype (Component_Typ, P, Related_Id, 'C'); + end if; + + Set_Etype (Component_Typ, Element_Type); + if not Nkind_In (Component_Typ, N_Identifier, N_Expanded_Name) then Check_SPARK_Restriction ("subtype mark required", Component_Typ); end if;