+2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_elab.adb Add new type Visited_Element
+ and update the contents of table Elab_Visited. Various code clean up.
+ (Check_Elab_Call): Determine whether a prior call to
+ the same subprogram was already examined within the same context.
+ (Check_Internal_Call_Continue): Register the subprogram being
+ called as examined within a particular context. Do not suppress
+ elaboration warnings.
+
+2017-04-27 Gary Dismukes <dismukes@adacore.com>
+
+ * xoscons.adb, osint.ads: Minor reformatting.
+
+2017-04-27 Bob Duff <duff@adacore.com>
+
+ * g-dyntab.ads, g-dyntab.adb: Misc cleanup. Rename
+ Table_Count_Type --> Table_Last_Type, because the name
+ was confusing (a "count" usually starts at zero). Add
+ functionality supported or needed by other tables packages
+ (Move, Release_Threshold).
+ * g-table.ads, g-table.adb: This is now just a thin wrapper
+ around g-dyntab.ads/g-dyntab.adb. Add functionality supported
+ or needed by other tables packages (Save, Restore).
+ * table.ads, table.adb: This is now just a thin wrapper around
+ * g-table.ads/g-table.adb.
+ * namet.h, scos.h, uintp.h: These files are reaching into the
+ private data of some instances of g-table, whose names changed,
+ so the above change requires some adjustment here. It now uses
+ public interfaces.
+
+2017-04-27 Bob Duff <duff@adacore.com>
+
+ * namet.adb, namet.ads: Minor: remove unused procedures.
+
+2017-04-27 Eric Botcazou <ebotcazou@adacore.com>
+
+ * checks.adb (Apply_Scalar_Range_Check): Initialize Ok variable too.
+ (Minimize_Eliminate_Overflows): Initialize Llo and Lhi.
+ Add pragma Warnings on Rtype variable in nested block. *
+ * exp_ch3.adb (Build_Init_Statements): Initialize VAR_LOC.
+ * exp_ch4.adb (Expand_Concatenate): Initialize 3 variables.
+ (Size_In_Storage_Elements): Add pragma Warnings on Res variable.
+ * exp_ch7.adb (Build_Adjust_Statements): Initialize Bod_Stmts.
+ (Process_Component_List_For_Finalize): Initialize Counter_Id.
+ (Build_Finalize_Statements): Initialize Bod_Stmts.
+ * exp_disp.adb (Expand_Dispatching_Call): Initialize SCIL_Node.
+
+2017-04-27 Claire Dross <dross@adacore.com>
+
+ * a-cfhama.adb, a-cfhamai.ads (=): Generic parameter removed to
+ allow the use of regular equality over elements in contracts.
+ (Formal_Model): Ghost package containing model functions that are
+ used in subprogram contracts.
+ (Current_To_Last): Removed, model
+ functions should be used instead.
+ (First_To_Previous): Removed, model functions should be used instead.
+ (Strict_Equal): Removed, model functions should be used instead.
+ (No_Overlap): Removed, model functions should be used instead.
+ (Equivalent_Keys): Functions over cursors are removed. They were
+ awkward with explicit container parameters.
+ * a-cofuma.adb, a-cofuma.ads (Lift_Equivalent_Keys): New lemma
+ (proof only) procedure to help GNATprove when equivalence over
+ keys is not equality.
+
2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* exp_util.adb, a-cfdlli.adb, a-cfdlli.ads, exp_ch9.adb, g-dyntab.adb,
-- --
-- B o d y --
-- --
--- Copyright (C) 2010-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2010-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- --
return Target;
end Copy;
- ---------------------
- -- Current_To_Last --
- ---------------------
-
- function Current_To_Last (Container : Map; Current : Cursor) return Map is
- Curs : Cursor := First (Container);
- C : Map (Container.Capacity, Container.Modulus) :=
- Copy (Container, Container.Capacity);
- Node : Count_Type;
-
- begin
- if Curs = No_Element then
- Clear (C);
- return C;
-
- elsif Current /= No_Element and not Has_Element (Container, Current) then
- raise Constraint_Error;
-
- else
- while Curs.Node /= Current.Node loop
- Node := Curs.Node;
- Delete (C, Curs);
- Curs := Next (Container, (Node => Node));
- end loop;
-
- return C;
- end if;
- end Current_To_Last;
-
---------------------
-- Default_Modulus --
---------------------
HT_Ops.Delete_Node_Sans_Free (Container, Position.Node);
Free (Container, Position.Node);
+ Position := No_Element;
end Delete;
-------------
return Equivalent_Keys (Key, Node.Key);
end Equivalent_Keys;
- function Equivalent_Keys
- (Left : Map;
- CLeft : Cursor;
- Right : Map;
- CRight : Cursor) return Boolean
- is
- begin
- if not Has_Element (Left, CLeft) then
- raise Constraint_Error with
- "Left cursor of Equivalent_Keys has no element";
- end if;
-
- if not Has_Element (Right, CRight) then
- raise Constraint_Error with
- "Right cursor of Equivalent_Keys has no element";
- end if;
-
- pragma Assert (Vet (Left, CLeft),
- "Left cursor of Equivalent_Keys is bad");
- pragma Assert (Vet (Right, CRight),
- "Right cursor of Equivalent_Keys is bad");
-
- declare
- LN : Node_Type renames Left.Nodes (CLeft.Node);
- RN : Node_Type renames Right.Nodes (CRight.Node);
- begin
- return Equivalent_Keys (LN.Key, RN.Key);
- end;
- end Equivalent_Keys;
-
- function Equivalent_Keys
- (Left : Map;
- CLeft : Cursor;
- Right : Key_Type) return Boolean
- is
- begin
- if not Has_Element (Left, CLeft) then
- raise Constraint_Error with
- "Left cursor of Equivalent_Keys has no element";
- end if;
-
- pragma Assert (Vet (Left, CLeft),
- "Left cursor in Equivalent_Keys is bad");
-
- declare
- LN : Node_Type renames Left.Nodes (CLeft.Node);
- begin
- return Equivalent_Keys (LN.Key, Right);
- end;
- end Equivalent_Keys;
-
- function Equivalent_Keys
- (Left : Key_Type;
- Right : Map;
- CRight : Cursor) return Boolean
- is
- begin
- if Has_Element (Right, CRight) then
- raise Constraint_Error with
- "Right cursor of Equivalent_Keys has no element";
- end if;
-
- pragma Assert (Vet (Right, CRight),
- "Right cursor of Equivalent_Keys is bad");
-
- declare
- RN : Node_Type renames Right.Nodes (CRight.Node);
-
- begin
- return Equivalent_Keys (Left, RN.Key);
- end;
- end Equivalent_Keys;
-
-------------
-- Exclude --
-------------
return (Node => Node);
end First;
- -----------------------
- -- First_To_Previous --
- -----------------------
+ ------------------
+ -- Formal_Model --
+ ------------------
- function First_To_Previous
- (Container : Map;
- Current : Cursor) return Map is
- Curs : Cursor;
- C : Map (Container.Capacity, Container.Modulus) :=
- Copy (Container, Container.Capacity);
- Node : Count_Type;
+ package body Formal_Model is
- begin
- Curs := Current;
+ ----------
+ -- Keys --
+ ----------
- if Curs = No_Element then
- return C;
+ function Keys (Container : Map) return K.Sequence is
+ Position : Count_Type := HT_Ops.First (Container);
+ R : K.Sequence;
- elsif not Has_Element (Container, Curs) then
- raise Constraint_Error;
+ begin
+ -- Can't use First, Next or Element here, since they depend on models
+ -- for their postconditions.
- else
- while Curs.Node /= 0 loop
- Node := Curs.Node;
- Delete (C, Curs);
- Curs := Next (Container, (Node => Node));
+ while Position /= 0 loop
+ R := K.Add (R, Container.Nodes (Position).Key);
+ Position := HT_Ops.Next (Container, Position);
end loop;
- return C;
- end if;
- end First_To_Previous;
+ return R;
+ end Keys;
+
+ ----------------------------
+ -- Lift_Abstraction_Level --
+ ----------------------------
+
+ procedure Lift_Abstraction_Level (Container : Map) is null;
+
+ -----------------------
+ -- Mapping_preserved --
+ -----------------------
+
+ function Mapping_Preserved
+ (K_Left : K.Sequence;
+ K_Right : K.Sequence;
+ P_Left : P.Map;
+ P_Right : P.Map) return Boolean
+ is
+ begin
+ for C of P_Left loop
+ if not P.Has_Key (P_Right, C)
+ or else P.Get (P_Left, C) > K.Length (K_Left)
+ or else P.Get (P_Right, C) > K.Length (K_Right)
+ or else K.Get (K_Left, P.Get (P_Left, C)) /=
+ K.Get (K_Right, P.Get (P_Right, C))
+ then
+ return False;
+ end if;
+ end loop;
+
+ return True;
+ end Mapping_Preserved;
+
+ -----------
+ -- Model --
+ -----------
+
+ function Model (Container : Map) return M.Map is
+ Position : Count_Type := HT_Ops.First (Container);
+ R : M.Map;
+
+ begin
+ -- Can't use First, Next or Element here, since they depend on models
+ -- for their postconditions.
+
+ while Position /= 0 loop
+ R := M.Add (Container => R,
+ New_Key => Container.Nodes (Position).Key,
+ New_Item => Container.Nodes (Position).Element);
+ Position := HT_Ops.Next (Container, Position);
+ end loop;
+
+ return R;
+ end Model;
+
+ ---------------
+ -- Positions --
+ ---------------
+
+ function Positions (Container : Map) return P.Map is
+ I : Count_Type := 1;
+ Position : Count_Type := HT_Ops.First (Container);
+ R : P.Map;
+
+ begin
+ -- Can't use First, Next or Element here, since they depend on models
+ -- for their postconditions.
+
+ while Position /= 0 loop
+ R := P.Add (R, (Node => Position), I);
+ pragma Assert (P.Length (R) = I);
+ Position := HT_Ops.Next (Container, Position);
+ I := I + 1;
+ end loop;
+
+ return R;
+ end Positions;
+
+ end Formal_Model;
----------
-- Free --
Position := Next (Container, Position);
end Next;
- -------------
- -- Overlap --
- -------------
-
- function Overlap (Left, Right : Map) return Boolean is
- Left_Node : Count_Type;
- Left_Nodes : Nodes_Type renames Left.Nodes;
-
- begin
- if Length (Right) = 0 or Length (Left) = 0 then
- return False;
- end if;
-
- if Left'Address = Right'Address then
- return True;
- end if;
-
- Left_Node := First (Left).Node;
- while Left_Node /= 0 loop
- declare
- N : Node_Type renames Left_Nodes (Left_Node);
- E : Key_Type renames N.Key;
- begin
- if Find (Right, E).Node /= 0 then
- return True;
- end if;
- end;
-
- Left_Node := HT_Ops.Next (Left, Left_Node);
- end loop;
-
- return False;
- end Overlap;
-
-------------
-- Replace --
-------------
Node.Next := Next;
end Set_Next;
- ------------------
- -- Strict_Equal --
- ------------------
-
- function Strict_Equal (Left, Right : Map) return Boolean is
- CuL : Cursor := First (Left);
- CuR : Cursor := First (Right);
-
- begin
- if Length (Left) /= Length (Right) then
- return False;
- end if;
-
- while CuL.Node /= 0 or else CuR.Node /= 0 loop
- if CuL.Node /= CuR.Node
- or else
- Left.Nodes (CuL.Node).Element /= Right.Nodes (CuR.Node).Element
- or else Left.Nodes (CuL.Node).Key /= Right.Nodes (CuR.Node).Key
- then
- return False;
- end if;
-
- CuL := Next (Left, CuL);
- CuR := Next (Right, CuR);
- end loop;
-
- return True;
- end Strict_Equal;
-
---------
-- Vet --
---------
-- --
-- S p e c --
-- --
--- Copyright (C) 2004-2015, Free Software Foundation, Inc. --
+-- Copyright (C) 2004-2017, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- and its previous version C'Old) for expressing properties, which is not
-- possible if cursors encapsulate an access to the underlying container.
--- There are four new functions:
-
--- function Strict_Equal (Left, Right : Map) return Boolean;
--- function Overlap (Left, Right : Map) return Boolean;
--- function First_To_Previous (Container : Map; Current : Cursor)
--- return Map;
--- function Current_To_Last (Container : Map; Current : Cursor)
--- return Map;
-
--- See detailed specifications for these subprograms
+-- 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;
private with Ada.Containers.Hash_Tables;
generic
with function Hash (Key : Key_Type) return Hash_Type;
with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
- with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Formal_Hashed_Maps with
- Pure,
SPARK_Mode
is
- pragma Annotate (GNATprove, External_Axiomatization);
pragma Annotate (CodePeer, Skip_Analysis);
type Map (Capacity : Count_Type; Modulus : Hash_Type) is private with
Iterable => (First => First,
Next => Next,
Has_Element => Has_Element,
- Element => Element),
- Default_Initial_Condition => Is_Empty (Map);
+ Element => Key),
+ Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0;
pragma Preelaborable_Initialization (Map);
- type Cursor is private;
- pragma Preelaborable_Initialization (Cursor);
-
Empty_Map : constant Map;
- No_Element : constant Cursor;
+ type Cursor is record
+ Node : Count_Type;
+ end record;
+
+ No_Element : constant Cursor := (Node => 0);
+
+ function Length (Container : Map) return Count_Type with
+ Global => null,
+ Post => Length'Result <= Container.Capacity;
+
+ pragma Unevaluated_Use_Of_Old (Allow);
+
+ package Formal_Model with Ghost is
+ subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
+
+ package M is new Ada.Containers.Functional_Maps
+ (Element_Type => Element_Type,
+ Key_Type => Key_Type,
+ Equivalent_Keys => Equivalent_Keys);
+
+ function "="
+ (Left : M.Map;
+ Right : M.Map) return Boolean renames M."=";
+
+ function "<="
+ (Left : M.Map;
+ Right : M.Map) return Boolean renames M."<=";
+
+ package K is new Ada.Containers.Functional_Vectors
+ (Element_Type => Key_Type,
+ Index_Type => Positive_Count_Type);
+
+ function "="
+ (Left : K.Sequence;
+ Right : K.Sequence) return Boolean renames K."=";
+
+ function "<"
+ (Left : K.Sequence;
+ Right : K.Sequence) return Boolean renames K."<";
+
+ function "<="
+ (Left : K.Sequence;
+ Right : K.Sequence) return Boolean renames K."<=";
+
+ package P is new Ada.Containers.Functional_Maps
+ (Key_Type => Cursor,
+ Element_Type => Positive_Count_Type,
+ Equivalent_Keys => "=");
+
+ function "="
+ (Left : P.Map;
+ Right : P.Map) return Boolean renames P."=";
+
+ function "<="
+ (Left : P.Map;
+ Right : P.Map) return Boolean renames P."<=";
+
+ function Mapping_Preserved
+ (K_Left : K.Sequence;
+ K_Right : K.Sequence;
+ P_Left : P.Map;
+ P_Right : P.Map) return Boolean
+ with
+ Ghost,
+ Global => null,
+ Post =>
+ (if Mapping_Preserved'Result then
+
+ -- Right contains all the cursors of Left
+
+ P.Keys_Included (P_Left, P_Right)
+
+ -- Mappings from cursors to elements induced by K_Left, P_Left
+ -- and K_Right, P_Right are the same.
+
+ and (for all C of P_Left =>
+ K.Get (K_Left, P.Get (P_Left, C)) =
+ 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
+ -- cursors nor order of elements are represented in this model. Keys are
+ -- modeled up to equivalence.
+
+ Ghost,
+ Global => null;
+
+ function Keys (Container : Map) return K.Sequence with
+ -- The Keys sequence represents the underlying list structure of maps
+ -- that is used for iteration. It stores the actual values of keys in
+ -- the map. It does not model cursors nor elements.
+
+ Ghost,
+ Global => null,
+ Post =>
+ K.Length (Keys'Result) = Length (Container)
+
+ -- It only contains keys contained in Model
+
+ and (for all Key of Keys'Result =>
+ M.Has_Key (Model (Container), Key))
+
+ -- It contains all the keys contained in Model
+
+ and
+ (for all Key of Model (Container) =>
+ (for some L of Keys'Result => Equivalent_Keys (L, Key)))
+
+ -- It has no duplicate
+
+ and
+ (for all I in 1 .. Length (Container) =>
+ (for all J in 1 .. Length (Container) =>
+ (if Equivalent_Keys
+ (K.Get (Keys'Result, I), K.Get (Keys'Result, J))
+ then I = J)));
+ pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys);
+
+ 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.
+
+ Ghost,
+ Global => null,
+ Post =>
+ not P.Has_Key (Positions'Result, No_Element)
+
+ -- Positions of cursors are smaller than the container's length.
+
+ and then
+ (for all I of Positions'Result =>
+ P.Get (Positions'Result, I) in 1 .. Length (Container)
+
+ -- No two cursors have the same position. Note that we do not
+ -- state that there is a cursor in the map for each position, as
+ -- it is rarely needed.
+
+ and then
+ (for all J of Positions'Result =>
+ (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
+ then I = J)));
+
+ 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
+ -- 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.
+
+ Ghost,
+ Global => null,
+ Post =>
+ (for all Key of Keys (Container) =>
+ (for some I of Positions (Container) =>
+ K.Get (Keys (Container), P.Get (Positions (Container), I)) =
+ Key));
+
+ function Contains
+ (C : M.Map;
+ K : Key_Type) return Boolean renames M.Has_Key;
+ -- To improve readability of contracts, we rename the function used to
+ -- search for a key in the model to Contains.
+
+ function Element
+ (C : M.Map;
+ K : Key_Type) return Element_Type renames M.Get;
+ -- To improve readability of contracts, we rename the function used to
+ -- access an element in the model to Element.
+ end Formal_Model;
+ use Formal_Model;
function "=" (Left, Right : Map) return Boolean with
- Global => null;
+ Global => null,
+ Post => "="'Result = (Model (Left) = Model (Right));
function Capacity (Container : Map) return Count_Type with
- Global => null;
+ Global => null,
+ Post => Capacity'Result = Container.Capacity;
procedure Reserve_Capacity
(Container : in out Map;
Capacity : Count_Type)
with
Global => null,
- Pre => Capacity <= Container.Capacity;
-
- function Length (Container : Map) return Count_Type with
- Global => null;
+ Pre => Capacity <= Container.Capacity,
+ Post => Model (Container) = Model (Container)'Old;
function Is_Empty (Container : Map) return Boolean with
- Global => null;
+ Global => null,
+ Post => Is_Empty'Result = M.Is_Empty (Model (Container));
procedure Clear (Container : in out Map) with
- Global => null;
+ Global => null,
+ Post => Length (Container) = 0 and M.Is_Empty (Model (Container));
procedure Assign (Target : in out Map; Source : Map) with
Global => null,
- Pre => Target.Capacity >= Length (Source);
+ Pre => Target.Capacity >= Length (Source),
+ Post =>
+ Model (Target) = Model (Source)
+ and Length (Source) = Length (Target)
+
+ -- Actual keys are preserved
+
+ and
+ (for all Key of Keys (Source) =>
+ Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key);
function Copy
(Source : Map;
Capacity : Count_Type := 0) return Map
with
Global => null,
- Pre => Capacity = 0 or else Capacity >= Source.Capacity;
+ Pre => Capacity = 0 or else Capacity >= Source.Capacity,
+ Post =>
+ Model (Copy'Result) = Model (Source)
+ and Keys (Copy'Result) = Keys (Source)
+ and Positions (Copy'Result) = Positions (Source)
+ and (if Capacity = 0 then
+ Copy'Result.Capacity = Source.Capacity
+ else
+ Copy'Result.Capacity = 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
+ -- - capacity=0 means use Source.Capacity as capacity of target
-- - the modulus cannot be changed.
function Key (Container : Map; Position : Cursor) return Key_Type with
Global => null,
- Pre => Has_Element (Container, Position);
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Key'Result =
+ K.Get (Keys (Container), P.Get (Positions (Container), Position));
+ pragma Annotate (GNATprove, Inline_For_Proof, Key);
function Element
(Container : Map;
Position : Cursor) return Element_Type
with
Global => null,
- Pre => Has_Element (Container, Position);
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Element'Result = Element (Model (Container), Key (Container, Position));
+ pragma Annotate (GNATprove, Inline_For_Proof, Element);
procedure Replace_Element
(Container : in out Map;
New_Item : Element_Type)
with
Global => null,
- Pre => Has_Element (Container, Position);
+ Pre => Has_Element (Container, Position),
+ Post =>
+
+ -- Order of keys and cursors are preserved
+
+ Keys (Container) = Keys (Container)'Old
+ and Positions (Container) = Positions (Container)'Old
+
+ -- New_Item is now associated to the key at position Position in
+ -- Container.
+
+ and Element (Container, Position) = New_Item
+
+ -- Elements associated to other keys are preserved
+
+ and M.Same_Keys (Model (Container), Model (Container)'Old)
+ and M.Elements_Equal_Except
+ (Model (Container),
+ Model (Container)'Old,
+ Key (Container, Position));
procedure Move (Target : in out Map; Source : in out Map) with
Global => null,
- Pre => Target.Capacity >= Length (Source);
+ Pre => Target.Capacity >= Length (Source),
+ Post =>
+ Model (Target) = Model (Source)'Old
+ and Length (Source)'Old = Length (Target)
+ and Length (Source) = 0
+
+ -- Actual keys are preserved
+
+ and
+ (for all Key of Keys (Source)'Old =>
+ Formal_Hashed_Maps.Key (Target, Find (Target, Key)) = Key);
procedure Insert
(Container : in out Map;
Position : out Cursor;
Inserted : out Boolean)
with
- Global => null,
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre =>
+ Length (Container) < Container.Capacity or Contains (Container, Key),
+ Post =>
+ Contains (Container, Key)
+ and Has_Element (Container, Position)
+ and Equivalent_Keys
+ (Formal_Hashed_Maps.Key (Container, Position), Key),
+ Contract_Cases =>
+
+ -- If Key is already in Container, it is not modified and Inserted is
+ -- set to False.
+
+ (Contains (Container, Key) =>
+ not Inserted
+ and Model (Container) = Model (Container)'Old
+ and Keys (Container) = Keys (Container)'Old
+ and Positions (Container) = Positions (Container)'Old,
+
+ -- Otherwise, Key is inserted in Container and Inserted is set to True
+
+ others =>
+ Inserted
+ and Length (Container) = Length (Container)'Old + 1
+
+ -- Key now maps to New_Item
+
+ and Formal_Hashed_Maps.Key (Container, Position) = Key
+ and Element (Model (Container), Key) = New_Item
+
+ -- Other keys are preserved
+
+ and Model (Container)'Old <= Model (Container)
+ and M.Keys_Included_Except
+ (Model (Container),
+ Model (Container)'Old,
+ Key)
+
+ -- Mapping from cursors to keys are preserved
+
+ and Mapping_Preserved
+ (K_Left => Keys (Container)'Old,
+ K_Right => Keys (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container))
+ and P.Keys_Included_Except
+ (Positions (Container),
+ Positions (Container)'Old,
+ Position));
procedure Insert
(Container : in out Map;
New_Item : Element_Type)
with
Global => null,
- Pre => Length (Container) < Container.Capacity
- and then (not Contains (Container, Key));
+ Pre =>
+ Length (Container) < Container.Capacity
+ and then (not Contains (Container, Key)),
+ Post =>
+ Length (Container) = Length (Container)'Old + 1
+ and Contains (Container, Key)
+
+ -- Key now maps to New_Item
+
+ and Formal_Hashed_Maps.Key (Container, Find (Container, Key)) = Key
+ and Element (Model (Container), Key) = New_Item
+
+ -- Other keys are preserved
+
+ and Model (Container)'Old <= Model (Container)
+ and M.Keys_Included_Except
+ (Model (Container),
+ Model (Container)'Old,
+ Key)
+
+ -- Mapping from cursors to keys are preserved
+
+ and Mapping_Preserved
+ (K_Left => Keys (Container)'Old,
+ K_Right => Keys (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container))
+ and P.Keys_Included_Except
+ (Positions (Container),
+ Positions (Container)'Old,
+ Find (Container, Key));
procedure Include
(Container : in out Map;
Key : Key_Type;
New_Item : Element_Type)
with
- Global => null,
- Pre => Length (Container) < Container.Capacity;
+ Global => null,
+ Pre =>
+ Length (Container) < Container.Capacity or Contains (Container, Key),
+ Post =>
+ Contains (Container, Key) and Element (Container, Key) = New_Item,
+ Contract_Cases =>
+
+ -- If Key is already in Container, Key is mapped to New_Item
+
+ (Contains (Container, Key) =>
+
+ -- Cursors are preserved
+
+ Positions (Container) = Positions (Container)'Old
+
+ -- The key equivalent to Key in Container is replaced by Key
+
+ and K.Get (Keys (Container),
+ P.Get (Positions (Container), Find (Container, Key))) =
+ Key
+ and K.Equal_Except
+ (Keys (Container)'Old,
+ Keys (Container),
+ P.Get (Positions (Container), Find (Container, Key)))
+
+ -- Elements associated to other keys are preserved
+
+ and M.Same_Keys (Model (Container), Model (Container)'Old)
+ and M.Elements_Equal_Except
+ (Model (Container),
+ Model (Container)'Old,
+ Key),
+
+ -- Otherwise, Key is inserted in Container
+
+ others =>
+ Length (Container) = Length (Container)'Old + 1
+
+ -- Other keys are preserved
+
+ and Model (Container)'Old <= Model (Container)
+ and M.Keys_Included_Except
+ (Model (Container),
+ Model (Container)'Old,
+ Key)
+
+ -- Mapping from cursors to keys are preserved
+
+ and Mapping_Preserved
+ (K_Left => Keys (Container)'Old,
+ K_Right => Keys (Container),
+ P_Left => Positions (Container)'Old,
+ P_Right => Positions (Container))
+ and P.Keys_Included_Except
+ (Positions (Container),
+ Positions (Container)'Old,
+ Find (Container, Key)));
procedure Replace
(Container : in out Map;
New_Item : Element_Type)
with
Global => null,
- Pre => Contains (Container, Key);
+ Pre => Contains (Container, Key),
+ Post =>
+
+ -- Cursors are preserved
+
+ Positions (Container) = Positions (Container)'Old
+
+ -- The key equivalent to Key in Container is replaced by Key
+
+ and K.Get (Keys (Container),
+ P.Get (Positions (Container), Find (Container, Key))) = Key
+ and K.Equal_Except
+ (Keys (Container)'Old,
+ Keys (Container),
+ P.Get (Positions (Container), Find (Container, Key)))
+
+ -- New_Item is now associated to the Key in Container
+
+ and Element (Model (Container), Key) = New_Item
+
+ -- Elements associated to other keys are preserved
+
+ and M.Same_Keys (Model (Container), Model (Container)'Old)
+ and M.Elements_Equal_Except
+ (Model (Container),
+ Model (Container)'Old,
+ Key);
procedure Exclude (Container : in out Map; Key : Key_Type) with
- Global => null;
+ Global => null,
+ Post => not Contains (Container, Key),
+ Contract_Cases =>
+
+ -- If Key is not in Container, nothing is changed
+
+ (not Contains (Container, Key) =>
+ Model (Container) = Model (Container)'Old
+ and Keys (Container) = Keys (Container)'Old
+ and Positions (Container) = Positions (Container)'Old,
+
+ -- Otherwise, Key is removed from Container
+
+ others =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- Other keys are preserved
+
+ and Model (Container) <= Model (Container)'Old
+ and M.Keys_Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Key)
+
+ -- Mapping from cursors to keys are preserved
+
+ and Mapping_Preserved
+ (K_Left => Keys (Container),
+ K_Right => Keys (Container)'Old,
+ P_Left => Positions (Container),
+ P_Right => Positions (Container)'Old)
+ and P.Keys_Included_Except
+ (Positions (Container)'Old,
+ Positions (Container),
+ Find (Container, Key)'Old));
procedure Delete (Container : in out Map; Key : Key_Type) with
Global => null,
- Pre => Contains (Container, Key);
+ Pre => Contains (Container, Key),
+ Post =>
+ Length (Container) = Length (Container)'Old - 1
+
+ -- Key is no longer in Container
+
+ and not Contains (Container, Key)
+
+ -- Other keys are preserved
+
+ and Model (Container) <= Model (Container)'Old
+ and M.Keys_Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Key)
+
+ -- Mapping from cursors to keys are preserved
+
+ and Mapping_Preserved
+ (K_Left => Keys (Container),
+ K_Right => Keys (Container)'Old,
+ P_Left => Positions (Container),
+ P_Right => Positions (Container)'Old)
+ and P.Keys_Included_Except
+ (Positions (Container)'Old,
+ Positions (Container),
+ Find (Container, Key)'Old);
procedure Delete (Container : in out Map; Position : in out Cursor) with
Global => null,
- Pre => Has_Element (Container, Position);
+ Pre => Has_Element (Container, Position),
+ Post =>
+ Position = No_Element
+ and Length (Container) = Length (Container)'Old - 1
+
+ -- The key at position Position is no longer in Container
+
+ and not Contains (Container, Key (Container, Position)'Old)
+ and not P.Has_Key (Positions (Container), Position'Old)
+
+ -- Other keys are preserved
+
+ and Model (Container) <= Model (Container)'Old
+ and M.Keys_Included_Except
+ (Model (Container)'Old,
+ Model (Container),
+ Key (Container, Position)'Old)
+
+ -- Mapping from cursors to keys are preserved
+
+ and Mapping_Preserved
+ (K_Left => Keys (Container),
+ K_Right => Keys (Container)'Old,
+ P_Left => Positions (Container),
+ P_Right => Positions (Container)'Old)
+ and P.Keys_Included_Except
+ (Positions (Container)'Old,
+ Positions (Container),
+ Position'Old);
function First (Container : Map) return Cursor with
- Global => null;
+ Global => null,
+ Contract_Cases =>
+ (Length (Container) = 0 =>
+ First'Result = No_Element,
+
+ others =>
+ Has_Element (Container, First'Result)
+ and P.Get (Positions (Container), First'Result) = 1);
function Next (Container : Map; Position : Cursor) return Cursor with
- Global => null,
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+ (Position = No_Element
+ or else P.Get (Positions (Container), Position) = Length (Container)
+ =>
+ Next'Result = No_Element,
+
+ others =>
+ Has_Element (Container, Next'Result)
+ and then P.Get (Positions (Container), Next'Result) =
+ P.Get (Positions (Container), Position) + 1);
procedure Next (Container : Map; Position : in out Cursor) with
- Global => null,
- Pre => Has_Element (Container, Position) or else Position = No_Element;
+ Global => null,
+ Pre =>
+ Has_Element (Container, Position) or else Position = No_Element,
+ Contract_Cases =>
+ (Position = No_Element
+ or else P.Get (Positions (Container), Position) = Length (Container)
+ =>
+ Position = No_Element,
+
+ others =>
+ Has_Element (Container, Position)
+ and then P.Get (Positions (Container), Position) =
+ P.Get (Positions (Container), Position'Old) + 1);
function Find (Container : Map; Key : Key_Type) return Cursor with
- Global => null;
+ Global => null,
+ Contract_Cases =>
- function Contains (Container : Map; Key : Key_Type) return Boolean with
- Global => null;
+ -- If Key is not is not contained in Container, Find returns No_Element
- function Element (Container : Map; Key : Key_Type) return Element_Type with
- Global => null,
- Pre => Contains (Container, Key);
+ (not Contains (Model (Container), Key) =>
+ Find'Result = No_Element,
- function Has_Element (Container : Map; Position : Cursor) return Boolean
- with
- Global => null;
+ -- Otherwise, Find returns a valid cusror in Container
- function Equivalent_Keys
- (Left : Map;
- CLeft : Cursor;
- Right : Map;
- CRight : Cursor) return Boolean
- with
- Global => null;
+ others =>
+ P.Has_Key (Positions (Container), Find'Result)
- function Equivalent_Keys
- (Left : Map;
- CLeft : Cursor;
- Right : Key_Type) return Boolean
- with
- Global => null;
+ -- The key designated by the result of Find is Key
- function Equivalent_Keys
- (Left : Key_Type;
- Right : Map;
- CRight : Cursor) return Boolean
- with
- Global => null;
-
- function Default_Modulus (Capacity : Count_Type) return Hash_Type with
- Global => null;
+ and Equivalent_Keys
+ (Formal_Hashed_Maps.Key (Container, Find'Result), Key));
- function Strict_Equal (Left, Right : Map) return Boolean with
- Ghost,
- 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 Contains (Container : Map; Key : Key_Type) return Boolean with
+ Global => null,
+ Post => Contains'Result = Contains (Model (Container), Key);
+ pragma Annotate (GNATprove, Inline_For_Proof, Contains);
- function First_To_Previous (Container : Map; Current : Cursor) return Map
- with
- Ghost,
+ function Element (Container : Map; Key : Key_Type) return Element_Type with
Global => null,
- Pre => Has_Element (Container, Current) or else Current = No_Element;
+ Pre => Contains (Container, Key),
+ Post => Element'Result = Element (Model (Container), Key);
+ pragma Annotate (GNATprove, Inline_For_Proof, Element);
- function Current_To_Last (Container : Map; Current : Cursor) return Map
+ function Has_Element (Container : Map; Position : Cursor) return Boolean
with
- Ghost,
Global => null,
- Pre => Has_Element (Container, Current) or else Current = No_Element;
- -- First_To_Previous returns a container containing all elements preceding
- -- Current (excluded) in Container. Current_To_Last returns a container
- -- containing all elements following Current (included) in Container.
- -- These two new functions can be used to express invariant properties in
- -- loops which iterate over containers. First_To_Previous returns the part
- -- of the container already scanned and Current_To_Last the part not
- -- scanned yet.
-
- function Overlap (Left, Right : Map) return Boolean with
+ Post =>
+ Has_Element'Result = P.Has_Key (Positions (Container), Position);
+ pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
+
+ function Default_Modulus (Capacity : Count_Type) return Hash_Type with
Global => null;
- -- Overlap returns True if the containers have common keys
private
pragma SPARK_Mode (Off);
use HT_Types;
- type Cursor is record
- Node : Count_Type;
- end record;
-
Empty_Map : constant Map := (Capacity => 0, Modulus => 0, others => <>);
- No_Element : constant Cursor := (Node => 0);
-
end Ada.Containers.Formal_Hashed_Maps;
K : constant Key_Type := Get (Left.Keys, I);
begin
if not Equivalent_Keys (K, New_Key)
- and then Get (Right.Elements, Find (Right.Keys, K)) /=
- Get (Left.Elements, I)
+ and then
+ (Find (Right.Keys, K) = 0
+ or else Get (Right.Elements, Find (Right.Keys, K)) /=
+ Get (Left.Elements, I))
then
return False;
end if;
begin
if not Equivalent_Keys (K, X)
and then not Equivalent_Keys (K, Y)
- and then Get (Right.Elements, Find (Right.Keys, K)) /=
- Get (Left.Elements, I)
+ and then
+ (Find (Right.Keys, K) = 0
+ or else Get (Right.Elements, Find (Right.Keys, K)) /=
+ Get (Left.Elements, I))
then
return False;
end if;
return Length (Container.Elements);
end Length;
+ --------------------------
+ -- Lift_Equivalent_Keys --
+ --------------------------
+
+ procedure Lift_Equivalent_Keys
+ (Container : Map;
+ Left : Key_Type;
+ Right : Key_Type)
+ is null;
+
---------------
-- Same_Keys --
---------------
-- 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
+ -- equivalence (quantification includes keys equivalent to keys of the
+ -- map).
-----------------------
-- Basic operations --
Global => null;
-- Return the number of mappings in Container
+ procedure Lift_Equivalent_Keys
+ (Container : Map;
+ Left : Key_Type;
+ Right : Key_Type)
+ -- Lemma function which can be called manually to allow GNATprove to deduce
+ -- that Has_Key and Get always return the same result on equivalent keys.
+
+ with
+ Ghost,
+ Global => null,
+ Pre => Equivalent_Keys (Left, Right),
+ Post =>
+ Has_Key (Container, Left) = Has_Key (Container, Right)
+ and (if Has_Key (Container, Left) then
+ Get (Container, Left) = Get (Container, Right));
+
------------------------
-- Property Functions --
------------------------
with
Global => null,
- Pre => Keys_Included_Except (Left, Right, New_Key),
Post =>
Elements_Equal_Except'Result =
(for all Key of Left =>
(if not Equivalent_Keys (Key, New_Key) then
- Get (Left, Key) = Get (Right, Key)));
+ Has_Key (Right, Key)
+ and then Get (Left, Key) = Get (Right, Key)));
function Elements_Equal_Except
(Left : Map;
with
Global => null,
- Pre => Keys_Included_Except (Left, Right, X, Y),
Post =>
Elements_Equal_Except'Result =
(for all Key of Left =>
(if not Equivalent_Keys (Key, X)
and not Equivalent_Keys (Key, Y)
then
- Get (Left, Key) = Get (Right, Key)));
+ Has_Key (Right, Key)
+ and then Get (Left, Key) = Get (Right, Key)));
----------------------------
-- Construction Functions --
S_Typ : Entity_Id;
Arr : Node_Id := Empty; -- initialize to prevent warning
Arr_Typ : Entity_Id := Empty; -- initialize to prevent warning
- OK : Boolean;
+ OK : Boolean := False; -- initialize to prevent warning
Is_Subscr_Ref : Boolean;
-- Set true if Expr is a subscript
Rlo, Rhi : Uint;
-- Ranges of values for right operand (operator case)
- Llo, Lhi : Uint;
+ Llo : Uint := No_Uint; -- initialize to prevent warning
+ Lhi : Uint := No_Uint; -- initialize to prevent warning
-- Ranges of values for left operand (operator case)
LLIB : constant Entity_Id := Base_Type (Standard_Long_Long_Integer);
else
declare
Rtype : Entity_Id;
+ pragma Warnings (Off, Rtype);
New_Alts : List_Id;
New_Exp : Node_Id;
if Present (Variant_Part (Comp_List)) then
declare
Variant_Alts : constant List_Id := New_List;
- Var_Loc : Source_Ptr;
+ Var_Loc : Source_Ptr := No_Location;
Variant : Node_Id;
begin
-- last operand is always retained, in case it provides the bounds for
-- a null result.
- Opnd : Node_Id;
+ Opnd : Node_Id := Empty;
-- Current operand being processed in the loop through operands. After
-- this loop is complete, always contains the last operand (which is not
-- the same as Operands (NN), since null operands are skipped).
-- This is either an integer literal node, or an identifier reference to
-- a constant entity initialized to the appropriate value.
- Last_Opnd_Low_Bound : Node_Id;
+ Last_Opnd_Low_Bound : Node_Id := Empty;
-- A tree node representing the low bound of the last operand. This
-- need only be set if the result could be null. It is used for the
-- special case of setting the right low bound for a null result.
-- This is of type Ityp.
- Last_Opnd_High_Bound : Node_Id;
+ Last_Opnd_High_Bound : Node_Id := Empty;
-- A tree node representing the high bound of the last operand. This
-- need only be set if the result could be null. It is used for the
-- special case of setting the right high bound for a null result.
declare
Len : Node_Id;
Res : Node_Id;
+ pragma Warnings (Off, Res);
begin
for J in 1 .. Number_Dimensions (E) loop
-- Local variables
- Bod_Stmts : List_Id;
+ Bod_Stmts : List_Id := No_List;
Finalizer_Decls : List_Id := No_List;
Rec_Def : Node_Id;
-- Local variables
Alts : List_Id;
- Counter_Id : Entity_Id;
+ Counter_Id : Entity_Id := Empty;
Decl : Node_Id;
Decl_Id : Entity_Id;
Decl_Typ : Entity_Id;
-- Local variables
- Bod_Stmts : List_Id;
+ Bod_Stmts : List_Id := No_List;
Finalizer_Decls : List_Id := No_List;
Rec_Def : Node_Id;
-- Local variables
New_Node : Node_Id;
- SCIL_Node : Node_Id;
+ SCIL_Node : Node_Id := Empty;
SCIL_Related_Node : Node_Id := Call_Node;
-- Start of processing for Expand_Dispatching_Call
with GNAT.Heap_Sort_G;
with Ada.Unchecked_Deallocation;
+with System;
package body GNAT.Dynamic_Tables is
-- Local Subprograms --
-----------------------
- procedure Grow (T : in out Instance; New_Last : Table_Count_Type);
+ procedure Grow (T : in out Instance; New_Last : Table_Last_Type);
-- This is called when we are about to set the value of Last to a value
-- that is larger than Last_Allocated. This reallocates the table to the
-- larger size, as indicated by New_Last. At the time this is called,
begin
if T.Table = Empty then
- pragma Assert (T.P.Last_Allocated = First - 1);
- pragma Assert (T.P.Last = First - 1);
+ pragma Assert (T.P = (Last_Allocated | Last => First - 1));
null;
else
Free (Temp);
T.Table := Empty;
- T.P.Last_Allocated := First - 1;
- T.P.Last := First - 1;
+ T.P := (Last_Allocated | Last => First - 1);
end if;
end Free;
-- Grow --
----------
- procedure Grow (T : in out Instance; New_Last : Table_Count_Type) is
+ procedure Grow (T : in out Instance; New_Last : Table_Last_Type) is
-- Note: Type Alloc_Ptr below needs to be declared locally so we know
-- the bounds. That means that the collection is local, so is finalized
subtype Table_Length_Type is Table_Index_Type'Base
range 0 .. Table_Index_Type'Base'Last;
- Old_Last_Allocated : constant Table_Count_Type := T.P.Last_Allocated;
+ Old_Last_Allocated : constant Table_Last_Type := T.P.Last_Allocated;
Old_Allocated_Length : constant Table_Length_Type :=
Old_Last_Allocated - First + 1;
Free (T);
end Init;
+ --------------
+ -- Is_Empty --
+ --------------
+
+ function Is_Empty (T : Instance) return Boolean is
+ Result : constant Boolean := T.P.Last = Table_Low_Bound - 1;
+ begin
+ pragma Assert (Result = (T.Table = Empty));
+ return Result;
+ end Is_Empty;
+
----------
-- Last --
----------
- function Last (T : Instance) return Table_Count_Type is
+ function Last (T : Instance) return Table_Last_Type is
begin
return T.P.Last;
end Last;
+ ----------
+ -- Move --
+ ----------
+
+ procedure Move (From, To : in out Instance) is
+ begin
+ pragma Assert (Is_Empty (To));
+ To := From;
+
+ From.Table := Empty;
+ From.Locked := False;
+ From.P.Last_Allocated := Table_Low_Bound - 1;
+ From.P.Last := Table_Low_Bound - 1;
+ pragma Assert (Is_Empty (From));
+ end Move;
+
-------------
-- Release --
-------------
procedure Release (T : in out Instance) is
- pragma Assert (not T.Locked);
- Old_Last_Allocated : constant Table_Count_Type := T.P.Last_Allocated;
+ Old_Last_Allocated : constant Table_Last_Type := T.P.Last_Allocated;
+
+ function New_Last_Allocated return Table_Last_Type;
+ -- Compute the new value of Last_Allocated. This is normally equal to
+ -- Last, but if Release_Threshold /= 0, then we need to take that into
+ -- account.
+
+ function New_Last_Allocated return Table_Last_Type is
+ subtype Table_Length_Type is Table_Index_Type'Base
+ range 0 .. Table_Index_Type'Base'Last;
+ Length : constant Table_Length_Type := T.P.Last - First + 1;
+ Comp_Size_In_Bytes : constant Table_Length_Type :=
+ Table_Type'Component_Size / System.Storage_Unit;
+ Length_Threshold : constant Table_Length_Type :=
+ Table_Length_Type (Release_Threshold) / Comp_Size_In_Bytes;
+ begin
+ if Release_Threshold = 0
+ or else Length < Length_Threshold
+ then
+ return T.P.Last;
+ else
+ declare
+ Extra_Length : constant Table_Length_Type := Length / 1000;
+ begin
+ return (Length + Extra_Length) - 1 + First;
+ end;
+ end if;
+ end New_Last_Allocated;
+
+ New_Last_Alloc : constant Table_Last_Type := New_Last_Allocated;
+
+ -- Start of processing for Release
+
begin
- if T.P.Last /= T.P.Last_Allocated then
+ if New_Last_Alloc < T.P.Last_Allocated then
pragma Assert (T.P.Last < T.P.Last_Allocated);
pragma Assert (T.Table /= Empty);
new Ada.Unchecked_Conversion (Table_Ptr, Old_Alloc_Ptr);
subtype Alloc_Type is
- Table_Type (First .. First + T.P.Last - 1);
+ Table_Type (First .. New_Last_Alloc);
type Alloc_Ptr is access all Alloc_Type;
function To_Table_Ptr is
- new Ada.Unchecked_Conversion (Alloc_Ptr, Table_Ptr);
+ new Ada.Unchecked_Conversion (Alloc_Ptr, Table_Ptr);
Old_Table : Old_Alloc_Ptr := To_Old_Alloc_Ptr (T.Table);
- New_Table : constant Alloc_Ptr :=
- new Alloc_Type'(Old_Table (Alloc_Type'Range));
+ New_Table : constant Alloc_Ptr := new Alloc_Type;
begin
- T.P.Last_Allocated := T.P.Last;
+ New_Table (Alloc_Type'Range) := Old_Table (Alloc_Type'Range);
+ T.P.Last_Allocated := New_Last_Alloc;
Free (Old_Table);
T.Table := To_Table_Ptr (New_Table);
end;
end if;
-
- pragma Assert (T.P.Last = T.P.Last_Allocated);
end Release;
--------------
-- Set_Last --
--------------
- procedure Set_Last (T : in out Instance; New_Val : Table_Count_Type) is
- pragma Assert (not T.Locked);
+ procedure Set_Last (T : in out Instance; New_Val : Table_Last_Type) is
begin
if New_Val > T.P.Last_Allocated then
Grow (T, New_Val);
-- --
-- S p e c --
-- --
--- Copyright (C) 2000-2016, AdaCore --
+-- Copyright (C) 2000-2017, AdaCore --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- arrays as closely as possible with the one additional capability of
-- dynamically modifying the value of the Last attribute.
--- This package provides a facility similar to that of GNAT.Table, except
--- that this package declares a type that can be used to define dynamic
--- instances of the table, while an instantiation of GNAT.Table creates a
--- single instance of the table type.
+-- This package provides a facility similar to that of Ada.Containers.Vectors.
-- Note that these three interfaces should remain synchronized to keep as much
--- coherency as possible among these three related units:
+-- coherency as possible among these related units:
--
-- GNAT.Dynamic_Tables
-- GNAT.Table
type Table_Component_Type is private;
type Table_Index_Type is range <>;
- Table_Low_Bound : Table_Index_Type;
- Table_Initial : Positive := 8;
- Table_Increment : Natural := 100;
+ Table_Low_Bound : Table_Index_Type;
+ Table_Initial : Positive := 8;
+ Table_Increment : Natural := 100;
+ Release_Threshold : Natural := 0; -- size in bytes
package GNAT.Dynamic_Tables is
-- The lower bound of Table_Index_Type is ignored.
- pragma Assert (Table_Low_Bound /= Table_Index_Type'Base'First);
+ -- Table_Component_Type must not be a type with controlled parts.
- function First return Table_Index_Type;
- pragma Inline (First);
- -- Export First as synonym for Table_Low_Bound (parallel with use of Last)
+ -- The Table_Initial value controls the allocation of the table when
+ -- it is first allocated.
+
+ -- The Table_Increment value controls the amount of increase, if the
+ -- table has to be increased in size. The value given is a percentage
+ -- value (e.g. 100 = increase table size by 100%, i.e. double it).
+
+ -- The Last and Set_Last subprograms provide control over the current
+ -- logical allocation. They are quite efficient, so they can be used
+ -- freely (expensive reallocation occurs only at major granularity
+ -- chunks controlled by the allocation parameters).
+
+ -- Note: we do not make the table components aliased, since this would
+ -- restrict the use of table for discriminated types. If it is necessary
+ -- to take the access of a table element, use Unrestricted_Access.
+
+ -- WARNING: On HPPA, the virtual addressing approach used in this unit
+ -- is incompatible with the indexing instructions on the HPPA. So when
+ -- using this unit, compile your application with -mdisable-indexing.
+
+ -- WARNING: If the table is reallocated, then the address of all its
+ -- components will change. So do not capture the address of an element
+ -- and then use the address later after the table may be reallocated.
+ -- One tricky case of this is passing an element of the table to a
+ -- subprogram by reference where the table gets reallocated during
+ -- the execution of the subprogram. The best rule to follow is never
+ -- to pass a table element as a parameter except for the case of IN
+ -- mode parameters with scalar values.
+
+ pragma Assert (Table_Low_Bound /= Table_Index_Type'Base'First);
subtype Valid_Table_Index_Type is Table_Index_Type'Base
range Table_Low_Bound .. Table_Index_Type'Base'Last;
- subtype Table_Count_Type is Table_Index_Type'Base
+ subtype Table_Last_Type is Table_Index_Type'Base
range Table_Low_Bound - 1 .. Table_Index_Type'Base'Last;
-- Table_Component_Type must not be a type with controlled parts.
-- Table : Table_Type renames T.Table (First .. Last (T));
- -- and the refer to components of Table.
+ -- and then refer to components of Table.
type Table_Ptr is access all Big_Table_Type;
for Table_Ptr'Storage_Size use 0;
-- an empty array.
type Instance is record
- Table : aliased Table_Ptr :=
+ Table : Table_Ptr :=
Empty_Table_Array_Ptr_To_Table_Ptr (Empty_Table_Array'Access);
-- The table itself. The lower bound is the value of First. Logically
-- the upper bound is the current value of Last (although the actual
-- to ensure bounds checking, as in:
--
-- Tab : Table_Type renames X.Table (First .. X.Last);
+ --
+ -- Note: The Table component must come first. See declarations of
+ -- SCO_Unit_Table and SCO_Table in scos.h.
Locked : Boolean := False;
- -- 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.
+ -- 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.
P : Table_Private;
end record;
+ function Is_Empty (T : Instance) return Boolean;
+
procedure Init (T : in out Instance);
-- Reinitializes the table to empty. There is no need to call this before
-- using a table; tables default to empty.
- function Last (T : Instance) return Table_Count_Type;
+ function First return Table_Index_Type;
+ pragma Inline (First);
+ -- Export First as synonym for Table_Low_Bound (parallel with use of Last)
+
+ function Last (T : Instance) return Table_Last_Type;
pragma Inline (Last);
-- Returns the current value of the last used entry in the table, which can
-- then be used as a subscript for Table.
procedure Release (T : in out Instance);
-- Storage is allocated in chunks according to the values given in the
- -- Table_Initial and Table_Increment parameters. A call to Release releases
- -- all storage that is allocated, but is not logically part of the current
- -- array value. Current array values are not affected by this call.
+ -- Table_Initial and Table_Increment parameters. If Release_Threshold is 0
+ -- or the length of the table does not exceed this threshold then a call to
+ -- Release releases all storage that is allocated, but is not logically
+ -- part of the current array value; otherwise the call to Release leaves
+ -- the current array value plus 0.1% of the current table length free
+ -- elements located at the end of the table. This parameter facilitates
+ -- reopening large tables and adding a few elements without allocating a
+ -- chunk of memory. In both cases current array values are not affected by
+ -- this call.
procedure Free (T : in out Instance);
-- Same as Init
- procedure Set_Last (T : in out Instance; New_Val : Table_Count_Type);
+ procedure Set_Last (T : in out Instance; New_Val : Table_Last_Type);
pragma Inline (Set_Last);
-- This procedure sets Last to the indicated value. If necessary the table
-- is reallocated to accommodate the new value (i.e. on return the
pragma Inline (Set_Item);
-- Put Item in the table at position Index. If Index points to an existing
-- item (i.e. it is in the range First .. Last (T)), the item is replaced.
- -- Otherwise (i.e. Index > Last (T), the table is expanded, and Last is set
- -- to Index.
+ -- Otherwise (i.e. Index > Last (T)), the table is expanded, and Last is
+ -- set to Index.
+
+ procedure Move (From, To : in out Instance);
+ -- Moves from From to To, and sets From to empty
procedure Allocate (T : in out Instance; Num : Integer := 1);
pragma Inline (Allocate);
private
type Table_Private is record
- Last_Allocated : Table_Count_Type := Table_Low_Bound - 1;
+ Last_Allocated : Table_Last_Type := Table_Low_Bound - 1;
-- Subscript of the maximum entry in the currently allocated table.
-- Initial value ensures that we initially allocate the table.
- Last : Table_Count_Type := Table_Low_Bound - 1;
+ Last : Table_Last_Type := Table_Low_Bound - 1;
-- Current value of Last function
-- Invariant: Last <= Last_Allocated
-- --
------------------------------------------------------------------------------
-with GNAT.Heap_Sort_G;
-
with System; use System;
with System.Memory; use System.Memory;
package body GNAT.Table is
- Min : constant Integer := Integer (Table_Low_Bound);
- -- Subscript of the minimum entry in the currently allocated table
-
- Max : Integer;
- -- Subscript of the maximum entry in the currently allocated table
-
- Length : Integer := 0;
- -- Number of entries in currently allocated table. The value of zero
- -- ensures that we initially allocate the table.
-
- Last_Val : Integer;
- -- Current value of Last
-
- -----------------------
- -- Local Subprograms --
- -----------------------
-
- procedure Reallocate;
- -- Reallocate the existing table according to the current value stored
- -- in Max. Works correctly to do an initial allocation if the table
- -- is currently null.
-
- pragma Warnings (Off);
- -- Turn off warnings. The following unchecked conversions are only used
- -- internally in this package, and cannot never result in any instances
- -- of improperly aliased pointers for the client of the package.
-
- function To_Address is new Ada.Unchecked_Conversion (Table_Ptr, Address);
- function To_Pointer is new Ada.Unchecked_Conversion (Address, Table_Ptr);
-
- pragma Warnings (On);
-
--------------
-- Allocate --
--------------
- function Allocate (Num : Integer := 1) return Table_Index_Type is
- Old_Last : constant Integer := Last_Val;
-
+ procedure Allocate (Num : Integer := 1) is
begin
- Last_Val := Last_Val + Num;
-
- if Last_Val > Max then
- Reallocate;
- end if;
+ Tab.Allocate (The_Instance, Num);
+ end Allocate;
- return Table_Index_Type (Old_Last + 1);
+ function Allocate (Num : Integer := 1) return Valid_Table_Index_Type is
+ Result : constant Valid_Table_Index_Type := Last + 1;
+ begin
+ Allocate (Num);
+ return Result;
end Allocate;
------------
procedure Append (New_Val : Table_Component_Type) is
begin
- Set_Item (Table_Index_Type (Last_Val + 1), New_Val);
+ Tab.Append (The_Instance, New_Val);
end Append;
----------------
procedure Append_All (New_Vals : Table_Type) is
begin
- for J in New_Vals'Range loop
- Append (New_Vals (J));
- end loop;
+ Tab.Append_All (The_Instance, New_Vals);
end Append_All;
--------------------
procedure Decrement_Last is
begin
- Last_Val := Last_Val - 1;
+ Tab.Decrement_Last (The_Instance);
end Decrement_Last;
-----------
function First return Table_Index_Type is
begin
- return Table_Low_Bound;
+ return Tab.First;
end First;
--------------
--------------
procedure For_Each is
- Quit : Boolean := False;
+ procedure For_Each is new Tab.For_Each (Action);
begin
- for Index in Table_Low_Bound .. Table_Index_Type (Last_Val) loop
- Action (Index, Table (Index), Quit);
- exit when Quit;
- end loop;
+ For_Each (The_Instance);
end For_Each;
----------
procedure Free is
begin
- Free (To_Address (Table));
- Table := null;
- Length := 0;
+ Tab.Free (The_Instance);
end Free;
--------------------
procedure Increment_Last is
begin
- Last_Val := Last_Val + 1;
-
- if Last_Val > Max then
- Reallocate;
- end if;
+ Tab.Increment_Last (The_Instance);
end Increment_Last;
+ --------------
+ -- Is_Empty --
+ --------------
+
+ function Is_Empty return Boolean is
+ begin
+ return Tab.Is_Empty (The_Instance);
+ end Is_Empty;
+
----------
-- Init --
----------
procedure Init is
- Old_Length : constant Integer := Length;
-
begin
- Last_Val := Min - 1;
- Max := Min + Table_Initial - 1;
- Length := Max - Min + 1;
-
- -- If table is same size as before (happens when table is never
- -- expanded which is a common case), then simply reuse it. Note
- -- that this also means that an explicit Init call right after
- -- the implicit one in the package body is harmless.
-
- if Old_Length = Length then
- return;
-
- -- Otherwise we can use Reallocate to get a table of the right size.
- -- Note that Reallocate works fine to allocate a table of the right
- -- initial size when it is first allocated.
-
- else
- Reallocate;
- end if;
+ Tab.Init (The_Instance);
end Init;
----------
-- Last --
----------
- function Last return Table_Index_Type is
+ function Last return Table_Last_Type is
begin
- return Table_Index_Type (Last_Val);
+ return Tab.Last (The_Instance);
end Last;
- ----------------
- -- Reallocate --
- ----------------
-
- procedure Reallocate is
- New_Size : size_t;
- New_Length : Long_Long_Integer;
-
- begin
- if Max < Last_Val then
- pragma Assert (not Locked);
-
- -- Now increment table length until it is sufficiently large. Use
- -- the increment value or 10, which ever is larger (the reason
- -- for the use of 10 here is to ensure that the table does really
- -- increase in size (which would not be the case for a table of
- -- length 10 increased by 3% for instance). Do the intermediate
- -- calculation in Long_Long_Integer to avoid overflow.
-
- while Max < Last_Val loop
- New_Length :=
- Long_Long_Integer (Length) *
- (100 + Long_Long_Integer (Table_Increment)) / 100;
- Length := Integer'Max (Integer (New_Length), Length + 10);
- Max := Min + Length - 1;
- end loop;
- end if;
-
- New_Size :=
- size_t ((Max - Min + 1) *
- (Table_Type'Component_Size / Storage_Unit));
-
- if Table = null then
- Table := To_Pointer (Alloc (New_Size));
-
- elsif New_Size > 0 then
- Table :=
- To_Pointer (Realloc (Ptr => To_Address (Table),
- Size => New_Size));
- end if;
-
- if Length /= 0 and then Table = null then
- raise Storage_Error;
- end if;
-
- end Reallocate;
-
-------------
-- Release --
-------------
procedure Release is
begin
- Length := Last_Val - Integer (Table_Low_Bound) + 1;
- Max := Last_Val;
- Reallocate;
+ Tab.Release (The_Instance);
end Release;
+ -------------
+ -- Restore --
+ -------------
+
+ procedure Restore (T : in out Saved_Table) is
+ begin
+ Init;
+ Tab.Move (From => T, To => The_Instance);
+ end Restore;
+
+ ----------
+ -- Save --
+ ----------
+
+ function Save return Saved_Table is
+ Result : Saved_Table;
+ begin
+ Tab.Move (From => The_Instance, To => Result);
+ return Result;
+ end Save;
+
--------------
-- Set_Item --
--------------
procedure Set_Item
- (Index : Table_Index_Type;
- Item : Table_Component_Type)
+ (Index : Valid_Table_Index_Type;
+ Item : Table_Component_Type)
is
- -- If Item is a value within the current allocation, and we are going to
- -- reallocate, then we must preserve an intermediate copy here before
- -- calling Increment_Last. Otherwise, if Table_Component_Type is passed
- -- by reference, we are going to end up copying from storage that might
- -- have been deallocated from Increment_Last calling Reallocate.
-
- subtype Allocated_Table_T is
- Table_Type (Table'First .. Table_Index_Type (Max + 1));
- -- A constrained table subtype one element larger than the currently
- -- allocated table.
-
- Allocated_Table_Address : constant System.Address :=
- Table.all'Address;
- -- Used for address clause below (we can't use non-static expression
- -- Table.all'Address directly in the clause because some older versions
- -- of the compiler do not allow it).
-
- Allocated_Table : Allocated_Table_T;
- pragma Import (Ada, Allocated_Table);
- pragma Suppress (Range_Check, On => Allocated_Table);
- for Allocated_Table'Address use Allocated_Table_Address;
- -- Allocated_Table represents the currently allocated array, plus one
- -- element (the supplementary element is used to have a convenient
- -- way of computing the address just past the end of the current
- -- allocation). Range checks are suppressed because this unit uses
- -- direct calls to System.Memory for allocation, and this can yield
- -- misaligned storage (and we cannot rely on the bootstrap compiler
- -- supporting specifically disabling alignment checks, so we need to
- -- suppress all range checks). It is safe to suppress this check here
- -- because we know that a (possibly misaligned) object of that type
- -- does actually exist at that address. ??? We should really improve
- -- the allocation circuitry here to
- -- guarantee proper alignment.
-
- Need_Realloc : constant Boolean := Integer (Index) > Max;
- -- True if this operation requires storage reallocation (which may
- -- involve moving table contents around).
-
begin
- -- If we're going to reallocate, check whether Item references an
- -- element of the currently allocated table.
-
- if Need_Realloc
- and then Allocated_Table'Address <= Item'Address
- and then Item'Address <
- Allocated_Table (Table_Index_Type (Max + 1))'Address
- then
- -- If so, save a copy on the stack because Increment_Last will
- -- reallocate storage and might deallocate the current table.
-
- declare
- Item_Copy : constant Table_Component_Type := Item;
- begin
- Set_Last (Index);
- Table (Index) := Item_Copy;
- end;
-
- else
- -- Here we know that either we won't reallocate (case of Index < Max)
- -- or that Item is not in the currently allocated table.
-
- if Integer (Index) > Last_Val then
- Set_Last (Index);
- end if;
-
- Table (Index) := Item;
- end if;
+ Tab.Set_Item (The_Instance, Index, Item);
end Set_Item;
--------------
-- Set_Last --
--------------
- procedure Set_Last (New_Val : Table_Index_Type) is
+ procedure Set_Last (New_Val : Table_Last_Type) is
begin
- if Integer (New_Val) < Last_Val then
- Last_Val := Integer (New_Val);
- else
- Last_Val := Integer (New_Val);
-
- if Last_Val > Max then
- Reallocate;
- end if;
- end if;
+ Tab.Set_Last (The_Instance, New_Val);
end Set_Last;
----------------
----------------
procedure Sort_Table is
-
- Temp : Table_Component_Type;
- -- A temporary position to simulate index 0
-
- -- Local subprograms
-
- function Index_Of (Idx : Natural) return Table_Index_Type;
- -- Return index of Idx'th element of table
-
- function Lower_Than (Op1, Op2 : Natural) return Boolean;
- -- Compare two components
-
- procedure Move (From : Natural; To : Natural);
- -- Move one component
-
- package Heap_Sort is new GNAT.Heap_Sort_G (Move, Lower_Than);
-
- --------------
- -- Index_Of --
- --------------
-
- function Index_Of (Idx : Natural) return Table_Index_Type is
- J : constant Integer'Base := Table_Index_Type'Pos (First) + Idx - 1;
- begin
- return Table_Index_Type'Val (J);
- end Index_Of;
-
- ----------
- -- Move --
- ----------
-
- procedure Move (From : Natural; To : Natural) is
- begin
- if From = 0 then
- Table (Index_Of (To)) := Temp;
- elsif To = 0 then
- Temp := Table (Index_Of (From));
- else
- Table (Index_Of (To)) := Table (Index_Of (From));
- end if;
- end Move;
-
- ----------------
- -- Lower_Than --
- ----------------
-
- function Lower_Than (Op1, Op2 : Natural) return Boolean is
- begin
- if Op1 = 0 then
- return Lt (Temp, Table (Index_Of (Op2)));
- elsif Op2 = 0 then
- return Lt (Table (Index_Of (Op1)), Temp);
- else
- return Lt (Table (Index_Of (Op1)), Table (Index_Of (Op2)));
- end if;
- end Lower_Than;
-
- -- Start of processing for Sort_Table
-
+ procedure Sort_Table is new Tab.Sort_Table (Lt);
begin
- Heap_Sort.Sort (Natural (Last - First) + 1);
+ Sort_Table (The_Instance);
end Sort_Table;
-begin
- Init;
end GNAT.Table;
-- --
------------------------------------------------------------------------------
--- Resizable one dimensional array support
+-- This package provides a singleton version of GNAT.Dynamic_Tables
+-- (g-dyntab.ads). See that package for documentation. This package just
+-- declares a single instance of GNAT.Dynamic_Tables.Instance, and provides
+-- wrappers for all the subprograms, passing that single instance.
--- This package provides an implementation of dynamically resizable one
--- dimensional arrays. The idea is to mimic the normal Ada semantics for
--- arrays as closely as possible with the one additional capability of
--- dynamically modifying the value of the Last attribute.
+-- Note that these three interfaces should remain synchronized to keep as much
+-- coherency as possible among these related units:
+--
+-- GNAT.Dynamic_Tables
+-- GNAT.Table
+-- Table (the compiler unit)
--- This package provides a facility similar to that of GNAT.Dynamic_Tables,
--- except that this package declares a single instance of the table type,
--- while an instantiation of GNAT.Dynamic_Tables creates a type that can be
--- used to define dynamic instances of the table.
+pragma Compiler_Unit_Warning;
--- Note that this interface should remain synchronized with those in
--- GNAT.Dynamic_Tables and the GNAT compiler source unit Table to keep
--- as much coherency as possible between these three related units.
+with GNAT.Dynamic_Tables;
generic
type Table_Component_Type is private;
type Table_Index_Type is range <>;
- Table_Low_Bound : Table_Index_Type;
- Table_Initial : Positive;
- Table_Increment : Natural;
+ Table_Low_Bound : Table_Index_Type;
+ Table_Initial : Positive := 8;
+ Table_Increment : Natural := 100;
+ Table_Name : String := ""; -- for debugging printouts
+ pragma Unreferenced (Table_Name);
+ Release_Threshold : Natural := 0;
package GNAT.Table is
pragma Elaborate_Body;
- -- Table_Component_Type and Table_Index_Type specify the type of the
- -- array, Table_Low_Bound is the lower bound. Table_Index_Type must be an
- -- integer type. The effect is roughly to declare:
-
- -- Table : array (Table_Index_Type range Table_Low_Bound .. <>)
- -- of Table_Component_Type;
-
- -- Note: since the upper bound can be one less than the lower
- -- bound for an empty array, the table index type must be able
- -- to cover this range, e.g. if the lower bound is 1, then the
- -- Table_Index_Type should be Natural rather than Positive.
-
- -- Table_Component_Type may be any Ada type, except that controlled
- -- types are not supported. Note however that default initialization
- -- will NOT occur for array components.
-
- -- The Table_Initial values controls the allocation of the table when
- -- it is first allocated, either by default, or by an explicit Init call.
-
- -- The Table_Increment value controls the amount of increase, if the
- -- table has to be increased in size. The value given is a percentage
- -- value (e.g. 100 = increase table size by 100%, i.e. double it).
-
- -- The Last and Set_Last subprograms provide control over the current
- -- logical allocation. They are quite efficient, so they can be used
- -- freely (expensive reallocation occurs only at major granularity
- -- chunks controlled by the allocation parameters).
-
- -- Note: we do not make the table components aliased, since this would
- -- restrict the use of table for discriminated types. If it is necessary
- -- to take the access of a table element, use Unrestricted_Access.
-
- -- WARNING: On HPPA, the virtual addressing approach used in this unit
- -- is incompatible with the indexing instructions on the HPPA. So when
- -- using this unit, compile your application with -mdisable-indexing.
-
- -- WARNING: If the table is reallocated, then the address of all its
- -- components will change. So do not capture the address of an element
- -- and then use the address later after the table may be reallocated.
- -- One tricky case of this is passing an element of the table to a
- -- subprogram by reference where the table gets reallocated during
- -- the execution of the subprogram. The best rule to follow is never
- -- to pass a table element as a parameter except for the case of IN
- -- mode parameters with scalar values.
-
- type Table_Type is
- array (Table_Index_Type range <>) of Table_Component_Type;
- subtype Big_Table_Type is
- Table_Type (Table_Low_Bound .. Table_Index_Type'Last);
- -- We work with pointers to a bogus array type that is constrained
- -- with the maximum possible range bound. This means that the pointer
- -- is a thin pointer, which is more efficient. Since subscript checks
- -- in any case must be on the logical, rather than physical bounds,
- -- safety is not compromised by this approach. These types should never
- -- be used by the client.
-
- type Table_Ptr is access all Big_Table_Type;
- for Table_Ptr'Storage_Size use 0;
- -- The table is actually represented as a pointer to allow reallocation.
- -- This type should never be used by the client.
-
- Table : aliased Table_Ptr := null;
- -- The table itself. The lower bound is the value of Low_Bound.
- -- Logically the upper bound is the current value of Last (although
- -- the actual size of the allocated table may be larger than this).
- -- The program may only access and modify Table entries in the range
- -- First .. Last.
-
- Locked : Boolean := False;
- -- 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.
+ package Tab is new GNAT.Dynamic_Tables
+ (Table_Component_Type,
+ Table_Index_Type,
+ Table_Low_Bound,
+ Table_Initial,
+ Table_Increment,
+ Release_Threshold);
+
+ subtype Valid_Table_Index_Type is Tab.Valid_Table_Index_Type;
+ subtype Table_Last_Type is Tab.Table_Last_Type;
+ subtype Table_Type is Tab.Table_Type;
+ subtype Big_Table_Type is Tab.Big_Table_Type;
+
+ subtype Table_Ptr is Tab.Table_Ptr;
+
+ The_Instance : Tab.Instance;
+ Table : Table_Ptr renames The_Instance.Table;
+ Locked : Boolean renames The_Instance.Locked;
+
+ function Is_Empty return Boolean;
procedure Init;
- -- This procedure allocates a new table of size Initial (freeing any
- -- previously allocated larger table). It is not necessary to call
- -- Init when a table is first instantiated (since the instantiation does
- -- the same initialization steps). However, it is harmless to do so, and
- -- Init is convenient in reestablishing a table for new use.
- function Last return Table_Index_Type;
+ function First return Table_Index_Type;
+ pragma Inline (First);
+
+ function Last return Table_Last_Type;
pragma Inline (Last);
- -- Returns the current value of the last used entry in the table, which
- -- can then be used as a subscript for Table. Note that the only way to
- -- modify Last is to call the Set_Last procedure. Last must always be
- -- used to determine the logically last entry.
procedure Release;
- -- Storage is allocated in chunks according to the values given in the
- -- Initial and Increment parameters. A call to Release releases all
- -- storage that is allocated, but is not logically part of the current
- -- array value. Current array values are not affected by this call.
procedure Free;
- -- Free all allocated memory for the table. A call to Init is required
- -- before any use of this table after calling Free.
- function First return Table_Index_Type;
- pragma Inline (First);
- -- Export First as synonym for Table_Low_Bound (parallel with use of Last)
-
- procedure Set_Last (New_Val : Table_Index_Type);
+ procedure Set_Last (New_Val : Table_Last_Type);
pragma Inline (Set_Last);
- -- This procedure sets Last to the indicated value. If necessary the
- -- table is reallocated to accommodate the new value (i.e. on return
- -- the allocated table has an upper bound of at least Last). If Set_Last
- -- reduces the size of the table, then logically entries are removed
- -- from the table. If Set_Last increases the size of the table, then
- -- new entries are logically added to the table.
procedure Increment_Last;
pragma Inline (Increment_Last);
- -- Adds 1 to Last (same as Set_Last (Last + 1)
procedure Decrement_Last;
pragma Inline (Decrement_Last);
- -- Subtracts 1 from Last (same as Set_Last (Last - 1)
procedure Append (New_Val : Table_Component_Type);
pragma Inline (Append);
- -- Equivalent to:
- -- x.Increment_Last;
- -- x.Table (x.Last) := New_Val;
- -- i.e. the table size is increased by one, and the given new item
- -- stored in the newly created table element.
procedure Append_All (New_Vals : Table_Type);
- -- Appends all components of New_Vals
procedure Set_Item
- (Index : Table_Index_Type;
+ (Index : Valid_Table_Index_Type;
Item : Table_Component_Type);
pragma Inline (Set_Item);
- -- Put Item in the table at position Index. The table is expanded if the
- -- current table length is less than Index and in that case Last is set to
- -- Index. Item will replace any value already present in the table at this
- -- position.
- function Allocate (Num : Integer := 1) return Table_Index_Type;
+ subtype Saved_Table is Tab.Instance;
+ -- Type used for Save/Restore subprograms
+
+ function Save return Saved_Table;
+ -- Resets table to empty, but saves old contents of table in returned
+ -- value, for possible later restoration by a call to Restore.
+
+ procedure Restore (T : in out Saved_Table);
+ -- Given a Saved_Table value returned by a prior call to Save, restores
+ -- the table to the state it was in at the time of the Save call.
+
+ procedure Allocate (Num : Integer := 1);
+ function Allocate (Num : Integer := 1) return Valid_Table_Index_Type;
pragma Inline (Allocate);
- -- Adds Num to Last, and returns the old value of Last + 1. Note that
- -- this function has the possible side effect of reallocating the table.
- -- This means that a reference X.Table (X.Allocate) is incorrect, since
- -- the call to X.Allocate may modify the results of calling X.Table.
+ -- Adds Num to Last. The function version also returns the old value of
+ -- Last + 1. Note that this function has the possible side effect of
+ -- reallocating the table. This means that a reference X.Table (X.Allocate)
+ -- is incorrect, since the call to X.Allocate may modify the results of
+ -- calling X.Table.
generic
with procedure Action
- (Index : Table_Index_Type;
+ (Index : Valid_Table_Index_Type;
Item : Table_Component_Type;
Quit : in out Boolean) is <>;
procedure For_Each;
- -- Calls procedure Action for each component of the table, or until
- -- one of these calls set Quit to True.
generic
with function Lt (Comp1, Comp2 : Table_Component_Type) return Boolean;
procedure Sort_Table;
- -- This procedure sorts the components of the table into ascending
- -- order making calls to Lt to do required comparisons, and using
- -- assignments to move components around. The Lt function returns True
- -- if Comp1 is less than Comp2 (in the sense of the desired sort), and
- -- False if Comp1 is greater than Comp2. For equal objects it does not
- -- matter if True or False is returned (it is slightly more efficient
- -- to return False). The sort is not stable (the order of equal items
- -- in the table is not preserved).
end GNAT.Table;
with Debug; use Debug;
with Opt; use Opt;
with Output; use Output;
+with System; use System;
with Tree_IO; use Tree_IO;
with Widechar; use Widechar;
Name_Entries.Release;
end Lock;
- ------------------------
- -- Name_Chars_Address --
- ------------------------
-
- function Name_Chars_Address return System.Address is
- begin
- return Name_Chars.Table (0)'Address;
- end Name_Chars_Address;
-
----------------
-- Name_Enter --
----------------
return Name_Enter (Buf);
end Name_Enter;
- --------------------------
- -- Name_Entries_Address --
- --------------------------
-
- function Name_Entries_Address return System.Address is
- begin
- return Name_Entries.Table (First_Name_Id)'Address;
- end Name_Entries_Address;
-
------------------------
-- Name_Entries_Count --
------------------------
with Alloc;
with Hostparm; use Hostparm;
with Table;
-with System; use System;
with Types; use Types;
package Namet is
-- Like Write_Name, except that the name written is the decoded name, as
-- described for Append_Decoded.
- function Name_Chars_Address return System.Address;
- -- Return starting address of name characters table (used in Back_End call
- -- to Gigi).
-
- function Name_Entries_Address return System.Address;
- -- Return starting address of Names table (used in Back_End call to Gigi)
-
function Name_Entries_Count return Nat;
-- Return current number of entries in the names table
* *
* C Header File *
* *
- * 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- *
};
/* Pointer to names table vector. */
-#define Names_Ptr namet__name_entries__table
+#define Names_Ptr namet__name_entries__tab__the_instance
extern struct Name_Entry *Names_Ptr;
/* Pointer to name characters table. */
-#define Name_Chars_Ptr namet__name_chars__table
+#define Name_Chars_Ptr namet__name_chars__tab__the_instance
extern char *Name_Chars_Ptr;
/* This is Hostparm.Max_Line_Length. */
-- The suffixes used for the ALI files
function Prep_Suffix return String;
- -- The suffix used for pre-processed files
+ -- The suffix used for preprocessed files
private
typedef struct SCO_Unit_Table_Entry *SCO_Unit_Table_Type;
-extern SCO_Unit_Table_Type scos__sco_unit_table__table;
-#define SCO_Unit_Table scos__sco_unit_table__table
+/* The following depends on the fact that The_Instance.Table
+ is the first component. */
+extern SCO_Unit_Table_Type scos__sco_unit_table__the_instance;
+#define SCO_Unit_Table scos__sco_unit_table__the_instance
extern Int scos__sco_unit_table__first(void);
#define SCO_Unit_Table_First scos__sco_unit_table__first
typedef struct SCO_Table_Entry *SCO_Table_Type;
-extern SCO_Table_Type scos__sco_table__table;
-#define SCO_Table scos__sco_table__table
+/* The following depends on the fact that The_Instance.Table
+ is the first component. */
+extern SCO_Table_Type scos__sco_table__the_instance;
+#define SCO_Table scos__sco_table__the_instance
extern Int scos__sco_table__first(void);
#define SCO_Table_First scos__sco_table__first
-- Elab_Call.Last) indicates the current depth of recursion and is used to
-- identify the outer level.
- type Elab_Call_Entry is record
+ type Elab_Call_Element is record
Cloc : Source_Ptr;
Ent : Entity_Id;
end record;
package Elab_Call is new Table.Table
- (Table_Component_Type => Elab_Call_Entry,
+ (Table_Component_Type => Elab_Call_Element,
Table_Index_Type => Int,
Table_Low_Bound => 1,
Table_Initial => 50,
Table_Increment => 100,
Table_Name => "Elab_Call");
- -- This table is initialized at the start of each outer level call. It
- -- holds the entities for all subprograms that have been examined for this
- -- particular outer level call, and is used to prevent both infinite
- -- recursion, and useless reanalysis of bodies already seen
+ -- The following table records all calls that have been processed starting
+ -- from an outer level call. The table prevents both infinite recursion and
+ -- useless reanalysis of calls within the same context. The use of context
+ -- is important because it allows for proper checks in more complex code:
+
+ -- if ... then
+ -- Call; -- requires a check
+ -- Call; -- does not need a check thanks to the table
+ -- elsif ... then
+ -- Call; -- requires a check, different context
+ -- end if;
+
+ -- Call; -- requires a check, different context
+
+ type Visited_Element is record
+ Subp_Id : Entity_Id;
+ -- The entity of the subprogram being called
+
+ Context : Node_Id;
+ -- The context where the call to the subprogram occurs
+ end record;
package Elab_Visited is new Table.Table
- (Table_Component_Type => Entity_Id,
+ (Table_Component_Type => Visited_Element,
Table_Index_Type => Int,
Table_Low_Bound => 1,
Table_Initial => 200,
Table_Increment => 100,
Table_Name => "Elab_Visited");
- -- This table stores calls to Check_Internal_Call that are delayed until
- -- all generics are instantiated and in particular until after all generic
- -- bodies have been inserted. We need to delay, because we need to be able
- -- to look through the inserted bodies.
+ -- The following table records delayed calls which must be examined after
+ -- all generic bodies have been instantiated.
type Delay_Element is record
N : Node_Id;
loop
if (Suppress_Elaboration_Warnings (Ent)
- or else Elaboration_Checks_Suppressed (Ent))
+ or else Elaboration_Checks_Suppressed (Ent))
and then (Inst_Case or else No (Alias (Ent)))
then
return;
Is_Internal_File_Name (Unit_File_Name (Get_Source_Unit (C_Scope)));
end if;
- -- Do not give a warning if the with'ed unit is internal and the
- -- caller is not internal (since the binder always elaborates
- -- internal units first).
+ -- Do not give a warning if the with'ed unit is internal and the caller
+ -- is not internal (since the binder always elaborates internal units
+ -- first).
- if Callee_Unit_Internal and (not Caller_Unit_Internal) then
+ if Callee_Unit_Internal and not Caller_Unit_Internal then
return;
end if;
- -- For now, if debug flag -gnatdE is not set, do no checking for
- -- one internal unit withing another. This fixes the problem with
- -- the sgi build and storage errors. To be resolved later ???
+ -- For now, if debug flag -gnatdE is not set, do no checking for one
+ -- internal unit withing another. This fixes the problem with the sgi
+ -- build and storage errors. To be resolved later ???
if (Callee_Unit_Internal and Caller_Unit_Internal)
and not Debug_Flag_EE
-- All_Errors_Mode.
if not All_Errors_Mode and not Dynamic_Elaboration_Checks then
- Set_Suppress_Elaboration_Warnings (W_Scope, True);
+ Set_Suppress_Elaboration_Warnings (W_Scope);
end if;
end if;
then
Error_Msg_Node_2 := W_Scope;
Error_Msg_NE
- ("info: call to& in elaboration code " &
- "requires pragma Elaborate_All on&?$?", N, E);
+ ("info: call to& in elaboration code requires pragma "
+ & "Elaborate_All on&?$?", N, E);
end if;
-- Set indication for binder to generate Elaborate_All
return;
end if;
- -- Nothing to do if this is a recursive call (i.e. a call to
- -- an entity that is already in the Elab_Call stack)
+ -- Determine whether a prior call to the same subprogram was already
+ -- examined within the same context. If this is the case, then there is
+ -- no need to proceed with the various warnings and checks because the
+ -- work was already done for the previous call.
- for J in 1 .. Elab_Visited.Last loop
- if Ent = Elab_Visited.Table (J) then
- return;
- end if;
- end loop;
+ declare
+ Self : constant Visited_Element :=
+ (Subp_Id => Ent, Context => Parent (N));
+
+ begin
+ for Index in 1 .. Elab_Visited.Last loop
+ if Self = Elab_Visited.Table (Index) then
+ return;
+ end if;
+ end loop;
+ end;
-- See if we need to analyze this reference. We analyze it if either of
-- the following conditions is met:
Outer_Level_Sloc := Loc;
end if;
- Elab_Visited.Append (E);
-
-- If the call is to a function that renames a literal, no check needed
if Ekind (E) = E_Enumeration_Literal then
return;
end if;
+ -- Register the subprogram as examined within this particular context.
+ -- This ensures that calls to the same subprogram but in different
+ -- contexts receive warnings and checks of their own since the calls
+ -- may be reached through different flow paths.
+
+ Elab_Visited.Append ((Subp_Id => E, Context => Parent (N)));
+
Sbody := Unit_Declaration_Node (E);
if not Nkind_In (Sbody, N_Subprogram_Body, N_Package_Body) then
then
null;
- -- If we have the instantiation case we are done, since we now
- -- know that the body of the generic appeared earlier.
+ -- If we have the instantiation case we are done, since we now know that
+ -- the body of the generic appeared earlier.
elsif Inst_Case then
return;
if GNATprove_Mode then
null;
- -- Deal with dynamic elaboration check
+ -- Generate an elaboration check
elsif not Elaboration_Checks_Suppressed (E) then
Set_Elaboration_Entity_Required (E);
- -- Case of no elaboration entity allocated yet
+ -- Create a declaration of the elaboration entity, and insert it
+ -- prior to the subprogram or the generic unit, within the same
+ -- scope. Since the subprogram may be overloaded, create a unique
+ -- entity.
if No (Elaboration_Entity (E)) then
-
- -- Create object declaration for elaboration entity, and put it
- -- just in front of the spec of the subprogram or generic unit,
- -- in the same scope as this unit. The subprogram may be over-
- -- loaded, so make the name of elaboration entity unique by
- -- means of a numeric suffix.
-
declare
Loce : constant Source_Ptr := Sloc (E);
Ent : constant Entity_Id :=
Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Chars (E), 'E', -1));
+ New_External_Name (Chars (E), 'E', -1));
begin
Set_Elaboration_Entity (E, Ent);
end;
end if;
- -- Generate check of the elaboration counter
+ -- Generate:
+ -- if Enn = 0 then
+ -- raise Program_Error with "access before elaboration";
+ -- end if;
Insert_Elab_Check (N,
- Make_Attribute_Reference (Loc,
- Attribute_Name => Name_Elaborated,
- Prefix => New_Occurrence_Of (E, Loc)));
+ Make_Attribute_Reference (Loc,
+ Attribute_Name => Name_Elaborated,
+ Prefix => New_Occurrence_Of (E, Loc)));
end if;
-- Generate the warning
("instantiation of& may occur before body is seen<l<",
N, Orig_Ent);
else
- -- A rather specific check. For Finalize/Adjust/Initialize,
- -- if the type has Warnings_Off set, suppress the warning.
+ -- A rather specific check. For Finalize/Adjust/Initialize, if
+ -- the type has Warnings_Off set, suppress the warning.
if Nam_In (Chars (E), Name_Adjust,
Name_Finalize,
Output_Calls (N, Check_Elab_Flag => False);
end if;
end if;
-
- -- Set flag to suppress further warnings on same subprogram
- -- unless in all errors mode
-
- if not All_Errors_Mode then
- Set_Suppress_Elaboration_Warnings (E);
- end if;
end Check_Internal_Call_Continue;
---------------------------
elsif Dynamic_Elaboration_Checks then
if not Elaboration_Checks_Suppressed (Ent)
and then not Cunit_SC
- and then
- not Restriction_Active (No_Entry_Calls_In_Elaboration_Code)
+ and then not Restriction_Active
+ (No_Entry_Calls_In_Elaboration_Code)
then
-- Runtime elaboration check required. Generate check of the
-- elaboration counter for the unit containing the entity.
Insert_Elab_Check (N,
Make_Attribute_Reference (Loc,
- Attribute_Name => Name_Elaborated,
- Prefix =>
- New_Occurrence_Of (Spec_Entity (Task_Scope), Loc)));
+ Prefix =>
+ New_Occurrence_Of (Spec_Entity (Task_Scope), Loc),
+ Attribute_Name => Name_Elaborated));
end if;
else
-- Force the binder to elaborate other unit first
- if not Suppress_Elaboration_Warnings (Ent)
+ if Elab_Info_Messages
+ and then not Suppress_Elaboration_Warnings (Ent)
and then not Elaboration_Checks_Suppressed (Ent)
- and then Elab_Info_Messages
and then not Suppress_Elaboration_Warnings (Task_Scope)
and then not Elaboration_Checks_Suppressed (Task_Scope)
then
Error_Msg_Node_2 := Task_Scope;
Error_Msg_NE
- ("info: activation of an instance of task type&" &
- " requires pragma Elaborate_All on &?$?", N, Ent);
+ ("info: activation of an instance of task type & requires "
+ & "pragma Elaborate_All on &?$?", N, Ent);
end if;
Activate_Elaborate_All_Desirable (N, Task_Scope);
Subp : Entity_Id;
Scop : Entity_Id)
is
- Elab_Unit : Entity_Id;
+ Elab_Unit : Entity_Id;
-- Check whether this is a call to an Initialize subprogram for a
-- controlled type. Note that Call can also be a 'Access attribute
-- reference, which now generates an elaboration check.
- Init_Call : constant Boolean :=
- Nkind (Call) = N_Procedure_Call_Statement
- and then Chars (Subp) = Name_Initialize
- and then Comes_From_Source (Subp)
- and then Present (Parameter_Associations (Call))
- and then Is_Controlled (Etype (First_Actual (Call)));
+ Init_Call : constant Boolean :=
+ Nkind (Call) = N_Procedure_Call_Statement
+ and then Chars (Subp) = Name_Initialize
+ and then Comes_From_Source (Subp)
+ and then Present (Parameter_Associations (Call))
+ and then Is_Controlled (Etype (First_Actual (Call)));
+
begin
-- If the unit is mentioned in a with_clause of the current unit, it is
-- visible, and we can set the elaboration flag.
or else (Is_Child_Unit (Scop) and then Is_Visible_Lib_Unit (Scop))
then
Activate_Elaborate_All_Desirable (Call, Scop);
- Set_Suppress_Elaboration_Warnings (Scop, True);
+ Set_Suppress_Elaboration_Warnings (Scop);
return;
end if;
-- If this is not an initialization call or a call using object notation
- -- we know that the unit of the called entity is in the context, and
- -- we can set the flag as well. The unit need not be visible if the call
+ -- we know that the unit of the called entity is in the context, and we
+ -- can set the flag as well. The unit need not be visible if the call
-- occurs within an instantiation.
if Is_Init_Proc (Subp)
else
Activate_Elaborate_All_Desirable (Call, Scop);
- Set_Suppress_Elaboration_Warnings (Scop, True);
+ Set_Suppress_Elaboration_Warnings (Scop);
return;
end if;
end if;
Activate_Elaborate_All_Desirable (Call, Elab_Unit);
- Set_Suppress_Elaboration_Warnings (Elab_Unit, True);
+ Set_Suppress_Elaboration_Warnings (Elab_Unit);
end Set_Elaboration_Constraint;
------------------------
if No (Corresponding_Body (N)) then
declare
Loc : constant Source_Ptr := Sloc (N);
- B : Node_Id;
- Formals : constant List_Id := Copy_Parameter_List (Ent);
- Nam : constant Entity_Id :=
+ Formals : constant List_Id := Copy_Parameter_List (Ent);
+ Nam : constant Entity_Id :=
Make_Defining_Identifier (Loc, Chars (Ent));
- Spec : Node_Id;
- Stats : constant List_Id :=
- New_List
- (Make_Raise_Program_Error (Loc,
+ Stats : constant List_Id :=
+ New_List (
+ Make_Raise_Program_Error (Loc,
Reason => PE_Access_Before_Elaboration));
+ Spec : Node_Id;
begin
if Ekind (Ent) = E_Function then
Spec :=
Make_Function_Specification (Loc,
- Defining_Unit_Name => Nam,
+ Defining_Unit_Name => Nam,
Parameter_Specifications => Formals,
- Result_Definition =>
+ Result_Definition =>
New_Copy_Tree
(Result_Definition (Specification (N))));
else
Spec :=
Make_Procedure_Specification (Loc,
- Defining_Unit_Name => Nam,
+ Defining_Unit_Name => Nam,
Parameter_Specifications => Formals);
end if;
- B := Make_Subprogram_Body (Loc,
- Specification => Spec,
- Declarations => New_List,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc, Stats));
- Insert_After (N, B);
- Analyze (B);
+ Insert_After_And_Analyze (N,
+ Make_Subprogram_Body (Loc,
+ Specification => Spec,
+ Declarations => New_List,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc, Stats)));
end;
end if;
end;
-- --
-- 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- --
-- --
------------------------------------------------------------------------------
-with Debug; use Debug;
-with Opt; use Opt;
-with Output; use Output;
with System; use System;
with Tree_IO; use Tree_IO;
with Unchecked_Conversion;
-pragma Elaborate_All (Output);
-
package body Table is
package body Table is
- Min : constant Int := Int (Table_Low_Bound);
- -- Subscript of the minimum entry in the currently allocated table
-
- Length : Int := 0;
- -- Number of entries in currently allocated table. The value of zero
- -- ensures that we initially allocate the table.
-
- -----------------------
- -- Local Subprograms --
- -----------------------
-
- procedure Reallocate;
- -- Reallocate the existing table according to the current value stored
- -- in Max. Works correctly to do an initial allocation if the table
- -- is currently null.
-
function Tree_Get_Table_Address return Address;
-- Return Null_Address if the table length is zero,
-- Table (First)'Address if not.
- pragma Warnings (Off);
- -- Turn off warnings. The following unchecked conversions are only used
- -- internally in this package, and cannot never result in any instances
- -- of improperly aliased pointers for the client of the package.
-
- function To_Address is new Unchecked_Conversion (Table_Ptr, Address);
- function To_Pointer is new Unchecked_Conversion (Address, Table_Ptr);
-
- pragma Warnings (On);
-
- ------------
- -- Append --
- ------------
-
- procedure Append (New_Val : Table_Component_Type) is
- begin
- Set_Item (Table_Index_Type (Last_Val + 1), New_Val);
- end Append;
-
- ----------------
- -- Append_All --
- ----------------
-
- procedure Append_All (New_Vals : Table_Type) is
- begin
- for J in New_Vals'Range loop
- Append (New_Vals (J));
- end loop;
- end Append_All;
-
- --------------------
- -- Decrement_Last --
- --------------------
-
- procedure Decrement_Last is
- begin
- Last_Val := Last_Val - 1;
- end Decrement_Last;
-
- ----------
- -- Free --
- ----------
-
- procedure Free is
- begin
- Free (To_Address (Table));
- Table := null;
- Length := 0;
- end Free;
-
- --------------------
- -- Increment_Last --
- --------------------
-
- procedure Increment_Last is
- begin
- Last_Val := Last_Val + 1;
-
- if Last_Val > Max then
- Reallocate;
- end if;
- end Increment_Last;
-
- ----------
- -- Init --
- ----------
-
- procedure Init is
- Old_Length : constant Int := Length;
-
- begin
- Locked := False;
- Last_Val := Min - 1;
- Max := Min + (Table_Initial * Table_Factor) - 1;
- Length := Max - Min + 1;
-
- -- If table is same size as before (happens when table is never
- -- expanded which is a common case), then simply reuse it. Note
- -- that this also means that an explicit Init call right after
- -- the implicit one in the package body is harmless.
-
- if Old_Length = Length then
- return;
-
- -- Otherwise we can use Reallocate to get a table of the right size.
- -- Note that Reallocate works fine to allocate a table of the right
- -- initial size when it is first allocated.
-
- else
- Reallocate;
- end if;
- end Init;
-
- ----------
- -- Last --
- ----------
-
- function Last return Table_Index_Type is
- begin
- return Table_Index_Type (Last_Val);
- end Last;
-
- ----------------
- -- Reallocate --
- ----------------
-
- procedure Reallocate is
- New_Size : Memory.size_t;
- New_Length : Long_Long_Integer;
-
- begin
- if Max < Last_Val then
- pragma Assert (not Locked);
-
- -- Make sure that we have at least the initial allocation. This
- -- is needed in cases where a zero length table is written out.
-
- Length := Int'Max (Length, Table_Initial);
-
- -- Now increment table length until it is sufficiently large. Use
- -- the increment value or 10, which ever is larger (the reason
- -- for the use of 10 here is to ensure that the table does really
- -- increase in size (which would not be the case for a table of
- -- length 10 increased by 3% for instance). Do the intermediate
- -- calculation in Long_Long_Integer to avoid overflow.
-
- while Max < Last_Val loop
- New_Length :=
- Long_Long_Integer (Length) *
- (100 + Long_Long_Integer (Table_Increment)) / 100;
- Length := Int'Max (Int (New_Length), Length + 10);
- Max := Min + Length - 1;
- end loop;
-
- if Debug_Flag_D then
- Write_Str ("--> Allocating new ");
- Write_Str (Table_Name);
- Write_Str (" table, size = ");
- Write_Int (Max - Min + 1);
- Write_Eol;
- end if;
- end if;
-
- -- Do the intermediate calculation in size_t to avoid signed overflow
-
- New_Size :=
- Memory.size_t (Max - Min + 1) *
- (Table_Type'Component_Size / Storage_Unit);
-
- if Table = null then
- Table := To_Pointer (Alloc (New_Size));
-
- elsif New_Size > 0 then
- Table :=
- To_Pointer (Realloc (Ptr => To_Address (Table),
- Size => New_Size));
- end if;
-
- if Length /= 0 and then Table = null then
- Set_Standard_Error;
- Write_Str ("available memory exhausted");
- Write_Eol;
- Set_Standard_Output;
- raise Unrecoverable_Error;
- end if;
- end Reallocate;
-
- -------------
- -- Release --
- -------------
-
- procedure Release is
- Extra_Length : Int;
- Size : Memory.size_t;
-
- begin
- Length := Last_Val - Int (Table_Low_Bound) + 1;
- Size := Memory.size_t (Length) *
- (Table_Type'Component_Size / Storage_Unit);
-
- -- If the size of the table exceeds the release threshold then leave
- -- space to store as many extra elements as 0.1% of the table length.
-
- if Release_Threshold > 0
- and then Size > Memory.size_t (Release_Threshold)
- then
- Extra_Length := Length / 1000;
- Length := Length + Extra_Length;
- Max := Int (Table_Low_Bound) + Length - 1;
-
- if Debug_Flag_D then
- Write_Str ("--> Release_Threshold reached (length=");
- Write_Int (Int (Size));
- Write_Str ("): leaving room space for ");
- Write_Int (Extra_Length);
- Write_Str (" components");
- Write_Eol;
- end if;
- else
- Max := Last_Val;
- end if;
-
- Reallocate;
- end Release;
-
- -------------
- -- Restore --
- -------------
-
- procedure Restore (T : Saved_Table) is
- begin
- Free (To_Address (Table));
- Last_Val := T.Last_Val;
- Max := T.Max;
- Table := T.Table;
- Length := Max - Min + 1;
- end Restore;
-
- ----------
- -- Save --
- ----------
-
- function Save return Saved_Table is
- Res : Saved_Table;
-
- begin
- Res.Last_Val := Last_Val;
- Res.Max := Max;
- Res.Table := Table;
-
- Table := null;
- Length := 0;
- Init;
- return Res;
- end Save;
-
- --------------
- -- Set_Item --
- --------------
-
- procedure Set_Item
- (Index : Table_Index_Type;
- Item : Table_Component_Type)
- is
- -- If Item is a value within the current allocation, and we are going
- -- to reallocate, then we must preserve an intermediate copy here
- -- before calling Increment_Last. Otherwise, if Table_Component_Type
- -- is passed by reference, we are going to end up copying from
- -- storage that might have been deallocated from Increment_Last
- -- calling Reallocate.
-
- subtype Allocated_Table_T is
- Table_Type (Table'First .. Table_Index_Type (Max + 1));
- -- A constrained table subtype one element larger than the currently
- -- allocated table.
-
- Allocated_Table_Address : constant System.Address :=
- Table.all'Address;
- -- Used for address clause below (we can't use non-static expression
- -- Table.all'Address directly in the clause because some older
- -- versions of the compiler do not allow it).
-
- Allocated_Table : Allocated_Table_T;
- pragma Import (Ada, Allocated_Table);
- pragma Suppress (Range_Check, On => Allocated_Table);
- for Allocated_Table'Address use Allocated_Table_Address;
- -- Allocated_Table represents the currently allocated array, plus one
- -- element (the supplementary element is used to have a convenient
- -- way of computing the address just past the end of the current
- -- allocation). Range checks are suppressed because this unit
- -- uses direct calls to System.Memory for allocation, and this can
- -- yield misaligned storage (and we cannot rely on the bootstrap
- -- compiler supporting specifically disabling alignment checks, so we
- -- need to suppress all range checks). It is safe to suppress this
- -- check here because we know that a (possibly misaligned) object
- -- of that type does actually exist at that address.
- -- ??? We should really improve the allocation circuitry here to
- -- guarantee proper alignment.
-
- Need_Realloc : constant Boolean := Int (Index) > Max;
- -- True if this operation requires storage reallocation (which may
- -- involve moving table contents around).
-
- begin
- -- If we're going to reallocate, check whether Item references an
- -- element of the currently allocated table.
-
- if Need_Realloc
- and then Allocated_Table'Address <= Item'Address
- and then Item'Address <
- Allocated_Table (Table_Index_Type (Max + 1))'Address
- then
- -- If so, save a copy on the stack because Increment_Last will
- -- reallocate storage and might deallocate the current table.
-
- declare
- Item_Copy : constant Table_Component_Type := Item;
- begin
- Set_Last (Index);
- Table (Index) := Item_Copy;
- end;
-
- else
- -- Here we know that either we won't reallocate (case of Index <
- -- Max) or that Item is not in the currently allocated table.
-
- if Int (Index) > Last_Val then
- Set_Last (Index);
- end if;
-
- Table (Index) := Item;
- end if;
- end Set_Item;
-
- --------------
- -- Set_Last --
- --------------
-
- procedure Set_Last (New_Val : Table_Index_Type) is
- begin
- if Int (New_Val) < Last_Val then
- Last_Val := Int (New_Val);
-
- else
- Last_Val := Int (New_Val);
-
- if Last_Val > Max then
- Reallocate;
- end if;
- end if;
- end Set_Last;
-
----------------------------
-- Tree_Get_Table_Address --
----------------------------
function Tree_Get_Table_Address return Address is
begin
- if Length = 0 then
+ if Is_Empty then
return Null_Address;
else
return Table (First)'Address;
-- does an implicit Release.
procedure Tree_Read is
+ Last : Int;
begin
- Tree_Read_Int (Max);
- Last_Val := Max;
- Length := Max - Min + 1;
- Reallocate;
+ Init;
+ Tree_Read_Int (Last);
+ Set_Last (Table_Last_Type (Last));
Tree_Read_Data
(Tree_Get_Table_Address,
- (Last_Val - Int (First) + 1) *
+ (Last - Int (First) + 1) *
-- Note the importance of parenthesizing the following division
-- to avoid the possibility of intermediate overflow.
Tree_Write_Int (Int (Last));
Tree_Write_Data
(Tree_Get_Table_Address,
- (Last_Val - Int (First) + 1) *
+ (Int (Last - First) + 1) *
(Table_Type'Component_Size / Storage_Unit));
end Tree_Write;
- begin
- Init;
end Table;
end Table;
-- --
-- S p e c --
-- --
--- 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- --
-- --
------------------------------------------------------------------------------
--- This package provides an implementation of dynamically resizable one
--- dimensional arrays. The idea is to mimic the normal Ada semantics for
--- arrays as closely as possible with the one additional capability of
--- dynamically modifying the value of the Last attribute.
+-- This package is a wrapper for GNAT.Table, for use in the compiler front
+-- end. It adds the Tree_Write/Tree_Read functionality; everything else is
+-- just a renaming of GNAT.Table. See GNAT.Table (g-table.ads) and
+-- GNAT.Dynamic_Tables (g-dyntab.ads) for documentation.
--- Note that this interface should remain synchronized with those in
--- GNAT.Table and GNAT.Dynamic_Tables to keep coherency between these
--- three related units.
+-- Note that these three interfaces should remain synchronized to keep as much
+-- coherency as possible among these related units:
+--
+-- GNAT.Dynamic_Tables
+-- GNAT.Table
+-- Table (the compiler unit)
with Types; use Types;
+with GNAT.Table;
package Table is
pragma Elaborate_Body;
Table_Low_Bound : Table_Index_Type;
Table_Initial : Pos;
Table_Increment : Nat;
- Table_Name : String;
+ Table_Name : String; -- for debugging printouts
Release_Threshold : Nat := 0;
package Table is
- -- Table_Component_Type and Table_Index_Type specify the type of the
- -- array, Table_Low_Bound is the lower bound. Table_Index_Type must be
- -- an integer type. The effect is roughly to declare:
-
- -- Table : array (Table_Index_Type range Table_Low_Bound .. <>)
- -- of Table_Component_Type;
-
- -- Note: since the upper bound can be one less than the lower
- -- bound for an empty array, the table index type must be able
- -- to cover this range, e.g. if the lower bound is 1, then the
- -- Table_Index_Type should be Natural rather than Positive.
-
- -- Table_Component_Type may be any Ada type, except that controlled
- -- types are not supported. Note however that default initialization
- -- will NOT occur for array components.
-
- -- The Table_Initial values controls the allocation of the table when
- -- it is first allocated, either by default, or by an explicit Init
- -- call. The value used is Opt.Table_Factor * Table_Initial.
-
- -- The Table_Increment value controls the amount of increase, if the
- -- table has to be increased in size. The value given is a percentage
- -- value (e.g. 100 = increase table size by 100%, i.e. double it).
-
- -- The Table_Name parameter is simply use in debug output messages it
- -- has no other usage, and is not referenced in non-debugging mode.
-
- -- The Last and Set_Last subprograms provide control over the current
- -- logical allocation. They are quite efficient, so they can be used
- -- freely (expensive reallocation occurs only at major granularity
- -- chunks controlled by the allocation parameters).
-
- -- Note: We do not make the table components aliased, since this would
- -- restrict the use of table for discriminated types. If it is necessary
- -- to take the access of a table element, use Unrestricted_Access.
-
- -- WARNING: On HPPA, the virtual addressing approach used in this unit
- -- is incompatible with the indexing instructions on the HPPA. So when
- -- using this unit, compile your application with -mdisable-indexing.
-
- -- WARNING: If the table is reallocated, then the address of all its
- -- components will change. So do not capture the address of an element
- -- and then use the address later after the table may be reallocated.
- -- One tricky case of this is passing an element of the table to a
- -- subprogram by reference where the table gets reallocated during
- -- the execution of the subprogram. The best rule to follow is never
- -- to pass a table element as a parameter except for the case of IN
- -- mode parameters with scalar values.
-
- type Table_Type is
- array (Table_Index_Type range <>) of Table_Component_Type;
-
- subtype Big_Table_Type is
- Table_Type (Table_Low_Bound .. Table_Index_Type'Last);
- -- We work with pointers to a bogus array type that is constrained
- -- with the maximum possible range bound. This means that the pointer
- -- is a thin pointer, which is more efficient. Since subscript checks
- -- in any case must be on the logical, rather than physical bounds,
- -- safety is not compromised by this approach.
-
- type Table_Ptr is access all Big_Table_Type;
- for Table_Ptr'Storage_Size use 0;
- -- The table is actually represented as a pointer to allow reallocation
-
- Table : aliased Table_Ptr := null;
- -- The table itself. The lower bound is the value of Low_Bound.
- -- Logically the upper bound is the current value of Last (although
- -- the actual size of the allocated table may be larger than this).
- -- The program may only access and modify Table entries in the range
- -- First .. Last.
-
- Locked : Boolean := False;
+ package Tab is new GNAT.Table
+ (Table_Component_Type,
+ Table_Index_Type,
+ Table_Low_Bound,
+ Positive (Table_Initial),
+ Natural (Table_Increment),
+ Table_Name,
+ Natural (Release_Threshold));
+
+ subtype Valid_Table_Index_Type is Tab.Valid_Table_Index_Type;
+ subtype Table_Last_Type is Tab.Table_Last_Type;
+ subtype Table_Type is Tab.Table_Type;
+ subtype Big_Table_Type is Tab.Big_Table_Type;
+
+ subtype Table_Ptr is Tab.Table_Ptr;
+
+ 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
-- not move during processing, which means that they cannot be expanded.
-- The Locked flag is used to enforce this restriction.
- procedure Init;
- -- This procedure allocates a new table of size Initial (freeing any
- -- previously allocated larger table). It is not necessary to call
- -- Init when a table is first instantiated (since the instantiation does
- -- the same initialization steps). However, it is harmless to do so, and
- -- Init is convenient in reestablishing a table for new use.
-
- function Last return Table_Index_Type;
- pragma Inline (Last);
- -- Returns the current value of the last used entry in the table, which
- -- can then be used as a subscript for Table. Note that the only way to
- -- modify Last is to call the Set_Last procedure. Last must always be
- -- used to determine the logically last entry.
-
- procedure Release;
- -- Storage is allocated in chunks according to the values given in the
- -- Initial and Increment parameters. If Release_Threshold is 0 or the
- -- length of the table does not exceed this threshold then a call to
- -- Release releases all storage that is allocated, but is not logically
- -- part of the current array value; otherwise the call to Release leaves
- -- the current array value plus 0.1% of the current table length free
- -- elements located at the end of the table (this parameter facilitates
- -- reopening large tables and adding a few elements without allocating a
- -- chunk of memory). In both cases current array values are not affected
- -- by this call.
-
- procedure Free;
- -- Free all allocated memory for the table. A call to init is required
- -- before any use of this table after calling Free.
-
- First : constant Table_Index_Type := Table_Low_Bound;
- -- Export First as synonym for Low_Bound (parallel with use of Last)
-
- procedure Set_Last (New_Val : Table_Index_Type);
- pragma Inline (Set_Last);
- -- This procedure sets Last to the indicated value. If necessary the
- -- table is reallocated to accommodate the new value (i.e. on return
- -- the allocated table has an upper bound of at least Last). If Set_Last
- -- reduces the size of the table, then logically entries are removed
- -- from the table. If Set_Last increases the size of the table, then
- -- new entries are logically added to the table.
-
- procedure Increment_Last;
- pragma Inline (Increment_Last);
- -- Adds 1 to Last (same as Set_Last (Last + 1)
-
- procedure Decrement_Last;
- pragma Inline (Decrement_Last);
- -- Subtracts 1 from Last (same as Set_Last (Last - 1)
-
- procedure Append (New_Val : Table_Component_Type);
- pragma Inline (Append);
- -- Equivalent to:
- -- x.Increment_Last;
- -- x.Table (x.Last) := New_Val;
- -- i.e. the table size is increased by one, and the given new item
- -- stored in the newly created table element.
-
- procedure Append_All (New_Vals : Table_Type);
- -- Appends all components of New_Vals
+ function Is_Empty return Boolean renames Tab.Is_Empty;
- procedure Set_Item
- (Index : Table_Index_Type;
- Item : Table_Component_Type);
- pragma Inline (Set_Item);
- -- Put Item in the table at position Index. The table is expanded if
- -- current table length is less than Index and in that case Last is set
- -- to Index. Item will replace any value already present in the table
- -- at this position.
+ procedure Init renames Tab.Init;
- type Saved_Table is private;
- -- Type used for Save/Restore subprograms
+ function First return Table_Index_Type renames Tab.First;
+ function Last return Table_Last_Type renames Tab.Last;
- function Save return Saved_Table;
- -- Resets table to empty, but saves old contents of table in returned
- -- value, for possible later restoration by a call to Restore.
+ procedure Release renames Tab.Release;
- procedure Restore (T : Saved_Table);
- -- Given a Saved_Table value returned by a prior call to Save, restores
- -- the table to the state it was in at the time of the Save call.
+ procedure Free renames Tab.Free;
- procedure Tree_Write;
- -- Writes out contents of table using Tree_IO
+ procedure Set_Last (New_Val : Table_Last_Type) renames Tab.Set_Last;
- procedure Tree_Read;
- -- Initializes table by reading contents previously written with the
- -- Tree_Write call (also using Tree_IO).
+ procedure Increment_Last renames Tab.Increment_Last;
+ procedure Decrement_Last renames Tab.Decrement_Last;
- private
+ procedure Append (New_Val : Table_Component_Type) renames Tab.Append;
+ procedure Append_All (New_Vals : Table_Type) renames Tab.Append_All;
- Last_Val : Int;
- -- Current value of Last. Note that we declare this in the private part
- -- because we don't want the client to modify Last except through one of
- -- the official interfaces (since a modification to Last may require a
- -- reallocation of the table).
+ procedure Set_Item
+ (Index : Valid_Table_Index_Type;
+ Item : Table_Component_Type) renames Tab.Set_Item;
- Max : Int;
- -- Subscript of the maximum entry in the currently allocated table
+ subtype Saved_Table is Tab.Saved_Table;
+ function Save return Saved_Table renames Tab.Save;
+ procedure Restore (T : in out Saved_Table) renames Tab.Restore;
- type Saved_Table is record
- Last_Val : Int;
- Max : Int;
- Table : Table_Ptr;
- end record;
+ procedure Tree_Write;
+ -- Writes out contents of table using Tree_IO
+
+ procedure Tree_Read;
+ -- Initializes table by reading contents previously written with the
+ -- Tree_Write call, also using Tree_IO.
end Table;
end Table;
* *
* C Header File *
* *
- * 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- *
the integer value itself. The origin of the Uints_Ptr table is adjusted so
that a Uint value of Uint_Bias indexes the first element. */
-#define Uints_Ptr (uintp__uints__table - Uint_Table_Start)
-extern struct Uint_Entry *uintp__uints__table;
+#define Uints_Ptr (uintp__uints__tab__the_instance - Uint_Table_Start)
+extern struct Uint_Entry *uintp__uints__tab__the_instance;
-#define Udigits_Ptr uintp__udigits__table
-extern int *uintp__udigits__table;
+#define Udigits_Ptr uintp__udigits__tab__the_instance
+extern int *uintp__udigits__tab__the_instance;
#ifdef __cplusplus
}
-- --
-- B o d y --
-- --
--- Copyright (C) 2008-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 2008-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- --
-- The base name of the template file is given by Argument (1). This program
-- generates the spec for this specified unit (let's call it UNIT_NAME).
--- It works in conjunction with a C template file which must be pre-processed
+-- It works in conjunction with a C template file which must be preprocessed
-- and compiled using the cross compiler. Two input files are used:
-- - the preprocessed C file: UNIT_NAME-tmplt.i
-- - the generated assembly file: UNIT_NAME-tmplt.s
projects / gcc.git / commitdiff