From de33eb3865a19e2fcc527de18e611de0703cb83a Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 27 Apr 2017 14:09:11 +0200 Subject: [PATCH] [multiple changes] 2017-04-27 Bob Duff * g-dyntab.ads, g-dyntab.adb: Add assertions to subprograms that can reallocate. * atree.adb, elists.adb, fname-uf.adb, ghost.adb, inline.adb, * lib.adb, namet.adb, nlists.adb, sem.adb, sinput.adb, stringt.adb: Reorder code so that above assertions do not fail. * table.ads: Remove obsolete comment on Locked. 2017-04-27 Claire Dross * a-cfdlli.ads: Code cleanup. 2017-04-27 Yannick Moy * exp_spark.adb (Expand_SPARK_Freeze_Type): Build a DIC procedure when needed for proof. (Expand_SPARK): Call the new procedure. * exp_util.ads Fix typo. 2017-04-27 Gary Dismukes * a-cofuma.ads, a-cfhama.ads: Minor reformatting, grammar, and typo fixes. From-SVN: r247323 --- gcc/ada/ChangeLog | 24 ++++++++++++++++++++++++ gcc/ada/a-cfdlli.ads | 4 ++-- gcc/ada/a-cfhama.ads | 42 +++++++++++++++++++++--------------------- gcc/ada/a-cofuma.ads | 2 +- gcc/ada/atree.adb | 8 ++++---- gcc/ada/elists.adb | 6 +++--- gcc/ada/exp_spark.adb | 25 +++++++++++++++++++++++++ gcc/ada/exp_util.ads | 2 +- gcc/ada/fname-uf.adb | 4 ++-- gcc/ada/g-dyntab.adb | 11 +++++++++++ gcc/ada/g-dyntab.ads | 8 ++++---- gcc/ada/ghost.adb | 2 +- gcc/ada/inline.adb | 10 +++++----- gcc/ada/lib.adb | 8 ++++---- gcc/ada/namet.adb | 10 +++++----- gcc/ada/nlists.adb | 10 ++++------ gcc/ada/sem.adb | 2 +- gcc/ada/sinput.adb | 2 +- gcc/ada/stringt.adb | 6 +++--- gcc/ada/table.ads | 8 -------- 20 files changed, 122 insertions(+), 72 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index d68ec0edd37..7c5953fd674 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,27 @@ +2017-04-27 Bob Duff + + * g-dyntab.ads, g-dyntab.adb: Add assertions to subprograms that + can reallocate. + * atree.adb, elists.adb, fname-uf.adb, ghost.adb, inline.adb, + * lib.adb, namet.adb, nlists.adb, sem.adb, sinput.adb, stringt.adb: + Reorder code so that above assertions do not fail. + * table.ads: Remove obsolete comment on Locked. + +2017-04-27 Claire Dross + + * a-cfdlli.ads: Code cleanup. + +2017-04-27 Yannick Moy + + * exp_spark.adb (Expand_SPARK_Freeze_Type): Build a DIC procedure + when needed for proof. (Expand_SPARK): Call the new procedure. + * exp_util.ads Fix typo. + +2017-04-27 Gary Dismukes + + * a-cofuma.ads, a-cfhama.ads: Minor reformatting, grammar, and typo + fixes. + 2017-04-27 Hristian Kirtchev * sem_elab.adb Add new type Visited_Element diff --git a/gcc/ada/a-cfdlli.ads b/gcc/ada/a-cfdlli.ads index 1a83b609499..596af5e4039 100644 --- a/gcc/ada/a-cfdlli.ads +++ b/gcc/ada/a-cfdlli.ads @@ -175,7 +175,7 @@ is -- Big contains all cursors of Small - P.Keys_Included (Small, Big) + (P.Keys_Included (Small, Big) -- Cursors located before Cut are not moved, cursors located -- after are shifted by Count. @@ -191,7 +191,7 @@ is and (for all I of Big => P.Has_Key (Small, I) - or P.Get (Big, I) - Count in Cut - Count .. Cut - 1); + or P.Get (Big, I) - Count in Cut - Count .. Cut - 1)); function P_Positions_Swapped (Left : P.Map; diff --git a/gcc/ada/a-cfhama.ads b/gcc/ada/a-cfhama.ads index bc10de02574..8f982fede25 100644 --- a/gcc/ada/a-cfhama.ads +++ b/gcc/ada/a-cfhama.ads @@ -44,8 +44,8 @@ -- and its previous version C'Old) for expressing properties, which is not -- possible if cursors encapsulate an access to the underlying container. --- Iteration over maps is done using the Iterable aspect which is SPARK --- compatible. For of iteration ranges over keys instead of elements. +-- Iteration over maps is done using the Iterable aspect, which is SPARK +-- compatible. "For of" iteration ranges over keys instead of elements. with Ada.Containers.Functional_Vectors; with Ada.Containers.Functional_Maps; @@ -153,7 +153,7 @@ is K.Get (K_Right, P.Get (P_Right, C)))); function Model (Container : Map) return M.Map with - -- The highlevel model of a map is a map from keys to elements. Neither + -- The high-level model of a map is a map from keys to elements. Neither -- cursors nor order of elements are represented in this model. Keys are -- modeled up to equivalence. @@ -193,14 +193,14 @@ is function Positions (Container : Map) return P.Map with -- The Positions map is used to model cursors. It only contains valid - -- cursors and map them to their position in the container. + -- cursors and maps them to their position in the container. Ghost, Global => null, Post => not P.Has_Key (Positions'Result, No_Element) - -- Positions of cursors are smaller than the container's length. + -- Positions of cursors are smaller than the container's length and then (for all I of Positions'Result => @@ -217,11 +217,11 @@ is procedure Lift_Abstraction_Level (Container : Map) with -- Lift_Abstraction_Level is a ghost procedure that does nothing but - -- assume that we can access to the same elements by iterating over + -- assume that we can access the same elements by iterating over -- positions or cursors. -- This information is not generally useful except when switching from - -- a lowlevel, cursor aware view of a container, to a highlevel - -- position based view. + -- a low-level, cursor-aware view of a container, to a high-level, + -- position-based view. Ghost, Global => null, @@ -328,17 +328,17 @@ is Pre => Has_Element (Container, Position), Post => - -- Order of keys and cursors are preserved + -- Order of keys and cursors is preserved Keys (Container) = Keys (Container)'Old and Positions (Container) = Positions (Container)'Old - -- New_Item is now associated to the key at position Position in + -- New_Item is now associated with the key at position Position in -- Container. and Element (Container, Position) = New_Item - -- Elements associated to other keys are preserved + -- Elements associated with other keys are preserved and M.Same_Keys (Model (Container), Model (Container)'Old) and M.Elements_Equal_Except @@ -405,7 +405,7 @@ is Model (Container)'Old, Key) - -- Mapping from cursors to keys are preserved + -- Mapping from cursors to keys is preserved and Mapping_Preserved (K_Left => Keys (Container)'Old, @@ -443,7 +443,7 @@ is Model (Container)'Old, Key) - -- Mapping from cursors to keys are preserved + -- Mapping from cursors to keys is preserved and Mapping_Preserved (K_Left => Keys (Container)'Old, @@ -485,7 +485,7 @@ is Keys (Container), P.Get (Positions (Container), Find (Container, Key))) - -- Elements associated to other keys are preserved + -- Elements associated with other keys are preserved and M.Same_Keys (Model (Container), Model (Container)'Old) and M.Elements_Equal_Except @@ -506,7 +506,7 @@ is Model (Container)'Old, Key) - -- Mapping from cursors to keys are preserved + -- Mapping from cursors to keys is preserved and Mapping_Preserved (K_Left => Keys (Container)'Old, @@ -540,11 +540,11 @@ is Keys (Container), P.Get (Positions (Container), Find (Container, Key))) - -- New_Item is now associated to the Key in Container + -- New_Item is now associated with the Key in Container and Element (Model (Container), Key) = New_Item - -- Elements associated to other keys are preserved + -- Elements associated with other keys are preserved and M.Same_Keys (Model (Container), Model (Container)'Old) and M.Elements_Equal_Except @@ -577,7 +577,7 @@ is Model (Container), Key) - -- Mapping from cursors to keys are preserved + -- Mapping from cursors to keys is preserved and Mapping_Preserved (K_Left => Keys (Container), @@ -607,7 +607,7 @@ is Model (Container), Key) - -- Mapping from cursors to keys are preserved + -- Mapping from cursors to keys is preserved and Mapping_Preserved (K_Left => Keys (Container), @@ -639,7 +639,7 @@ is Model (Container), Key (Container, Position)'Old) - -- Mapping from cursors to keys are preserved + -- Mapping from cursors to keys is preserved and Mapping_Preserved (K_Left => Keys (Container), @@ -700,7 +700,7 @@ is (not Contains (Model (Container), Key) => Find'Result = No_Element, - -- Otherwise, Find returns a valid cusror in Container + -- Otherwise, Find returns a valid cursor in Container others => P.Has_Key (Positions (Container), Find'Result) diff --git a/gcc/ada/a-cofuma.ads b/gcc/ada/a-cofuma.ads index 1172d118952..3f968dcaeb0 100644 --- a/gcc/ada/a-cofuma.ads +++ b/gcc/ada/a-cofuma.ads @@ -48,7 +48,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is -- Maps are empty when default initialized. -- "For in" quantification over maps should not be used. -- "For of" quantification over maps iterates over keys. - -- Note that, for proof, for of quantification is understood modulo + -- Note that, for proof, "for of" quantification is understood modulo -- equivalence (quantification includes keys equivalent to keys of the -- map). diff --git a/gcc/ada/atree.adb b/gcc/ada/atree.adb index 9137602b15c..0505b86868d 100644 --- a/gcc/ada/atree.adb +++ b/gcc/ada/atree.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2017, 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- -- @@ -1579,12 +1579,12 @@ package body Atree is procedure Lock is begin - Nodes.Locked := True; - Flags.Locked := True; - Orig_Nodes.Locked := True; Nodes.Release; + Nodes.Locked := True; Flags.Release; + Flags.Locked := True; Orig_Nodes.Release; + Orig_Nodes.Locked := True; end Lock; ---------------- diff --git a/gcc/ada/elists.adb b/gcc/ada/elists.adb index c35b51d92db..881d78cc88e 100644 --- a/gcc/ada/elists.adb +++ b/gcc/ada/elists.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2017, 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- -- @@ -320,10 +320,10 @@ package body Elists is procedure Lock is begin - Elists.Locked := True; - Elmts.Locked := True; Elists.Release; + Elists.Locked := True; Elmts.Release; + Elmts.Locked := True; end Lock; -------------------- diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index abc79f3df94..d7f1571a0b3 100644 --- a/gcc/ada/exp_spark.adb +++ b/gcc/ada/exp_spark.adb @@ -53,6 +53,9 @@ package body Exp_SPARK is -- Replace occurrences of System'To_Address by calls to -- System.Storage_Elements.To_Address + procedure Expand_SPARK_Freeze_Type (E : Entity_Id); + -- Build the DIC procedure of a type when needed, if not already done + procedure Expand_SPARK_N_Object_Declaration (N : Node_Id); -- Perform object-declaration-specific expansion @@ -122,6 +125,11 @@ package body Exp_SPARK is when N_Object_Renaming_Declaration => Expand_SPARK_N_Object_Renaming_Declaration (N); + when N_Freeze_Entity => + if Is_Type (Entity (N)) then + Expand_SPARK_Freeze_Type (Entity (N)); + end if; + -- In SPARK mode, no other constructs require expansion when others => @@ -233,6 +241,23 @@ package body Exp_SPARK is end if; end Expand_SPARK_N_Attribute_Reference; + ------------------------------ + -- Expand_SPARK_Freeze_Type -- + ------------------------------ + + procedure Expand_SPARK_Freeze_Type (E : Entity_Id) is + begin + -- When a DIC is inherited by a tagged type, it may need to be + -- specialized to the descendant type, hence build a separate DIC + -- procedure for it as done during regular expansion for compilation. + + if Has_DIC (E) + and then Is_Tagged_Type (E) + then + Build_DIC_Procedure_Body (E, For_Freeze => True); + end if; + end Expand_SPARK_Freeze_Type; + --------------------------------------- -- Expand_SPARK_N_Object_Declaration -- --------------------------------------- diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads index e5fff4002e2..3f60993b1a3 100644 --- a/gcc/ada/exp_util.ads +++ b/gcc/ada/exp_util.ads @@ -283,7 +283,7 @@ package Exp_Util is For_Freeze : Boolean := False); -- Create the body of the procedure which verifies the assertion expression -- of pragma Default_Initial_Condition at run time. Flag For_Freeze should - -- be set when the body is construction as part of the freezing actions for + -- be set when the body is constructed as part of the freezing actions for -- Typ. procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id); diff --git a/gcc/ada/fname-uf.adb b/gcc/ada/fname-uf.adb index 416557666e2..dea7a0020bc 100644 --- a/gcc/ada/fname-uf.adb +++ b/gcc/ada/fname-uf.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2017, 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- -- @@ -549,8 +549,8 @@ package body Fname.UF is procedure Lock is begin - SFN_Table.Locked := True; SFN_Table.Release; + SFN_Table.Locked := True; end Lock; ------------------- diff --git a/gcc/ada/g-dyntab.adb b/gcc/ada/g-dyntab.adb index 384d5137817..60bf3455c28 100644 --- a/gcc/ada/g-dyntab.adb +++ b/gcc/ada/g-dyntab.adb @@ -59,6 +59,7 @@ package body GNAT.Dynamic_Tables is begin -- Note that Num can be negative + pragma Assert (not T.Locked); Set_Last (T, T.P.Last + Table_Index_Type'Base (Num)); end Allocate; @@ -68,6 +69,7 @@ package body GNAT.Dynamic_Tables is procedure Append (T : in out Instance; New_Val : Table_Component_Type) is begin + pragma Assert (not T.Locked); Set_Item (T, T.P.Last + 1, New_Val); end Append; @@ -88,6 +90,7 @@ package body GNAT.Dynamic_Tables is procedure Decrement_Last (T : in out Instance) is begin + pragma Assert (not T.Locked); Allocate (T, -1); end Decrement_Last; @@ -118,6 +121,7 @@ package body GNAT.Dynamic_Tables is ---------- procedure Free (T : in out Instance) is + pragma Assert (not T.Locked); subtype Alloc_Type is Table_Type (First .. T.P.Last_Allocated); type Alloc_Ptr is access all Alloc_Type; @@ -228,6 +232,7 @@ package body GNAT.Dynamic_Tables is procedure Increment_Last (T : in out Instance) is begin + pragma Assert (not T.Locked); Allocate (T, 1); end Increment_Last; @@ -237,6 +242,7 @@ package body GNAT.Dynamic_Tables is procedure Init (T : in out Instance) is begin + pragma Assert (not T.Locked); Free (T); end Init; @@ -266,6 +272,8 @@ package body GNAT.Dynamic_Tables is procedure Move (From, To : in out Instance) is begin + pragma Assert (not From.Locked); + pragma Assert (not To.Locked); pragma Assert (Is_Empty (To)); To := From; @@ -281,6 +289,7 @@ package body GNAT.Dynamic_Tables is ------------- procedure Release (T : in out Instance) is + pragma Assert (not T.Locked); Old_Last_Allocated : constant Table_Last_Type := T.P.Last_Allocated; function New_Last_Allocated return Table_Last_Type; @@ -355,6 +364,7 @@ package body GNAT.Dynamic_Tables is Index : Valid_Table_Index_Type; Item : Table_Component_Type) is + pragma Assert (not T.Locked); Item_Copy : constant Table_Component_Type := Item; begin -- If Set_Last is going to reallocate the table, we make a copy of Item, @@ -386,6 +396,7 @@ package body GNAT.Dynamic_Tables is procedure Set_Last (T : in out Instance; New_Val : Table_Last_Type) is begin + pragma Assert (not T.Locked); if New_Val > T.P.Last_Allocated then Grow (T, New_Val); end if; diff --git a/gcc/ada/g-dyntab.ads b/gcc/ada/g-dyntab.ads index 9bfccc2822e..b3095b64fbf 100644 --- a/gcc/ada/g-dyntab.ads +++ b/gcc/ada/g-dyntab.ads @@ -173,10 +173,10 @@ package GNAT.Dynamic_Tables is -- SCO_Unit_Table and SCO_Table in scos.h. Locked : Boolean := False; - -- Table expansion is permitted only if this is False. A client may set - -- Locked to True, in which case any attempt to expand the table will - -- cause an assertion failure. Note that while a table is locked, its - -- address in memory remains fixed and unchanging. + -- Table reallocation is permitted only if this is False. A client may + -- set Locked to True, in which case any operation that might expand or + -- shrink the table will cause an assertion failure. While a table is + -- locked, its address in memory remains fixed and unchanging. P : Table_Private; end record; diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index 0e65b7b21db..beb05f4ecdd 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -1091,8 +1091,8 @@ package body Ghost is procedure Lock is begin - Ignored_Ghost_Units.Locked := True; Ignored_Ghost_Units.Release; + Ignored_Ghost_Units.Locked := True; end Lock; ----------------------------------- diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index ff07aea4f99..0b9affdce7b 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2017, 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- -- @@ -4184,14 +4184,14 @@ package body Inline is procedure Lock is begin - Pending_Instantiations.Locked := True; - Inlined_Bodies.Locked := True; - Successors.Locked := True; - Inlined.Locked := True; Pending_Instantiations.Release; + Pending_Instantiations.Locked := True; Inlined_Bodies.Release; + Inlined_Bodies.Locked := True; Successors.Release; + Successors.Locked := True; Inlined.Release; + Inlined.Locked := True; end Lock; -------------------------------- diff --git a/gcc/ada/lib.adb b/gcc/ada/lib.adb index ea8b061eaff..cce586c06c7 100644 --- a/gcc/ada/lib.adb +++ b/gcc/ada/lib.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2017, 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- -- @@ -1046,12 +1046,12 @@ package body Lib is procedure Lock is begin - Linker_Option_Lines.Locked := True; - Load_Stack.Locked := True; - Units.Locked := True; Linker_Option_Lines.Release; + Linker_Option_Lines.Locked := True; Load_Stack.Release; + Load_Stack.Locked := True; Units.Release; + Units.Locked := True; end Lock; --------------- diff --git a/gcc/ada/namet.adb b/gcc/ada/namet.adb index 20dd504b018..b87dd91e7b1 100644 --- a/gcc/ada/namet.adb +++ b/gcc/ada/namet.adb @@ -1088,10 +1088,10 @@ package body Namet is begin Name_Chars.Set_Last (Name_Chars.Last + Name_Chars_Reserve); Name_Entries.Set_Last (Name_Entries.Last + Name_Entries_Reserve); - Name_Chars.Locked := True; - Name_Entries.Locked := True; Name_Chars.Release; + Name_Chars.Locked := True; Name_Entries.Release; + Name_Entries.Locked := True; end Lock; ---------------- @@ -1708,11 +1708,11 @@ package body Namet is procedure Unlock is begin - Name_Chars.Set_Last (Name_Chars.Last - Name_Chars_Reserve); - Name_Entries.Set_Last (Name_Entries.Last - Name_Entries_Reserve); Name_Chars.Locked := False; - Name_Entries.Locked := False; + Name_Chars.Set_Last (Name_Chars.Last - Name_Chars_Reserve); Name_Chars.Release; + Name_Entries.Locked := False; + Name_Entries.Set_Last (Name_Entries.Last - Name_Entries_Reserve); Name_Entries.Release; end Unlock; diff --git a/gcc/ada/nlists.adb b/gcc/ada/nlists.adb index db6a5c88ea1..7050c3e0ff5 100644 --- a/gcc/ada/nlists.adb +++ b/gcc/ada/nlists.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2017, 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- -- @@ -721,14 +721,12 @@ package body Nlists is procedure Lock is begin - Lists.Locked := True; Lists.Release; - - Prev_Node.Locked := True; - Next_Node.Locked := True; - + Lists.Locked := True; Prev_Node.Release; + Prev_Node.Locked := True; Next_Node.Release; + Next_Node.Locked := True; end Lock; ---------------- diff --git a/gcc/ada/sem.adb b/gcc/ada/sem.adb index 9cde60eb180..f277e03d2a7 100644 --- a/gcc/ada/sem.adb +++ b/gcc/ada/sem.adb @@ -1227,8 +1227,8 @@ package body Sem is procedure Lock is begin - Scope_Stack.Locked := True; Scope_Stack.Release; + Scope_Stack.Locked := True; end Lock; ---------------- diff --git a/gcc/ada/sinput.adb b/gcc/ada/sinput.adb index 237818d9f58..a5f345d8143 100644 --- a/gcc/ada/sinput.adb +++ b/gcc/ada/sinput.adb @@ -678,8 +678,8 @@ package body Sinput is procedure Lock is begin - Source_File.Locked := True; Source_File.Release; + Source_File.Locked := True; end Lock; ---------------------- diff --git a/gcc/ada/stringt.adb b/gcc/ada/stringt.adb index 5070b1fab28..c59ec30a20d 100644 --- a/gcc/ada/stringt.adb +++ b/gcc/ada/stringt.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2017, 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- -- @@ -128,10 +128,10 @@ package body Stringt is procedure Lock is begin - String_Chars.Locked := True; - Strings.Locked := True; String_Chars.Release; + String_Chars.Locked := True; Strings.Release; + Strings.Locked := True; end Lock; ---------- diff --git a/gcc/ada/table.ads b/gcc/ada/table.ads index 70626655492..066dc4ff18d 100644 --- a/gcc/ada/table.ads +++ b/gcc/ada/table.ads @@ -78,14 +78,6 @@ package Table is Table : Table_Ptr renames Tab.Table; Locked : Boolean renames Tab.Locked; - -- Table expansion is permitted only if this switch is set to False. A - -- client may set Locked to True, in which case any attempt to expand - -- the table will cause an assertion failure. Note that while a table - -- is locked, its address in memory remains fixed and unchanging. This - -- feature is used to control table expansion during Gigi processing. - -- Gigi assumes that tables other than the Uint and Ureal tables do - -- not move during processing, which means that they cannot be expanded. - -- The Locked flag is used to enforce this restriction. function Is_Empty return Boolean renames Tab.Is_Empty; -- 2.30.2