From patchwork Thu Jan 11 09:02:53 2018 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 858936 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (mailfrom) smtp.mailfrom=gcc.gnu.org (client-ip=209.132.180.131; helo=sourceware.org; envelope-from=gcc-patches-return-470782-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="dMSTdvT3"; dkim-atps=neutral Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 3zHKg2008Pz9t3F for ; Thu, 11 Jan 2018 20:03:39 +1100 (AEDT) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=sSqyQOVxuEfjREVpaZwtFaqoC9tskhChtQr2ipp3qTdMordj0S SxnxSX3EdDh02o/dgCGe3l53asexM6k3r7TFILrfW84rd7zZcUkXv0kjLREx+TSH 8VJnykjzYz8wIsADiZrDySeSDJMI2Ygq0MamsBkM7rgBb8XeDYlueof4I= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=Y2gdKmPSIdybeNsZFkgPmNx4Jjs=; b=dMSTdvT3TdrMxJ/rzpzE fPjJ7KRjb/0zwODYkC6jsOMTQuH5iD1TR0FZ4vZFpf6ejIAZqJPnnheNtVt1wL34 bmJDnd6rm87ujVSNqA4tUtx0m7gjzC87W+7TsbnejQS4BDQdJnlMLG81DgEk6dVY vqQWRM1MlvTBNqaRRlJ5sls= Received: (qmail 90878 invoked by alias); 11 Jan 2018 09:03:32 -0000 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 Received: (qmail 18896 invoked by uid 89); 11 Jan 2018 09:02:56 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-11.9 required=5.0 tests=AWL, BAYES_00, GIT_PATCH_2, GIT_PATCH_3, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.2 spammy=entities X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Thu, 11 Jan 2018 09:02:55 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 041A3117BC0; Thu, 11 Jan 2018 04:02:54 -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 q62iEIhOI33d; Thu, 11 Jan 2018 04:02:53 -0500 (EST) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id E4C2B117BBE; Thu, 11 Jan 2018 04:02:53 -0500 (EST) Received: by tron.gnat.com (Postfix, from userid 4862) id E086350B; Thu, 11 Jan 2018 04:02:53 -0500 (EST) Date: Thu, 11 Jan 2018 04:02:53 -0500 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Inconsistent scope chain due to quantified expression Message-ID: <20180111090253.GA102816@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes This patch corrects the minor decoration performed on invariant procedures in case the procedure is not inserted into the tree and analyzed. The decoration now constructs a proper first/next/last entity chain containing the single formal parameter which represents the object of the related type. The chain then ensures that any other entities generated by the [pre]analysis of the invariant expression will be properly added to the chain. The issue was discovered during the development of the GNATprove tool and is not visible to end users. No simple test is available because this would require a debug session. Tested on x86_64-pc-linux-gnu, committed on trunk 2018-01-11 Hristian Kirtchev gcc/ada/ * exp_util.adb (Build_Invariant_Procedure_Declaration): Set the last entity of the generated invariant procedure in order to construct a proper entity chain. --- gcc/ada/exp_util.adb +++ gcc/ada/exp_util.adb @@ -3466,6 +3466,7 @@ package body Exp_Util is Set_Scope (Obj_Id, Proc_Id); Set_First_Entity (Proc_Id, Obj_Id); + Set_Last_Entity (Proc_Id, Obj_Id); -- Generate: -- procedure [Partial_]Invariant (_object : );