From patchwork Mon Nov 7 16:22:46 2011 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 124126 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 6C5FDB6F72 for ; Tue, 8 Nov 2011 03:23:05 +1100 (EST) Received: (qmail 27955 invoked by alias); 7 Nov 2011 16:23:01 -0000 Received: (qmail 27945 invoked by uid 22791); 7 Nov 2011 16:23:00 -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, 07 Nov 2011 16:22:47 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 845252BAF96; Mon, 7 Nov 2011 11:22:46 -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 1Uhb33JXH+UT; Mon, 7 Nov 2011 11:22:46 -0500 (EST) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 726F82BAB9B; Mon, 7 Nov 2011 11:22:46 -0500 (EST) Received: by kwai.gnat.com (Postfix, from userid 4192) id 69C4A92BF6; Mon, 7 Nov 2011 11:22:46 -0500 (EST) Date: Mon, 7 Nov 2011 11:22:46 -0500 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Define unique entity for parameter (used in Alfa mode) Message-ID: <20111107162246.GA7683@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 For the formal verification backend, to be used in Alfa mode, define the unique entity representing a parameter. Tested on x86_64-pc-linux-gnu, committed on trunk 2011-11-07 Yannick Moy * sem_util.adb (Unique_Entity): For a parameter on a subprogram body that has a corresponding parameter on the subprogram declaration, define the unique entity as being the declaration one. Index: sem_util.adb =================================================================== --- sem_util.adb (revision 181090) +++ sem_util.adb (working copy) @@ -12835,6 +12835,11 @@ U := Corresponding_Spec (P); end if; + when Formal_Kind => + if Present (Spec_Entity (E)) then + U := Spec_Entity (E); + end if; + when others => null; end case;