From patchwork Wed Aug 14 09:53:12 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: 1146894 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-506906-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="J1u+GBy3"; 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 467lKy3j0Wz9sN1 for ; Wed, 14 Aug 2019 19:54:30 +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=s2yE59atkiF2YKPvX6qrFnYKj9Riip1vjYtKHFq1er+zsWnvZH 2jl6z7Ms5HOI6Ph0PWRQ+fQNwCkuwnaigbOg+XcqPQml1FksTRlu7c9F0GG0bwMU jaFIG3h3eRkJOBXUVFMpa2QWHXl4N+6PyOJky7obCGp571O2R6gpv267o= 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=4BcHdkOu9mTzRm3hEYeyjf7mBnQ=; b=J1u+GBy3c0CJ06YpGA9t LIVj2hP8uustx5SOZRYoVT2F+eGXidDcMwGA2/FyRrtymHUpStAgnX2DB3Au5Vi8 2shF2jDJS5LCqFPhGLaBHElZTgbG150SY9ueO1RrHCB3SsXhA2atHaUkDsmMXxxT +EpWMZn35Mq9WoNBG2RsXHg= Received: (qmail 73464 invoked by alias); 14 Aug 2019 09:53:18 -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 73411 invoked by uid 89); 14 Aug 2019 09:53:17 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-11.0 required=5.0 tests=AWL, 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; Wed, 14 Aug 2019 09:53:16 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id D4ED056107; Wed, 14 Aug 2019 05:53:12 -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 GiMzdbzEUE5r; Wed, 14 Aug 2019 05:53:12 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id C3BCF11626C; Wed, 14 Aug 2019 05:53:12 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id C26E36CC; Wed, 14 Aug 2019 05:53:12 -0400 (EDT) Date: Wed, 14 Aug 2019 05:53:12 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Ed Schonberg Subject: [Ada] Crash on quantified expression in disabled assertion Message-ID: <20190814095312.GA52138@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes The defining identifier of a quantified expression may be the freeze point of its type. If the quantified expression appears in an assertion that is disavbled, the freeze node for that type may appear in a tree that will be discarded when the enclosing pragma is elaborated. To ensure that the freeze node is reachable for subsquent uses we must generate its freeze node explicitly when the quantified expression is analyzed. Tested on x86_64-pc-linux-gnu, committed on trunk 2019-08-14 Ed Schonberg gcc/ada/ * exp_ch4.adb (Expand_N_Quantified_Expression): Freeze explicitly the type of the loop parameter. gcc/testsuite/ * gnat.dg/assert2.adb, gnat.dg/assert2.ads: New testcase. --- gcc/ada/exp_ch4.adb +++ gcc/ada/exp_ch4.adb @@ -10337,8 +10337,30 @@ package body Exp_Ch4 is Flag : Entity_Id; Scheme : Node_Id; Stmts : List_Id; + Var : Entity_Id; begin + -- Ensure that the bound variable is properly frozen. We must do + -- this before expansion because the expression is about to be + -- converted into a loop, and resulting freeze nodes may end up + -- in the wrong place in the tree. + + if Present (Iter_Spec) then + Var := Defining_Identifier (Iter_Spec); + else + Var := Defining_Identifier (Loop_Spec); + end if; + + declare + P : Node_Id := Parent (N); + begin + while Nkind (P) in N_Subexpr loop + P := Parent (P); + end loop; + + Freeze_Before (P, Etype (Var)); + end; + -- Create the declaration of the flag which tracks the status of the -- quantified expression. Generate: --- /dev/null new file mode 100644 +++ gcc/testsuite/gnat.dg/assert2.adb @@ -0,0 +1,5 @@ +-- { dg-do compile } + +package body Assert2 is + procedure Dummy is null; +end Assert2; --- /dev/null new file mode 100644 +++ gcc/testsuite/gnat.dg/assert2.ads @@ -0,0 +1,15 @@ +package Assert2 + with SPARK_Mode +is + type Living is new Integer; + function Is_Martian (Unused : Living) return Boolean is (False); + + function Is_Green (Unused : Living) return Boolean is (True); + + pragma Assert + (for all M in Living => (if Is_Martian (M) then Is_Green (M))); + pragma Assert + (for all M in Living => (if Is_Martian (M) then not Is_Green (M))); + + procedure Dummy; +end Assert2;