+2014-02-19 Matthew Heaney <heaney@adacore.com>
+
+ * a-chtgop.ads (Checked_Index): New operation.
+ (Next): Changed mode of hash table.
+ * a-chtgop.adb (Adjust, Delete_Node_Sans_Free): Detect tampering
+ (Generic_Read, Reserve_Capacity): Ditto.
+ (Generic_Equal): Detect tampering.
+ (Next): Changed mode of hash table, detect tampering.
+ * a-chtgke.ads (Checked_Index, Checked_Equivalent_Keys): New
+ operation.
+ (Find): Changed mode of hash table.
+ * a-chtgke.adb (Checked_Equivalent_Keys): New operation
+ (Delete_Key_Sans_Free, Generic_Conditional_Insert): Detect
+ tampering.
+ (Find): Changed mode of hash table, check for tampering.
+ (Generic_Replace_Element): Check for tampering.
+ * a-chtgbk.ads (Checked_Index, Checked_Equivalent_Keys): New operation.
+ * a-chtgbk.adb (Checked_Index, Checked_Equivalent_Keys): New
+ operation (Delete_Key_Sans_Free, Generic_Conditional_Insert):
+ Detect tampering.
+ (Find, Generic_Replace_Element): Check for tampering.
+ * a-chtgbo.ads (Checked_Index): New operation.
+ * a-chtgbo.adb (Checked_Index): New operation
+ (Delete_Node_Sans_Free, Generic_Equal): Detect tampering.
+ (Generic_Read, Next): Ditto.
+ * a-cohase.adb, a-cihase.adb (Is_In): Changed mode of hash
+ table (Difference, Intersection): Use variable view of
+ source, detect tampering (Find, Is_Subset, Overlap): Use
+ variable view of container (Symmetric_Difference, Union):
+ Detect tampering (Vet): Use Checked_Index to detect tampering
+ (Constant_Reference, Element, Find): Use variable view of
+ container.
+ (Update_Element_Preserving_Key): Detect tampering.
+ * a-cbhase.adb (Difference, Find, Is_In): Use variable view
+ of container.
+ (Is_Subset): Ditto.
+ (Equivalent_Sets, Overlap): Use Node's Next component.
+ (Vet): Use Checked_Index to detect tampering.
+ (Constant_Reference, Element, Find): Use variable view of container.
+ (Update_Element_Preserving_Key): Detect tampering.
+ * a-cohama.adb, a-cihama.adb, a-cbhama.adb (Constant_Reference,
+ Element, Find): Use variable view of container.
+ (Reference): Rename hash table component.
+ (Vet): Use Checked_Index to detect tampering.
+
+2014-02-19 Arnaud Charlet <charlet@adacore.com>
+
+ * adabkend.adb (Scan_Compiler_Arguments): Add missing handling
+ of -nostdinc.
+
+2014-02-19 Thomas Quinot <quinot@adacore.com>
+
+ * tbuild.adb (New_Occurrence_Of, New_Rerefence_To): Guard
+ against calls without Def_Id.
+
+2014-02-19 Claire Dross <dross@adacore.com>
+
+ * a-cfdlli.ads, a-cfhase.ads, a-cforma.ads, a-cfhama.ads, a-cforse.ads,
+ a-cofove.ads: Add global annotations to subprograms.
+
+2014-02-19 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_prag.adb (Analyze_Initial_Condition_In_Decl_Part): Remove
+ constants Errors, Pack_Id and Pack_Init. Remove variable Vars.
+ Initial_Condition no longer requires the presence of pragma
+ Initialized. Do not try to diagnose whether all variables mentioned in
+ pragma Initializes also appear in Initial_Condition.
+ (Collect_Variables): Removed.
+ (Match_Variable): Removed.
+ (Match_Variables): Removed.
+ (Report_Unused_Variables): Removed.
+
+2014-02-19 Thomas Quinot <quinot@adacore.com>
+
+ * gnat_rm.texi (pragma Stream_Convert): Minor rewording.
+
2014-02-19 Robert Dewar <dewar@adacore.com>
* sem_util.adb, sem_util.ads, prj-conf.adb, s-os_lib.adb: Minor
(Container : aliased Map;
Key : Key_Type) return Constant_Reference_Type
is
- Node : constant Count_Type := Key_Ops.Find (Container, Key);
+ Node : constant Count_Type :=
+ Key_Ops.Find (Container'Unrestricted_Access.all, Key);
begin
if Node = 0 then
-------------
function Element (Container : Map; Key : Key_Type) return Element_Type is
- Node : constant Count_Type := Key_Ops.Find (Container, Key);
+ Node : constant Count_Type :=
+ Key_Ops.Find (Container'Unrestricted_Access.all, Key);
begin
if Node = 0 then
----------
function Find (Container : Map; Key : Key_Type) return Cursor is
- Node : constant Count_Type := Key_Ops.Find (Container, Key);
+ Node : constant Count_Type :=
+ Key_Ops.Find (Container'Unrestricted_Access.all, Key);
begin
if Node = 0 then
return No_Element;
return False;
end if;
- X := M.Buckets (Key_Ops.Index (M, M.Nodes (Position.Node).Key));
+ X := M.Buckets (Key_Ops.Checked_Index
+ (M, M.Nodes (Position.Node).Key));
for J in 1 .. M.Length loop
if X = Position.Node then
is
Tgt_Node, Src_Node : Count_Type;
+ Src : Set renames Source'Unrestricted_Access.all;
+
TN : Nodes_Type renames Target.Nodes;
SN : Nodes_Type renames Source.Nodes;
HT_Ops.Free (Target, Tgt_Node);
end if;
- Src_Node := HT_Ops.Next (Source, Src_Node);
+ Src_Node := HT_Ops.Next (Src, Src_Node);
end loop;
else
return True;
end if;
- R_Node := HT_Ops.Next (R_HT, R_Node);
+ R_Node := Next (R_HT.Nodes (R_Node));
end loop;
end Find_Equivalent_Key;
pragma Assert (Vet (Left), "bad Left cursor in Equivalent_Elements");
pragma Assert (Vet (Right), "bad Right cursor in Equivalent_Elements");
+ -- AI05-0022 requires that a container implementation detect element
+ -- tampering by a generic actual subprogram. However, the following case
+ -- falls outside the scope of that AI. Randy Brukardt explained on the
+ -- ARG list on 2013/02/07 that:
+
+ -- (Begin Quote):
+ -- But for an operation like "<" [the ordered set analog of
+ -- Equivalent_Elements], there is no need to "dereference" a cursor
+ -- after the call to the generic formal parameter function, so nothing
+ -- bad could happen if tampering is undetected. And the operation can
+ -- safely return a result without a problem even if an element is
+ -- deleted from the container.
+ -- (End Quote).
+
declare
LN : Node_Type renames Left.Container.Nodes (Left.Node);
RN : Node_Type renames Right.Container.Nodes (Right.Node);
(Container : Set;
Item : Element_Type) return Cursor
is
- Node : constant Count_Type := Element_Keys.Find (Container, Item);
+ Node : constant Count_Type :=
+ Element_Keys.Find (Container'Unrestricted_Access.all, Item);
begin
return (if Node = 0 then No_Element
else Cursor'(Container'Unrestricted_Access, Node));
function Is_In (HT : Set; Key : Node_Type) return Boolean is
begin
- return Element_Keys.Find (HT, Key.Element) /= 0;
+ return Element_Keys.Find (HT'Unrestricted_Access.all, Key.Element) /= 0;
end Is_In;
---------------
if not Is_In (Of_Set, SN (Subset_Node)) then
return False;
end if;
- Subset_Node := HT_Ops.Next (Subset, Subset_Node);
+ Subset_Node := HT_Ops.Next
+ (Subset'Unrestricted_Access.all, Subset_Node);
end loop;
return True;
if Is_In (Right, Left.Nodes (Left_Node)) then
return True;
end if;
- Left_Node := HT_Ops.Next (Left, Left_Node);
+ Left_Node := HT_Ops.Next (Left'Unrestricted_Access.all, Left_Node);
end loop;
return False;
return False;
end if;
- X := S.Buckets (Element_Keys.Index (S, N (Position.Node).Element));
+ X := S.Buckets (Element_Keys.Checked_Index
+ (S, N (Position.Node).Element));
for J in 1 .. S.Length loop
if X = Position.Node then
(Container : aliased Set;
Key : Key_Type) return Constant_Reference_Type
is
- Node : constant Count_Type := Key_Keys.Find (Container, Key);
+ Node : constant Count_Type :=
+ Key_Keys.Find (Container'Unrestricted_Access.all, Key);
begin
if Node = 0 then
(Container : Set;
Key : Key_Type) return Element_Type
is
- Node : constant Count_Type := Key_Keys.Find (Container, Key);
+ Node : constant Count_Type :=
+ Key_Keys.Find (Container'Unrestricted_Access.all, Key);
begin
if Node = 0 then
- raise Constraint_Error with "key not in map"; -- ??? "set"
+ raise Constraint_Error with "key not in set";
end if;
return Container.Nodes (Node).Element;
(Container : Set;
Key : Key_Type) return Cursor
is
- Node : constant Count_Type := Key_Keys.Find (Container, Key);
+ Node : constant Count_Type :=
+ Key_Keys.Find (Container'Unrestricted_Access.all, Key);
begin
return (if Node = 0 then No_Element
else Cursor'(Container'Unrestricted_Access, Node));
(Vet (Position),
"bad cursor in Update_Element_Preserving_Key");
- -- Record bucket now, in case key is changed
-
- Indx := HT_Ops.Index (Container.Buckets, N (Position.Node));
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
declare
E : Element_Type renames N (Position.Node).Element;
B : Natural renames Container.Busy;
L : Natural renames Container.Lock;
+ Eq : Boolean;
+
begin
B := B + 1;
L := L + 1;
begin
+ -- Record bucket now, in case key is changed
+ Indx := HT_Ops.Index (Container.Buckets, N (Position.Node));
+
Process (E);
+
+ Eq := Equivalent_Keys (K, Key (E));
exception
when others =>
L := L - 1;
L := L - 1;
B := B - 1;
- if Equivalent_Keys (K, Key (E)) then
- pragma Assert (Hash (K) = Hash (E));
+ if Eq then
return;
end if;
end;
No_Element : constant Cursor;
- function "=" (Left, Right : List) return Boolean;
+ function "=" (Left, Right : List) return Boolean with
+ Global => null;
- function Length (Container : List) return Count_Type;
+ function Length (Container : List) return Count_Type with
+ Global => null;
- function Is_Empty (Container : List) return Boolean;
+ function Is_Empty (Container : List) return Boolean with
+ Global => null;
- procedure Clear (Container : in out List);
+ procedure Clear (Container : in out List) with
+ Global => null;
procedure Assign (Target : in out List; Source : List) with
- Pre => Target.Capacity >= Length (Source);
+ Global => null,
+ Pre => Target.Capacity >= Length (Source);
function Copy (Source : List; Capacity : Count_Type := 0) return List with
- Pre => Capacity = 0 or else Capacity >= Source.Capacity;
+ Global => null,
+ Pre => Capacity = 0 or else Capacity >= Source.Capacity;
function Element
(Container : List;
Position : Cursor) return Element_Type
with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
procedure Replace_Element
(Container : in out List;
Position : Cursor;
New_Item : Element_Type)
with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
procedure Move (Target : in out List; Source : in out List) with
- Pre => Target.Capacity >= Length (Source);
+ Global => null,
+ Pre => Target.Capacity >= Length (Source);
procedure Insert
(Container : in out List;
New_Item : Element_Type;
Count : Count_Type := 1)
with
- Pre => Length (Container) + Count <= Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element);
+ Global => null,
+ Pre => Length (Container) + Count <= Container.Capacity
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element);
procedure Insert
(Container : in out List;
Position : out Cursor;
Count : Count_Type := 1)
with
- Pre => Length (Container) + Count <= Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element);
+ Global => null,
+ Pre => Length (Container) + Count <= Container.Capacity
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element);
procedure Insert
(Container : in out List;
Position : out Cursor;
Count : Count_Type := 1)
with
- Pre => Length (Container) + Count <= Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element);
+ Global => null,
+ Pre => Length (Container) + Count <= Container.Capacity
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element);
procedure Prepend
(Container : in out List;
New_Item : Element_Type;
Count : Count_Type := 1)
with
- Pre => Length (Container) + Count <= Container.Capacity;
+ Global => null,
+ Pre => Length (Container) + Count <= Container.Capacity;
procedure Append
(Container : in out List;
New_Item : Element_Type;
Count : Count_Type := 1)
with
- Pre => Length (Container) + Count <= Container.Capacity;
+ Global => null,
+ Pre => Length (Container) + Count <= Container.Capacity;
procedure Delete
(Container : in out List;
Position : in out Cursor;
Count : Count_Type := 1)
with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
procedure Delete_First
(Container : in out List;
- Count : Count_Type := 1);
+ Count : Count_Type := 1)
+ with
+ Global => null;
procedure Delete_Last
(Container : in out List;
- Count : Count_Type := 1);
+ Count : Count_Type := 1)
+ with
+ Global => null;
- procedure Reverse_Elements (Container : in out List);
+ procedure Reverse_Elements (Container : in out List) with
+ Global => null;
procedure Swap
(Container : in out List;
I, J : Cursor)
with
- Pre => Has_Element (Container, I) and then Has_Element (Container, J);
+ Global => null,
+ Pre => Has_Element (Container, I) and then Has_Element (Container, J);
procedure Swap_Links
(Container : in out List;
I, J : Cursor)
with
- Pre => Has_Element (Container, I) and then Has_Element (Container, J);
+ Global => null,
+ Pre => Has_Element (Container, I) and then Has_Element (Container, J);
procedure Splice
(Target : in out List;
Before : Cursor;
Source : in out List)
with
- Pre => Length (Source) + Length (Target) <= Target.Capacity
- and then (Has_Element (Target, Before)
- or else Before = No_Element);
+ Global => null,
+ Pre => Length (Source) + Length (Target) <= Target.Capacity
+ and then (Has_Element (Target, Before)
+ or else Before = No_Element);
procedure Splice
(Target : in out List;
Source : in out List;
Position : in out Cursor)
with
- Pre => Length (Source) + Length (Target) <= Target.Capacity
- and then (Has_Element (Target, Before)
- or else Before = No_Element)
- and then Has_Element (Source, Position);
+ Global => null,
+ Pre => Length (Source) + Length (Target) <= Target.Capacity
+ and then (Has_Element (Target, Before)
+ or else Before = No_Element)
+ and then Has_Element (Source, Position);
procedure Splice
(Container : in out List;
Before : Cursor;
Position : Cursor)
with
- Pre => 2 * Length (Container) <= Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element)
- and then Has_Element (Container, Position);
+ Global => null,
+ Pre => 2 * Length (Container) <= Container.Capacity
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element)
+ and then Has_Element (Container, Position);
- function First (Container : List) return Cursor;
+ function First (Container : List) return Cursor with
+ Global => null;
function First_Element (Container : List) return Element_Type with
- Pre => not Is_Empty (Container);
+ Global => null,
+ Pre => not Is_Empty (Container);
- function Last (Container : List) return Cursor;
+ function Last (Container : List) return Cursor with
+ Global => null;
function Last_Element (Container : List) return Element_Type with
- Pre => not Is_Empty (Container);
+ Global => null,
+ Pre => not Is_Empty (Container);
function Next (Container : List; Position : Cursor) return Cursor with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
procedure Next (Container : List; Position : in out Cursor) with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Previous (Container : List; Position : Cursor) return Cursor with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
procedure Previous (Container : List; Position : in out Cursor) with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Find
(Container : List;
Item : Element_Type;
Position : Cursor := No_Element) return Cursor
with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Reverse_Find
(Container : List;
Item : Element_Type;
Position : Cursor := No_Element) return Cursor
with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Contains
(Container : List;
- Item : Element_Type) return Boolean;
+ Item : Element_Type) return Boolean
+ with
+ Global => null;
- function Has_Element (Container : List; Position : Cursor) return Boolean;
+ function Has_Element (Container : List; Position : Cursor) return Boolean
+ with
+ Global => null;
generic
with function "<" (Left, Right : Element_Type) return Boolean is <>;
package Generic_Sorting is
- function Is_Sorted (Container : List) return Boolean;
+ function Is_Sorted (Container : List) return Boolean with
+ Global => null;
- procedure Sort (Container : in out List);
+ procedure Sort (Container : in out List) with
+ Global => null;
- procedure Merge (Target, Source : in out List);
+ procedure Merge (Target, Source : in out List) with
+ Global => null;
end Generic_Sorting;
- function Strict_Equal (Left, Right : List) return Boolean;
+ function Strict_Equal (Left, Right : List) return Boolean with
+ Global => null;
-- Strict_Equal returns True if the containers are physically equal, i.e.
-- they are structurally equal (function "=" returns True) and that they
-- have the same set of cursors.
function Left (Container : List; Position : Cursor) return List with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Right (Container : List; Position : Cursor) return List with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
-- Left returns a container containing all elements preceding Position
-- (excluded) in Container. Right returns a container containing all
-- elements following Position (included) in Container. These two new
No_Element : constant Cursor;
- function "=" (Left, Right : Map) return Boolean;
+ function "=" (Left, Right : Map) return Boolean with
+ Global => null;
- function Capacity (Container : Map) return Count_Type;
+ function Capacity (Container : Map) return Count_Type with
+ Global => null;
procedure Reserve_Capacity
(Container : in out Map;
Capacity : Count_Type)
with
- Pre => Capacity <= Container.Capacity;
+ Global => null,
+ Pre => Capacity <= Container.Capacity;
- function Length (Container : Map) return Count_Type;
+ function Length (Container : Map) return Count_Type with
+ Global => null;
- function Is_Empty (Container : Map) return Boolean;
+ function Is_Empty (Container : Map) return Boolean with
+ Global => null;
- procedure Clear (Container : in out Map);
+ procedure Clear (Container : in out Map) with
+ Global => null;
procedure Assign (Target : in out Map; Source : Map) with
- Pre => Target.Capacity >= Length (Source);
+ Global => null,
+ Pre => Target.Capacity >= Length (Source);
function Copy
(Source : Map;
Capacity : Count_Type := 0) return Map
with
- Pre => Capacity = 0 or else Capacity >= Source.Capacity;
+ Global => null,
+ Pre => Capacity = 0 or else Capacity >= Source.Capacity;
-- Copy returns a container stricty equal to Source. It must have
-- the same cursors associated with each element. Therefore:
-- - capacity=0 means use container.capacity as capacity of target
-- - the modulus cannot be changed.
function Key (Container : Map; Position : Cursor) return Key_Type with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
function Element
(Container : Map;
Position : Cursor) return Element_Type
with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
procedure Replace_Element
(Container : in out Map;
Position : Cursor;
New_Item : Element_Type)
with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
procedure Move (Target : in out Map; Source : in out Map) with
- Pre => Target.Capacity >= Length (Source);
+ Global => null,
+ Pre => Target.Capacity >= Length (Source);
procedure Insert
(Container : in out Map;
Position : out Cursor;
Inserted : out Boolean)
with
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre => Length (Container) < Container.Capacity;
procedure Insert
(Container : in out Map;
Key : Key_Type;
New_Item : Element_Type)
with
- Pre => Length (Container) < Container.Capacity
- and then (not Contains (Container, Key));
+ Global => null,
+ Pre => Length (Container) < Container.Capacity
+ and then (not Contains (Container, Key));
procedure Include
(Container : in out Map;
Key : Key_Type;
New_Item : Element_Type)
with
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre => Length (Container) < Container.Capacity;
procedure Replace
(Container : in out Map;
Key : Key_Type;
New_Item : Element_Type)
with
- Pre => Contains (Container, Key);
+ Global => null,
+ Pre => Contains (Container, Key);
- procedure Exclude (Container : in out Map; Key : Key_Type);
+ procedure Exclude (Container : in out Map; Key : Key_Type) with
+ Global => null;
procedure Delete (Container : in out Map; Key : Key_Type) with
- Pre => Contains (Container, Key);
+ Global => null,
+ Pre => Contains (Container, Key);
procedure Delete (Container : in out Map; Position : in out Cursor) with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
- function First (Container : Map) return Cursor;
+ function First (Container : Map) return Cursor with
+ Global => null;
function Next (Container : Map; Position : Cursor) return Cursor with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
procedure Next (Container : Map; Position : in out Cursor) with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
- function Find (Container : Map; Key : Key_Type) return Cursor;
+ function Find (Container : Map; Key : Key_Type) return Cursor with
+ Global => null;
- function Contains (Container : Map; Key : Key_Type) return Boolean;
+ function Contains (Container : Map; Key : Key_Type) return Boolean with
+ Global => null;
function Element (Container : Map; Key : Key_Type) return Element_Type with
- Pre => Contains (Container, Key);
+ Global => null,
+ Pre => Contains (Container, Key);
- function Has_Element (Container : Map; Position : Cursor) return Boolean;
+ function Has_Element (Container : Map; Position : Cursor) return Boolean
+ with
+ Global => null;
function Equivalent_Keys
(Left : Map;
CLeft : Cursor;
Right : Map;
- CRight : Cursor) return Boolean;
+ CRight : Cursor) return Boolean
+ with
+ Global => null;
function Equivalent_Keys
(Left : Map;
CLeft : Cursor;
- Right : Key_Type) return Boolean;
+ Right : Key_Type) return Boolean
+ with
+ Global => null;
function Equivalent_Keys
(Left : Key_Type;
Right : Map;
- CRight : Cursor) return Boolean;
+ CRight : Cursor) return Boolean
+ with
+ Global => null;
- function Default_Modulus (Capacity : Count_Type) return Hash_Type;
+ function Default_Modulus (Capacity : Count_Type) return Hash_Type with
+ Global => null;
- function Strict_Equal (Left, Right : Map) return Boolean;
+ function Strict_Equal (Left, Right : Map) return Boolean with
+ Global => null;
-- Strict_Equal returns True if the containers are physically equal, i.e.
-- they are structurally equal (function "=" returns True) and that they
-- have the same set of cursors.
function Left (Container : Map; Position : Cursor) return Map with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Right (Container : Map; Position : Cursor) return Map with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
-- Left returns a container containing all elements preceding Position
-- (excluded) in Container. Right returns a container containing all
-- elements following Position (included) in Container. These two new
-- iterate over containers. Left returns the part of the container already
-- scanned and Right the part not scanned yet.
- function Overlap (Left, Right : Map) return Boolean;
+ function Overlap (Left, Right : Map) return Boolean with
+ Global => null;
-- Overlap returns True if the containers have common keys
private
No_Element : constant Cursor;
- function "=" (Left, Right : Set) return Boolean;
+ function "=" (Left, Right : Set) return Boolean with
+ Global => null;
- function Equivalent_Sets (Left, Right : Set) return Boolean;
+ function Equivalent_Sets (Left, Right : Set) return Boolean with
+ Global => null;
- function To_Set (New_Item : Element_Type) return Set;
+ function To_Set (New_Item : Element_Type) return Set with
+ Global => null;
- function Capacity (Container : Set) return Count_Type;
+ function Capacity (Container : Set) return Count_Type with
+ Global => null;
procedure Reserve_Capacity
(Container : in out Set;
Capacity : Count_Type)
with
- Pre => Capacity <= Container.Capacity;
+ Global => null,
+ Pre => Capacity <= Container.Capacity;
- function Length (Container : Set) return Count_Type;
+ function Length (Container : Set) return Count_Type with
+ Global => null;
- function Is_Empty (Container : Set) return Boolean;
+ function Is_Empty (Container : Set) return Boolean with
+ Global => null;
- procedure Clear (Container : in out Set);
+ procedure Clear (Container : in out Set) with
+ Global => null;
procedure Assign (Target : in out Set; Source : Set) with
- Pre => Target.Capacity >= Length (Source);
+ Global => null,
+ Pre => Target.Capacity >= Length (Source);
function Copy
(Source : Set;
Capacity : Count_Type := 0) return Set
with
- Pre => Capacity = 0 or else Capacity >= Source.Capacity;
+ Global => null,
+ Pre => Capacity = 0 or else Capacity >= Source.Capacity;
function Element
(Container : Set;
Position : Cursor) return Element_Type
with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
procedure Replace_Element
(Container : in out Set;
Position : Cursor;
New_Item : Element_Type)
with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
procedure Move (Target : in out Set; Source : in out Set) with
- Pre => Target.Capacity >= Length (Source);
+ Global => null,
+ Pre => Target.Capacity >= Length (Source);
procedure Insert
(Container : in out Set;
Position : out Cursor;
Inserted : out Boolean)
with
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre => Length (Container) < Container.Capacity;
procedure Insert (Container : in out Set; New_Item : Element_Type) with
- Pre => Length (Container) < Container.Capacity
- and then (not Contains (Container, New_Item));
+ Global => null,
+ Pre => Length (Container) < Container.Capacity
+ and then (not Contains (Container, New_Item));
procedure Include (Container : in out Set; New_Item : Element_Type) with
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre => Length (Container) < Container.Capacity;
procedure Replace (Container : in out Set; New_Item : Element_Type) with
- Pre => Contains (Container, New_Item);
+ Global => null,
+ Pre => Contains (Container, New_Item);
- procedure Exclude (Container : in out Set; Item : Element_Type);
+ procedure Exclude (Container : in out Set; Item : Element_Type) with
+ Global => null;
procedure Delete (Container : in out Set; Item : Element_Type) with
- Pre => Contains (Container, Item);
+ Global => null,
+ Pre => Contains (Container, Item);
procedure Delete (Container : in out Set; Position : in out Cursor) with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
procedure Union (Target : in out Set; Source : Set) with
- Pre => Length (Target) + Length (Source) -
- Length (Intersection (Target, Source)) <= Target.Capacity;
+ Global => null,
+ Pre => Length (Target) + Length (Source) -
+ Length (Intersection (Target, Source)) <= Target.Capacity;
- function Union (Left, Right : Set) return Set;
+ function Union (Left, Right : Set) return Set with
+ Global => null,
+ Pre => Length (Left) + Length (Right) -
+ Length (Intersection (Left, Right)) <= Count_Type'Last;
function "or" (Left, Right : Set) return Set renames Union;
- procedure Intersection (Target : in out Set; Source : Set);
+ procedure Intersection (Target : in out Set; Source : Set) with
+ Global => null;
- function Intersection (Left, Right : Set) return Set;
+ function Intersection (Left, Right : Set) return Set with
+ Global => null;
function "and" (Left, Right : Set) return Set renames Intersection;
- procedure Difference (Target : in out Set; Source : Set);
+ procedure Difference (Target : in out Set; Source : Set) with
+ Global => null;
- function Difference (Left, Right : Set) return Set;
+ function Difference (Left, Right : Set) return Set with
+ Global => null;
function "-" (Left, Right : Set) return Set renames Difference;
- procedure Symmetric_Difference (Target : in out Set; Source : Set);
+ procedure Symmetric_Difference (Target : in out Set; Source : Set) with
+ Global => null,
+ Pre => Length (Target) + Length (Source) -
+ 2 * Length (Intersection (Target, Source)) <= Target.Capacity;
- function Symmetric_Difference (Left, Right : Set) return Set;
+ function Symmetric_Difference (Left, Right : Set) return Set with
+ Global => null,
+ Pre => Length (Left) + Length (Right) -
+ 2 * Length (Intersection (Left, Right)) <= Count_Type'Last;
function "xor" (Left, Right : Set) return Set
renames Symmetric_Difference;
- function Overlap (Left, Right : Set) return Boolean;
+ function Overlap (Left, Right : Set) return Boolean with
+ Global => null;
- function Is_Subset (Subset : Set; Of_Set : Set) return Boolean;
+ function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with
+ Global => null;
- function First (Container : Set) return Cursor;
+ function First (Container : Set) return Cursor with
+ Global => null;
function Next (Container : Set; Position : Cursor) return Cursor with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
procedure Next (Container : Set; Position : in out Cursor) with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Find
(Container : Set;
- Item : Element_Type) return Cursor;
+ Item : Element_Type) return Cursor
+ with
+ Global => null;
- function Contains (Container : Set; Item : Element_Type) return Boolean;
+ function Contains (Container : Set; Item : Element_Type) return Boolean with
+ Global => null;
- function Has_Element (Container : Set; Position : Cursor) return Boolean;
+ function Has_Element (Container : Set; Position : Cursor) return Boolean
+ with
+ Global => null;
function Equivalent_Elements (Left : Set; CLeft : Cursor;
- Right : Set; CRight : Cursor) return Boolean;
+ Right : Set; CRight : Cursor) return Boolean
+ with
+ Global => null;
function Equivalent_Elements
(Left : Set; CLeft : Cursor;
- Right : Element_Type) return Boolean;
+ Right : Element_Type) return Boolean
+ with
+ Global => null;
function Equivalent_Elements
(Left : Element_Type;
- Right : Set; CRight : Cursor) return Boolean;
+ Right : Set; CRight : Cursor) return Boolean
+ with
+ Global => null;
- function Default_Modulus (Capacity : Count_Type) return Hash_Type;
+ function Default_Modulus (Capacity : Count_Type) return Hash_Type with
+ Global => null;
generic
type Key_Type (<>) is private;
package Generic_Keys is
- function Key (Container : Set; Position : Cursor) return Key_Type;
+ function Key (Container : Set; Position : Cursor) return Key_Type with
+ Global => null;
- function Element (Container : Set; Key : Key_Type) return Element_Type;
+ function Element (Container : Set; Key : Key_Type) return Element_Type
+ with
+ Global => null;
procedure Replace
(Container : in out Set;
Key : Key_Type;
- New_Item : Element_Type);
+ New_Item : Element_Type)
+ with
+ Global => null;
- procedure Exclude (Container : in out Set; Key : Key_Type);
+ procedure Exclude (Container : in out Set; Key : Key_Type) with
+ Global => null;
- procedure Delete (Container : in out Set; Key : Key_Type);
+ procedure Delete (Container : in out Set; Key : Key_Type) with
+ Global => null;
- function Find (Container : Set; Key : Key_Type) return Cursor;
+ function Find (Container : Set; Key : Key_Type) return Cursor with
+ Global => null;
- function Contains (Container : Set; Key : Key_Type) return Boolean;
+ function Contains (Container : Set; Key : Key_Type) return Boolean with
+ Global => null;
end Generic_Keys;
- function Strict_Equal (Left, Right : Set) return Boolean;
+ function Strict_Equal (Left, Right : Set) return Boolean with
+ Global => null;
-- Strict_Equal returns True if the containers are physically equal, i.e.
-- they are structurally equal (function "=" returns True) and that they
-- have the same set of cursors.
function Left (Container : Set; Position : Cursor) return Set with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Right (Container : Set; Position : Cursor) return Set with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
-- Left returns a container containing all elements preceding Position
-- (excluded) in Container. Right returns a container containing all
-- elements following Position (included) in Container. These two new
pragma Annotate (GNATprove, External_Axiomatization);
pragma Pure;
- function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
+ function Equivalent_Keys (Left, Right : Key_Type) return Boolean with
+ Global => null;
type Map (Capacity : Count_Type) is private with
Iterable => (First => First,
No_Element : constant Cursor;
- function "=" (Left, Right : Map) return Boolean;
+ function "=" (Left, Right : Map) return Boolean with
+ Global => null;
- function Length (Container : Map) return Count_Type;
+ function Length (Container : Map) return Count_Type with
+ Global => null;
- function Is_Empty (Container : Map) return Boolean;
+ function Is_Empty (Container : Map) return Boolean with
+ Global => null;
- procedure Clear (Container : in out Map);
+ procedure Clear (Container : in out Map) with
+ Global => null;
procedure Assign (Target : in out Map; Source : Map) with
- Pre => Target.Capacity >= Length (Source);
+ Global => null,
+ Pre => Target.Capacity >= Length (Source);
function Copy (Source : Map; Capacity : Count_Type := 0) return Map with
- Pre => Capacity = 0 or else Capacity >= Source.Capacity;
+ Global => null,
+ Pre => Capacity = 0 or else Capacity >= Source.Capacity;
function Key (Container : Map; Position : Cursor) return Key_Type with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
function Element
(Container : Map;
Position : Cursor) return Element_Type
with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
procedure Replace_Element
(Container : in out Map;
Position : Cursor;
New_Item : Element_Type)
with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
procedure Move (Target : in out Map; Source : in out Map) with
- Pre => Target.Capacity >= Length (Source);
+ Global => null,
+ Pre => Target.Capacity >= Length (Source);
procedure Insert
(Container : in out Map;
Position : out Cursor;
Inserted : out Boolean)
with
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre => Length (Container) < Container.Capacity;
procedure Insert
(Container : in out Map;
Key : Key_Type;
New_Item : Element_Type)
with
- Pre => Length (Container) < Container.Capacity
- and then (not Contains (Container, Key));
+ Global => null,
+ Pre => Length (Container) < Container.Capacity
+ and then (not Contains (Container, Key));
procedure Include
(Container : in out Map;
Key : Key_Type;
New_Item : Element_Type)
with
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre => Length (Container) < Container.Capacity;
procedure Replace
(Container : in out Map;
Key : Key_Type;
New_Item : Element_Type)
with
- Pre => Contains (Container, Key);
+ Global => null,
+ Pre => Contains (Container, Key);
- procedure Exclude (Container : in out Map; Key : Key_Type);
+ procedure Exclude (Container : in out Map; Key : Key_Type) with
+ Global => null;
procedure Delete (Container : in out Map; Key : Key_Type) with
- Pre => Contains (Container, Key);
+ Global => null,
+ Pre => Contains (Container, Key);
procedure Delete (Container : in out Map; Position : in out Cursor) with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
- procedure Delete_First (Container : in out Map);
+ procedure Delete_First (Container : in out Map) with
+ Global => null;
- procedure Delete_Last (Container : in out Map);
+ procedure Delete_Last (Container : in out Map) with
+ Global => null;
- function First (Container : Map) return Cursor;
+ function First (Container : Map) return Cursor with
+ Global => null;
function First_Element (Container : Map) return Element_Type with
- Pre => not Is_Empty (Container);
+ Global => null,
+ Pre => not Is_Empty (Container);
function First_Key (Container : Map) return Key_Type with
- Pre => not Is_Empty (Container);
+ Global => null,
+ Pre => not Is_Empty (Container);
- function Last (Container : Map) return Cursor;
+ function Last (Container : Map) return Cursor with
+ Global => null;
function Last_Element (Container : Map) return Element_Type with
- Pre => not Is_Empty (Container);
+ Global => null,
+ Pre => not Is_Empty (Container);
function Last_Key (Container : Map) return Key_Type with
- Pre => not Is_Empty (Container);
+ Global => null,
+ Pre => not Is_Empty (Container);
function Next (Container : Map; Position : Cursor) return Cursor with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
procedure Next (Container : Map; Position : in out Cursor) with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Previous (Container : Map; Position : Cursor) return Cursor with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
procedure Previous (Container : Map; Position : in out Cursor) with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
- function Find (Container : Map; Key : Key_Type) return Cursor;
+ function Find (Container : Map; Key : Key_Type) return Cursor with
+ Global => null;
function Element (Container : Map; Key : Key_Type) return Element_Type with
- Pre => Contains (Container, Key);
+ Global => null,
+ Pre => Contains (Container, Key);
- function Floor (Container : Map; Key : Key_Type) return Cursor;
+ function Floor (Container : Map; Key : Key_Type) return Cursor with
+ Global => null;
- function Ceiling (Container : Map; Key : Key_Type) return Cursor;
+ function Ceiling (Container : Map; Key : Key_Type) return Cursor with
+ Global => null;
- function Contains (Container : Map; Key : Key_Type) return Boolean;
+ function Contains (Container : Map; Key : Key_Type) return Boolean with
+ Global => null;
- function Has_Element (Container : Map; Position : Cursor) return Boolean;
+ function Has_Element (Container : Map; Position : Cursor) return Boolean
+ with
+ Global => null;
- function Strict_Equal (Left, Right : Map) return Boolean;
+ function Strict_Equal (Left, Right : Map) return Boolean with
+ Global => null;
-- Strict_Equal returns True if the containers are physically equal, i.e.
-- they are structurally equal (function "=" returns True) and that they
-- have the same set of cursors.
function Left (Container : Map; Position : Cursor) return Map with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Right (Container : Map; Position : Cursor) return Map with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
-- Left returns a container containing all elements preceding Position
-- (excluded) in Container. Right returns a container containing all
-- elements following Position (included) in Container. These two new
-- iterate over containers. Left returns the part of the container already
-- scanned and Right the part not scanned yet.
- function Overlap (Left, Right : Map) return Boolean;
+ function Overlap (Left, Right : Map) return Boolean with
+ Global => null;
-- Overlap returns True if the containers have common keys
private
pragma Annotate (GNATprove, External_Axiomatization);
pragma Pure;
- function Equivalent_Elements (Left, Right : Element_Type) return Boolean;
+ function Equivalent_Elements (Left, Right : Element_Type) return Boolean
+ with
+ Global => null;
type Set (Capacity : Count_Type) is private with
Iterable => (First => First,
No_Element : constant Cursor;
- function "=" (Left, Right : Set) return Boolean;
+ function "=" (Left, Right : Set) return Boolean with
+ Global => null;
- function Equivalent_Sets (Left, Right : Set) return Boolean;
+ function Equivalent_Sets (Left, Right : Set) return Boolean with
+ Global => null;
- function To_Set (New_Item : Element_Type) return Set;
+ function To_Set (New_Item : Element_Type) return Set with
+ Global => null;
- function Length (Container : Set) return Count_Type;
+ function Length (Container : Set) return Count_Type with
+ Global => null;
- function Is_Empty (Container : Set) return Boolean;
+ function Is_Empty (Container : Set) return Boolean with
+ Global => null;
- procedure Clear (Container : in out Set);
+ procedure Clear (Container : in out Set) with
+ Global => null;
procedure Assign (Target : in out Set; Source : Set) with
Pre => Target.Capacity >= Length (Source);
function Copy (Source : Set; Capacity : Count_Type := 0) return Set with
- Pre => Capacity = 0 or else Capacity >= Source.Capacity;
+ Global => null,
+ Pre => Capacity = 0 or else Capacity >= Source.Capacity;
function Element
(Container : Set;
Position : Cursor) return Element_Type
with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
procedure Replace_Element
(Container : in out Set;
Position : Cursor;
New_Item : Element_Type)
with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
procedure Move (Target : in out Set; Source : in out Set) with
- Pre => Target.Capacity >= Length (Source);
+ Global => null,
+ Pre => Target.Capacity >= Length (Source);
procedure Insert
(Container : in out Set;
Position : out Cursor;
Inserted : out Boolean)
with
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre => Length (Container) < Container.Capacity;
procedure Insert
(Container : in out Set;
New_Item : Element_Type)
with
- Pre => Length (Container) < Container.Capacity
- and then (not Contains (Container, New_Item));
+ Global => null,
+ Pre => Length (Container) < Container.Capacity
+ and then (not Contains (Container, New_Item));
procedure Include
(Container : in out Set;
New_Item : Element_Type)
with
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre => Length (Container) < Container.Capacity;
procedure Replace
(Container : in out Set;
New_Item : Element_Type)
with
- Pre => Contains (Container, New_Item);
+ Global => null,
+ Pre => Contains (Container, New_Item);
procedure Exclude
(Container : in out Set;
- Item : Element_Type);
+ Item : Element_Type)
+ with
+ Global => null;
procedure Delete
(Container : in out Set;
Item : Element_Type)
with
- Pre => Contains (Container, Item);
+ Global => null,
+ Pre => Contains (Container, Item);
procedure Delete
(Container : in out Set;
Position : in out Cursor)
with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
- procedure Delete_First (Container : in out Set);
+ procedure Delete_First (Container : in out Set) with
+ Global => null;
- procedure Delete_Last (Container : in out Set);
+ procedure Delete_Last (Container : in out Set) with
+ Global => null;
procedure Union (Target : in out Set; Source : Set) with
- Pre => Length (Target) + Length (Source) -
- Length (Intersection (Target, Source)) <= Target.Capacity;
+ Global => null,
+ Pre => Length (Target) + Length (Source) -
+ Length (Intersection (Target, Source)) <= Target.Capacity;
- function Union (Left, Right : Set) return Set;
+ function Union (Left, Right : Set) return Set with
+ Global => null,
+ Pre => Length (Left) + Length (Right) -
+ Length (Intersection (Left, Right)) <= Count_Type'Last;
function "or" (Left, Right : Set) return Set renames Union;
- procedure Intersection (Target : in out Set; Source : Set);
+ procedure Intersection (Target : in out Set; Source : Set) with
+ Global => null;
- function Intersection (Left, Right : Set) return Set;
+ function Intersection (Left, Right : Set) return Set with
+ Global => null;
function "and" (Left, Right : Set) return Set renames Intersection;
- procedure Difference (Target : in out Set; Source : Set);
+ procedure Difference (Target : in out Set; Source : Set) with
+ Global => null;
- function Difference (Left, Right : Set) return Set;
+ function Difference (Left, Right : Set) return Set with
+ Global => null;
function "-" (Left, Right : Set) return Set renames Difference;
- procedure Symmetric_Difference (Target : in out Set; Source : Set);
+ procedure Symmetric_Difference (Target : in out Set; Source : Set) with
+ Global => null,
+ Pre => Length (Target) + Length (Source) -
+ 2 * Length (Intersection (Target, Source)) <= Target.Capacity;
- function Symmetric_Difference (Left, Right : Set) return Set;
+ function Symmetric_Difference (Left, Right : Set) return Set with
+ Global => null,
+ Pre => Length (Left) + Length (Right) -
+ 2 * Length (Intersection (Left, Right)) <= Count_Type'Last;
function "xor" (Left, Right : Set) return Set renames Symmetric_Difference;
- function Overlap (Left, Right : Set) return Boolean;
+ function Overlap (Left, Right : Set) return Boolean with
+ Global => null;
- function Is_Subset (Subset : Set; Of_Set : Set) return Boolean;
+ function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with
+ Global => null;
- function First (Container : Set) return Cursor;
+ function First (Container : Set) return Cursor with
+ Global => null;
function First_Element (Container : Set) return Element_Type with
- Pre => not Is_Empty (Container);
+ Global => null,
+ Pre => not Is_Empty (Container);
function Last (Container : Set) return Cursor;
function Last_Element (Container : Set) return Element_Type with
- Pre => not Is_Empty (Container);
+ Global => null,
+ Pre => not Is_Empty (Container);
function Next (Container : Set; Position : Cursor) return Cursor with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
procedure Next (Container : Set; Position : in out Cursor) with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Previous (Container : Set; Position : Cursor) return Cursor with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
procedure Previous (Container : Set; Position : in out Cursor) with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
- function Find (Container : Set; Item : Element_Type) return Cursor;
+ function Find (Container : Set; Item : Element_Type) return Cursor with
+ Global => null;
- function Floor (Container : Set; Item : Element_Type) return Cursor;
+ function Floor (Container : Set; Item : Element_Type) return Cursor with
+ Global => null;
- function Ceiling (Container : Set; Item : Element_Type) return Cursor;
+ function Ceiling (Container : Set; Item : Element_Type) return Cursor with
+ Global => null;
- function Contains (Container : Set; Item : Element_Type) return Boolean;
+ function Contains (Container : Set; Item : Element_Type) return Boolean with
+ Global => null;
- function Has_Element (Container : Set; Position : Cursor) return Boolean;
+ function Has_Element (Container : Set; Position : Cursor) return Boolean
+ with
+ Global => null;
generic
type Key_Type (<>) is private;
package Generic_Keys is
- function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
+ function Equivalent_Keys (Left, Right : Key_Type) return Boolean with
+ Global => null;
- function Key (Container : Set; Position : Cursor) return Key_Type;
+ function Key (Container : Set; Position : Cursor) return Key_Type with
+ Global => null;
- function Element (Container : Set; Key : Key_Type) return Element_Type;
+ function Element (Container : Set; Key : Key_Type) return Element_Type
+ with
+ Global => null;
procedure Replace
(Container : in out Set;
Key : Key_Type;
- New_Item : Element_Type);
+ New_Item : Element_Type)
+ with
+ Global => null;
- procedure Exclude (Container : in out Set; Key : Key_Type);
+ procedure Exclude (Container : in out Set; Key : Key_Type) with
+ Global => null;
- procedure Delete (Container : in out Set; Key : Key_Type);
+ procedure Delete (Container : in out Set; Key : Key_Type) with
+ Global => null;
- function Find (Container : Set; Key : Key_Type) return Cursor;
+ function Find (Container : Set; Key : Key_Type) return Cursor with
+ Global => null;
- function Floor (Container : Set; Key : Key_Type) return Cursor;
+ function Floor (Container : Set; Key : Key_Type) return Cursor with
+ Global => null;
- function Ceiling (Container : Set; Key : Key_Type) return Cursor;
+ function Ceiling (Container : Set; Key : Key_Type) return Cursor with
+ Global => null;
- function Contains (Container : Set; Key : Key_Type) return Boolean;
+ function Contains (Container : Set; Key : Key_Type) return Boolean with
+ Global => null;
end Generic_Keys;
- function Strict_Equal (Left, Right : Set) return Boolean;
+ function Strict_Equal (Left, Right : Set) return Boolean with
+ Global => null;
-- Strict_Equal returns True if the containers are physically equal, i.e.
-- they are structurally equal (function "=" returns True) and that they
-- have the same set of cursors.
function Left (Container : Set; Position : Cursor) return Set with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Right (Container : Set; Position : Cursor) return Set with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
-- Left returns a container containing all elements preceding Position
-- (excluded) in Container. Right returns a container containing all
-- elements following Position (included) in Container. These two new
-- --
-- B o d y --
-- --
--- Copyright (C) 2004-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2013, Free Software Foundation, Inc. --
-- --
-- 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- --
package body Ada.Containers.Hash_Tables.Generic_Bounded_Keys is
+ -----------------------------
+ -- Checked_Equivalent_Keys --
+ -----------------------------
+
+ function Checked_Equivalent_Keys
+ (HT : aliased in out Hash_Table_Type'Class;
+ Key : Key_Type;
+ Node : Count_Type) return Boolean
+ is
+ Result : Boolean;
+
+ B : Natural renames HT.Busy;
+ L : Natural renames HT.Lock;
+
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Result := Equivalent_Keys (Key, HT.Nodes (Node));
+
+ B := B - 1;
+ L := L - 1;
+
+ return Result;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+
+ raise;
+ end Checked_Equivalent_Keys;
+
+ -------------------
+ -- Checked_Index --
+ -------------------
+
+ function Checked_Index
+ (HT : aliased in out Hash_Table_Type'Class;
+ Key : Key_Type) return Hash_Type
+ is
+ Result : Hash_Type;
+
+ B : Natural renames HT.Busy;
+ L : Natural renames HT.Lock;
+
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Result := HT.Buckets'First + Hash (Key) mod HT.Buckets'Length;
+
+ B := B - 1;
+ L := L - 1;
+
+ return Result;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+
+ raise;
+ end Checked_Index;
+
--------------------------
-- Delete_Key_Sans_Free --
--------------------------
return;
end if;
- Indx := Index (HT, Key);
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ if HT.Busy > 0 then
+ raise Program_Error with
+ "attempt to tamper with cursors (container is busy)";
+ end if;
+
+ Indx := Checked_Index (HT, Key);
X := HT.Buckets (Indx);
if X = 0 then
return;
end if;
- if Equivalent_Keys (Key, HT.Nodes (X)) then
+ if Checked_Equivalent_Keys (HT, Key, X) then
if HT.Busy > 0 then
raise Program_Error with
"attempt to tamper with cursors (container is busy)";
return;
end if;
- if Equivalent_Keys (Key, HT.Nodes (X)) then
+ if Checked_Equivalent_Keys (HT, Key, X) then
if HT.Busy > 0 then
raise Program_Error with
"attempt to tamper with cursors (container is busy)";
return 0;
end if;
- Indx := Index (HT, Key);
+ Indx := Checked_Index (HT'Unrestricted_Access.all, Key);
Node := HT.Buckets (Indx);
while Node /= 0 loop
- if Equivalent_Keys (Key, HT.Nodes (Node)) then
+ if Checked_Equivalent_Keys
+ (HT'Unrestricted_Access.all, Key, Node)
+ then
return Node;
end if;
Node := Next (HT.Nodes (Node));
Node : out Count_Type;
Inserted : out Boolean)
is
- Indx : constant Hash_Type := Index (HT, Key);
- B : Count_Type renames HT.Buckets (Indx);
+ Indx : Hash_Type;
begin
- if B = 0 then
- if HT.Busy > 0 then
- raise Program_Error with
- "attempt to tamper with cursors (container is busy)";
- end if;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ if HT.Busy > 0 then
+ raise Program_Error with
+ "attempt to tamper with cursors (container is busy)";
+ end if;
+
+ Indx := Checked_Index (HT, Key);
+ Node := HT.Buckets (Indx);
+ if Node = 0 then
if HT.Length = HT.Capacity then
raise Capacity_Error with "no more capacity for insertion";
end if;
Inserted := True;
- B := Node;
+ HT.Buckets (Indx) := Node;
HT.Length := HT.Length + 1;
return;
end if;
- Node := B;
loop
- if Equivalent_Keys (Key, HT.Nodes (Node)) then
+ if Checked_Equivalent_Keys (HT, Key, Node) then
Inserted := False;
return;
end if;
exit when Node = 0;
end loop;
- if HT.Busy > 0 then
- raise Program_Error with
- "attempt to tamper with cursors (container is busy)";
- end if;
-
if HT.Length = HT.Capacity then
raise Capacity_Error with "no more capacity for insertion";
end if;
Node := New_Node;
- Set_Next (HT.Nodes (Node), Next => B);
+ Set_Next (HT.Nodes (Node), Next => HT.Buckets (Indx));
Inserted := True;
- B := Node;
+ HT.Buckets (Indx) := Node;
HT.Length := HT.Length + 1;
end Generic_Conditional_Insert;
- -----------
- -- Index --
- -----------
-
- function Index
- (HT : Hash_Table_Type'Class;
- Key : Key_Type) return Hash_Type is
- begin
- return HT.Buckets'First + Hash (Key) mod HT.Buckets'Length;
- end Index;
-
-----------------------------
-- Generic_Replace_Element --
-----------------------------
BB : Buckets_Type renames HT.Buckets;
NN : Nodes_Type renames HT.Nodes;
- Old_Hash : constant Hash_Type := Hash (NN (Node));
- Old_Indx : constant Hash_Type := BB'First + Old_Hash mod BB'Length;
-
- New_Hash : constant Hash_Type := Hash (Key);
- New_Indx : constant Hash_Type := BB'First + New_Hash mod BB'Length;
+ Old_Indx : Hash_Type;
+ New_Indx : constant Hash_Type := Checked_Index (HT, Key);
New_Bucket : Count_Type renames BB (New_Indx);
N, M : Count_Type;
begin
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ declare
+ B : Natural renames HT.Busy;
+ L : Natural renames HT.Lock;
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Old_Indx := Hash (NN (Node)) mod HT.Buckets'Length;
+
+ B := B - 1;
+ L := L - 1;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+
+ raise;
+ end;
+
-- Replace_Element is allowed to change a node's key to Key
-- (generic formal operation Assign provides the mechanism), but
-- only if Key is not already in the hash table. (In a unique-key
-- hash table as this one, a key is mapped to exactly one node.)
- if Equivalent_Keys (Key, NN (Node)) then
- pragma Assert (New_Hash = Old_Hash);
-
+ if Checked_Equivalent_Keys (HT, Key, Node) then
if HT.Lock > 0 then
raise Program_Error with
"attempt to tamper with elements (container is locked)";
-- stays in the same bucket.
Assign (NN (Node), Key);
- pragma Assert (Hash (NN (Node)) = New_Hash);
- pragma Assert (Equivalent_Keys (Key, NN (Node)));
return;
end if;
N := New_Bucket;
while N /= 0 loop
- if Equivalent_Keys (Key, NN (N)) then
+ if Checked_Equivalent_Keys (HT, Key, N) then
pragma Assert (N /= Node);
raise Program_Error with
"attempt to replace existing element";
end if;
Assign (NN (Node), Key);
- pragma Assert (Hash (NN (Node)) = New_Hash);
- pragma Assert (Equivalent_Keys (Key, NN (Node)));
return;
end if;
-- modified (except for any possible side-effect Assign had on Node).
Assign (NN (Node), Key);
- pragma Assert (Hash (NN (Node)) = New_Hash);
- pragma Assert (Equivalent_Keys (Key, NN (Node)));
-- Now we can safely remove the node from its current bucket
New_Bucket := Node;
end Generic_Replace_Element;
+ -----------
+ -- Index --
+ -----------
+
+ function Index
+ (HT : Hash_Table_Type'Class;
+ Key : Key_Type) return Hash_Type is
+ begin
+ return HT.Buckets'First + Hash (Key) mod HT.Buckets'Length;
+ end Index;
+
end Ada.Containers.Hash_Tables.Generic_Bounded_Keys;
-- --
-- S p e c --
-- --
--- Copyright (C) 2004-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2013, Free Software Foundation, Inc. --
-- --
-- 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- --
pragma Inline (Index);
-- Returns the bucket number (array index value) for the given key
+ function Checked_Index
+ (HT : aliased in out Hash_Table_Type'Class;
+ 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 : aliased in out Hash_Table_Type'Class;
+ 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;
Key : Key_Type;
-- --
-- B o d y --
-- --
--- Copyright (C) 2004-2011, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2013, Free Software Foundation, Inc. --
-- --
-- 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- --
package body Ada.Containers.Hash_Tables.Generic_Bounded_Operations is
+ -------------------
+ -- Checked_Index --
+ -------------------
+
+ function Checked_Index
+ (Hash_Table : aliased in out Hash_Table_Type'Class;
+ Node : Count_Type) return Hash_Type
+ is
+ Result : Hash_Type;
+
+ B : Natural renames Hash_Table.Busy;
+ L : Natural renames Hash_Table.Lock;
+
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Result := Index (Hash_Table, Hash_Table.Nodes (Node));
+
+ B := B - 1;
+ L := L - 1;
+
+ return Result;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+
+ raise;
+ end Checked_Index;
+
-----------
-- Clear --
-----------
"attempt to delete node from empty hashed container";
end if;
- Indx := Index (HT, HT.Nodes (X));
+ Indx := Checked_Index (HT, X);
Prev := HT.Buckets (Indx);
if Prev = 0 then
function Generic_Equal
(L, R : Hash_Table_Type'Class) return Boolean
is
+ BL : Natural renames L'Unrestricted_Access.Busy;
+ LL : Natural renames L'Unrestricted_Access.Lock;
+
+ BR : Natural renames R'Unrestricted_Access.Busy;
+ LR : Natural renames R'Unrestricted_Access.Lock;
+
+ Result : Boolean;
+
L_Index : Hash_Type;
L_Node : Count_Type;
L_Index := L_Index + 1;
end loop;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ BL := BL + 1;
+ LL := LL + 1;
+
+ BR := BR + 1;
+ LR := LR + 1;
+
-- For each node of hash table L, search for an equivalent node in hash
-- table R.
N := L.Length;
loop
if not Find (HT => R, Key => L.Nodes (L_Node)) then
- return False;
+ Result := False;
+ exit;
end if;
N := N - 1;
-- We have exhausted the nodes in this bucket
if N = 0 then
- return True;
+ Result := True;
+ exit;
end if;
-- Find the next bucket
end loop;
end if;
end loop;
+
+ BL := BL - 1;
+ LL := LL - 1;
+
+ BR := BR - 1;
+ LR := LR - 1;
+
+ return Result;
+ exception
+ when others =>
+ BL := BL - 1;
+ LL := LL - 1;
+
+ BR := BR - 1;
+ LR := LR - 1;
+
+ raise;
end Generic_Equal;
-----------------------
for J in 1 .. N loop
declare
Node : constant Count_Type := New_Node (Stream);
- Indx : constant Hash_Type := Index (HT, HT.Nodes (Node));
+ Indx : constant Hash_Type := Checked_Index (HT, Node);
B : Count_Type renames HT.Buckets (Indx);
begin
Set_Next (HT.Nodes (Node), Next => B);
(HT : Hash_Table_Type'Class;
Node : Count_Type) return Count_Type
is
- Result : Count_Type := Next (HT.Nodes (Node));
+ Result : Count_Type;
+ First : Hash_Type;
begin
+ Result := Next (HT.Nodes (Node));
+
if Result /= 0 then -- another node in same bucket
return Result;
end if;
-- This was the last node in the bucket, so move to the next
-- bucket, and start searching for next node from there.
- for Indx in Index (HT, HT.Nodes (Node)) + 1 .. HT.Buckets'Last loop
+ First := Checked_Index (HT'Unrestricted_Access.all, Node) + 1;
+ for Indx in First .. HT.Buckets'Last loop
Result := HT.Buckets (Indx);
if Result /= 0 then -- bucket is not empty
-- --
-- S p e c --
-- --
--- Copyright (C) 2004-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2013, Free Software Foundation, Inc. --
-- --
-- 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- --
-- Uses the hash value of Node to compute its Hash_Table buckets array
-- index.
+ function Checked_Index
+ (Hash_Table : aliased in out Hash_Table_Type'Class;
+ 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;
-- --
-- B o d y --
-- --
--- Copyright (C) 2004-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2013, Free Software Foundation, Inc. --
-- --
-- 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- --
package body Ada.Containers.Hash_Tables.Generic_Keys is
+ -----------------------------
+ -- Checked_Equivalent_Keys --
+ -----------------------------
+
+ function Checked_Equivalent_Keys
+ (HT : aliased in out Hash_Table_Type;
+ Key : Key_Type;
+ Node : Node_Access) return Boolean
+ is
+ Result : Boolean;
+
+ B : Natural renames HT.Busy;
+ L : Natural renames HT.Lock;
+
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Result := Equivalent_Keys (Key, Node);
+
+ B := B - 1;
+ L := L - 1;
+
+ return Result;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+
+ raise;
+ end Checked_Equivalent_Keys;
+
+ -------------------
+ -- Checked_Index --
+ -------------------
+
+ function Checked_Index
+ (HT : aliased in out Hash_Table_Type;
+ Key : Key_Type) return Hash_Type
+ is
+ Result : Hash_Type;
+
+ B : Natural renames HT.Busy;
+ L : Natural renames HT.Lock;
+
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Result := Hash (Key) mod HT.Buckets'Length;
+
+ B := B - 1;
+ L := L - 1;
+
+ return Result;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+
+ raise;
+ end Checked_Index;
+
--------------------------
-- Delete_Key_Sans_Free --
--------------------------
return;
end if;
- Indx := Index (HT, Key);
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ if HT.Busy > 0 then
+ raise Program_Error with
+ "attempt to tamper with cursors (container is busy)";
+ end if;
+
+ Indx := Checked_Index (HT, Key);
X := HT.Buckets (Indx);
if X = null then
return;
end if;
- if Equivalent_Keys (Key, X) then
+ if Checked_Equivalent_Keys (HT, Key, X) then
if HT.Busy > 0 then
raise Program_Error with
"attempt to tamper with cursors (container is busy)";
return;
end if;
- if Equivalent_Keys (Key, X) then
+ if Checked_Equivalent_Keys (HT, Key, X) then
if HT.Busy > 0 then
raise Program_Error with
"attempt to tamper with cursors (container is busy)";
----------
function Find
- (HT : Hash_Table_Type;
- Key : Key_Type) return Node_Access is
-
+ (HT : aliased in out Hash_Table_Type;
+ Key : Key_Type) return Node_Access
+ is
Indx : Hash_Type;
Node : Node_Access;
return null;
end if;
- Indx := Index (HT, Key);
+ Indx := Checked_Index (HT, Key);
Node := HT.Buckets (Indx);
while Node /= null loop
- if Equivalent_Keys (Key, Node) then
+ if Checked_Equivalent_Keys (HT, Key, Node) then
return Node;
end if;
Node := Next (Node);
Node : out Node_Access;
Inserted : out Boolean)
is
- Indx : constant Hash_Type := Index (HT, Key);
- B : Node_Access renames HT.Buckets (Indx);
+ Indx : Hash_Type;
begin
- if B = null then
- if HT.Busy > 0 then
- raise Program_Error with
- "attempt to tamper with cursors (container is busy)";
- end if;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ if HT.Busy > 0 then
+ raise Program_Error with
+ "attempt to tamper with cursors (container is busy)";
+ end if;
+
+ Indx := Checked_Index (HT, Key);
+ Node := HT.Buckets (Indx);
+ if Node = null then
if HT.Length = Count_Type'Last then
raise Constraint_Error;
end if;
Node := New_Node (Next => null);
Inserted := True;
- B := Node;
+ HT.Buckets (Indx) := Node;
HT.Length := HT.Length + 1;
return;
end if;
- Node := B;
loop
- if Equivalent_Keys (Key, Node) then
+ if Checked_Equivalent_Keys (HT, Key, Node) then
Inserted := False;
return;
end if;
exit when Node = null;
end loop;
- if HT.Busy > 0 then
- raise Program_Error with
- "attempt to tamper with cursors (container is busy)";
- end if;
-
if HT.Length = Count_Type'Last then
raise Constraint_Error;
end if;
- Node := New_Node (Next => B);
+ Node := New_Node (Next => HT.Buckets (Indx));
Inserted := True;
- B := Node;
+ HT.Buckets (Indx) := Node;
HT.Length := HT.Length + 1;
end Generic_Conditional_Insert;
- -----------
- -- Index --
- -----------
-
- function Index
- (HT : Hash_Table_Type;
- Key : Key_Type) return Hash_Type is
- begin
- return Hash (Key) mod HT.Buckets'Length;
- end Index;
-
-----------------------------
-- Generic_Replace_Element --
-----------------------------
pragma Assert (HT.Length > 0);
pragma Assert (Node /= null);
- Old_Hash : constant Hash_Type := Hash (Node);
- Old_Indx : constant Hash_Type := Old_Hash mod HT.Buckets'Length;
-
- New_Hash : constant Hash_Type := Hash (Key);
- New_Indx : constant Hash_Type := New_Hash mod HT.Buckets'Length;
+ Old_Indx : Hash_Type;
+ New_Indx : constant Hash_Type := Checked_Index (HT, Key);
New_Bucket : Node_Access renames HT.Buckets (New_Indx);
N, M : Node_Access;
begin
- if Equivalent_Keys (Key, Node) then
- pragma Assert (New_Hash = Old_Hash);
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ declare
+ B : Natural renames HT.Busy;
+ L : Natural renames HT.Lock;
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Old_Indx := Hash (Node) mod HT.Buckets'Length;
+ B := B - 1;
+ L := L - 1;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+
+ raise;
+ end;
+
+ if Checked_Equivalent_Keys (HT, Key, Node) then
if HT.Lock > 0 then
raise Program_Error with
"attempt to tamper with elements (container is locked)";
-- change is allowed.
Assign (Node, Key);
- pragma Assert (Hash (Node) = New_Hash);
- pragma Assert (Equivalent_Keys (Key, Node));
return;
end if;
N := New_Bucket;
while N /= null loop
- if Equivalent_Keys (Key, N) then
+ if Checked_Equivalent_Keys (HT, Key, N) then
pragma Assert (N /= Node);
raise Program_Error with
"attempt to replace existing element";
end if;
Assign (Node, Key);
- pragma Assert (Hash (Node) = New_Hash);
- pragma Assert (Equivalent_Keys (Key, Node));
return;
end if;
-- modified (except for any possible side-effect Assign had on Node).
Assign (Node, Key);
- pragma Assert (Hash (Node) = New_Hash);
- pragma Assert (Equivalent_Keys (Key, Node));
-- Now we can safely remove the node from its current bucket
New_Bucket := Node;
end Generic_Replace_Element;
+ -----------
+ -- Index --
+ -----------
+
+ function Index
+ (HT : Hash_Table_Type;
+ Key : Key_Type) return Hash_Type
+ is
+ begin
+ return Hash (Key) mod HT.Buckets'Length;
+ end Index;
+
end Ada.Containers.Hash_Tables.Generic_Keys;
-- --
-- S p e c --
-- --
--- Copyright (C) 2004-2009, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2013, Free Software Foundation, Inc. --
-- --
-- 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- --
pragma Inline (Index);
-- Returns the bucket number (array index value) for the given key
+ function Checked_Index
+ (HT : aliased in out 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 : aliased in out Hash_Table_Type;
+ Key : Key_Type;
+ Node : Node_Access) 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;
Key : Key_Type;
-- without deallocating it. Program_Error is raised if the hash
-- table is busy.
- function Find (HT : Hash_Table_Type; Key : Key_Type) return Node_Access;
+ function Find
+ (HT : aliased in out Hash_Table_Type;
+ Key : Key_Type) return Node_Access;
-- Returns the node (if any) corresponding to the given key
generic
-- --
-- B o d y --
-- --
--- Copyright (C) 2004-2010, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2013, Free Software Foundation, Inc. --
-- --
-- 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- --
-- See note above
- pragma Assert (Index (HT, Dst_Node) = Src_Index);
+ pragma Assert (Checked_Index (HT, Dst_Node) = Src_Index);
begin
HT.Buckets (Src_Index) := Dst_Node;
-- See note above
- pragma Assert (Index (HT, Dst_Node) = Src_Index);
+ pragma Assert (Checked_Index (HT, Dst_Node) = Src_Index);
begin
Set_Next (Node => Dst_Prev, Next => Dst_Node);
return HT.Buckets'Length;
end Capacity;
+ -------------------
+ -- Checked_Index --
+ -------------------
+
+ function Checked_Index
+ (Hash_Table : aliased in out Hash_Table_Type;
+ Buckets : Buckets_Type;
+ Node : Node_Access) return Hash_Type
+ is
+ Result : Hash_Type;
+
+ B : Natural renames Hash_Table.Busy;
+ L : Natural renames Hash_Table.Lock;
+
+ begin
+ B := B + 1;
+ L := L + 1;
+
+ Result := Index (Buckets, Node);
+
+ B := B - 1;
+ L := L - 1;
+
+ return Result;
+ exception
+ when others =>
+ B := B - 1;
+ L := L - 1;
+
+ raise;
+ end Checked_Index;
+
+ function Checked_Index
+ (Hash_Table : aliased in out Hash_Table_Type;
+ Node : Node_Access) return Hash_Type
+ is
+ begin
+ return Checked_Index (Hash_Table, Hash_Table.Buckets.all, Node);
+ end Checked_Index;
+
-----------
-- Clear --
-----------
"attempt to delete node from empty hashed container";
end if;
- Indx := Index (HT, X);
+ Indx := Checked_Index (HT, X);
Prev := HT.Buckets (Indx);
if Prev = null then
function Generic_Equal
(L, R : Hash_Table_Type) return Boolean
is
+ BL : Natural renames L'Unrestricted_Access.Busy;
+ LL : Natural renames L'Unrestricted_Access.Lock;
+
+ BR : Natural renames R'Unrestricted_Access.Busy;
+ LR : Natural renames R'Unrestricted_Access.Lock;
+
+ Result : Boolean;
+
L_Index : Hash_Type;
L_Node : Node_Access;
L_Index := L_Index + 1;
end loop;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ BL := BL + 1;
+ LL := LL + 1;
+
+ BR := BR + 1;
+ LR := LR + 1;
+
-- For each node of hash table L, search for an equivalent node in hash
-- table R.
N := L.Length;
loop
if not Find (HT => R, Key => L_Node) then
- return False;
+ Result := False;
+ exit;
end if;
N := N - 1;
-- We have exhausted the nodes in this bucket
if N = 0 then
- return True;
+ Result := True;
+ exit;
end if;
-- Find the next bucket
end loop;
end if;
end loop;
+
+ BL := BL - 1;
+ LL := LL - 1;
+
+ BR := BR - 1;
+ LR := LR - 1;
+
+ return Result;
+ exception
+ when others =>
+ BL := BL - 1;
+ LL := LL - 1;
+
+ BR := BR - 1;
+ LR := LR - 1;
+
+ raise;
end Generic_Equal;
-----------------------
for J in 1 .. N loop
declare
Node : constant Node_Access := New_Node (Stream);
- Indx : constant Hash_Type := Index (HT, Node);
+ Indx : constant Hash_Type := Checked_Index (HT, Node);
B : Node_Access renames HT.Buckets (Indx);
begin
Set_Next (Node => Node, Next => B);
----------
function Next
- (HT : Hash_Table_Type;
+ (HT : aliased in out Hash_Table_Type;
Node : Node_Access) return Node_Access
is
- Result : Node_Access := Next (Node);
+ Result : Node_Access;
+ First : Hash_Type;
begin
+ Result := Next (Node);
+
if Result /= null then
return Result;
end if;
- for Indx in Index (HT, Node) + 1 .. HT.Buckets'Last loop
+ First := Checked_Index (HT, Node) + 1;
+ for Indx in First .. HT.Buckets'Last loop
Result := HT.Buckets (Indx);
if Result /= null then
Src_Node : constant Node_Access := Src_Bucket;
Dst_Index : constant Hash_Type :=
- Index (Dst_Buckets.all, Src_Node);
+ Checked_Index (HT, Dst_Buckets.all, Src_Node);
Dst_Bucket : Node_Access renames Dst_Buckets (Dst_Index);
-- --
-- S p e c --
-- --
--- Copyright (C) 2004-2009, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2013, Free Software Foundation, Inc. --
-- --
-- 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- --
-- Uses the hash value of Node to compute its Hash_Table buckets array
-- index.
+ function Checked_Index
+ (Hash_Table : aliased in out Hash_Table_Type;
+ Buckets : Buckets_Type;
+ Node : Node_Access) 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.
+
+ function Checked_Index
+ (Hash_Table : aliased in out Hash_Table_Type;
+ Node : Node_Access) return Hash_Type;
+ -- Calls Checked_Index using Hash_Table's buckets array.
+
procedure Adjust (HT : in out Hash_Table_Type);
-- Used to implement controlled Adjust. It is assumed that HT has the value
-- of the bit-wise copy that immediately follows controlled Finalize.
-- bucket.
function Next
- (HT : Hash_Table_Type;
+ (HT : aliased in out Hash_Table_Type;
Node : Node_Access) return Node_Access;
-- 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
(Container : aliased Map;
Key : Key_Type) return Constant_Reference_Type
is
- Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+ HT : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+ Node : constant Node_Access := Key_Ops.Find (HT, Key);
begin
if Node = null then
end if;
declare
- M : Map renames Container'Unrestricted_Access.all;
- HT : Hash_Table_Type renames M.HT'Unrestricted_Access.all;
B : Natural renames HT.Busy;
L : Natural renames HT.Lock;
begin
-------------
function Element (Container : Map; Key : Key_Type) return Element_Type is
- Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+ HT : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+ Node : constant Node_Access := Key_Ops.Find (HT, Key);
begin
if Node = null then
----------
function Find (Container : Map; Key : Key_Type) return Cursor is
- Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+ HT : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+ Node : constant Node_Access := Key_Ops.Find (HT, Key);
begin
if Node = null then
(Container : aliased in out Map;
Key : Key_Type) return Reference_Type
is
- Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+ HT : Hash_Table_Type renames Container.HT;
+ Node : constant Node_Access := Key_Ops.Find (HT, Key);
begin
if Node = null then
end if;
declare
- M : Map renames Container'Unrestricted_Access.all;
- HT : Hash_Table_Type renames M.HT'Unrestricted_Access.all;
B : Natural renames HT.Busy;
L : Natural renames HT.Lock;
begin
return False;
end if;
- X := HT.Buckets (Key_Ops.Index (HT, Position.Node.Key.all));
+ X := HT.Buckets (Key_Ops.Checked_Index (HT, Position.Node.Key.all));
for J in 1 .. HT.Length loop
if X = Position.Node then
Node : out Node_Access;
Inserted : out Boolean);
- function Is_In (HT : Hash_Table_Type; Key : Node_Access) return Boolean;
+ function Is_In
+ (HT : aliased in out Hash_Table_Type;
+ Key : Node_Access) return Boolean;
pragma Inline (Is_In);
function Next (Node : Node_Access) return Node_Access;
(Target : in out Set;
Source : Set)
is
+ Src_HT : Hash_Table_Type renames Source'Unrestricted_Access.HT;
Tgt_Node : Node_Access;
begin
return;
end if;
- if Source.HT.Length = 0 then
+ if Src_HT.Length = 0 then
return;
end if;
"attempt to tamper with cursors (set is busy)";
end if;
- if Source.HT.Length < Target.HT.Length then
+ if Src_HT.Length < Target.HT.Length then
declare
Src_Node : Node_Access;
begin
- Src_Node := HT_Ops.First (Source.HT);
+ Src_Node := HT_Ops.First (Src_HT);
while Src_Node /= null loop
Tgt_Node := Element_Keys.Find (Target.HT, Src_Node.Element.all);
Free (Tgt_Node);
end if;
- Src_Node := HT_Ops.Next (Source.HT, Src_Node);
+ Src_Node := HT_Ops.Next (Src_HT, Src_Node);
end loop;
end;
else
Tgt_Node := HT_Ops.First (Target.HT);
while Tgt_Node /= null loop
- if Is_In (Source.HT, Tgt_Node) then
+ if Is_In (Src_HT, Tgt_Node) then
declare
X : Node_Access := Tgt_Node;
begin
end Difference;
function Difference (Left, Right : Set) return Set is
- Buckets : HT_Types.Buckets_Access;
- Length : Count_Type;
+ Left_HT : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+ Right_HT : Hash_Table_Type renames Right'Unrestricted_Access.HT;
+ Buckets : HT_Types.Buckets_Access;
+ Length : Count_Type;
begin
if Left'Address = Right'Address then
procedure Process (L_Node : Node_Access) is
begin
- if not Is_In (Right.HT, L_Node) then
+ if not Is_In (Right_HT, L_Node) then
declare
- Src : Element_Type renames L_Node.Element.all;
- Indx : constant Hash_Type := Hash (Src) mod Buckets'Length;
+ -- Per AI05-0022, the container implementation is required
+ -- to detect element tampering by a generic actual
+ -- subprogram, hence the use of Checked_Index instead of a
+ -- simple invocation of generic formal Hash.
+
+ Indx : constant Hash_Type :=
+ HT_Ops.Checked_Index (Left_HT, Buckets.all, L_Node);
+
Bucket : Node_Access renames Buckets (Indx);
+ Src : Element_Type renames L_Node.Element.all;
Tgt : Element_Access := new Element_Type'(Src);
+
begin
Bucket := new Node_Type'(Tgt, Bucket);
exception
pragma Assert (Vet (Left), "bad Left cursor in Equivalent_Elements");
pragma Assert (Vet (Right), "bad Right cursor in Equivalent_Elements");
+ -- AI05-0022 requires that a container implementation detect element
+ -- tampering by a generic actual subprogram. However, the following case
+ -- falls outside the scope of that AI. Randy Brukardt explained on the
+ -- ARG list on 2013/02/07 that:
+
+ -- (Begin Quote):
+ -- But for an operation like "<" [the ordered set analog of
+ -- Equivalent_Elements], there is no need to "dereference" a cursor
+ -- after the call to the generic formal parameter function, so nothing
+ -- bad could happen if tampering is undetected. And the operation can
+ -- safely return a result without a problem even if an element is
+ -- deleted from the container.
+ -- (End Quote).
+
return Equivalent_Elements
(Left.Node.Element.all,
Right.Node.Element.all);
(Container : Set;
Item : Element_Type) return Cursor
is
- Node : constant Node_Access := Element_Keys.Find (Container.HT, Item);
+ HT : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+ Node : constant Node_Access := Element_Keys.Find (HT, Item);
begin
return (if Node = null then No_Element
else Cursor'(Container'Unrestricted_Access, Node));
(Target : in out Set;
Source : Set)
is
+ Src_HT : Hash_Table_Type renames Source'Unrestricted_Access.HT;
Tgt_Node : Node_Access;
begin
Tgt_Node := HT_Ops.First (Target.HT);
while Tgt_Node /= null loop
- if Is_In (Source.HT, Tgt_Node) then
+ if Is_In (Src_HT, Tgt_Node) then
Tgt_Node := HT_Ops.Next (Target.HT, Tgt_Node);
else
end Intersection;
function Intersection (Left, Right : Set) return Set is
- Buckets : HT_Types.Buckets_Access;
- Length : Count_Type;
+ Left_HT : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+ Right_HT : Hash_Table_Type renames Right'Unrestricted_Access.HT;
+ Buckets : HT_Types.Buckets_Access;
+ Length : Count_Type;
begin
if Left'Address = Right'Address then
procedure Process (L_Node : Node_Access) is
begin
- if Is_In (Right.HT, L_Node) then
+ if Is_In (Right_HT, L_Node) then
declare
- Src : Element_Type renames L_Node.Element.all;
+ -- Per AI05-0022, the container implementation is required
+ -- to detect element tampering by a generic actual
+ -- subprogram, hence the use of Checked_Index instead of a
+ -- simple invocation of generic formal Hash.
- Indx : constant Hash_Type := Hash (Src) mod Buckets'Length;
+ Indx : constant Hash_Type :=
+ HT_Ops.Checked_Index (Left_HT, Buckets.all, L_Node);
Bucket : Node_Access renames Buckets (Indx);
+ Src : Element_Type renames L_Node.Element.all;
Tgt : Element_Access := new Element_Type'(Src);
begin
-- Is_In --
-----------
- function Is_In (HT : Hash_Table_Type; Key : Node_Access) return Boolean is
+ function Is_In
+ (HT : aliased in out Hash_Table_Type;
+ Key : Node_Access) return Boolean
+ is
begin
return Element_Keys.Find (HT, Key.Element.all) /= null;
end Is_In;
(Subset : Set;
Of_Set : Set) return Boolean
is
+ Subset_HT : Hash_Table_Type renames Subset'Unrestricted_Access.HT;
+ Of_Set_HT : Hash_Table_Type renames Of_Set'Unrestricted_Access.HT;
Subset_Node : Node_Access;
begin
return False;
end if;
- Subset_Node := HT_Ops.First (Subset.HT);
+ Subset_Node := HT_Ops.First (Subset_HT);
while Subset_Node /= null loop
- if not Is_In (Of_Set.HT, Subset_Node) then
+ if not Is_In (Of_Set_HT, Subset_Node) then
return False;
end if;
- Subset_Node := HT_Ops.Next (Subset.HT, Subset_Node);
+ Subset_Node := HT_Ops.Next (Subset_HT, Subset_Node);
end loop;
return True;
-------------
function Overlap (Left, Right : Set) return Boolean is
+ Left_HT : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+ Right_HT : Hash_Table_Type renames Right'Unrestricted_Access.HT;
Left_Node : Node_Access;
begin
return True;
end if;
- Left_Node := HT_Ops.First (Left.HT);
+ Left_Node := HT_Ops.First (Left_HT);
while Left_Node /= null loop
- if Is_In (Right.HT, Left_Node) then
+ if Is_In (Right_HT, Left_Node) then
return True;
end if;
- Left_Node := HT_Ops.Next (Left.HT, Left_Node);
+ Left_Node := HT_Ops.Next (Left_HT, Left_Node);
end loop;
return False;
(Target : in out Set;
Source : Set)
is
+ Tgt_HT : Hash_Table_Type renames Target.HT;
+ Src_HT : Hash_Table_Type renames Source.HT'Unrestricted_Access.all;
+
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ TB : Natural renames Tgt_HT.Busy;
+ TL : Natural renames Tgt_HT.Lock;
+
+ SB : Natural renames Src_HT.Busy;
+ SL : Natural renames Src_HT.Lock;
+
begin
if Target'Address = Source'Address then
Clear (Target);
return;
end if;
- if Target.HT.Busy > 0 then
+ if TB > 0 then
raise Program_Error with
"attempt to tamper with cursors (set is busy)";
end if;
declare
N : constant Count_Type := Target.Length + Source.Length;
begin
- if N > HT_Ops.Capacity (Target.HT) then
- HT_Ops.Reserve_Capacity (Target.HT, N);
+ if N > HT_Ops.Capacity (Tgt_HT) then
+ HT_Ops.Reserve_Capacity (Tgt_HT, N);
end if;
end;
procedure Process (Src_Node : Node_Access) is
E : Element_Type renames Src_Node.Element.all;
- B : Buckets_Type renames Target.HT.Buckets.all;
+ B : Buckets_Type renames Tgt_HT.Buckets.all;
J : constant Hash_Type := Hash (E) mod B'Length;
- N : Count_Type renames Target.HT.Length;
+ N : Count_Type renames Tgt_HT.Length;
begin
declare
-- Start of processing for Iterate_Source_When_Empty_Target
begin
- Iterate (Source.HT);
+ TB := TB + 1;
+ TL := TL + 1;
+
+ SB := SB + 1;
+ SL := SL + 1;
+
+ Iterate (Src_HT);
+
+ SL := SL - 1;
+ SB := SB - 1;
+
+ TL := TL - 1;
+ TB := TB - 1;
+
+ exception
+ when others =>
+ SL := SL - 1;
+ SB := SB - 1;
+
+ TL := TL - 1;
+ TB := TB - 1;
+
+ raise;
end Iterate_Source_When_Empty_Target;
else
procedure Process (Src_Node : Node_Access) is
E : Element_Type renames Src_Node.Element.all;
- B : Buckets_Type renames Target.HT.Buckets.all;
+ B : Buckets_Type renames Tgt_HT.Buckets.all;
J : constant Hash_Type := Hash (E) mod B'Length;
- N : Count_Type renames Target.HT.Length;
+ N : Count_Type renames Tgt_HT.Length;
begin
if B (J) = null then
-- Start of processing for Iterate_Source
begin
- Iterate (Source.HT);
+ TB := TB + 1;
+ TL := TL + 1;
+
+ SB := SB + 1;
+ SL := SL + 1;
+
+ Iterate (Src_HT);
+
+ SL := SL - 1;
+ SB := SB - 1;
+
+ TL := TL - 1;
+ TB := TB - 1;
+
+ exception
+ when others =>
+ SL := SL - 1;
+ SB := SB - 1;
+
+ TL := TL - 1;
+ TB := TB - 1;
+
+ raise;
end Iterate_Source;
end if;
end Symmetric_Difference;
function Symmetric_Difference (Left, Right : Set) return Set is
- Buckets : HT_Types.Buckets_Access;
- Length : Count_Type;
+ Left_HT : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+ Right_HT : Hash_Table_Type renames Right'Unrestricted_Access.HT;
+ Buckets : HT_Types.Buckets_Access;
+ Length : Count_Type;
begin
if Left'Address = Right'Address then
procedure Process (L_Node : Node_Access) is
begin
- if not Is_In (Right.HT, L_Node) then
+ if not Is_In (Right_HT, L_Node) then
declare
E : Element_Type renames L_Node.Element.all;
- J : constant Hash_Type := Hash (E) mod Buckets'Length;
+
+ -- Per AI05-0022, the container implementation is required
+ -- to detect element tampering by a generic actual
+ -- subprogram, hence the use of Checked_Index instead of a
+ -- simple invocation of generic formal Hash.
+
+ J : constant Hash_Type :=
+ HT_Ops.Checked_Index (Left_HT, Buckets.all, L_Node);
begin
declare
-- Start of processing for Iterate_Left
begin
- Iterate (Left.HT);
+ Iterate (Left_HT);
exception
when others =>
HT_Ops.Free_Hash_Table (Buckets);
procedure Process (R_Node : Node_Access) is
begin
- if not Is_In (Left.HT, R_Node) then
+ if not Is_In (Left_HT, R_Node) then
declare
E : Element_Type renames R_Node.Element.all;
- J : constant Hash_Type := Hash (E) mod Buckets'Length;
+
+ -- Per AI05-0022, the container implementation is required
+ -- to detect element tampering by a generic actual
+ -- subprogram, hence the use of Checked_Index instead of a
+ -- simple invocation of generic formal Hash.
+
+ J : constant Hash_Type :=
+ HT_Ops.Checked_Index (Right_HT, Buckets.all, R_Node);
begin
declare
-- Start of processing for Iterate_Right
begin
- Iterate (Right.HT);
+ Iterate (Right_HT);
exception
when others =>
HT_Ops.Free_Hash_Table (Buckets);
end Union;
function Union (Left, Right : Set) return Set is
- Buckets : HT_Types.Buckets_Access;
- Length : Count_Type;
+ Left_HT : Hash_Table_Type renames Left.HT'Unrestricted_Access.all;
+ Right_HT : Hash_Table_Type renames Right.HT'Unrestricted_Access.all;
+ Buckets : HT_Types.Buckets_Access;
+ Length : Count_Type;
begin
if Left'Address = Right'Address then
raise;
end Process;
- -- Start of processing for Process
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram, hence the use of
+ -- Checked_Index instead of a simple invocation of generic formal
+ -- Hash.
+
+ B : Integer renames Left_HT.Busy;
+ L : Integer renames Left_HT.Lock;
+
+ -- Start of processing for Iterate_Left
begin
+ B := B + 1;
+ L := L + 1;
+
Iterate (Left.HT);
+
+ L := L - 1;
+ B := B - 1;
exception
when others =>
+ L := L - 1;
+ B := B - 1;
+
HT_Ops.Free_Hash_Table (Buckets);
raise;
end Iterate_Left;
Length := Length + 1;
end Process;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram, hence the use of
+ -- Checked_Index instead of a simple invocation of generic formal
+ -- Hash.
+
+ LB : Integer renames Left_HT.Busy;
+ LL : Integer renames Left_HT.Lock;
+
+ RB : Integer renames Right_HT.Busy;
+ RL : Integer renames Right_HT.Lock;
+
-- Start of processing for Iterate_Right
begin
+ LB := LB + 1;
+ LL := LL + 1;
+
+ RB := RB + 1;
+ RL := RL + 1;
+
Iterate (Right.HT);
+
+ RL := RL - 1;
+ RB := RB - 1;
+
+ LL := LL - 1;
+ LB := LB - 1;
exception
when others =>
+ RL := RL - 1;
+ RB := RB - 1;
+
+ LL := LL - 1;
+ LB := LB - 1;
+
HT_Ops.Free_Hash_Table (Buckets);
raise;
end Iterate_Right;
return False;
end if;
- X := HT.Buckets (Element_Keys.Index (HT, Position.Node.Element.all));
+ X := HT.Buckets (Element_Keys.Checked_Index
+ (HT,
+ Position.Node.Element.all));
for J in 1 .. HT.Length loop
if X = Position.Node then
(Container : aliased Set;
Key : Key_Type) return Constant_Reference_Type
is
- Node : constant Node_Access :=
- Key_Keys.Find (Container.HT, Key);
+ HT : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+ Node : constant Node_Access := Key_Keys.Find (HT, Key);
begin
if Node = null then
end if;
declare
- HT : Hash_Table_Type renames Container'Unrestricted_Access.all.HT;
B : Natural renames HT.Busy;
L : Natural renames HT.Lock;
begin
Key_Keys.Delete_Key_Sans_Free (Container.HT, Key, X);
if X = null then
- raise Constraint_Error with "key not in map"; -- ??? "set"
+ raise Constraint_Error with "key not in set";
end if;
Free (X);
(Container : Set;
Key : Key_Type) return Element_Type
is
- Node : constant Node_Access := Key_Keys.Find (Container.HT, Key);
+ HT : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+ Node : constant Node_Access := Key_Keys.Find (HT, Key);
begin
if Node = null then
- raise Constraint_Error with "key not in map"; -- ??? "set"
+ raise Constraint_Error with "key not in set";
end if;
return Node.Element.all;
(Container : Set;
Key : Key_Type) return Cursor
is
- Node : constant Node_Access := Key_Keys.Find (Container.HT, Key);
+ HT : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+ Node : constant Node_Access := Key_Keys.Find (HT, Key);
begin
return (if Node = null then No_Element
else Cursor'(Container'Unrestricted_Access, Node));
(Vet (Position),
"bad cursor in Update_Element_Preserving_Key");
- Indx := HT_Ops.Index (HT, Position.Node);
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
declare
E : Element_Type renames Position.Node.Element.all;
B : Natural renames HT.Busy;
L : Natural renames HT.Lock;
+ Eq : Boolean;
+
begin
B := B + 1;
L := L + 1;
begin
+ Indx := HT_Ops.Index (HT, Position.Node);
Process (E);
+ Eq := Equivalent_Keys (K, Key (E));
exception
when others =>
L := L - 1;
L := L - 1;
B := B - 1;
- if Equivalent_Keys (K, Key (E)) then
- pragma Assert (Hash (K) = Hash (E));
+ if Eq then
return;
end if;
end;
No_Element : constant Cursor;
- function "=" (Left, Right : Vector) return Boolean;
+ function "=" (Left, Right : Vector) return Boolean with
+ Global => null;
function To_Vector
(New_Item : Element_Type;
- Length : Count_Type) return Vector;
+ Length : Count_Type) return Vector
+ with
+ Global => null;
- function "&" (Left, Right : Vector) return Vector;
+ function "&" (Left, Right : Vector) return Vector with
+ Global => null,
+ Pre => Capacity_Range'Last - Length (Left) >= Length (Right);
- function "&" (Left : Vector; Right : Element_Type) return Vector;
+ function "&" (Left : Vector; Right : Element_Type) return Vector with
+ Global => null,
+ Pre => Length (Left) < Capacity_Range'Last;
- function "&" (Left : Element_Type; Right : Vector) return Vector;
+ function "&" (Left : Element_Type; Right : Vector) return Vector with
+ Global => null,
+ Pre => Length (Right) < Capacity_Range'Last;
- function "&" (Left, Right : Element_Type) return Vector;
+ function "&" (Left, Right : Element_Type) return Vector with
+ Global => null,
+ Pre => Capacity_Range'Last >= 2;
- function Capacity (Container : Vector) return Count_Type;
+ function Capacity (Container : Vector) return Count_Type with
+ Global => null;
procedure Reserve_Capacity
(Container : in out Vector;
Capacity : Count_Type)
with
- Pre => Capacity <= Container.Capacity;
+ Global => null,
+ Pre => Capacity <= Container.Capacity;
- function Length (Container : Vector) return Count_Type;
+ function Length (Container : Vector) return Count_Type with
+ Global => null;
procedure Set_Length
(Container : in out Vector;
New_Length : Count_Type)
with
- Pre => New_Length <= Length (Container);
+ Global => null,
+ Pre => New_Length <= Length (Container);
- function Is_Empty (Container : Vector) return Boolean;
+ function Is_Empty (Container : Vector) return Boolean with
+ Global => null;
- procedure Clear (Container : in out Vector);
+ procedure Clear (Container : in out Vector) with
+ Global => null;
procedure Assign (Target : in out Vector; Source : Vector) with
- Pre => Length (Source) <= Target.Capacity;
+ Global => null,
+ Pre => Length (Source) <= Target.Capacity;
function Copy
(Source : Vector;
Capacity : Count_Type := 0) return Vector
with
- Pre => Length (Source) <= Capacity and then Capacity in Capacity_Range;
+ Global => null,
+ Pre => Length (Source) <= Capacity and then Capacity in Capacity_Range;
function To_Cursor
(Container : Vector;
- Index : Extended_Index) return Cursor;
+ Index : Extended_Index) return Cursor
+ with
+ Global => null;
- function To_Index (Position : Cursor) return Extended_Index;
+ function To_Index (Position : Cursor) return Extended_Index with
+ Global => null;
function Element
(Container : Vector;
Index : Index_Type) return Element_Type
with
- Pre => First_Index (Container) <= Index
- and then Index <= Last_Index (Container);
+ Global => null,
+ Pre => First_Index (Container) <= Index
+ and then Index <= Last_Index (Container);
function Element
(Container : Vector;
Position : Cursor) return Element_Type
with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
procedure Replace_Element
(Container : in out Vector;
Index : Index_Type;
New_Item : Element_Type)
with
- Pre => First_Index (Container) <= Index
- and then Index <= Last_Index (Container);
+ Global => null,
+ Pre => First_Index (Container) <= Index
+ and then Index <= Last_Index (Container);
procedure Replace_Element
(Container : in out Vector;
Position : Cursor;
New_Item : Element_Type)
with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
procedure Move (Target : in out Vector; Source : in out Vector) with
- Pre => Length (Source) <= Target.Capacity;
+ Global => null,
+ Pre => Length (Source) <= Target.Capacity;
procedure Insert
(Container : in out Vector;
Before : Extended_Index;
New_Item : Vector)
with
- Pre => First_Index (Container) <= Before
- and then Before <= Last_Index (Container) + 1
- and then Length (Container) < Container.Capacity;
+ Global => null,
+ Pre => First_Index (Container) <= Before
+ and then Before <= Last_Index (Container) + 1
+ and then Length (Container) < Container.Capacity;
procedure Insert
(Container : in out Vector;
Before : Cursor;
New_Item : Vector)
with
- Pre => Length (Container) < Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element);
+ Global => null,
+ Pre => Length (Container) < Container.Capacity
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element);
procedure Insert
(Container : in out Vector;
New_Item : Vector;
Position : out Cursor)
with
- Pre => Length (Container) < Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element);
+ Global => null,
+ Pre => Length (Container) < Container.Capacity
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element);
procedure Insert
(Container : in out Vector;
New_Item : Element_Type;
Count : Count_Type := 1)
with
- Pre => First_Index (Container) <= Before
- and then Before <= Last_Index (Container) + 1
- and then Length (Container) + Count <= Container.Capacity;
+ Global => null,
+ Pre => First_Index (Container) <= Before
+ and then Before <= Last_Index (Container) + 1
+ and then Length (Container) + Count <= Container.Capacity;
procedure Insert
(Container : in out Vector;
New_Item : Element_Type;
Count : Count_Type := 1)
with
- Pre => Length (Container) + Count <= Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element);
+ Global => null,
+ Pre => Length (Container) + Count <= Container.Capacity
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element);
procedure Insert
(Container : in out Vector;
Position : out Cursor;
Count : Count_Type := 1)
with
- Pre => Length (Container) + Count <= Container.Capacity
- and then (Has_Element (Container, Before)
- or else Before = No_Element);
+ Global => null,
+ Pre => Length (Container) + Count <= Container.Capacity
+ and then (Has_Element (Container, Before)
+ or else Before = No_Element);
procedure Prepend
(Container : in out Vector;
New_Item : Vector)
with
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre => Length (Container) < Container.Capacity;
procedure Prepend
(Container : in out Vector;
New_Item : Element_Type;
Count : Count_Type := 1)
with
- Pre => Length (Container) + Count <= Container.Capacity;
+ Global => null,
+ Pre => Length (Container) + Count <= Container.Capacity;
procedure Append
(Container : in out Vector;
New_Item : Vector)
with
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre => Length (Container) < Container.Capacity;
procedure Append
(Container : in out Vector;
New_Item : Element_Type;
Count : Count_Type := 1)
with
- Pre => Length (Container) + Count <= Container.Capacity;
+ Global => null,
+ Pre => Length (Container) + Count <= Container.Capacity;
procedure Delete
(Container : in out Vector;
Index : Extended_Index;
Count : Count_Type := 1)
with
- Pre => First_Index (Container) <= Index
- and then Index <= Last_Index (Container) + 1;
+ Global => null,
+ Pre => First_Index (Container) <= Index
+ and then Index <= Last_Index (Container) + 1;
procedure Delete
(Container : in out Vector;
Position : in out Cursor;
Count : Count_Type := 1)
with
- Pre => Has_Element (Container, Position);
+ Global => null,
+ Pre => Has_Element (Container, Position);
procedure Delete_First
(Container : in out Vector;
- Count : Count_Type := 1);
+ Count : Count_Type := 1)
+ with
+ Global => null;
procedure Delete_Last
(Container : in out Vector;
- Count : Count_Type := 1);
+ Count : Count_Type := 1)
+ with
+ Global => null;
- procedure Reverse_Elements (Container : in out Vector);
+ procedure Reverse_Elements (Container : in out Vector) with
+ Global => null;
procedure Swap (Container : in out Vector; I, J : Index_Type) with
- Pre => First_Index (Container) <= I and then I <= Last_Index (Container)
- and then First_Index (Container) <= J
- and then J <= Last_Index (Container);
+ Global => null,
+ Pre => First_Index (Container) <= I
+ and then I <= Last_Index (Container)
+ and then First_Index (Container) <= J
+ and then J <= Last_Index (Container);
procedure Swap (Container : in out Vector; I, J : Cursor) with
- Pre => Has_Element (Container, I) and then Has_Element (Container, J);
+ Global => null,
+ Pre => Has_Element (Container, I) and then Has_Element (Container, J);
- function First_Index (Container : Vector) return Index_Type;
+ function First_Index (Container : Vector) return Index_Type with
+ Global => null;
- function First (Container : Vector) return Cursor;
+ function First (Container : Vector) return Cursor with
+ Global => null;
function First_Element (Container : Vector) return Element_Type with
- Pre => not Is_Empty (Container);
+ Global => null,
+ Pre => not Is_Empty (Container);
- function Last_Index (Container : Vector) return Extended_Index;
+ function Last_Index (Container : Vector) return Extended_Index with
+ Global => null;
- function Last (Container : Vector) return Cursor;
+ function Last (Container : Vector) return Cursor with
+ Global => null;
function Last_Element (Container : Vector) return Element_Type with
- Pre => not Is_Empty (Container);
+ Global => null,
+ Pre => not Is_Empty (Container);
function Next (Container : Vector; Position : Cursor) return Cursor with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
procedure Next (Container : Vector; Position : in out Cursor) with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Previous (Container : Vector; Position : Cursor) return Cursor with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
procedure Previous (Container : Vector; Position : in out Cursor) with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Find_Index
(Container : Vector;
Item : Element_Type;
- Index : Index_Type := Index_Type'First) return Extended_Index;
+ Index : Index_Type := Index_Type'First) return Extended_Index
+ with
+ Global => null;
function Find
(Container : Vector;
Item : Element_Type;
Position : Cursor := No_Element) return Cursor
with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Reverse_Find_Index
(Container : Vector;
Item : Element_Type;
- Index : Index_Type := Index_Type'Last) return Extended_Index;
+ Index : Index_Type := Index_Type'Last) return Extended_Index
+ with
+ Global => null;
function Reverse_Find
(Container : Vector;
Item : Element_Type;
Position : Cursor := No_Element) return Cursor
with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Contains
(Container : Vector;
- Item : Element_Type) return Boolean;
+ Item : Element_Type) return Boolean
+ with
+ Global => null;
- function Has_Element (Container : Vector; Position : Cursor) return Boolean;
+ function Has_Element (Container : Vector; Position : Cursor) return Boolean
+ with
+ Global => null;
generic
with function "<" (Left, Right : Element_Type) return Boolean is <>;
package Generic_Sorting is
- function Is_Sorted (Container : Vector) return Boolean;
+ function Is_Sorted (Container : Vector) return Boolean with
+ Global => null;
- procedure Sort (Container : in out Vector);
+ procedure Sort (Container : in out Vector) with
+ Global => null;
- procedure Merge (Target : in out Vector; Source : in out Vector);
+ procedure Merge (Target : in out Vector; Source : in out Vector) with
+ Global => null;
end Generic_Sorting;
- function Strict_Equal (Left, Right : Vector) return Boolean;
+ function Strict_Equal (Left, Right : Vector) return Boolean with
+ Global => null;
-- Strict_Equal returns True if the containers are physically equal, i.e.
-- they are structurally equal (function "=" returns True) and that they
-- have the same set of cursors.
function Left (Container : Vector; Position : Cursor) return Vector with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
function Right (Container : Vector; Position : Cursor) return Vector with
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre => Has_Element (Container, Position) or else Position = No_Element;
-- Left returns a container containing all elements preceding Position
-- (excluded) in Container. Right returns a container containing all
-- elements following Position (included) in Container. These two new
(Container : aliased Map;
Key : Key_Type) return Constant_Reference_Type
is
- Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+ HT : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+ Node : constant Node_Access := Key_Ops.Find (HT, Key);
begin
if Node = null then
end if;
declare
- HT : Hash_Table_Type renames Container'Unrestricted_Access.all.HT;
B : Natural renames HT.Busy;
L : Natural renames HT.Lock;
begin
-------------
function Element (Container : Map; Key : Key_Type) return Element_Type is
- Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+ HT : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+ Node : constant Node_Access := Key_Ops.Find (HT, Key);
begin
if Node = null then
----------
function Find (Container : Map; Key : Key_Type) return Cursor is
- Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+ HT : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+ Node : constant Node_Access := Key_Ops.Find (HT, Key);
begin
if Node = null then
(Container : aliased in out Map;
Key : Key_Type) return Reference_Type
is
- Node : constant Node_Access := Key_Ops.Find (Container.HT, Key);
+ HT : Hash_Table_Type renames Container.HT;
+ Node : constant Node_Access := Key_Ops.Find (HT, Key);
begin
if Node = null then
end if;
declare
- HT : Hash_Table_Type renames Container'Unrestricted_Access.all.HT;
B : Natural renames HT.Busy;
L : Natural renames HT.Lock;
begin
return False;
end if;
- X := HT.Buckets (Key_Ops.Index (HT, Position.Node.Key));
+ X := HT.Buckets (Key_Ops.Checked_Index (HT, Position.Node.Key));
for J in 1 .. HT.Length loop
if X = Position.Node then
Inserted : out Boolean);
function Is_In
- (HT : Hash_Table_Type;
+ (HT : aliased in out Hash_Table_Type;
Key : Node_Access) return Boolean;
pragma Inline (Is_In);
Source : Set)
is
Tgt_Node : Node_Access;
+ Src_HT : Hash_Table_Type renames Source'Unrestricted_Access.HT;
begin
if Target'Address = Source'Address then
return;
end if;
- if Source.HT.Length = 0 then
+ if Src_HT.Length = 0 then
return;
end if;
"attempt to tamper with cursors (set is busy)";
end if;
- if Source.HT.Length < Target.HT.Length then
+ if Src_HT.Length < Target.HT.Length then
declare
Src_Node : Node_Access;
begin
- Src_Node := HT_Ops.First (Source.HT);
+ Src_Node := HT_Ops.First (Src_HT);
while Src_Node /= null loop
Tgt_Node := Element_Keys.Find (Target.HT, Src_Node.Element);
Free (Tgt_Node);
end if;
- Src_Node := HT_Ops.Next (Source.HT, Src_Node);
+ Src_Node := HT_Ops.Next (Src_HT, Src_Node);
end loop;
end;
else
Tgt_Node := HT_Ops.First (Target.HT);
while Tgt_Node /= null loop
- if Is_In (Source.HT, Tgt_Node) then
+ if Is_In (Src_HT, Tgt_Node) then
declare
X : Node_Access := Tgt_Node;
begin
end Difference;
function Difference (Left, Right : Set) return Set is
- Buckets : HT_Types.Buckets_Access;
- Length : Count_Type;
+ Left_HT : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+ Right_HT : Hash_Table_Type renames Right'Unrestricted_Access.HT;
+ Buckets : HT_Types.Buckets_Access;
+ Length : Count_Type;
begin
if Left'Address = Right'Address then
return Empty_Set;
end if;
- if Left.HT.Length = 0 then
+ if Left_HT.Length = 0 then
return Empty_Set;
end if;
- if Right.HT.Length = 0 then
+ if Right_HT.Length = 0 then
return Left;
end if;
procedure Process (L_Node : Node_Access) is
begin
- if not Is_In (Right.HT, L_Node) then
+ if not Is_In (Right_HT, L_Node) then
declare
+ -- Per AI05-0022, the container implementation is required
+ -- to detect element tampering by a generic actual
+ -- subprogram, hence the use of Checked_Index instead of a
+ -- simple invocation of generic formal Hash.
+
J : constant Hash_Type :=
- Hash (L_Node.Element) mod Buckets'Length;
+ HT_Ops.Checked_Index (Left_HT, Buckets.all, L_Node);
Bucket : Node_Access renames Buckets (J);
-- Start of processing for Iterate_Left
begin
- Iterate (Left.HT);
+ Iterate (Left_HT);
exception
when others =>
HT_Ops.Free_Hash_Table (Buckets);
pragma Assert (Vet (Left), "bad Left cursor in Equivalent_Elements");
pragma Assert (Vet (Right), "bad Right cursor in Equivalent_Elements");
+ -- AI05-0022 requires that a container implementation detect element
+ -- tampering by a generic actual subprogram. However, the following case
+ -- falls outside the scope of that AI. Randy Brukardt explained on the
+ -- ARG list on 2013/02/07 that:
+
+ -- (Begin Quote):
+ -- But for an operation like "<" [the ordered set analog of
+ -- Equivalent_Elements], there is no need to "dereference" a cursor
+ -- after the call to the generic formal parameter function, so nothing
+ -- bad could happen if tampering is undetected. And the operation can
+ -- safely return a result without a problem even if an element is
+ -- deleted from the container.
+ -- (End Quote).
+
return Equivalent_Elements (Left.Node.Element, Right.Node.Element);
end Equivalent_Elements;
(Container : Set;
Item : Element_Type) return Cursor
is
- Node : constant Node_Access := Element_Keys.Find (Container.HT, Item);
+ HT : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+ Node : constant Node_Access := Element_Keys.Find (HT, Item);
begin
if Node = null then
(Target : in out Set;
Source : Set)
is
+ Src_HT : Hash_Table_Type renames Source'Unrestricted_Access.HT;
Tgt_Node : Node_Access;
begin
Tgt_Node := HT_Ops.First (Target.HT);
while Tgt_Node /= null loop
- if Is_In (Source.HT, Tgt_Node) then
+ if Is_In (Src_HT, Tgt_Node) then
Tgt_Node := HT_Ops.Next (Target.HT, Tgt_Node);
else
end Intersection;
function Intersection (Left, Right : Set) return Set is
- Buckets : HT_Types.Buckets_Access;
- Length : Count_Type;
+ Left_HT : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+ Right_HT : Hash_Table_Type renames Right'Unrestricted_Access.HT;
+ Buckets : HT_Types.Buckets_Access;
+ Length : Count_Type;
begin
if Left'Address = Right'Address then
procedure Process (L_Node : Node_Access) is
begin
- if Is_In (Right.HT, L_Node) then
+ if Is_In (Right_HT, L_Node) then
declare
+ -- Per AI05-0022, the container implementation is required
+ -- to detect element tampering by a generic actual
+ -- subprogram, hence the use of Checked_Index instead of a
+ -- simple invocation of generic formal Hash.
+
J : constant Hash_Type :=
- Hash (L_Node.Element) mod Buckets'Length;
+ HT_Ops.Checked_Index (Left_HT, Buckets.all, L_Node);
Bucket : Node_Access renames Buckets (J);
-- Start of processing for Iterate_Left
begin
- Iterate (Left.HT);
+ Iterate (Left_HT);
exception
when others =>
HT_Ops.Free_Hash_Table (Buckets);
-- Is_In --
-----------
- function Is_In (HT : Hash_Table_Type; Key : Node_Access) return Boolean is
+ function Is_In
+ (HT : aliased in out Hash_Table_Type;
+ Key : Node_Access) return Boolean
+ is
begin
return Element_Keys.Find (HT, Key.Element) /= null;
end Is_In;
---------------
function Is_Subset (Subset : Set; Of_Set : Set) return Boolean is
+ Subset_HT : Hash_Table_Type renames Subset'Unrestricted_Access.HT;
+ Of_Set_HT : Hash_Table_Type renames Of_Set'Unrestricted_Access.HT;
Subset_Node : Node_Access;
begin
return False;
end if;
- Subset_Node := HT_Ops.First (Subset.HT);
+ Subset_Node := HT_Ops.First (Subset_HT);
while Subset_Node /= null loop
- if not Is_In (Of_Set.HT, Subset_Node) then
+ if not Is_In (Of_Set_HT, Subset_Node) then
return False;
end if;
- Subset_Node := HT_Ops.Next (Subset.HT, Subset_Node);
+ Subset_Node := HT_Ops.Next (Subset_HT, Subset_Node);
end loop;
return True;
-------------
function Overlap (Left, Right : Set) return Boolean is
+ Left_HT : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+ Right_HT : Hash_Table_Type renames Right'Unrestricted_Access.HT;
Left_Node : Node_Access;
begin
return True;
end if;
- Left_Node := HT_Ops.First (Left.HT);
+ Left_Node := HT_Ops.First (Left_HT);
while Left_Node /= null loop
- if Is_In (Right.HT, Left_Node) then
+ if Is_In (Right_HT, Left_Node) then
return True;
end if;
- Left_Node := HT_Ops.Next (Left.HT, Left_Node);
+ Left_Node := HT_Ops.Next (Left_HT, Left_Node);
end loop;
return False;
(Target : in out Set;
Source : Set)
is
+ Tgt_HT : Hash_Table_Type renames Target.HT;
+ Src_HT : Hash_Table_Type renames Source.HT'Unrestricted_Access.all;
+
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
+
+ TB : Natural renames Tgt_HT.Busy;
+ TL : Natural renames Tgt_HT.Lock;
+
+ SB : Natural renames Src_HT.Busy;
+ SL : Natural renames Src_HT.Lock;
+
begin
if Target'Address = Source'Address then
Clear (Target);
return;
end if;
- if Target.HT.Busy > 0 then
+ if TB > 0 then
raise Program_Error with
"attempt to tamper with cursors (set is busy)";
end if;
declare
N : constant Count_Type := Target.Length + Source.Length;
begin
- if N > HT_Ops.Capacity (Target.HT) then
- HT_Ops.Reserve_Capacity (Target.HT, N);
+ if N > HT_Ops.Capacity (Tgt_HT) then
+ HT_Ops.Reserve_Capacity (Tgt_HT, N);
end if;
end;
procedure Process (Src_Node : Node_Access) is
E : Element_Type renames Src_Node.Element;
- B : Buckets_Type renames Target.HT.Buckets.all;
+ B : Buckets_Type renames Tgt_HT.Buckets.all;
J : constant Hash_Type := Hash (E) mod B'Length;
- N : Count_Type renames Target.HT.Length;
+ N : Count_Type renames Tgt_HT.Length;
begin
B (J) := new Node_Type'(E, B (J));
-- Start of processing for Iterate_Source_When_Empty_Target
begin
- Iterate (Source.HT);
+ TB := TB + 1;
+ TL := TL + 1;
+
+ SB := SB + 1;
+ SL := SL + 1;
+
+ Iterate (Src_HT);
+
+ SL := SL - 1;
+ SB := SB - 1;
+
+ TL := TL - 1;
+ TB := TB - 1;
+
+ exception
+ when others =>
+ SL := SL - 1;
+ SB := SB - 1;
+
+ TL := TL - 1;
+ TB := TB - 1;
+
+ raise;
end Iterate_Source_When_Empty_Target;
else
procedure Process (Src_Node : Node_Access) is
E : Element_Type renames Src_Node.Element;
- B : Buckets_Type renames Target.HT.Buckets.all;
+ B : Buckets_Type renames Tgt_HT.Buckets.all;
J : constant Hash_Type := Hash (E) mod B'Length;
- N : Count_Type renames Target.HT.Length;
+ N : Count_Type renames Tgt_HT.Length;
begin
if B (J) = null then
-- Start of processing for Iterate_Source
begin
- Iterate (Source.HT);
+ TB := TB + 1;
+ TL := TL + 1;
+
+ SB := SB + 1;
+ SL := SL + 1;
+
+ Iterate (Src_HT);
+
+ SL := SL - 1;
+ SB := SB - 1;
+
+ TL := TL - 1;
+ TB := TB - 1;
+
+ exception
+ when others =>
+ SL := SL - 1;
+ SB := SB - 1;
+
+ TL := TL - 1;
+ TB := TB - 1;
+
+ raise;
end Iterate_Source;
end if;
end Symmetric_Difference;
function Symmetric_Difference (Left, Right : Set) return Set is
- Buckets : HT_Types.Buckets_Access;
- Length : Count_Type;
+ Left_HT : Hash_Table_Type renames Left'Unrestricted_Access.HT;
+ Right_HT : Hash_Table_Type renames Right'Unrestricted_Access.HT;
+ Buckets : HT_Types.Buckets_Access;
+ Length : Count_Type;
begin
if Left'Address = Right'Address then
procedure Process (L_Node : Node_Access) is
begin
- if not Is_In (Right.HT, L_Node) then
+ if not Is_In (Right_HT, L_Node) then
declare
E : Element_Type renames L_Node.Element;
- J : constant Hash_Type := Hash (E) mod Buckets'Length;
+
+ -- Per AI05-0022, the container implementation is required
+ -- to detect element tampering by a generic actual
+ -- subprogram, hence the use of Checked_Index instead of a
+ -- simple invocation of generic formal Hash.
+
+ J : constant Hash_Type :=
+ HT_Ops.Checked_Index (Left_HT, Buckets.all, L_Node);
begin
Buckets (J) := new Node_Type'(E, Buckets (J));
-- Start of processing for Iterate_Left
begin
- Iterate (Left.HT);
+ Iterate (Left_HT);
exception
when others =>
HT_Ops.Free_Hash_Table (Buckets);
procedure Process (R_Node : Node_Access) is
begin
- if not Is_In (Left.HT, R_Node) then
+ if not Is_In (Left_HT, R_Node) then
declare
E : Element_Type renames R_Node.Element;
- J : constant Hash_Type := Hash (E) mod Buckets'Length;
+
+ -- Per AI05-0022, the container implementation is required
+ -- to detect element tampering by a generic actual
+ -- subprogram, hence the use of Checked_Index instead of a
+ -- simple invocation of generic formal Hash.
+
+ J : constant Hash_Type :=
+ HT_Ops.Checked_Index (Right_HT, Buckets.all, R_Node);
begin
Buckets (J) := new Node_Type'(E, Buckets (J));
-- Start of processing for Iterate_Right
begin
- Iterate (Right.HT);
+ Iterate (Right_HT);
exception
when others =>
HT_Ops.Free_Hash_Table (Buckets);
end Union;
function Union (Left, Right : Set) return Set is
- Buckets : HT_Types.Buckets_Access;
- Length : Count_Type;
+ Left_HT : Hash_Table_Type renames Left.HT'Unrestricted_Access.all;
+ Right_HT : Hash_Table_Type renames Right.HT'Unrestricted_Access.all;
+ Buckets : HT_Types.Buckets_Access;
+ Length : Count_Type;
begin
if Left'Address = Right'Address then
Buckets (J) := new Node_Type'(L_Node.Element, Buckets (J));
end Process;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram, hence the use of
+ -- Checked_Index instead of a simple invocation of generic formal
+ -- Hash.
+
+ B : Integer renames Left_HT.Busy;
+ L : Integer renames Left_HT.Lock;
+
-- Start of processing for Iterate_Left
begin
- Iterate (Left.HT);
+ B := B + 1;
+ L := L + 1;
+
+ Iterate (Left_HT);
+
+ L := L - 1;
+ B := B - 1;
exception
when others =>
+ L := L - 1;
+ B := B - 1;
+
HT_Ops.Free_Hash_Table (Buckets);
raise;
end Iterate_Left;
Length := Length + 1;
end Process;
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram, hence the use of
+ -- Checked_Index instead of a simple invocation of generic formal
+ -- Hash.
+
+ LB : Integer renames Left_HT.Busy;
+ LL : Integer renames Left_HT.Lock;
+
+ RB : Integer renames Right_HT.Busy;
+ RL : Integer renames Right_HT.Lock;
+
-- Start of processing for Iterate_Right
begin
- Iterate (Right.HT);
+ LB := LB + 1;
+ LL := LL + 1;
+
+ RB := RB + 1;
+ RL := RL + 1;
+
+ Iterate (Right_HT);
+
+ RL := RL - 1;
+ RB := RB - 1;
+
+ LL := LL - 1;
+ LB := LB - 1;
exception
when others =>
+ RL := RL - 1;
+ RB := RB - 1;
+
+ LL := LL - 1;
+ LB := LB - 1;
+
HT_Ops.Free_Hash_Table (Buckets);
raise;
end Iterate_Right;
return False;
end if;
- X := HT.Buckets (Element_Keys.Index (HT, Position.Node.Element));
+ X := HT.Buckets (Element_Keys.Checked_Index
+ (HT,
+ Position.Node.Element));
for J in 1 .. HT.Length loop
if X = Position.Node then
(Container : aliased Set;
Key : Key_Type) return Constant_Reference_Type
is
- Node : constant Node_Access := Key_Keys.Find (Container.HT, Key);
+ HT : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+ Node : constant Node_Access := Key_Keys.Find (HT, Key);
begin
if Node = null then
end if;
declare
- HT : Hash_Table_Type renames Container'Unrestricted_Access.all.HT;
B : Natural renames HT.Busy;
L : Natural renames HT.Lock;
begin
(Container : Set;
Key : Key_Type) return Element_Type
is
- Node : constant Node_Access := Key_Keys.Find (Container.HT, Key);
+ HT : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+ Node : constant Node_Access := Key_Keys.Find (HT, Key);
begin
if Node = null then
- raise Constraint_Error with "key not in map"; -- ??? "set"
+ raise Constraint_Error with "key not in set";
end if;
return Node.Element;
(Container : Set;
Key : Key_Type) return Cursor
is
- Node : constant Node_Access := Key_Keys.Find (Container.HT, Key);
+ HT : Hash_Table_Type renames Container'Unrestricted_Access.HT;
+ Node : constant Node_Access := Key_Keys.Find (HT, Key);
begin
if Node = null then
(Vet (Position),
"bad cursor in Update_Element_Preserving_Key");
- Indx := HT_Ops.Index (HT, Position.Node);
+ -- Per AI05-0022, the container implementation is required to detect
+ -- element tampering by a generic actual subprogram.
declare
E : Element_Type renames Position.Node.Element;
B : Natural renames HT.Busy;
L : Natural renames HT.Lock;
+ Eq : Boolean;
+
begin
B := B + 1;
L := L + 1;
begin
+ Indx := HT_Ops.Index (HT, Position.Node);
Process (E);
+ Eq := Equivalent_Keys (K, Key (E));
exception
when others =>
L := L - 1;
L := L - 1;
B := B - 1;
- if Equivalent_Keys (K, Key (E)) then
- pragma Assert (Hash (K) = Hash (E));
+ if Eq then
return;
end if;
end;
elsif not Is_Switch (Argv) then
Add_File (Argv);
+ -- We must recognize -nostdinc to suppress visibility on the
+ -- standard GNAT RTL sources.
+
+ elsif Argv (Argv'First + 1 .. Argv'Last) = "nostdinc" then
+ Opt.No_Stdinc := True;
+
-- Front end switch
elsif Is_Front_End_Switch (Argv) then
@end smallexample
@noindent
-This pragma provides an efficient way of providing stream functions for
-types defined in packages. Not only is it simpler to use than declaring
-the necessary functions with attribute representation clauses, but more
-significantly, it allows the declaration to made in such a way that the
-stream packages are not loaded unless they are needed. The use of
+This pragma provides an efficient way of providing user-defined stream
+attributes. Not only is it simpler to use than specifying the attributes
+directly, but more importantly, it allows the specification to be made in such
+a way that the predefined unit Ada.Streams is not loaded unless it is actually
+needed (i.e. unless the stream attributes are actually used); the use of
the Stream_Convert pragma adds no overhead at all, unless the stream
attributes are actually used on the designated type.
--------------------------------------------
procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id) is
- Pack_Id : constant Entity_Id := Defining_Entity (Parent (Parent (N)));
- Prag_Init : constant Node_Id :=
- Get_Pragma (Pack_Id, Pragma_Initializes);
- -- The related pragma Initializes
-
- Vars : Elist_Id := No_Elist;
- -- A list of all variables declared in pragma Initializes
-
- procedure Collect_Variables;
- -- Inspect the initialization list of pragma Initializes and collect the
- -- entities of all variables declared within the related package.
-
- function Match_Variable (N : Node_Id) return Traverse_Result;
- -- Determine whether arbitrary node N denotes a variable declared in the
- -- visible declarations of the related package.
-
- procedure Report_Unused_Variables;
- -- Emit errors for all variables found in list Vars
-
- -----------------------
- -- Collect_Variables --
- -----------------------
-
- procedure Collect_Variables is
- procedure Collect_Variable (Item : Node_Id);
- -- Determine whether Item denotes a variable that appears in the
- -- related package and if it does, add it to list Vars.
-
- ----------------------
- -- Collect_Variable --
- ----------------------
-
- procedure Collect_Variable (Item : Node_Id) is
- Item_Id : Entity_Id;
-
- begin
- if Is_Entity_Name (Item) and then Present (Entity (Item)) then
- Item_Id := Entity (Item);
-
- -- The item is a variable declared in the related package
-
- if Ekind (Item_Id) = E_Variable
- and then Scope (Item_Id) = Pack_Id
- then
- Add_Item (Item_Id, Vars);
- end if;
- end if;
- end Collect_Variable;
-
- -- Local variables
-
- Inits : constant Node_Id :=
- Get_Pragma_Arg
- (First (Pragma_Argument_Associations (Prag_Init)));
- Init : Node_Id;
-
- -- Start of processing for Collect_Variables
-
- begin
- -- Multiple initialization items appear as an aggregate
-
- if Nkind (Inits) = N_Aggregate
- and then Present (Expressions (Inits))
- then
- Init := First (Expressions (Inits));
- while Present (Init) loop
- Collect_Variable (Init);
-
- Next (Init);
- end loop;
-
- -- Single initialization item
-
- else
- Collect_Variable (Inits);
- end if;
- end Collect_Variables;
-
- --------------------
- -- Match_Variable --
- --------------------
-
- function Match_Variable (N : Node_Id) return Traverse_Result is
- Var_Id : Entity_Id;
-
- begin
- -- Find a variable declared within the related package and try to
- -- remove it from the list of collected variables found in pragma
- -- Initializes.
-
- if Is_Entity_Name (N)
- and then Present (Entity (N))
- then
- Var_Id := Entity (N);
-
- if Ekind (Var_Id) = E_Variable
- and then Scope (Var_Id) = Pack_Id
- then
- Remove (Vars, Var_Id);
- end if;
- end if;
-
- return OK;
- end Match_Variable;
-
- procedure Match_Variables is new Traverse_Proc (Match_Variable);
-
- -----------------------------
- -- Report_Unused_Variables --
- -----------------------------
-
- procedure Report_Unused_Variables is
- Posted : Boolean := False;
- Var_Elmt : Elmt_Id;
- Var_Id : Entity_Id;
-
- begin
- if Present (Vars) then
- Var_Elmt := First_Elmt (Vars);
- while Present (Var_Elmt) loop
- Var_Id := Node (Var_Elmt);
-
- if not Posted then
- Posted := True;
- Error_Msg_Name_1 := Name_Initial_Condition;
- Error_Msg_N
- ("expression of % must mention the following variables",
- N);
- end if;
-
- Error_Msg_Sloc := Sloc (Var_Id);
- Error_Msg_NE ("\ & declared #", N, Var_Id);
-
- Next_Elmt (Var_Elmt);
- end loop;
- end if;
- end Report_Unused_Variables;
-
- Expr : constant Node_Id :=
- Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
- Errors : constant Nat := Serious_Errors_Detected;
-
- -- Start of processing for Analyze_Initial_Condition_In_Decl_Part
+ Expr : constant Node_Id :=
+ Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
begin
Set_Analyzed (N);
- -- Pragma Initial_Condition depends on the names enumerated in pragma
- -- Initializes. Without those, the analysis cannot take place.
-
- if No (Prag_Init) then
- Error_Msg_Name_1 := Name_Initial_Condition;
- Error_Msg_Name_2 := Name_Initializes;
-
- Error_Msg_N ("% requires the presence of aspect or pragma %", N);
- return;
- end if;
-
-- The expression is preanalyzed because it has not been moved to its
-- final place yet. A direct analysis may generate side effects and this
-- is not desired at this point.
Preanalyze_And_Resolve (Expr, Standard_Boolean);
-
- -- Perform variable matching only when the expression is legal
-
- if Serious_Errors_Detected = Errors then
- Collect_Variables;
-
- -- Verify that all variables mentioned in pragma Initializes are used
- -- in the expression of pragma Initial_Condition.
-
- Match_Variables (Expr);
- end if;
-
- -- Emit errors for all variables that should participate in the
- -- expression of pragma Initial_Condition.
-
- if Serious_Errors_Detected = Errors then
- Report_Unused_Variables;
- end if;
end Analyze_Initial_Condition_In_Decl_Part;
--------------------------------------
(Def_Id : Entity_Id;
Loc : Source_Ptr) return Node_Id
is
+ pragma Assert (Present (Def_Id) and then Nkind (Def_Id) in N_Entity);
Occurrence : Node_Id;
begin
(Def_Id : Entity_Id;
Loc : Source_Ptr) return Node_Id
is
- pragma Assert (Nkind (Def_Id) in N_Entity);
+ pragma Assert (Present (Def_Id) and then Nkind (Def_Id) in N_Entity);
Occurrence : Node_Id;
begin
Occurrence := New_Node (N_Identifier, Loc);
projects / platform / upstream / linaro-gcc.git / commitdiff