+2014-08-04 Hristian Kirtchev <kirtchev@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.
+
+2014-08-04 Nicolas Roche <roche@adacore.com>
+
+ * g-dirope.adb: Minor reformating.
+
2014-08-04 Robert Dewar <dewar@adacore.com>
* sem_ch6.adb: Minor reformatting.
-- --
-- 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 --
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,
pragma Inline (Has_Element);
pragma Inline (Equivalent_Keys);
pragma Inline (Next);
+ pragma SPARK_Mode (Off);
type Node_Type is record
Key : Key_Type;
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;
-- --
-- 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 --
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,
-- scanned yet.
private
-
pragma Inline (Next);
+ pragma SPARK_Mode (Off);
type Node_Type is
record
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;
-- --
-- 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 --
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;
function Overlap (Left, Right : Map) return Boolean with
Global => null;
-- Overlap returns True if the containers have common keys
-private
+private
pragma Inline (Next);
pragma Inline (Previous);
+ pragma SPARK_Mode (Off);
subtype Node_Access is Count_Type;
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;
-- --
-- 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 --
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
-- scanned yet.
private
-
pragma Inline (Next);
pragma Inline (Previous);
+ pragma SPARK_Mode (Off);
type Node_Type is record
Has_Element : Boolean := False;
-- --
-- B o d y --
-- --
--- Copyright (C) 1998-2012, AdaCore --
+-- Copyright (C) 1998-2014, AdaCore --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
end Read;
-------------------------
- -- Read_Is_Thread_Sage --
+ -- Read_Is_Thread_Safe --
-------------------------
function Read_Is_Thread_Safe return Boolean is
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)
("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;
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.
+
+ if SPARK_Mode = On then
+ if Is_Access_Type (Discr_Type) then
+ SPARK_Msg_N
+ ("discriminant cannot have an access type",
+ 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;
- -- Ada 2005 (AI-230): Access discriminant allowed in non-limited
- -- record types
+ -- Normal Ada rules
- if Ada_Version < Ada_2005 then
- Check_Access_Discriminant_Requires_Limited
- (Discr, Discriminant_Type (Discr));
- end if;
+ 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
+ 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);
-- 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
-- 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
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;
projects / thirdparty / gcc.git / commitdiff
