===================================================================
@@ -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);
===================================================================
@@ -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
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- 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;
===================================================================
@@ -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;
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- 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;
===================================================================
@@ -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
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- 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;
===================================================================
@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
+-- 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;