From patchwork Mon Aug 6 07:52:38 2012 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 175287 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 262012C0098 for ; Mon, 6 Aug 2012 17:52:59 +1000 (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=1344844380; 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=R0qq16stcptilw/W4+kF GnAO2Zw=; b=DKH/aTQAT9HUnzk+CXt4CQuxnkHMP6SWbzG+uzj23+FPY2JFZf57 5XABE5R7fmqgH8ZUjzBoWXzG2Ak/7zNtjLorPK1MP4w1Wf8x7y5FB7Xe7gIe+4Z+ uW5RAK4mEx9UFuuNnXYf3rdV+Dwi2Qa3y48fFM4jGp7K4jyqcbH6YPE= 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=Y8uEVCAVt3mgg578CQlA5c/WjRKqdjOf0ajj5P1PpV3uSPwL+pDNCMqCyUM5oO GBEIOjZKmJqcQNXOMT2evorxUuRLVodMnqzuR4+SftAR8rS7HYBrDslLFXji6ka3 SCPZV+kPhy4ueWeJGgPykAIG6jNBzrNhKUKZkAWjOs2Qw=; Received: (qmail 11393 invoked by alias); 6 Aug 2012 07:52:56 -0000 Received: (qmail 11385 invoked by uid 22791); 6 Aug 2012 07:52:55 -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; Mon, 06 Aug 2012 07:52:39 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 781361C76C2; Mon, 6 Aug 2012 03:52:38 -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 OzA5y1OD+uoP; Mon, 6 Aug 2012 03:52:38 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 4FC931C7693; Mon, 6 Aug 2012 03:52:38 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 50D3F92BF6; Mon, 6 Aug 2012 03:52:38 -0400 (EDT) Date: Mon, 6 Aug 2012 03:52:38 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Skip special expansion in Alfa mode Message-ID: <20120806075238.GA26736@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 Alfa mode for formal verification, a special expansion of the iterator is not needed, as the formal verification backend directly deals with the source form of the iterator. Thus, skip this expansion. Tested on x86_64-pc-linux-gnu, committed on trunk 2012-08-06 Yannick Moy * sem_ch5.adb (Analyze_Iterator_Specification): Do not perform an expansion of the iterator in Alfa mode. Index: sem_ch5.adb =================================================================== --- sem_ch5.adb (revision 190158) +++ sem_ch5.adb (working copy) @@ -1665,16 +1665,21 @@ -- If the domain of iteration is an expression, create a declaration for -- it, so that finalization actions are introduced outside of the loop. -- The declaration must be a renaming because the body of the loop may - -- assign to elements. When the context is a quantified expression, the - -- renaming declaration is delayed until the expansion phase. + -- assign to elements. if not Is_Entity_Name (Iter_Name) + + -- When the context is a quantified expression, the renaming + -- declaration is delayed until the expansion phase if we are + -- doing expansion. + and then (Nkind (Parent (N)) /= N_Quantified_Expression + or else Operating_Mode = Check_Semantics) - -- The following two tests need comments ??? + -- Do not perform this expansion in Alfa mode, since the formal + -- verification directly deals with the source form of the iterator. - or else Operating_Mode = Check_Semantics - or else Alfa_Mode) + and then not Alfa_Mode then declare Id : constant Entity_Id := Make_Temporary (Loc, 'R', Iter_Name); @@ -1711,7 +1716,7 @@ -- Container is an entity or an array with uncontrolled components, or -- else it is a container iterator given by a function call, typically -- called Iterate in the case of predefined containers, even though - -- Iterate is not a reserved name. What matter is that the return type + -- Iterate is not a reserved name. What matters is that the return type -- of the function is an iterator type. elsif Is_Entity_Name (Iter_Name) then