From patchwork Mon Aug 4 12:43:00 2014 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 376262 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]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 9B785140077 for ; Mon, 4 Aug 2014 22:43:27 +1000 (EST) 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=TGpnpaM/piDSiNoaVjyasv67tlv9PkQYgOW1Y3BUGqEjZQsgZJ ekCXhVXnfWWziX4mFIh8q39Ae7kbVMcn7pr+WmuyWXd4zaTPk71959pgsdTq02It h2u2IhtPZF4zbpC+6V0P29vXehPDe/EjFRtFJ5cWQs8rdagitKN7p2aew= 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=lSr4MKjyRuj0xcrFWm8yWKi7ooE=; b=xmNRvJE9oIBRdIJ5EXnH sGasFaIIwJXfYEXNA0CmaP9KXh+nEGuUEXcL0RCk7JJwZ0OGXFpHtDHTa/4oqPIT yvqv3fUJn5Gz0pPtdZhY6vyzVgSDjbPQVUl1uYo7yOMQecUu4mAvAh05dbjNoVfW EaTzZPrYaOP20I0A4/Qsi60= Received: (qmail 20367 invoked by alias); 4 Aug 2014 12:43:20 -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 20351 invoked by uid 89); 4 Aug 2014 12:43:16 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-1.9 required=5.0 tests=BAYES_00, T_FILL_THIS_FORM_SHORT autolearn=ham version=3.3.2 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 (AES256-SHA encrypted) ESMTPS; Mon, 04 Aug 2014 12:43:02 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 983F5116466; Mon, 4 Aug 2014 08:43:00 -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 rYU-N8pLXLm4; Mon, 4 Aug 2014 08:43:00 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [IPv6:2620:20:4000:0:a6ba:dbff:fe26:1f63]) by rock.gnat.com (Postfix) with ESMTP id 7551D116403; Mon, 4 Aug 2014 08:43:00 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 74CA93FE21; Mon, 4 Aug 2014 08:43:00 -0400 (EDT) Date: Mon, 4 Aug 2014 08:43:00 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Use of discriminants in derived types for SPARK 2014 Message-ID: <20140804124300.GA747@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.21 (2010-09-15) This patch implements the following rules related to the discriminants of derived types: The type of a discriminant_specification shall be discrete. A discriminant_specification shall not occur as part of a derived type declaration whose parent type is discriminated. ------------ -- Source -- ------------ -- discriminants.ads package Discriminants with SPARK_Mode is type Integer_Ptr is access all Integer; type OK_1 (D : Integer) is null record; type Error_1 (D : access Integer) is null record; type Error_2 (D : Integer_Ptr) is null record; type Error_3 (D : Float) is null record; type Parent_1 (D : Integer) is tagged null record; type Error_4 (D2 : Integer) is new Parent_1 (1) with null record; type Parent_2 (D : Integer := 2) is tagged limited null record; type Error_5 (D2 : Integer) is limited new Parent_2 (2) with null record; type Parent_3 (D : Integer) is null record; type Error_6 (D2 : Integer) is new Parent_3 (3); end Discriminants; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c discriminants.ads discriminants.ads:5:22: discriminant cannot have an access type discriminants.ads:6:22: discriminant cannot have an access type discriminants.ads:7:22: discriminant must have a discrete type discriminants.ads:10:19: discriminants not allowed if parent type is discriminated discriminants.ads:13:19: discriminants not allowed if parent type is discriminated discriminants.ads:16:19: discriminants not allowed if parent type is discriminated Tested on x86_64-pc-linux-gnu, committed on trunk 2014-08-04 Hristian Kirtchev * a-cfhama.ads, a-cfhase.ads, a-cforma.ads, a-cforse.ads Add SPARK_Mode pragmas to the public and private part of the unit. * sem_ch3.adb (Derive_Type_Declaration): Ensure that a derived type cannot have discriminants if the parent type already has discriminants. (Process_Discriminants): Ensure that the type of a discriminant is discrete. * sem_ch6.adb (Analyze_Subprogram_Body_Helper): The check on SPARK_Mode compatibility between a spec and a body can now be safely performed while processing a generic. * sem_ch7.adb (Analyze_Package_Body_Helper): The check on SPARK_Mode compatibility between a spec and a body can now be safely performed while processing a generic. * sem_prag.adb (Analyze_Pragma): Pragma SPARK_Mode can now be safely analyzed when processing a generic. Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 213566) +++ sem_ch3.adb (working copy) @@ -15046,7 +15046,7 @@ end if; -- Only composite types other than array types are allowed to have - -- discriminants. In SPARK, no types are allowed to have discriminants. + -- discriminants. if Present (Discriminant_Specifications (N)) then if (Is_Elementary_Type (Parent_Type) @@ -15057,8 +15057,22 @@ ("elementary or array type cannot have discriminants", Defining_Identifier (First (Discriminant_Specifications (N)))); Set_Has_Discriminants (T, False); + + -- The type is allowed to have discriminants + else Check_SPARK_05_Restriction ("discriminant type is not allowed", N); + + -- The following check is only relevant when SPARK_Mode is on as + -- it is not a standard Ada legality rule. A derived type cannot + -- have discriminants if the parent type is discriminated. + + if SPARK_Mode = On and then Has_Discriminants (Parent_Type) then + SPARK_Msg_N + ("discriminants not allowed if parent type is discriminated", + Defining_Identifier + (First (Discriminant_Specifications (N)))); + end if; end if; end if; @@ -18024,24 +18038,44 @@ end if; end if; - if Is_Access_Type (Discr_Type) then + -- The following checks are only relevant when SPARK_Mode is on as + -- they are not standard Ada legality rules. - -- Ada 2005 (AI-230): Access discriminant allowed in non-limited - -- record types + if SPARK_Mode = On then + if Is_Access_Type (Discr_Type) then + SPARK_Msg_N + ("discriminant cannot have an access type", + Discriminant_Type (Discr)); - if Ada_Version < Ada_2005 then - Check_Access_Discriminant_Requires_Limited - (Discr, Discriminant_Type (Discr)); + elsif not Is_Discrete_Type (Discr_Type) then + SPARK_Msg_N + ("discriminant must have a discrete type", + Discriminant_Type (Discr)); end if; - if Ada_Version = Ada_83 and then Comes_From_Source (Discr) then + -- Normal Ada rules + + else + if Is_Access_Type (Discr_Type) then + + -- Ada 2005 (AI-230): Access discriminant allowed in non- + -- limited record types + + if Ada_Version < Ada_2005 then + Check_Access_Discriminant_Requires_Limited + (Discr, Discriminant_Type (Discr)); + end if; + + if Ada_Version = Ada_83 and then Comes_From_Source (Discr) then + Error_Msg_N + ("(Ada 83) access discriminant not allowed", Discr); + end if; + + elsif not Is_Discrete_Type (Discr_Type) then Error_Msg_N - ("(Ada 83) access discriminant not allowed", Discr); + ("discriminants must have a discrete or access type", + Discriminant_Type (Discr)); end if; - - elsif not Is_Discrete_Type (Discr_Type) then - Error_Msg_N ("discriminants must have a discrete or access type", - Discriminant_Type (Discr)); end if; Set_Etype (Defining_Identifier (Discr), Discr_Type); Index: sem_ch7.adb =================================================================== --- sem_ch7.adb (revision 213570) +++ sem_ch7.adb (working copy) @@ -439,7 +439,7 @@ -- Verify that the SPARK_Mode of the body agrees with that of its spec - if not Inside_A_Generic and then Present (SPARK_Pragma (Body_Id)) then + if Present (SPARK_Pragma (Body_Id)) then if Present (SPARK_Aux_Pragma (Spec_Id)) then if Get_SPARK_Mode_From_Pragma (SPARK_Aux_Pragma (Spec_Id)) = Off and then Index: a-cfhase.ads =================================================================== --- a-cfhase.ads (revision 213536) +++ a-cfhase.ads (working copy) @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2004-2013, Free Software Foundation, Inc. -- +-- Copyright (C) 2004-2014, Free Software Foundation, Inc. -- -- -- -- This specification is derived from the Ada Reference Manual for use with -- -- GNAT. The copyright notice above, and the license provisions that follow -- @@ -70,6 +70,7 @@ package Ada.Containers.Formal_Hashed_Sets is pragma Annotate (GNATprove, External_Axiomatization); pragma Pure; + pragma SPARK_Mode (On); type Set (Capacity : Count_Type; Modulus : Hash_Type) is private with Iterable => (First => First, @@ -329,8 +330,8 @@ -- scanned yet. private - pragma Inline (Next); + pragma SPARK_Mode (Off); type Node_Type is record @@ -343,7 +344,7 @@ Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type); type Set (Capacity : Count_Type; Modulus : Hash_Type) is - new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record; + new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record; use HT_Types; Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 213571) +++ sem_prag.adb (working copy) @@ -19243,13 +19243,6 @@ Rewrite (N, Make_Null_Statement (Loc)); Analyze (N); return; - - -- Do not analyze the pragma when it appears inside a generic - -- because the semantic information of the related context is - -- scarce. - - elsif Inside_A_Generic then - return; end if; GNAT_Pragma; Index: a-cforma.ads =================================================================== --- a-cforma.ads (revision 213536) +++ a-cforma.ads (working copy) @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2004-2013, Free Software Foundation, Inc. -- +-- Copyright (C) 2004-2014, Free Software Foundation, Inc. -- -- -- -- This specification is derived from the Ada Reference Manual for use with -- -- GNAT. The copyright notice above, and the license provisions that follow -- @@ -69,6 +69,7 @@ package Ada.Containers.Formal_Ordered_Maps is pragma Annotate (GNATprove, External_Axiomatization); pragma Pure; + pragma SPARK_Mode (On); function Equivalent_Keys (Left, Right : Key_Type) return Boolean with Global => null; @@ -265,10 +266,11 @@ function Overlap (Left, Right : Map) return Boolean with Global => null; -- Overlap returns True if the containers have common keys + private - pragma Inline (Next); pragma Inline (Previous); + pragma SPARK_Mode (Off); subtype Node_Access is Count_Type; @@ -288,7 +290,7 @@ new Ada.Containers.Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type); type Map (Capacity : Count_Type) is - new Tree_Types.Tree_Type (Capacity) with null record; + new Tree_Types.Tree_Type (Capacity) with null record; type Cursor is record Node : Node_Access; Index: sem_ch6.adb =================================================================== --- sem_ch6.adb (revision 213571) +++ sem_ch6.adb (working copy) @@ -3741,10 +3741,7 @@ -- Verify that the SPARK_Mode of the body agrees with that of its spec - if not Inside_A_Generic - and then Present (Spec_Id) - and then Present (SPARK_Pragma (Body_Id)) - then + if Present (Spec_Id) and then Present (SPARK_Pragma (Body_Id)) then if Present (SPARK_Pragma (Spec_Id)) then if Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) = Off and then Index: a-cfhama.ads =================================================================== --- a-cfhama.ads (revision 213536) +++ a-cfhama.ads (working copy) @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2004-2013, Free Software Foundation, Inc. -- +-- Copyright (C) 2004-2014, Free Software Foundation, Inc. -- -- -- -- This specification is derived from the Ada Reference Manual for use with -- -- GNAT. The copyright notice above, and the license provisions that follow -- @@ -68,6 +68,7 @@ package Ada.Containers.Formal_Hashed_Maps is pragma Annotate (GNATprove, External_Axiomatization); pragma Pure; + pragma SPARK_Mode (On); type Map (Capacity : Count_Type; Modulus : Hash_Type) is private with Iterable => (First => First, @@ -276,6 +277,7 @@ pragma Inline (Has_Element); pragma Inline (Equivalent_Keys); pragma Inline (Next); + pragma SPARK_Mode (Off); type Node_Type is record Key : Key_Type; @@ -285,11 +287,10 @@ end record; package HT_Types is new - Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types - (Node_Type); + Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type); type Map (Capacity : Count_Type; Modulus : Hash_Type) is - new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record; + new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record; use HT_Types; Index: a-cforse.ads =================================================================== --- a-cforse.ads (revision 213536) +++ a-cforse.ads (working copy) @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2004-2013, Free Software Foundation, Inc. -- +-- Copyright (C) 2004-2014, Free Software Foundation, Inc. -- -- -- -- This specification is derived from the Ada Reference Manual for use with -- -- GNAT. The copyright notice above, and the license provisions that follow -- @@ -67,6 +67,7 @@ package Ada.Containers.Formal_Ordered_Sets is pragma Annotate (GNATprove, External_Axiomatization); pragma Pure; + pragma SPARK_Mode (On); function Equivalent_Elements (Left, Right : Element_Type) return Boolean with @@ -347,9 +348,9 @@ -- scanned yet. private - pragma Inline (Next); pragma Inline (Previous); + pragma SPARK_Mode (Off); type Node_Type is record Has_Element : Boolean := False;