From patchwork Fri Mar 30 09:24:19 2012 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 149595 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 15AD6B6EEF for ; Fri, 30 Mar 2012 20:24:37 +1100 (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=1333704279; 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=YI6gwI15NjE4NL9plci0 nLri6Oc=; b=K3xtKzErmpIcm7Hig9LbeeKrVm0HEZJL+Exw87BgZJpa9gMyIIGf FwRmog6SeCML541UOx6cGX7giG93hH1+ltjM5om28TPldXfQ72wSe5xCw3LdpUPU zqj/QzAWn1RYgxyFTvLHG13PU0fUMJs9dsHCwr1JSBFXbgHJHatlA7E= 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=NI8JU6mYi/mmqEaQ42Yb/4FxUFOqoF3zzFTptF+f5o03vifapIcv4eclQroQHo wu9EWkGO6gVEcLrJiR7XfCsT0oEia+JJ0+o0fK/5gMlltE+XsBQRlILOb96BkvEw 2fKH4pxyI/zfm+5/y1L1drw8ecTbVn3mc5lMOq87wzo+U=; Received: (qmail 20971 invoked by alias); 30 Mar 2012 09:24:35 -0000 Received: (qmail 20961 invoked by uid 22791); 30 Mar 2012 09:24:33 -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; Fri, 30 Mar 2012 09:24:20 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id E9F271C6BF6; Fri, 30 Mar 2012 05:24: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 MJbitiCy4b4m; Fri, 30 Mar 2012 05:24:19 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id CBB581C6BF5; Fri, 30 Mar 2012 05:24:19 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id C8C4792BF6; Fri, 30 Mar 2012 05:24:19 -0400 (EDT) Date: Fri, 30 Mar 2012 05:24:19 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Generate Alfa cross-references for instantiations of generics Message-ID: <20120330092419.GA24057@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 order to apply formal verification to code with instantiations of generics, we must get Alfa cross-references for this code. This consists mostly in enabling the generation of instances in Alfa mode, and adapting the Alfa xref code. Tested on x86_64-pc-linux-gnu, committed on trunk 2012-03-30 Yannick Moy * lib-xref-alfa.adb (Generate_Dereference): Use Get_Code_Unit instead of Get_Source_Unit to get file for reference. (Traverse_Compilation_Unit): Do not add scopes for generic units. * lib-xref.adb (Generate_Reference): Use Get_Code_Unit instead of Get_Source_Unit to get file for reference. * sem_ch12.adb (Analyze_Package_Instantiation): Enable instantiation in Alfa mode. Index: sem_ch12.adb =================================================================== --- sem_ch12.adb (revision 185995) +++ sem_ch12.adb (working copy) @@ -3704,7 +3704,6 @@ or else Might_Inline_Subp) and then not Is_Actual_Pack and then not Inline_Now - and then not Alfa_Mode and then (Operating_Mode = Generate_Code or else (Operating_Mode = Check_Semantics and then ASIS_Mode)); Index: lib-xref-alfa.adb =================================================================== --- lib-xref-alfa.adb (revision 186001) +++ lib-xref-alfa.adb (working copy) @@ -1051,15 +1051,13 @@ Loc : constant Source_Ptr := Sloc (N); Index : Nat; - Ref : Source_Ptr; Ref_Scope : Entity_Id; -- Start of processing for Generate_Dereference begin - Ref := Original_Location (Loc); - if Ref > No_Location then + if Loc > No_Location then Drefs.Increment_Last; Index := Drefs.Last; @@ -1075,21 +1073,21 @@ Ref_Scope := Enclosing_Subprogram_Or_Package (N); Deref.Ent := Heap; - Deref.Loc := Ref; + Deref.Loc := Loc; Deref.Typ := Typ; -- It is as if the special "Heap" was defined in every scope where -- it is referenced. - Deref.Eun := Get_Source_Unit (Ref); - Deref.Lun := Get_Source_Unit (Ref); + Deref.Eun := Get_Code_Unit (Loc); + Deref.Lun := Get_Code_Unit (Loc); Deref.Ref_Scope := Ref_Scope; Deref.Ent_Scope := Ref_Scope; Deref_Entry.Def := No_Location; - Deref_Entry.Ent_Scope_File := Get_Source_Unit (Ref_Scope); + Deref_Entry.Ent_Scope_File := Get_Code_Unit (N); end; end if; end Generate_Dereference; @@ -1125,6 +1123,14 @@ Lu := Proper_Body (Lu); end if; + -- Do not add scopes for generic units + + if Nkind (Lu) = N_Package_Body + and then Ekind (Corresponding_Spec (Lu)) in Generic_Unit_Kind + then + return; + end if; + -- Call Process on all declarations if Nkind (Lu) in N_Declaration Index: lib-xref.adb =================================================================== --- lib-xref.adb (revision 186001) +++ lib-xref.adb (working copy) @@ -378,7 +378,6 @@ Def : Source_Ptr; Ent : Entity_Id; Ent_Scope : Entity_Id; - Ent_Scope_File : Unit_Number_Type; Formal : Entity_Id; Kind : Entity_Kind; Nod : Node_Id; @@ -633,6 +632,16 @@ or else Typ = 'i' or else Typ = 'k' or else (Typ = 'b' and then Is_Generic_Instance (E)) + + -- Allow the generation of references to reads, writes and calls + -- in Alfa mode when the related context comes from an instance. + + or else + (Alfa_Mode + and then In_Extended_Main_Code_Unit (N) + and then (Typ = 'm' + or else Typ = 'r' + or else Typ = 's')) then null; else @@ -880,11 +889,12 @@ -- Ignore references from within an instance. The only exceptions to -- this are default subprograms, for which we generate an implicit - -- reference. + -- reference and compilations in Alfa_Mode. and then (Instantiation_Location (Sloc (N)) = No_Location - or else Typ = 'i') + or else Typ = 'i' + or else Alfa_Mode) -- Ignore dummy references @@ -995,9 +1005,6 @@ -- Record reference to entity - Ref := Original_Location (Sloc (Nod)); - Def := Original_Location (Sloc (Ent)); - if Actual_Typ = 'p' and then Is_Subprogram (Nod) and then Present (Overridden_Operation (Nod)) @@ -1006,6 +1013,9 @@ end if; if Alfa_Mode then + Ref := Sloc (Nod); + Def := Sloc (Ent); + Ref_Scope := Alfa.Enclosing_Subprogram_Or_Package (Nod); Ent_Scope := Alfa.Enclosing_Subprogram_Or_Package (Ent); @@ -1018,22 +1028,30 @@ return; end if; - Ent_Scope_File := Get_Source_Unit (Ent_Scope); + Add_Entry + ((Ent => Ent, + Loc => Ref, + Typ => Actual_Typ, + Eun => Get_Code_Unit (Def), + Lun => Get_Code_Unit (Ref), + Ref_Scope => Ref_Scope, + Ent_Scope => Ent_Scope), + Ent_Scope_File => Get_Code_Unit (Ent)); + else - Ref_Scope := Empty; - Ent_Scope := Empty; - Ent_Scope_File := No_Unit; + Ref := Original_Location (Sloc (Nod)); + Def := Original_Location (Sloc (Ent)); + + Add_Entry + ((Ent => Ent, + Loc => Ref, + Typ => Actual_Typ, + Eun => Get_Source_Unit (Def), + Lun => Get_Source_Unit (Ref), + Ref_Scope => Empty, + Ent_Scope => Empty), + Ent_Scope_File => No_Unit); end if; - - Add_Entry - ((Ent => Ent, - Loc => Ref, - Typ => Actual_Typ, - Eun => Get_Source_Unit (Def), - Lun => Get_Source_Unit (Ref), - Ref_Scope => Ref_Scope, - Ent_Scope => Ent_Scope), - Ent_Scope_File => Ent_Scope_File); end if; end Generate_Reference;