From patchwork Mon Sep 19 08:32:51 2011 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 115300 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 03E08B6FF5 for ; Mon, 19 Sep 2011 18:33:17 +1000 (EST) Received: (qmail 1327 invoked by alias); 19 Sep 2011 08:33:10 -0000 Received: (qmail 1307 invoked by uid 22791); 19 Sep 2011 08:33:09 -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, 19 Sep 2011 08:32:51 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 2308D2BAE6D; Mon, 19 Sep 2011 04:32:51 -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 En9l+ZPzR-z8; Mon, 19 Sep 2011 04:32:51 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 101A52BAE6C; Mon, 19 Sep 2011 04:32:51 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 0D36F92BF6; Mon, 19 Sep 2011 04:32:51 -0400 (EDT) Date: Mon, 19 Sep 2011 04:32:51 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Deal with references for Alfa mode through multiple renamings Message-ID: <20110919083251.GA16377@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 Get the enclosing entity through possible multiple renamings, not only once, which may come from source or from the translation of generic instantiations. Only for the Alfa mode for formal verification. Tested on x86_64-pc-linux-gnu, committed on trunk 2011-09-19 Yannick Moy * lib-xref.adb (Generate_Reference): Take into account multiple renamings for Alfa refs. Index: lib-xref.adb =================================================================== --- lib-xref.adb (revision 178956) +++ lib-xref.adb (working copy) @@ -391,6 +391,10 @@ Kind : Entity_Kind; -- If Formal is non-Empty, then its Ekind, otherwise E_Void + function Get_Through_Renamings (E : Entity_Id) return Entity_Id; + -- Get the enclosing entity through renamings, which may come from + -- source or from the translation of generic instantiations. + function Is_On_LHS (Node : Node_Id) return Boolean; -- Used to check if a node is on the left hand side of an assignment. -- The following cases are handled: @@ -412,6 +416,22 @@ -- exceptions where we do not want to set this flag, see body for -- details of these exceptional cases. + --------------------------- + -- Get_Through_Renamings -- + --------------------------- + + function Get_Through_Renamings (E : Entity_Id) return Entity_Id is + Result : Entity_Id := E; + begin + while Present (Result) + and then Is_Object (Result) + and then Present (Renamed_Object (Result)) + loop + Result := Get_Enclosing_Object (Renamed_Object (Result)); + end loop; + return Result; + end Get_Through_Renamings; + --------------- -- Is_On_LHS -- --------------- @@ -955,11 +975,8 @@ -- the renaming, which is needed to compute a valid set of effects -- (reads, writes) for the enclosing subprogram. - if Alfa_Mode - and then Is_Object (Ent) - and then Present (Renamed_Object (Ent)) - then - Ent := Get_Enclosing_Object (Renamed_Object (Ent)); + if Alfa_Mode then + Ent := Get_Through_Renamings (Ent); -- If no enclosing object, then it could be a reference to any -- location not tracked individually, like heap-allocated data.