public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r13-404] [Ada] Adapt body of formal sets and maps for SPARK
@ 2022-05-13 8:09 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-05-13 8:09 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:f8e12e78628238a9e3cf68ce9376aa2e28e0506f
commit r13-404-gf8e12e78628238a9e3cf68ce9376aa2e28e0506f
Author: Yannick Moy <moy@adacore.com>
Date: Thu Feb 17 08:58:30 2022 +0100
[Ada] Adapt body of formal sets and maps for SPARK
Remove violations of SPARK rules, to prepare for the proof of hashed
sets and maps:
- Make the type of hash tables not tagged, so that it will be possible
to mark the type of nodes as having relaxed initialization.
- Remove comparison of addresses as check or optimization: as a check,
it is not necessary in SPARK as the caller cannot pass in aliased
parameters in such cases; as an optimization, it is not possible in
SPARK code.
- Avoid aliasing when inserting a node in the hash table. The code for
insertion in sets and maps was explicitly aliasing a global for the
container and a parameter for its hash table component, both being
written. Rewrite the code to pass only the hash table as parameter.
- Insert constants for subtype constraints, which cannot depend on
variables in SPARK code.
- Use procedures instead of functions when side-effects are expected.
- Rename variables whose value is only written through calls and not
read, using Unused prefix, so that flow analysis does not warn about
it.
gcc/ada/
* libgnat/a-cfhama.adb (Generic_Allocate): Retype to avoid
aliasing.
(Assign, Move): Remove address comparison.
(Include): Insert constants for subtype constraints.
(Insert): Rewrite to avoid aliasing and function with side-effects.
* libgnat/a-cfhase.adb (Generic_Allocate): Retype to avoid
aliasing.
(Assign, Move): Remove address comparison.
(Difference, Intersection, Is_Subset, Overlap,
Symmetric_Difference, Union): Remove address comparison. Insert
constants for subtype constraints.
(Insert): Rewrite to avoid aliasing and function with
side-effects.
* libgnat/a-chtgfk.adb (Checked_Equivalent_Keys, Checked_Index,
Delete_Key_Sans_Free, Find, Generic_Replace_Element, Index):
Type for hash tables not tagged anymore.
(Generic_Conditional_Insert): New_Node generic formal is a
procedure taking the hash table as first parameter now, to avoid
aliasing in the caller.
* libgnat/a-chtgfk.ads: Same.
* libgnat/a-chtgfo.adb (Checked_Index, Clear,
Delete_Node_At_Index, Delete_Node_Sans_Free, First, Free,
Generic_Allocate, Generic_Iteration, Generic_Read,
Generic_Write, Index, Next): Type for hash tables not tagged
anymore.
(Generic_Equal): Removed tagged. Remove address comparison.
* libgnat/a-chtgfo.ads: Same.
* libgnat/a-cohata.ads (Hash_Table_Type): Remove tagged.
Diff:
---
gcc/ada/libgnat/a-cfhama.adb | 41 +++++----
gcc/ada/libgnat/a-cfhase.adb | 196 +++++++++++++++++--------------------------
gcc/ada/libgnat/a-chtgfk.adb | 24 +++---
gcc/ada/libgnat/a-chtgfk.ads | 18 ++--
gcc/ada/libgnat/a-chtgfo.adb | 32 ++++---
gcc/ada/libgnat/a-chtgfo.ads | 28 +++----
gcc/ada/libgnat/a-cohata.ads | 2 +-
7 files changed, 145 insertions(+), 196 deletions(-)
diff --git a/gcc/ada/libgnat/a-cfhama.adb b/gcc/ada/libgnat/a-cfhama.adb
index c688a86d1e1..c2a7c595854 100644
--- a/gcc/ada/libgnat/a-cfhama.adb
+++ b/gcc/ada/libgnat/a-cfhama.adb
@@ -56,7 +56,7 @@ is
generic
with procedure Set_Element (Node : in out Node_Type);
procedure Generic_Allocate
- (HT : in out Map;
+ (HT : in out HT_Types.Hash_Table_Type;
Node : out Count_Type);
function Hash_Node (Node : Node_Type) return Hash_Type;
@@ -154,10 +154,6 @@ is
-- Start of processing for Assign
begin
- if Target'Address = Source'Address then
- return;
- end if;
-
if Target.Capacity < Length (Source) then
raise Constraint_Error with -- correct exception ???
"Source length exceeds Target capacity";
@@ -556,13 +552,16 @@ is
-- Generic_Allocate --
----------------------
- procedure Generic_Allocate (HT : in out Map; Node : out Count_Type) is
+ procedure Generic_Allocate
+ (HT : in out HT_Types.Hash_Table_Type;
+ Node : out Count_Type)
+ is
procedure Allocate is
new HT_Ops.Generic_Allocate (Set_Element);
begin
- Allocate (HT.Content, Node);
- HT.Content.Nodes (Node).Has_Element := True;
+ Allocate (HT, Node);
+ HT.Nodes (Node).Has_Element := True;
end Generic_Allocate;
-----------------
@@ -606,7 +605,8 @@ is
if not Inserted then
declare
- N : Node_Type renames Container.Content.Nodes (Position.Node);
+ P : constant Count_Type := Position.Node;
+ N : Node_Type renames Container.Content.Nodes (P);
begin
N.Key := Key;
N.Element := New_Item;
@@ -628,7 +628,9 @@ is
procedure Assign_Key (Node : in out Node_Type);
pragma Inline (Assign_Key);
- function New_Node return Count_Type;
+ procedure New_Node
+ (HT : in out HT_Types.Hash_Table_Type;
+ Node : out Count_Type);
pragma Inline (New_Node);
procedure Local_Insert is
@@ -651,11 +653,12 @@ is
-- New_Node --
--------------
- function New_Node return Count_Type is
- Result : Count_Type;
+ procedure New_Node
+ (HT : in out HT_Types.Hash_Table_Type;
+ Node : out Count_Type)
+ is
begin
- Allocate (Container, Result);
- return Result;
+ Allocate (HT, Node);
end New_Node;
-- Start of processing for Insert
@@ -669,11 +672,11 @@ is
Key : Key_Type;
New_Item : Element_Type)
is
- Position : Cursor;
- Inserted : Boolean;
+ Unused_Position : Cursor;
+ Inserted : Boolean;
begin
- Insert (Container, Key, New_Item, Position, Inserted);
+ Insert (Container, Key, New_Item, Unused_Position, Inserted);
if not Inserted then
raise Constraint_Error with "attempt to insert key already in map";
@@ -727,10 +730,6 @@ is
Y : Count_Type;
begin
- if Target'Address = Source'Address then
- return;
- end if;
-
if Target.Capacity < Length (Source) then
raise Constraint_Error with -- ???
"Source length exceeds Target capacity";
diff --git a/gcc/ada/libgnat/a-cfhase.adb b/gcc/ada/libgnat/a-cfhase.adb
index 786abf1dc99..834f43a6c4e 100644
--- a/gcc/ada/libgnat/a-cfhase.adb
+++ b/gcc/ada/libgnat/a-cfhase.adb
@@ -58,7 +58,7 @@ is
generic
with procedure Set_Element (Node : in out Node_Type);
procedure Generic_Allocate
- (HT : in out Set;
+ (HT : in out Hash_Table_Type;
Node : out Count_Type);
function Hash_Node (Node : Node_Type) return Hash_Type;
@@ -167,22 +167,18 @@ is
--------------------
procedure Insert_Element (Source_Node : Count_Type) is
- N : Node_Type renames Source.Content.Nodes (Source_Node);
- X : Count_Type;
- B : Boolean;
+ N : Node_Type renames Source.Content.Nodes (Source_Node);
+ Unused_X : Count_Type;
+ B : Boolean;
begin
- Insert (Target, N.Element, X, B);
+ Insert (Target, N.Element, Unused_X, B);
pragma Assert (B);
end Insert_Element;
-- Start of processing for Assign
begin
- if Target'Address = Source'Address then
- return;
- end if;
-
if Target.Capacity < Length (Source) then
raise Storage_Error with "not enough capacity"; -- SE or CE? ???
end if;
@@ -335,11 +331,6 @@ is
SN : Nodes_Type renames Source.Content.Nodes;
begin
- if Target'Address = Source'Address then
- Clear (Target);
- return;
- end if;
-
Src_Length := Source.Content.Length;
if Src_Length = 0 then
@@ -393,13 +384,13 @@ is
-------------
procedure Process (L_Node : Count_Type) is
- B : Boolean;
- E : Element_Type renames Left.Content.Nodes (L_Node).Element;
- X : Count_Type;
+ B : Boolean;
+ E : Element_Type renames Left.Content.Nodes (L_Node).Element;
+ Unused_X : Count_Type;
begin
if Find (Right, E).Node = 0 then
- Insert (Target, E, X, B);
+ Insert (Target, E, Unused_X, B);
pragma Assert (B);
end if;
end Process;
@@ -411,14 +402,7 @@ is
end Difference;
function Difference (Left : Set; Right : Set) return Set is
- C : Count_Type;
- H : Hash_Type;
-
begin
- if Left'Address = Right'Address then
- return Empty_Set;
- end if;
-
if Length (Left) = 0 then
return Empty_Set;
end if;
@@ -427,12 +411,14 @@ is
return Copy (Left);
end if;
- C := Length (Left);
- H := Default_Modulus (C);
-
- return S : Set (C, H) do
- Difference (Left, Right, Target => S);
- end return;
+ declare
+ C : constant Count_Type := Length (Left);
+ H : constant Hash_Type := Default_Modulus (C);
+ begin
+ return S : Set (C, H) do
+ Difference (Left, Right, Target => S);
+ end return;
+ end;
end Difference;
-------------
@@ -461,7 +447,7 @@ is
function Equivalent_Sets (Left, Right : Set) return Boolean is
function Find_Equivalent_Key
- (R_HT : Hash_Table_Type'Class;
+ (R_HT : Hash_Table_Type;
L_Node : Node_Type) return Boolean;
pragma Inline (Find_Equivalent_Key);
@@ -473,7 +459,7 @@ is
-------------------------
function Find_Equivalent_Key
- (R_HT : Hash_Table_Type'Class;
+ (R_HT : Hash_Table_Type;
L_Node : Node_Type) return Boolean
is
R_Index : constant Hash_Type :=
@@ -793,11 +779,14 @@ is
-- Generic_Allocate --
----------------------
- procedure Generic_Allocate (HT : in out Set; Node : out Count_Type) is
+ procedure Generic_Allocate
+ (HT : in out Hash_Table_Type;
+ Node : out Count_Type)
+ is
procedure Allocate is new HT_Ops.Generic_Allocate (Set_Element);
begin
- Allocate (HT.Content, Node);
- HT.Content.Nodes (Node).Has_Element := True;
+ Allocate (HT, Node);
+ HT.Nodes (Node).Has_Element := True;
end Generic_Allocate;
package body Generic_Keys with SPARK_Mode => Off is
@@ -1031,11 +1020,11 @@ is
end Insert;
procedure Insert (Container : in out Set; New_Item : Element_Type) is
- Inserted : Boolean;
- Position : Cursor;
+ Inserted : Boolean;
+ Unused_Position : Cursor;
begin
- Insert (Container, New_Item, Position, Inserted);
+ Insert (Container, New_Item, Unused_Position, Inserted);
if not Inserted then
raise Constraint_Error with
@@ -1052,7 +1041,9 @@ is
procedure Allocate_Set_Element (Node : in out Node_Type);
pragma Inline (Allocate_Set_Element);
- function New_Node return Count_Type;
+ procedure New_Node
+ (HT : in out Hash_Table_Type;
+ Node : out Count_Type);
pragma Inline (New_Node);
procedure Local_Insert is
@@ -1074,11 +1065,12 @@ is
-- New_Node --
--------------
- function New_Node return Count_Type is
- Result : Count_Type;
+ procedure New_Node
+ (HT : in out Hash_Table_Type;
+ Node : out Count_Type)
+ is
begin
- Allocate (Container, Result);
- return Result;
+ Allocate (HT, Node);
end New_Node;
-- Start of processing for Insert
@@ -1096,10 +1088,6 @@ is
TN : Nodes_Type renames Target.Content.Nodes;
begin
- if Target'Address = Source'Address then
- return;
- end if;
-
if Source.Content.Length = 0 then
Clear (Target);
return;
@@ -1133,13 +1121,13 @@ is
-------------
procedure Process (L_Node : Count_Type) is
- E : Element_Type renames Left.Content.Nodes (L_Node).Element;
- X : Count_Type;
- B : Boolean;
+ E : Element_Type renames Left.Content.Nodes (L_Node).Element;
+ Unused_X : Count_Type;
+ B : Boolean;
begin
if Find (Right, E).Node /= 0 then
- Insert (Target, E, X, B);
+ Insert (Target, E, Unused_X, B);
pragma Assert (B);
end if;
end Process;
@@ -1151,17 +1139,11 @@ is
end Intersection;
function Intersection (Left : Set; Right : Set) return Set is
- C : Count_Type;
- H : Hash_Type;
+ C : constant Count_Type :=
+ Count_Type'Min (Length (Left), Length (Right)); -- ???
+ H : constant Hash_Type := Default_Modulus (C);
begin
- if Left'Address = Right'Address then
- return Copy (Left);
- end if;
-
- C := Count_Type'Min (Length (Left), Length (Right)); -- ???
- H := Default_Modulus (C);
-
return S : Set (C, H) do
if Length (Left) /= 0 and Length (Right) /= 0 then
Intersection (Left, Right, Target => S);
@@ -1196,10 +1178,6 @@ is
Subset_Nodes : Nodes_Type renames Subset.Content.Nodes;
begin
- if Subset'Address = Of_Set'Address then
- return True;
- end if;
-
if Length (Subset) > Length (Of_Set) then
return False;
end if;
@@ -1207,7 +1185,8 @@ is
Subset_Node := First (Subset).Node;
while Subset_Node /= 0 loop
declare
- N : Node_Type renames Subset_Nodes (Subset_Node);
+ S : constant Count_Type := Subset_Node;
+ N : Node_Type renames Subset_Nodes (S);
E : Element_Type renames N.Element;
begin
@@ -1242,10 +1221,6 @@ is
X, Y : Count_Type;
begin
- if Target'Address = Source'Address then
- return;
- end if;
-
if Target.Capacity < Length (Source) then
raise Constraint_Error with -- ???
"Source length exceeds Target capacity";
@@ -1312,14 +1287,11 @@ is
return False;
end if;
- if Left'Address = Right'Address then
- return True;
- end if;
-
Left_Node := First (Left).Node;
while Left_Node /= 0 loop
declare
- N : Node_Type renames Left_Nodes (Left_Node);
+ L : constant Count_Type := Left_Node;
+ N : Node_Type renames Left_Nodes (L);
E : Element_Type renames N.Element;
begin
if Find (Right, E).Node /= 0 then
@@ -1416,15 +1388,15 @@ is
-------------
procedure Process (Source_Node : Count_Type) is
- B : Boolean;
- N : Node_Type renames Source.Content.Nodes (Source_Node);
- X : Count_Type;
+ B : Boolean;
+ N : Node_Type renames Source.Content.Nodes (Source_Node);
+ Unused_X : Count_Type;
begin
if Is_In (Target, N) then
Delete (Target, N.Element);
else
- Insert (Target, N.Element, X, B);
+ Insert (Target, N.Element, Unused_X, B);
pragma Assert (B);
end if;
end Process;
@@ -1432,11 +1404,6 @@ is
-- Start of processing for Symmetric_Difference
begin
- if Target'Address = Source'Address then
- Clear (Target);
- return;
- end if;
-
if Length (Target) = 0 then
Assign (Target, Source);
return;
@@ -1446,14 +1413,7 @@ is
end Symmetric_Difference;
function Symmetric_Difference (Left : Set; Right : Set) return Set is
- C : Count_Type;
- H : Hash_Type;
-
begin
- if Left'Address = Right'Address then
- return Empty_Set;
- end if;
-
if Length (Right) = 0 then
return Copy (Left);
end if;
@@ -1462,13 +1422,15 @@ is
return Copy (Right);
end if;
- C := Length (Left) + Length (Right);
- H := Default_Modulus (C);
-
- return S : Set (C, H) do
- Difference (Left, Right, S);
- Difference (Right, Left, S);
- end return;
+ declare
+ C : constant Count_Type := Length (Left) + Length (Right);
+ H : constant Hash_Type := Default_Modulus (C);
+ begin
+ return S : Set (C, H) do
+ Difference (Left, Right, S);
+ Difference (Right, Left, S);
+ end return;
+ end;
end Symmetric_Difference;
------------
@@ -1476,12 +1438,12 @@ is
------------
function To_Set (New_Item : Element_Type) return Set is
- X : Count_Type;
- B : Boolean;
+ Unused_X : Count_Type;
+ B : Boolean;
begin
return S : Set (Capacity => 1, Modulus => 1) do
- Insert (S, New_Item, X, B);
+ Insert (S, New_Item, Unused_X, B);
pragma Assert (B);
end return;
end To_Set;
@@ -1504,32 +1466,21 @@ is
N : Node_Type renames Source.Content.Nodes (Src_Node);
E : Element_Type renames N.Element;
- X : Count_Type;
- B : Boolean;
+ Unused_X : Count_Type;
+ Unused_B : Boolean;
begin
- Insert (Target, E, X, B);
+ Insert (Target, E, Unused_X, Unused_B);
end Process;
-- Start of processing for Union
begin
- if Target'Address = Source'Address then
- return;
- end if;
-
Iterate (Source.Content);
end Union;
function Union (Left : Set; Right : Set) return Set is
- C : Count_Type;
- H : Hash_Type;
-
begin
- if Left'Address = Right'Address then
- return Copy (Left);
- end if;
-
if Length (Right) = 0 then
return Copy (Left);
end if;
@@ -1538,12 +1489,15 @@ is
return Copy (Right);
end if;
- C := Length (Left) + Length (Right);
- H := Default_Modulus (C);
- return S : Set (C, H) do
- Assign (Target => S, Source => Left);
- Union (Target => S, Source => Right);
- end return;
+ declare
+ C : constant Count_Type := Length (Left) + Length (Right);
+ H : constant Hash_Type := Default_Modulus (C);
+ begin
+ return S : Set (C, H) do
+ Assign (Target => S, Source => Left);
+ Union (Target => S, Source => Right);
+ end return;
+ end;
end Union;
---------
diff --git a/gcc/ada/libgnat/a-chtgfk.adb b/gcc/ada/libgnat/a-chtgfk.adb
index 57967f9883e..338eb352d9b 100644
--- a/gcc/ada/libgnat/a-chtgfk.adb
+++ b/gcc/ada/libgnat/a-chtgfk.adb
@@ -36,7 +36,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Keys is
-----------------------------
function Checked_Equivalent_Keys
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type;
Node : Count_Type) return Boolean
is
@@ -49,7 +49,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Keys is
-------------------
function Checked_Index
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type) return Hash_Type
is
begin
@@ -61,7 +61,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Keys is
--------------------------
procedure Delete_Key_Sans_Free
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Key : Key_Type;
X : out Count_Type)
is
@@ -108,7 +108,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Keys is
----------
function Find
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type) return Count_Type
is
Indx : Hash_Type;
@@ -119,13 +119,11 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Keys is
return 0;
end if;
- Indx := Checked_Index (HT'Unrestricted_Access.all, Key);
+ Indx := Checked_Index (HT, Key);
Node := HT.Buckets (Indx);
while Node /= 0 loop
- if Checked_Equivalent_Keys
- (HT'Unrestricted_Access.all, Key, Node)
- then
+ if Checked_Equivalent_Keys (HT, Key, Node) then
return Node;
end if;
Node := Next (HT.Nodes (Node));
@@ -139,7 +137,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Keys is
--------------------------------
procedure Generic_Conditional_Insert
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Key : Key_Type;
Node : out Count_Type;
Inserted : out Boolean)
@@ -155,7 +153,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Keys is
raise Capacity_Error with "no more capacity for insertion";
end if;
- Node := New_Node;
+ New_Node (HT, Node);
Set_Next (HT.Nodes (Node), Next => 0);
Inserted := True;
@@ -181,7 +179,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Keys is
raise Capacity_Error with "no more capacity for insertion";
end if;
- Node := New_Node;
+ New_Node (HT, Node);
Set_Next (HT.Nodes (Node), Next => HT.Buckets (Indx));
Inserted := True;
@@ -195,7 +193,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Keys is
-----------------------------
procedure Generic_Replace_Element
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Node : Count_Type;
Key : Key_Type)
is
@@ -307,7 +305,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Keys is
-----------
function Index
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type) return Hash_Type is
begin
return HT.Buckets'First + Hash (Key) mod HT.Buckets'Length;
diff --git a/gcc/ada/libgnat/a-chtgfk.ads b/gcc/ada/libgnat/a-chtgfk.ads
index 633887f5499..8a044871909 100644
--- a/gcc/ada/libgnat/a-chtgfk.ads
+++ b/gcc/ada/libgnat/a-chtgfk.ads
@@ -54,27 +54,27 @@ package Ada.Containers.Hash_Tables.Generic_Formal_Keys is
pragma Pure;
function Index
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type) return Hash_Type;
pragma Inline (Index);
-- Returns the bucket number (array index value) for the given key
function Checked_Index
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type) return Hash_Type;
pragma Inline (Checked_Index);
-- Calls Index, but also locks and unlocks the container, per AI05-0022, in
-- order to detect element tampering by the generic actual Hash function.
function Checked_Equivalent_Keys
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type;
Node : Count_Type) return Boolean;
-- Calls Equivalent_Keys, but locks and unlocks the container, per
-- AI05-0022, in order to detect element tampering by that generic actual.
procedure Delete_Key_Sans_Free
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Key : Key_Type;
X : out Count_Type);
-- Removes the node (if any) with the given key from the hash table,
@@ -82,14 +82,16 @@ package Ada.Containers.Hash_Tables.Generic_Formal_Keys is
-- table is busy.
function Find
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Key_Type) return Count_Type;
-- Returns the node (if any) corresponding to the given key
generic
- with function New_Node return Count_Type;
+ with procedure New_Node
+ (HT : in out Hash_Table_Type;
+ Node : out Count_Type);
procedure Generic_Conditional_Insert
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Key : Key_Type;
Node : out Count_Type;
Inserted : out Boolean);
@@ -103,7 +105,7 @@ package Ada.Containers.Hash_Tables.Generic_Formal_Keys is
with function Hash (Node : Node_Type) return Hash_Type;
with procedure Assign (Node : in out Node_Type; Key : Key_Type);
procedure Generic_Replace_Element
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Node : Count_Type;
Key : Key_Type);
-- Assigns Key to Node, possibly changing its equivalence class. If Node
diff --git a/gcc/ada/libgnat/a-chtgfo.adb b/gcc/ada/libgnat/a-chtgfo.adb
index 063537ea8ac..e35163df67f 100644
--- a/gcc/ada/libgnat/a-chtgfo.adb
+++ b/gcc/ada/libgnat/a-chtgfo.adb
@@ -38,7 +38,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Operations is
-------------------
function Checked_Index
- (Hash_Table : Hash_Table_Type'Class;
+ (Hash_Table : Hash_Table_Type;
Node : Count_Type) return Hash_Type
is
begin
@@ -49,7 +49,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Operations is
-- Clear --
-----------
- procedure Clear (HT : in out Hash_Table_Type'Class) is
+ procedure Clear (HT : in out Hash_Table_Type) is
begin
HT.Length := 0;
-- HT.Busy := 0;
@@ -63,7 +63,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Operations is
--------------------------
procedure Delete_Node_At_Index
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Indx : Hash_Type;
X : Count_Type)
is
@@ -106,7 +106,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Operations is
---------------------------
procedure Delete_Node_Sans_Free
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
X : Count_Type)
is
pragma Assert (X /= 0);
@@ -162,7 +162,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Operations is
-- First --
-----------
- function First (HT : Hash_Table_Type'Class) return Count_Type is
+ function First (HT : Hash_Table_Type) return Count_Type is
Indx : Hash_Type;
begin
@@ -185,7 +185,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Operations is
----------
procedure Free
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
X : Count_Type)
is
N : Nodes_Type renames HT.Nodes;
@@ -300,7 +300,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Operations is
----------------------
procedure Generic_Allocate
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Node : out Count_Type)
is
N : Nodes_Type renames HT.Nodes;
@@ -338,7 +338,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Operations is
-------------------
function Generic_Equal
- (L, R : Hash_Table_Type'Class) return Boolean
+ (L, R : Hash_Table_Type) return Boolean
is
L_Index : Hash_Type;
L_Node : Count_Type;
@@ -346,10 +346,6 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Operations is
N : Count_Type;
begin
- if L'Address = R'Address then
- return True;
- end if;
-
if L.Length /= R.Length then
return False;
end if;
@@ -403,7 +399,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Operations is
-- Generic_Iteration --
-----------------------
- procedure Generic_Iteration (HT : Hash_Table_Type'Class) is
+ procedure Generic_Iteration (HT : Hash_Table_Type) is
Node : Count_Type;
begin
@@ -426,7 +422,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Operations is
procedure Generic_Read
(Stream : not null access Root_Stream_Type'Class;
- HT : out Hash_Table_Type'Class)
+ HT : out Hash_Table_Type)
is
N : Count_Type'Base;
@@ -467,7 +463,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Operations is
procedure Generic_Write
(Stream : not null access Root_Stream_Type'Class;
- HT : Hash_Table_Type'Class)
+ HT : Hash_Table_Type)
is
procedure Write (Node : Count_Type);
pragma Inline (Write);
@@ -500,7 +496,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Operations is
end Index;
function Index
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Node : Node_Type) return Hash_Type is
begin
return Index (HT.Buckets, Node);
@@ -511,7 +507,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Operations is
----------
function Next
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Node : Count_Type) return Count_Type
is
Result : Count_Type;
@@ -527,7 +523,7 @@ package body Ada.Containers.Hash_Tables.Generic_Formal_Operations is
-- This was the last node in the bucket, so move to the next
-- bucket, and start searching for next node from there.
- First := Checked_Index (HT'Unrestricted_Access.all, Node) + 1;
+ First := Checked_Index (HT, Node) + 1;
for Indx in First .. HT.Buckets'Last loop
Result := HT.Buckets (Indx);
diff --git a/gcc/ada/libgnat/a-chtgfo.ads b/gcc/ada/libgnat/a-chtgfo.ads
index 4936c737c44..b20ef6961a5 100644
--- a/gcc/ada/libgnat/a-chtgfo.ads
+++ b/gcc/ada/libgnat/a-chtgfo.ads
@@ -56,36 +56,36 @@ package Ada.Containers.Hash_Tables.Generic_Formal_Operations is
-- Uses the hash value of Node to compute its Buckets array index
function Index
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Node : Node_Type) return Hash_Type;
pragma Inline (Index);
-- Uses the hash value of Node to compute its Hash_Table buckets array
-- index.
function Checked_Index
- (Hash_Table : Hash_Table_Type'Class;
+ (Hash_Table : Hash_Table_Type;
Node : Count_Type) return Hash_Type;
-- Calls Index, but also locks and unlocks the container, per AI05-0022, in
-- order to detect element tampering by the generic actual Hash function.
generic
with function Find
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Key : Node_Type) return Boolean;
- function Generic_Equal (L, R : Hash_Table_Type'Class) return Boolean;
+ function Generic_Equal (L, R : Hash_Table_Type) return Boolean;
-- Used to implement hashed container equality. For each node in hash table
-- L, it calls Find to search for an equivalent item in hash table R. If
-- Find returns False for any node then Generic_Equal terminates
-- immediately and returns False. Otherwise if Find returns True for every
-- node then Generic_Equal returns True.
- procedure Clear (HT : in out Hash_Table_Type'Class);
+ procedure Clear (HT : in out Hash_Table_Type);
-- Deallocates each node in hash table HT. (Note that it only deallocates
-- the nodes, not the buckets array.) Program_Error is raised if the hash
-- table is busy.
procedure Delete_Node_At_Index
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Indx : Hash_Type;
X : Count_Type);
-- Delete a node whose bucket position is known. extracted from following
@@ -95,31 +95,31 @@ package Ada.Containers.Hash_Tables.Generic_Formal_Operations is
-- not correspond to the hash code that determines its bucket.
procedure Delete_Node_Sans_Free
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
X : Count_Type);
-- Removes node X from the hash table without deallocating the node
generic
with procedure Set_Element (Node : in out Node_Type);
procedure Generic_Allocate
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
Node : out Count_Type);
-- Claim a node from the free store. Generic_Allocate first
-- calls Set_Element on the potential node, and then returns
-- the node's index as the value of the Node parameter.
procedure Free
- (HT : in out Hash_Table_Type'Class;
+ (HT : in out Hash_Table_Type;
X : Count_Type);
-- Return a node back to the free store, from where it had
-- been previously claimed via Generic_Allocate.
- function First (HT : Hash_Table_Type'Class) return Count_Type;
+ function First (HT : Hash_Table_Type) return Count_Type;
-- Returns the head of the list in the first (lowest-index) non-empty
-- bucket.
function Next
- (HT : Hash_Table_Type'Class;
+ (HT : Hash_Table_Type;
Node : Count_Type) return Count_Type;
-- Returns the node that immediately follows Node. This corresponds to
-- either the next node in the same bucket, or (if Node is the last node in
@@ -128,7 +128,7 @@ package Ada.Containers.Hash_Tables.Generic_Formal_Operations is
generic
with procedure Process (Node : Count_Type);
- procedure Generic_Iteration (HT : Hash_Table_Type'Class);
+ procedure Generic_Iteration (HT : Hash_Table_Type);
-- Calls Process for each node in hash table HT
generic
@@ -138,7 +138,7 @@ package Ada.Containers.Hash_Tables.Generic_Formal_Operations is
Node : Node_Type);
procedure Generic_Write
(Stream : not null access Root_Stream_Type'Class;
- HT : Hash_Table_Type'Class);
+ HT : Hash_Table_Type);
-- Used to implement the streaming attribute for hashed containers. It
-- calls Write for each node to write its value into Stream.
@@ -148,7 +148,7 @@ package Ada.Containers.Hash_Tables.Generic_Formal_Operations is
return Count_Type;
procedure Generic_Read
(Stream : not null access Root_Stream_Type'Class;
- HT : out Hash_Table_Type'Class);
+ HT : out Hash_Table_Type);
-- Used to implement the streaming attribute for hashed containers. It
-- first clears hash table HT, then populates the hash table by calling
-- New_Node for each item in Stream.
diff --git a/gcc/ada/libgnat/a-cohata.ads b/gcc/ada/libgnat/a-cohata.ads
index 2f035e37860..b9f775f7375 100644
--- a/gcc/ada/libgnat/a-cohata.ads
+++ b/gcc/ada/libgnat/a-cohata.ads
@@ -89,7 +89,7 @@ package Ada.Containers.Hash_Tables is
type Hash_Table_Type
(Capacity : Count_Type;
Modulus : Hash_Type) is
- tagged record
+ record
Length : Count_Type := 0;
Free : Count_Type'Base := -1;
Nodes : Nodes_Type (1 .. Capacity);
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-05-13 8:09 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-05-13 8:09 [gcc r13-404] [Ada] Adapt body of formal sets and maps for SPARK Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).