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 <kirtc...@adacore.com>
* 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;
