OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[multiple changes]

Browse Source 
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.

From-SVN: r213575
This commit is contained in:
Arnaud Charlet 2014-08-04 14:42:52 +02:00
parent 31acf1bb11
commit f1c7be38ad
10 changed files with 90 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
gcc/ada/ChangeLog
View File

@ -1,3 +1,25 @@
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.

9
gcc/ada/a-cfhama.ads
View File

@ -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 @@ generic
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 @@ private
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 @@ private
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;

7
gcc/ada/a-cfhase.ads
View File

@ -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 @@ generic
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 @@ package Ada.Containers.Formal_Hashed_Sets is
-- scanned yet.
private
pragma Inline (Next);
pragma SPARK_Mode (Off);
type Node_Type is
record
@ -343,7 +344,7 @@ private
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;

8
gcc/ada/a-cforma.ads
View File

@ -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 @@ generic
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 @@ package Ada.Containers.Formal_Ordered_Maps is
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;
@ -288,7 +290,7 @@ private
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;

5
gcc/ada/a-cforse.ads
View File

@ -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 @@ generic
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 @@ package Ada.Containers.Formal_Ordered_Sets is
-- scanned yet.
private
pragma Inline (Next);
pragma Inline (Previous);
pragma SPARK_Mode (Off);
type Node_Type is record
Has_Element : Boolean := False;

4
gcc/ada/g-dirope.adb
View File

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -693,7 +693,7 @@ package body GNAT.Directory_Operations is
end Read;
-------------------------
-- Read_Is_Thread_Sage --
-- Read_Is_Thread_Safe --
-------------------------
function Read_Is_Thread_Safe return Boolean is

60
gcc/ada/sem_ch3.adb
View File

@ -15046,7 +15046,7 @@ package body Sem_Ch3 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)
@ -15057,8 +15057,22 @@ package body Sem_Ch3 is
("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 @@ package body Sem_Ch3 is
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);

5
gcc/ada/sem_ch6.adb
View File

@ -3741,10 +3741,7 @@ package body Sem_Ch6 is
-- 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

2
gcc/ada/sem_ch7.adb
View File

@ -439,7 +439,7 @@ package body Sem_Ch7 is
-- 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

7
gcc/ada/sem_prag.adb
View File

@ -19243,13 +19243,6 @@ package body Sem_Prag is
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;