From patchwork Tue Nov 6 09:49:30 2012 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 197430 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 5A84D2C0095 for ; Tue, 6 Nov 2012 20:49:43 +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=1352800183; 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=rHoveY+b6GV/2U9zAjbp RLK+NGI=; b=MMV6kIfRoUiJfsNCn40aCGFMvUxnsXbB8NMAjmTAN8W2TdPHVRjG ksXUZGXdqZRiDgW7eLfwbrmFNoY04lfA9FkiNO7FnxZCitvKeXOQUGLBLB0DEe9s 8AjjX4Gikh5gC4NMEN23FMDd9X3xJtuRX/am/CHHFmgDyHDIk1ewW4g= 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=x0s8Qg5+PpEKa3NDcl57XahFsfwTzhLFGTCekZPx5svaTpT7AoG7rv3EREqk6f LBeRbYTK8anhJHZtfi2B58n34ZvFIHZBe3yV7KNEOJo1LXnABOGQqmPokJexgmC/ 08sdFappqNGpH+2vsjpK5QaIzQ4/68+urMcWHmaFrmeoI=; Received: (qmail 22705 invoked by alias); 6 Nov 2012 09:49:37 -0000 Received: (qmail 22696 invoked by uid 22791); 6 Nov 2012 09:49:36 -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; Tue, 06 Nov 2012 09:49:31 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id A43491C7FD6; Tue, 6 Nov 2012 04:49:30 -0500 (EST) 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 yLjTVF-ec43h; Tue, 6 Nov 2012 04:49:30 -0500 (EST) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 881C01C7FD3; Tue, 6 Nov 2012 04:49:30 -0500 (EST) Received: by kwai.gnat.com (Postfix, from userid 4192) id 841143FF09; Tue, 6 Nov 2012 04:49:30 -0500 (EST) Date: Tue, 6 Nov 2012 04:49:30 -0500 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Correct possible double qualification of names in formal mode Message-ID: <20121106094930.GA4055@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 the special mode for formal verification, the entity was not marked as having a qualified name after being passed to Qualify_Entity_Name, which lead to multiple qualification when Qualify_Entity_Name was called multiple times on the same entity. The assumptions that it is called only once on each entity is wrong, because scopes (containing entities) may be put more than once on the qualification stack, once every time they are expanded, and expansion may be called multiple times on the same node. The fact that names are marked as qualified does not break the behavior of Unique_Name to fully qualify names based on scope names, because this function looks at the other flag Has_Fully_Qualified_Name, not set in formal verification mode. Tested on x86_64-pc-linux-gnu, committed on trunk 2012-11-06 Yannick Moy * exp_dbug.adb (Qualify_Entity_Name): Mark entity as having a qualified name after being treated, in formal verification mode. Index: exp_dbug.adb =================================================================== --- exp_dbug.adb (revision 193208) +++ exp_dbug.adb (working copy) @@ -1307,12 +1307,13 @@ if Has_Qualified_Name (Ent) then return; - -- In formal verification mode, simply append a suffix for homonyms, but - -- do not mark the name as being qualified. We used to qualify entity - -- names as full expansion does, but this was removed as this prevents - -- the verification back-end from using a short name for debugging and - -- user interaction. The verification back-end already takes care of - -- qualifying names when needed. + -- In formal verification mode, simply append a suffix for homonyms. + -- We used to qualify entity names as full expansion does, but this was + -- removed as this prevents the verification back-end from using a short + -- name for debugging and user interaction. The verification back-end + -- already takes care of qualifying names when needed. Still mark the + -- name as being qualified, as Qualify_Entity_Name may be called more + -- than once on the same entity. elsif Alfa_Mode then if Has_Homonym (Ent) then @@ -1322,6 +1323,7 @@ Set_Chars (Ent, Name_Enter); end if; + Set_Has_Qualified_Name (Ent); return; -- If the entity is a variable encoding the debug name for an object