From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 111213 invoked by alias); 13 Aug 2019 08:32:12 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Received: (qmail 110916 invoked by uid 89); 13 Aug 2019 08:32:10 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-10.6 required=5.0 tests=AWL,BAYES_00,GIT_PATCH_2,GIT_PATCH_3,SPF_NEUTRAL autolearn=ham version=3.3.1 spammy=UD:F X-HELO: eggs.gnu.org Received: from eggs.gnu.org (HELO eggs.gnu.org) (209.51.188.92) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Tue, 13 Aug 2019 08:32:09 +0000 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1hxSDo-0001dM-Bm for gcc-patches@gcc.gnu.org; Tue, 13 Aug 2019 04:32:01 -0400 Received: from rock.gnat.com ([205.232.38.15]:53673) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1hxSDo-0001cx-2i for gcc-patches@gcc.gnu.org; Tue, 13 Aug 2019 04:32:00 -0400 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 6C784560F0; Tue, 13 Aug 2019 04:31:59 -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 B+WIOSKBlP73; Tue, 13 Aug 2019 04:31:59 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 7CFA6560F6; Tue, 13 Aug 2019 04:31:57 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id 7BC7D6B4; Tue, 13 Aug 2019 04:31:57 -0400 (EDT) Date: Tue, 13 Aug 2019 08:32:00 -0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Avoid crash in GNATprove_Mode on allocator inside type Message-ID: <20190813083157.GA38580@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="Kj7319i9nmIyA2yE" Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-detected-operating-system: by eggs.gnu.org: GNU/Linux 3.x X-Received-From: 205.232.38.15 X-IsSubscribed: yes X-SW-Source: 2019-08/txt/msg00806.txt.bz2 --Kj7319i9nmIyA2yE Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Content-length: 751 In the special mode for GNATprove, subtypes should be declared for allocators when constraints are used. This was done previously but it does not work inside spec expressions, as the declaration is not inserted and analyzed in the AST in that case, leading to a later crash on an incomplete entity. Thus, no declaration should be created in such a case, letting GNATprove later reject such code due to the use of an allocator in an interfering context. Tested on x86_64-pc-linux-gnu, committed on trunk 2019-08-13 Yannick Moy gcc/ada/ * sem_ch4.adb (Analyze_Allocator): Do not insert subtype declaration for allocator inside a spec expression. gcc/testsuite/ * gnat.dg/allocator2.adb, gnat.dg/allocator2.ads: New testcase. --Kj7319i9nmIyA2yE Content-Type: text/x-diff; charset=us-ascii Content-Disposition: attachment; filename="patch.diff" Content-length: 1782 --- gcc/ada/sem_ch4.adb +++ gcc/ada/sem_ch4.adb @@ -676,9 +676,15 @@ package body Sem_Ch4 is -- In GNATprove mode we need to preserve the link between -- the original subtype indication and the anonymous subtype, - -- to extend proofs to constrained acccess types. - - if Expander_Active or else GNATprove_Mode then + -- to extend proofs to constrained acccess types. We only do + -- that outside of spec expressions, otherwise the declaration + -- cannot be inserted and analyzed. In such a case, GNATprove + -- later rejects the allocator as it is not used here in + -- a non-interfering context (SPARK 4.8(2) and 7.1.3(12)). + + if Expander_Active + or else (GNATprove_Mode and then not In_Spec_Expression) + then Def_Id := Make_Temporary (Loc, 'S'); Insert_Action (E, --- /dev/null new file mode 100644 +++ gcc/testsuite/gnat.dg/allocator2.adb @@ -0,0 +1,6 @@ +-- { dg-do compile } +-- { dg-options "-gnatd.F" } + +package body Allocator2 is + procedure Dummy is null; +end Allocator2; --- /dev/null new file mode 100644 +++ gcc/testsuite/gnat.dg/allocator2.ads @@ -0,0 +1,15 @@ +pragma SPARK_Mode; +package Allocator2 is + type Nat_Array is array (Positive range <>) of Natural with + Default_Component_Value => 0; + type Nat_Stack (Max : Natural) is record + Content : Nat_Array (1 .. Max); + end record; + type Stack_Acc is access Nat_Stack; + type My_Rec is private; +private + type My_Rec is record + My_Stack : Stack_Acc := new Nat_Stack (Max => 10); + end record; + procedure Dummy; +end Allocator2; --Kj7319i9nmIyA2yE--