From patchwork Mon Nov 7 16:25:52 2011 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 124128 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 E2574B6F7C for ; Tue, 8 Nov 2011 03:26:23 +1100 (EST) Received: (qmail 646 invoked by alias); 7 Nov 2011 16:26:18 -0000 Received: (qmail 580 invoked by uid 22791); 7 Nov 2011 16:26:06 -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:25:54 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 1535F2BB0CB; Mon, 7 Nov 2011 11:25:53 -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 mu7oSCotS3ND; Mon, 7 Nov 2011 11:25:53 -0500 (EST) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 02A512BB00A; Mon, 7 Nov 2011 11:25:53 -0500 (EST) Received: by kwai.gnat.com (Postfix, from userid 4192) id 0082292BF6; Mon, 7 Nov 2011 11:25:52 -0500 (EST) Date: Mon, 7 Nov 2011 11:25:52 -0500 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] In Alfa mode, record also modifications not coming from source Message-ID: <20111107162552.GA21262@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 Alfa mode is meant for formal verification, in which we must gather all modifications to variables, even those not coming from source. This is in particular the case for rewritings of renamings in Alfa mode. Tested on x86_64-pc-linux-gnu, committed on trunk 2011-11-07 Yannick Moy * sem_util.adb (Note_Possible_Modification): In Alfa mode, generate a reference for a modification even when the modification does not come from source. Index: sem_util.adb =================================================================== --- sem_util.adb (revision 181092) +++ sem_util.adb (working copy) @@ -10837,7 +10837,9 @@ -- source. This excludes, for example, calls to a dispatching -- assignment operation when the left-hand side is tagged. - if Modification_Comes_From_Source then + if Modification_Comes_From_Source + or else Alfa_Mode + then Generate_Reference (Ent, Exp, 'm'); -- If the target of the assignment is the bound variable