From patchwork Mon Aug 29 08:22:15 2011 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 111972 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 6F6CBB6F77 for ; Mon, 29 Aug 2011 18:22:44 +1000 (EST) Received: (qmail 30266 invoked by alias); 29 Aug 2011 08:22:35 -0000 Received: (qmail 30257 invoked by uid 22791); 29 Aug 2011 08:22:33 -0000 X-SWARE-Spam-Status: No, hits=-2.0 required=5.0 tests=AWL, BAYES_00, RP_MATCHES_RCVD X-Spam-Check-By: sourceware.org Received: from mel.act-europe.fr (HELO mel.act-europe.fr) (194.98.77.210) by sourceware.org (qpsmtpd/0.43rc1) with ESMTP; Mon, 29 Aug 2011 08:22:20 +0000 Received: from localhost (localhost [127.0.0.1]) by filtered-smtp.eu.adacore.com (Postfix) with ESMTP id 8FC80CB02AF; Mon, 29 Aug 2011 10:22:21 +0200 (CEST) Received: from mel.act-europe.fr ([127.0.0.1]) by localhost (smtp.eu.adacore.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id WtLiX2ciTLQ5; Mon, 29 Aug 2011 10:22:11 +0200 (CEST) Received: from saumur.act-europe.fr (saumur.act-europe.fr [10.10.0.183]) by mel.act-europe.fr (Postfix) with ESMTP id 555D6CB016C; Mon, 29 Aug 2011 10:22:11 +0200 (CEST) Received: by saumur.act-europe.fr (Postfix, from userid 525) id 1E91624524F; Mon, 29 Aug 2011 10:22:15 +0200 (CEST) Date: Mon, 29 Aug 2011 10:22:15 +0200 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Prevent expansion of array aggregates in formal verification mode Message-ID: <20110829082215.GA14609@adacore.com> Mime-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.9i X-IsSubscribed: yes 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 The backend for formal verification handles much more easily aggregates that are not expanded into loops, as this happens with array aggregates, so prevent expansion in this mode. Tested on x86_64-pc-linux-gnu, committed on trunk 2011-08-29 Yannick Moy * exp_aggr.adb (Expand_Array_Aggregate): Do not expand array aggregates in formal verification. Index: exp_aggr.adb =================================================================== --- exp_aggr.adb (revision 178155) +++ exp_aggr.adb (working copy) @@ -4664,6 +4664,12 @@ Check_Same_Aggr_Bounds (N, 1); end if; + -- In formal verification mode, leave the aggregate non-expanded + + if ALFA_Mode then + return; + end if; + -- STEP 2 -- Here we test for is packed array aggregate that we can handle at