From patchwork Thu Jul 11 08:03:48 2019 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: 1130684 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-504890-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dmarc=none (p=none dis=none) header.from=adacore.com Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="hVisVzkz"; 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 45kpWc109Sz9sNg for ; Thu, 11 Jul 2019 18:05:15 +1000 (AEST) 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=MUxBhMhBhRUwNqw06A/zqzBGh3CZZouDldRbVZV4M8b+x6ZzGC /avloTa8qQ2eIHeTcb9Ruc4BjAmJ8Bv6Opi1gp48+uolq19RL4sn2QFOABTrwMt9 MHAR95psf/pBoacH75rHW0CXDhD0VPer1mBzk55FIb+r+h9cAvk964ess= 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=q8OV/3V8J4QS1jFAC6sTYC3T2gg=; b=hVisVzkzTuYsxcbYwsDU TXFosNO7WRk1bgzO0Tp3rMFrx7Uk1IqaYJVu5730TahR1FWPdyxUc3YALb4esCcA 5uRInCg8zoy8eqFq2tvWXBN4KVMTFo6f5HOXCLw2oSDiC00hN1+mJvvp8YC7/i5n 8fU1uuxO942RlvSBd4fZ7gg= Received: (qmail 87598 invoked by alias); 11 Jul 2019 08:03:50 -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 87512 invoked by uid 89); 11 Jul 2019 08:03:50 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-11.9 required=5.0 tests=BAYES_00, GIT_PATCH_2, GIT_PATCH_3, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.1 spammy= 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 Jul 2019 08:03:48 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 75C94561F1; Thu, 11 Jul 2019 04:03:48 -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 VGCHoWfyTGQy; Thu, 11 Jul 2019 04:03:48 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [IPv6:2620:20:4000:0:46a8:42ff:fe0e:e294]) by rock.gnat.com (Postfix) with ESMTP id 64C4C561F3; Thu, 11 Jul 2019 04:03:48 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id 635DA6F7; Thu, 11 Jul 2019 04:03:48 -0400 (EDT) Date: Thu, 11 Jul 2019 04:03:48 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Avoid spurious errors on dimensionality checking in GNATprove Message-ID: <20190711080347.GA95293@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes In the special GNATprove mode of the frontend, automatic inlining is performed, which may lead to spurious errors on dimensionality checking. Avoid performing this checking on inlined code, which has already been checked for dimensionality errors. There is no impact on compilation. Tested on x86_64-pc-linux-gnu, committed on trunk 2019-07-11 Yannick Moy gcc/ada/ * sem_res.adb (Resolve_Call): Do not perform dimensionality checking on inlined bodies. --- gcc/ada/sem_res.adb +++ gcc/ada/sem_res.adb @@ -6949,7 +6949,9 @@ package body Sem_Res is -- Check the dimensions of the actuals in the call. For function calls, -- propagate the dimensions from the returned type to N. - Analyze_Dimension_Call (N, Nam); + if not In_Inlined_Body then + Analyze_Dimension_Call (N, Nam); + end if; -- All done, evaluate call and deal with elaboration issues