gcc/ada/libgnat/a-cfhama.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT LIBRARY COMPONENTS                          --
   4 --                                                                          --
   5 --    A D A . C O N T A I N E R S . F O R M A L _ H A S H E D _ M A P S     --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2010-2017, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  12 -- terms of the  GNU General Public License as published  by the Free Soft- --
  13 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  14 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  15 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  16 -- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
  17 --                                                                          --
  18 -- As a special exception under Section 7 of GPL version 3, you are granted --
  19 -- additional permissions described in the GCC Runtime Library Exception,   --
  20 -- version 3.1, as published by the Free Software Foundation.               --
  21 --                                                                          --
  22 -- You should have received a copy of the GNU General Public License and    --
  23 -- a copy of the GCC Runtime Library Exception along with this program;     --
  24 -- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
  25 -- <http://www.gnu.org/licenses/>.                                          --
  26 ------------------------------------------------------------------------------
  27
  28 with Ada.Containers.Hash_Tables.Generic_Bounded_Operations;
  29 pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Operations);
  30
  31 with Ada.Containers.Hash_Tables.Generic_Bounded_Keys;
  32 pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Bounded_Keys);
  33
  34 with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers;
  35
  36 with System; use type System.Address;
  37
  38 package body Ada.Containers.Formal_Hashed_Maps with
  39   SPARK_Mode => Off
  40 is
  41    -----------------------
  42    -- Local Subprograms --
  43    -----------------------
  44
  45    --  All local subprograms require comments ???
  46
  47    function Equivalent_Keys
  48      (Key  : Key_Type;
  49       Node : Node_Type) return Boolean;
  50    pragma Inline (Equivalent_Keys);
  51
  52    procedure Free
  53      (HT : in out Map;
  54       X  : Count_Type);
  55
  56    generic
  57       with procedure Set_Element (Node : in out Node_Type);
  58    procedure Generic_Allocate
  59      (HT   : in out Map;
  60       Node : out Count_Type);
  61
  62    function Hash_Node (Node : Node_Type) return Hash_Type;
  63    pragma Inline (Hash_Node);
  64
  65    function Next (Node : Node_Type) return Count_Type;
  66    pragma Inline (Next);
  67
  68    procedure Set_Next (Node : in out Node_Type; Next : Count_Type);
  69    pragma Inline (Set_Next);
  70
  71    function Vet (Container : Map; Position : Cursor) return Boolean;
  72
  73    --------------------------
  74    -- Local Instantiations --
  75    --------------------------
  76
  77    package HT_Ops is
  78      new Hash_Tables.Generic_Bounded_Operations
  79        (HT_Types  => HT_Types,
  80         Hash_Node => Hash_Node,
  81         Next      => Next,
  82         Set_Next  => Set_Next);
  83
  84    package Key_Ops is
  85      new Hash_Tables.Generic_Bounded_Keys
  86        (HT_Types        => HT_Types,
  87         Next            => Next,
  88         Set_Next        => Set_Next,
  89         Key_Type        => Key_Type,
  90         Hash            => Hash,
  91         Equivalent_Keys => Equivalent_Keys);
  92
  93    ---------
  94    -- "=" --
  95    ---------
  96
  97    function "=" (Left, Right : Map) return Boolean is
  98    begin
  99       if Length (Left) /= Length (Right) then
 100          return False;
 101       end if;
 102
 103       if Length (Left) = 0 then
 104          return True;
 105       end if;
 106
 107       declare
 108          Node  : Count_Type;
 109          ENode : Count_Type;
 110
 111       begin
 112          Node := Left.First.Node;
 113          while Node /= 0 loop
 114             ENode :=
 115               Find
 116                 (Container => Right,
 117                  Key       => Left.Nodes (Node).Key).Node;
 118
 119             if ENode = 0 or else
 120               Right.Nodes (ENode).Element /= Left.Nodes (Node).Element
 121             then
 122                return False;
 123             end if;
 124
 125             Node := HT_Ops.Next (Left, Node);
 126          end loop;
 127
 128          return True;
 129       end;
 130    end "=";
 131
 132    ------------
 133    -- Assign --
 134    ------------
 135
 136    procedure Assign (Target : in out Map; Source : Map) is
 137       procedure Insert_Element (Source_Node : Count_Type);
 138       pragma Inline (Insert_Element);
 139
 140       procedure Insert_Elements is
 141         new HT_Ops.Generic_Iteration (Insert_Element);
 142
 143       --------------------
 144       -- Insert_Element --
 145       --------------------
 146
 147       procedure Insert_Element (Source_Node : Count_Type) is
 148          N : Node_Type renames Source.Nodes (Source_Node);
 149       begin
 150          Insert (Target, N.Key, N.Element);
 151       end Insert_Element;
 152
 153       --  Start of processing for Assign
 154
 155    begin
 156       if Target'Address = Source'Address then
 157          return;
 158       end if;
 159
 160       if Target.Capacity < Length (Source) then
 161          raise Constraint_Error with  -- correct exception ???
 162            "Source length exceeds Target capacity";
 163       end if;
 164
 165       Clear (Target);
 166
 167       Insert_Elements (Source);
 168    end Assign;
 169
 170    --------------
 171    -- Capacity --
 172    --------------
 173
 174    function Capacity (Container : Map) return Count_Type is
 175    begin
 176       return Container.Nodes'Length;
 177    end Capacity;
 178
 179    -----------
 180    -- Clear --
 181    -----------
 182
 183    procedure Clear (Container : in out Map) is
 184    begin
 185       HT_Ops.Clear (Container);
 186    end Clear;
 187
 188    --------------
 189    -- Contains --
 190    --------------
 191
 192    function Contains (Container : Map; Key : Key_Type) return Boolean is
 193    begin
 194       return Find (Container, Key) /= No_Element;
 195    end Contains;
 196
 197    ----------
 198    -- Copy --
 199    ----------
 200
 201    function Copy
 202      (Source   : Map;
 203       Capacity : Count_Type := 0) return Map
 204    is
 205       C      : constant Count_Type :=
 206                  Count_Type'Max (Capacity, Source.Capacity);
 207       Cu     : Cursor;
 208       H      : Hash_Type;
 209       N      : Count_Type;
 210       Target : Map (C, Source.Modulus);
 211
 212    begin
 213       if 0 < Capacity and then Capacity < Source.Capacity then
 214          raise Capacity_Error;
 215       end if;
 216
 217       Target.Length := Source.Length;
 218       Target.Free := Source.Free;
 219
 220       H := 1;
 221       while H <= Source.Modulus loop
 222          Target.Buckets (H) := Source.Buckets (H);
 223          H := H + 1;
 224       end loop;
 225
 226       N := 1;
 227       while N <= Source.Capacity loop
 228          Target.Nodes (N) := Source.Nodes (N);
 229          N := N + 1;
 230       end loop;
 231
 232       while N <= C loop
 233          Cu := (Node => N);
 234          Free (Target, Cu.Node);
 235          N := N + 1;
 236       end loop;
 237
 238       return Target;
 239    end Copy;
 240
 241    ---------------------
 242    -- Default_Modulus --
 243    ---------------------
 244
 245    function Default_Modulus (Capacity : Count_Type) return Hash_Type is
 246    begin
 247       return To_Prime (Capacity);
 248    end Default_Modulus;
 249
 250    ------------
 251    -- Delete --
 252    ------------
 253
 254    procedure Delete (Container : in out Map; Key : Key_Type) is
 255       X : Count_Type;
 256
 257    begin
 258       Key_Ops.Delete_Key_Sans_Free (Container, Key, X);
 259
 260       if X = 0 then
 261          raise Constraint_Error with "attempt to delete key not in map";
 262       end if;
 263
 264       Free (Container, X);
 265    end Delete;
 266
 267    procedure Delete (Container : in out Map; Position : in out Cursor) is
 268    begin
 269       if not Has_Element (Container, Position) then
 270          raise Constraint_Error with
 271            "Position cursor of Delete has no element";
 272       end if;
 273
 274       pragma Assert (Vet (Container, Position), "bad cursor in Delete");
 275
 276       HT_Ops.Delete_Node_Sans_Free (Container, Position.Node);
 277
 278       Free (Container, Position.Node);
 279       Position := No_Element;
 280    end Delete;
 281
 282    -------------
 283    -- Element --
 284    -------------
 285
 286    function Element (Container : Map; Key : Key_Type) return Element_Type is
 287       Node : constant Count_Type := Find (Container, Key).Node;
 288
 289    begin
 290       if Node = 0 then
 291          raise Constraint_Error with
 292            "no element available because key not in map";
 293       end if;
 294
 295       return Container.Nodes (Node).Element;
 296    end Element;
 297
 298    function Element (Container : Map; Position : Cursor) return Element_Type is
 299    begin
 300       if not Has_Element (Container, Position) then
 301          raise Constraint_Error with "Position cursor equals No_Element";
 302       end if;
 303
 304       pragma Assert
 305         (Vet (Container, Position), "bad cursor in function Element");
 306
 307       return Container.Nodes (Position.Node).Element;
 308    end Element;
 309
 310    ---------------------
 311    -- Equivalent_Keys --
 312    ---------------------
 313
 314    function Equivalent_Keys
 315      (Key  : Key_Type;
 316       Node : Node_Type) return Boolean
 317    is
 318    begin
 319       return Equivalent_Keys (Key, Node.Key);
 320    end Equivalent_Keys;
 321
 322    -------------
 323    -- Exclude --
 324    -------------
 325
 326    procedure Exclude (Container : in out Map; Key : Key_Type) is
 327       X : Count_Type;
 328    begin
 329       Key_Ops.Delete_Key_Sans_Free (Container, Key, X);
 330       Free (Container, X);
 331    end Exclude;
 332
 333    ----------
 334    -- Find --
 335    ----------
 336
 337    function Find (Container : Map; Key : Key_Type) return Cursor is
 338       Node : constant Count_Type := Key_Ops.Find (Container, Key);
 339
 340    begin
 341       if Node = 0 then
 342          return No_Element;
 343       end if;
 344
 345       return (Node => Node);
 346    end Find;
 347
 348    -----------
 349    -- First --
 350    -----------
 351
 352    function First (Container : Map) return Cursor is
 353       Node : constant Count_Type := HT_Ops.First (Container);
 354
 355    begin
 356       if Node = 0 then
 357          return No_Element;
 358       end if;
 359
 360       return (Node => Node);
 361    end First;
 362
 363    ------------------
 364    -- Formal_Model --
 365    ------------------
 366
 367    package body Formal_Model is
 368
 369       ----------
 370       -- Find --
 371       ----------
 372
 373       function Find
 374         (Container : K.Sequence;
 375          Key       : Key_Type) return Count_Type
 376       is
 377       begin
 378          for I in 1 .. K.Length (Container) loop
 379             if Equivalent_Keys (Key, K.Get (Container, I)) then
 380                return I;
 381             end if;
 382          end loop;
 383          return 0;
 384       end Find;
 385
 386       ---------------------
 387       -- K_Keys_Included --
 388       ---------------------
 389
 390       function K_Keys_Included
 391         (Left  : K.Sequence;
 392          Right : K.Sequence) return Boolean
 393       is
 394       begin
 395          for I in 1 .. K.Length (Left) loop
 396             if not K.Contains (Right, 1, K.Length (Right), K.Get (Left, I))
 397             then
 398                return False;
 399             end if;
 400          end loop;
 401
 402          return True;
 403       end K_Keys_Included;
 404
 405       ----------
 406       -- Keys --
 407       ----------
 408
 409       function Keys (Container : Map) return K.Sequence is
 410          Position : Count_Type := HT_Ops.First (Container);
 411          R        : K.Sequence;
 412
 413       begin
 414          --  Can't use First, Next or Element here, since they depend on models
 415          --  for their postconditions.
 416
 417          while Position /= 0 loop
 418             R := K.Add (R, Container.Nodes (Position).Key);
 419             Position := HT_Ops.Next (Container, Position);
 420          end loop;
 421
 422          return R;
 423       end Keys;
 424
 425       ----------------------------
 426       -- Lift_Abstraction_Level --
 427       ----------------------------
 428
 429       procedure Lift_Abstraction_Level (Container : Map) is null;
 430
 431       -----------------------
 432       -- Mapping_preserved --
 433       -----------------------
 434
 435       function Mapping_Preserved
 436         (K_Left  : K.Sequence;
 437          K_Right : K.Sequence;
 438          P_Left  : P.Map;
 439          P_Right : P.Map) return Boolean
 440       is
 441       begin
 442          for C of P_Left loop
 443             if not P.Has_Key (P_Right, C)
 444               or else P.Get (P_Left,  C) > K.Length (K_Left)
 445               or else P.Get (P_Right, C) > K.Length (K_Right)
 446               or else K.Get (K_Left,  P.Get (P_Left,  C)) /=
 447                       K.Get (K_Right, P.Get (P_Right, C))
 448             then
 449                return False;
 450             end if;
 451          end loop;
 452
 453          return True;
 454       end Mapping_Preserved;
 455
 456       -----------
 457       -- Model --
 458       -----------
 459
 460       function Model (Container : Map) return M.Map is
 461          Position : Count_Type := HT_Ops.First (Container);
 462          R        : M.Map;
 463
 464       begin
 465          --  Can't use First, Next or Element here, since they depend on models
 466          --  for their postconditions.
 467
 468          while Position /= 0 loop
 469             R :=
 470               M.Add
 471                 (Container => R,
 472                  New_Key   => Container.Nodes (Position).Key,
 473                  New_Item  => Container.Nodes (Position).Element);
 474
 475             Position := HT_Ops.Next (Container, Position);
 476          end loop;
 477
 478          return R;
 479       end Model;
 480
 481       ---------------
 482       -- Positions --
 483       ---------------
 484
 485       function Positions (Container : Map) return P.Map is
 486          I        : Count_Type := 1;
 487          Position : Count_Type := HT_Ops.First (Container);
 488          R        : P.Map;
 489
 490       begin
 491          --  Can't use First, Next or Element here, since they depend on models
 492          --  for their postconditions.
 493
 494          while Position /= 0 loop
 495             R := P.Add (R, (Node => Position), I);
 496             pragma Assert (P.Length (R) = I);
 497             Position := HT_Ops.Next (Container, Position);
 498             I := I + 1;
 499          end loop;
 500
 501          return R;
 502       end Positions;
 503
 504    end Formal_Model;
 505
 506    ----------
 507    -- Free --
 508    ----------
 509
 510    procedure Free (HT : in out Map; X : Count_Type) is
 511    begin
 512       HT.Nodes (X).Has_Element := False;
 513       HT_Ops.Free (HT, X);
 514    end Free;
 515
 516    ----------------------
 517    -- Generic_Allocate --
 518    ----------------------
 519
 520    procedure Generic_Allocate (HT : in out Map; Node : out Count_Type) is
 521       procedure Allocate is
 522         new HT_Ops.Generic_Allocate (Set_Element);
 523
 524    begin
 525       Allocate (HT, Node);
 526       HT.Nodes (Node).Has_Element := True;
 527    end Generic_Allocate;
 528
 529    -----------------
 530    -- Has_Element --
 531    -----------------
 532
 533    function Has_Element (Container : Map; Position : Cursor) return Boolean is
 534    begin
 535       if Position.Node = 0
 536         or else not Container.Nodes (Position.Node).Has_Element
 537       then
 538          return False;
 539       else
 540          return True;
 541       end if;
 542    end Has_Element;
 543
 544    ---------------
 545    -- Hash_Node --
 546    ---------------
 547
 548    function Hash_Node (Node : Node_Type) return Hash_Type is
 549    begin
 550       return Hash (Node.Key);
 551    end Hash_Node;
 552
 553    -------------
 554    -- Include --
 555    -------------
 556
 557    procedure Include
 558      (Container : in out Map;
 559       Key       : Key_Type;
 560       New_Item  : Element_Type)
 561    is
 562       Position : Cursor;
 563       Inserted : Boolean;
 564
 565    begin
 566       Insert (Container, Key, New_Item, Position, Inserted);
 567
 568       if not Inserted then
 569          declare
 570             N : Node_Type renames Container.Nodes (Position.Node);
 571          begin
 572             N.Key := Key;
 573             N.Element := New_Item;
 574          end;
 575       end if;
 576    end Include;
 577
 578    ------------
 579    -- Insert --
 580    ------------
 581
 582    procedure Insert
 583      (Container : in out Map;
 584       Key       : Key_Type;
 585       New_Item  : Element_Type;
 586       Position  : out Cursor;
 587       Inserted  : out Boolean)
 588    is
 589       procedure Assign_Key (Node : in out Node_Type);
 590       pragma Inline (Assign_Key);
 591
 592       function New_Node return Count_Type;
 593       pragma Inline (New_Node);
 594
 595       procedure Local_Insert is
 596         new Key_Ops.Generic_Conditional_Insert (New_Node);
 597
 598       procedure Allocate is
 599         new Generic_Allocate (Assign_Key);
 600
 601       -----------------
 602       --  Assign_Key --
 603       -----------------
 604
 605       procedure Assign_Key (Node : in out Node_Type) is
 606       begin
 607          Node.Key := Key;
 608          Node.Element := New_Item;
 609       end Assign_Key;
 610
 611       --------------
 612       -- New_Node --
 613       --------------
 614
 615       function New_Node return Count_Type is
 616          Result : Count_Type;
 617       begin
 618          Allocate (Container, Result);
 619          return Result;
 620       end New_Node;
 621
 622    --  Start of processing for Insert
 623
 624    begin
 625       Local_Insert (Container, Key, Position.Node, Inserted);
 626    end Insert;
 627
 628    procedure Insert
 629      (Container : in out Map;
 630       Key       : Key_Type;
 631       New_Item  : Element_Type)
 632    is
 633       Position : Cursor;
 634       pragma Unreferenced (Position);
 635
 636       Inserted : Boolean;
 637
 638    begin
 639       Insert (Container, Key, New_Item, Position, Inserted);
 640
 641       if not Inserted then
 642          raise Constraint_Error with "attempt to insert key already in map";
 643       end if;
 644    end Insert;
 645
 646    --------------
 647    -- Is_Empty --
 648    --------------
 649
 650    function Is_Empty (Container : Map) return Boolean is
 651    begin
 652       return Length (Container) = 0;
 653    end Is_Empty;
 654
 655    ---------
 656    -- Key --
 657    ---------
 658
 659    function Key (Container : Map; Position : Cursor) return Key_Type is
 660    begin
 661       if not Has_Element (Container, Position) then
 662          raise Constraint_Error with
 663            "Position cursor of function Key has no element";
 664       end if;
 665
 666       pragma Assert (Vet (Container, Position), "bad cursor in function Key");
 667
 668       return Container.Nodes (Position.Node).Key;
 669    end Key;
 670
 671    ------------
 672    -- Length --
 673    ------------
 674
 675    function Length (Container : Map) return Count_Type is
 676    begin
 677       return Container.Length;
 678    end Length;
 679
 680    ----------
 681    -- Move --
 682    ----------
 683
 684    procedure Move
 685      (Target : in out Map;
 686       Source : in out Map)
 687    is
 688       NN : HT_Types.Nodes_Type renames Source.Nodes;
 689       X  : Count_Type;
 690       Y  : Count_Type;
 691
 692    begin
 693       if Target'Address = Source'Address then
 694          return;
 695       end if;
 696
 697       if Target.Capacity < Length (Source) then
 698          raise Constraint_Error with  -- ???
 699            "Source length exceeds Target capacity";
 700       end if;
 701
 702       Clear (Target);
 703
 704       if Source.Length = 0 then
 705          return;
 706       end if;
 707
 708       X := HT_Ops.First (Source);
 709       while X /= 0 loop
 710          Insert (Target, NN (X).Key, NN (X).Element);  -- optimize???
 711
 712          Y := HT_Ops.Next (Source, X);
 713
 714          HT_Ops.Delete_Node_Sans_Free (Source, X);
 715          Free (Source, X);
 716
 717          X := Y;
 718       end loop;
 719    end Move;
 720
 721    ----------
 722    -- Next --
 723    ----------
 724
 725    function Next (Node : Node_Type) return Count_Type is
 726    begin
 727       return Node.Next;
 728    end Next;
 729
 730    function Next (Container : Map; Position : Cursor) return Cursor is
 731    begin
 732       if Position.Node = 0 then
 733          return No_Element;
 734       end if;
 735
 736       if not Has_Element (Container, Position) then
 737          raise Constraint_Error with "Position has no element";
 738       end if;
 739
 740       pragma Assert (Vet (Container, Position), "bad cursor in function Next");
 741
 742       declare
 743          Node : constant Count_Type := HT_Ops.Next (Container, Position.Node);
 744
 745       begin
 746          if Node = 0 then
 747             return No_Element;
 748          end if;
 749
 750          return (Node => Node);
 751       end;
 752    end Next;
 753
 754    procedure Next (Container : Map; Position : in out Cursor) is
 755    begin
 756       Position := Next (Container, Position);
 757    end Next;
 758
 759    -------------
 760    -- Replace --
 761    -------------
 762
 763    procedure Replace
 764      (Container : in out Map;
 765       Key       : Key_Type;
 766       New_Item  : Element_Type)
 767    is
 768       Node : constant Count_Type := Key_Ops.Find (Container, Key);
 769
 770    begin
 771       if Node = 0 then
 772          raise Constraint_Error with "attempt to replace key not in map";
 773       end if;
 774
 775       declare
 776          N : Node_Type renames Container.Nodes (Node);
 777       begin
 778          N.Key := Key;
 779          N.Element := New_Item;
 780       end;
 781    end Replace;
 782
 783    ---------------------
 784    -- Replace_Element --
 785    ---------------------
 786
 787    procedure Replace_Element
 788      (Container : in out Map;
 789       Position  : Cursor;
 790       New_Item  : Element_Type)
 791    is
 792    begin
 793       if not Has_Element (Container, Position) then
 794          raise Constraint_Error with
 795            "Position cursor of Replace_Element has no element";
 796       end if;
 797
 798       pragma Assert
 799         (Vet (Container, Position), "bad cursor in Replace_Element");
 800
 801       Container.Nodes (Position.Node).Element := New_Item;
 802    end Replace_Element;
 803
 804    ----------------------
 805    -- Reserve_Capacity --
 806    ----------------------
 807
 808    procedure Reserve_Capacity
 809      (Container : in out Map;
 810       Capacity  : Count_Type)
 811    is
 812    begin
 813       if Capacity > Container.Capacity then
 814          raise Capacity_Error with "requested capacity is too large";
 815       end if;
 816    end Reserve_Capacity;
 817
 818    --------------
 819    -- Set_Next --
 820    --------------
 821
 822    procedure Set_Next (Node : in out Node_Type; Next : Count_Type) is
 823    begin
 824       Node.Next := Next;
 825    end Set_Next;
 826
 827    ---------
 828    -- Vet --
 829    ---------
 830
 831    function Vet (Container : Map; Position : Cursor) return Boolean is
 832    begin
 833       if Position.Node = 0 then
 834          return True;
 835       end if;
 836
 837       declare
 838          X : Count_Type;
 839
 840       begin
 841          if Container.Length = 0 then
 842             return False;
 843          end if;
 844
 845          if Container.Capacity = 0 then
 846             return False;
 847          end if;
 848
 849          if Container.Buckets'Length = 0 then
 850             return False;
 851          end if;
 852
 853          if Position.Node > Container.Capacity then
 854             return False;
 855          end if;
 856
 857          if Container.Nodes (Position.Node).Next = Position.Node then
 858             return False;
 859          end if;
 860
 861          X :=
 862            Container.Buckets
 863              (Key_Ops.Index (Container, Container.Nodes (Position.Node).Key));
 864
 865          for J in 1 .. Container.Length loop
 866             if X = Position.Node then
 867                return True;
 868             end if;
 869
 870             if X = 0 then
 871                return False;
 872             end if;
 873
 874             if X = Container.Nodes (X).Next then
 875
 876                --  Prevent unnecessary looping
 877
 878                return False;
 879             end if;
 880
 881             X := Container.Nodes (X).Next;
 882          end loop;
 883
 884          return False;
 885       end;
 886    end Vet;
 887
 888 end Ada.Containers.Formal_Hashed_Maps;