FreeChainXenon/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

[multiple changes]

Browse source 
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.

From-SVN: r247320
This commit is contained in:
Arnaud Charlet 2017-04-27 13:01:32 +02:00
parent 27eaddda0f
commit a6d25cadec
24 changed files with 1232 additions and 1450 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

65
gcc/ada/ChangeLog
View file

@ -1,3 +1,68 @@
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,

288
gcc/ada/a-cfhama.adb
View file

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -237,35 +237,6 @@ is
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 --
---------------------
@ -304,6 +275,7 @@ is
HT_Ops.Delete_Node_Sans_Free (Container, Position.Node);
Free (Container, Position.Node);
Position := No_Element;
end Delete;
-------------
@ -346,79 +318,6 @@ is
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 --
-------------
@ -460,37 +359,109 @@ is
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 --
@ -747,40 +718,6 @@ is
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 --
-------------
@ -850,35 +787,6 @@ is
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 --
---------

676
gcc/ada/a-cfhama.ads
View file

@ -6,7 +6,7 @@
-- --
-- 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 --
@ -44,17 +44,11 @@
-- 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
@ -63,77 +57,267 @@ 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;
@ -141,11 +325,40 @@ is
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;
@ -154,8 +367,55 @@ is
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;
@ -163,16 +423,100 @@ is
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;
@ -180,99 +524,213 @@ is
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 =>
-- If Key is not is not contained in Container, Find returns No_Element
(not Contains (Model (Container), Key) =>
Find'Result = No_Element,
-- Otherwise, Find returns a valid cusror in Container
others =>
P.Has_Key (Positions (Container), Find'Result)
-- The key designated by the result of Find is Key
and Equivalent_Keys
(Formal_Hashed_Maps.Key (Container, Find'Result), Key));
function Contains (Container : Map; Key : Key_Type) return Boolean with
Global => null;
Global => null,
Post => Contains'Result = Contains (Model (Container), Key);
pragma Annotate (GNATprove, Inline_For_Proof, Contains);
function Element (Container : Map; Key : Key_Type) return Element_Type with
Global => null,
Pre => Contains (Container, Key);
Pre => Contains (Container, Key),
Post => Element'Result = Element (Model (Container), Key);
pragma Annotate (GNATprove, Inline_For_Proof, Element);
function Has_Element (Container : Map; Position : Cursor) return Boolean
with
Global => null;
function Equivalent_Keys
(Left : Map;
CLeft : Cursor;
Right : Map;
CRight : Cursor) return Boolean
with
Global => null;
function Equivalent_Keys
(Left : Map;
CLeft : Cursor;
Right : Key_Type) return Boolean
with
Global => null;
function Equivalent_Keys
(Left : Key_Type;
Right : Map;
CRight : Cursor) return Boolean
with
Global => null;
Global => null,
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;
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 First_To_Previous (Container : Map; Current : Cursor) return Map
with
Ghost,
Global => null,
Pre => Has_Element (Container, Current) or else Current = No_Element;
function Current_To_Last (Container : Map; Current : Cursor) return Map
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
Global => null;
-- Overlap returns True if the containers have common keys
private
pragma SPARK_Mode (Off);
@ -302,12 +760,6 @@ private
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;

22
gcc/ada/a-cofuma.adb
View file

@ -93,8 +93,10 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
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;
@ -116,8 +118,10 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
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;
@ -229,6 +233,16 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
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 --
---------------

27
gcc/ada/a-cofuma.ads
View file

@ -48,6 +48,9 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
-- Maps are empty when default initialized.
-- "For in" quantification over maps should not be used.
-- "For of" quantification over maps iterates over keys.
-- Note that, for proof, for of quantification is understood modulo
-- equivalence (quantification includes keys equivalent to keys of the
-- map).
-----------------------
-- Basic operations --
@ -71,6 +74,22 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
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 --
------------------------
@ -162,12 +181,12 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
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;
@ -179,14 +198,14 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
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 --

6
gcc/ada/checks.adb
View file

@ -2738,7 +2738,7 @@ package body Checks is
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
@ -7936,7 +7936,8 @@ package body Checks is
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);
@ -8238,6 +8239,7 @@ package body Checks is
else
declare
Rtype : Entity_Id;
pragma Warnings (Off, Rtype);
New_Alts : List_Id;
New_Exp : Node_Id;

2
gcc/ada/exp_ch3.adb
View file

@ -3174,7 +3174,7 @@ package body Exp_Ch3 is
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

7
gcc/ada/exp_ch4.adb
View file

@ -2700,7 +2700,7 @@ package body Exp_Ch4 is
-- 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).
@ -2742,13 +2742,13 @@ package body Exp_Ch4 is
-- 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.
@ -4036,6 +4036,7 @@ package body Exp_Ch4 is
declare
Len : Node_Id;
Res : Node_Id;
pragma Warnings (Off, Res);
begin
for J in 1 .. Number_Dimensions (E) loop

6
gcc/ada/exp_ch7.adb
View file

@ -6722,7 +6722,7 @@ package body Exp_Ch7 is
-- Local variables
Bod_Stmts : List_Id;
Bod_Stmts : List_Id := No_List;
Finalizer_Decls : List_Id := No_List;
Rec_Def : Node_Id;
@ -7068,7 +7068,7 @@ package body Exp_Ch7 is
-- 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;
@ -7305,7 +7305,7 @@ package body Exp_Ch7 is
-- Local variables
Bod_Stmts : List_Id;
Bod_Stmts : List_Id := No_List;
Finalizer_Decls : List_Id := No_List;
Rec_Def : Node_Id;

2
gcc/ada/exp_disp.adb
View file

@ -673,7 +673,7 @@ package body Exp_Disp is
-- 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

94
gcc/ada/g-dyntab.adb
View file

@ -34,6 +34,7 @@ pragma Compiler_Unit_Warning;
with GNAT.Heap_Sort_G;
with Ada.Unchecked_Deallocation;
with System;
package body GNAT.Dynamic_Tables is
@ -44,7 +45,7 @@ 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,
@ -128,14 +129,12 @@ package body GNAT.Dynamic_Tables is
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;
@ -143,7 +142,7 @@ package body GNAT.Dynamic_Tables is
-- 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
@ -158,7 +157,7 @@ package body GNAT.Dynamic_Tables is
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;
@ -241,24 +240,82 @@ package body GNAT.Dynamic_Tables is
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);
@ -272,23 +329,21 @@ package body GNAT.Dynamic_Tables is
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;
--------------
@ -329,8 +384,7 @@ package body GNAT.Dynamic_Tables is
-- 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);

101
gcc/ada/g-dyntab.ads
View file

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -36,13 +36,10 @@
-- 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
@ -56,9 +53,10 @@ generic
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
@ -69,15 +67,42 @@ 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.
@ -112,7 +137,7 @@ package GNAT.Dynamic_Tables is
-- 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;
@ -132,7 +157,7 @@ package GNAT.Dynamic_Tables is
-- 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
@ -143,35 +168,50 @@ package GNAT.Dynamic_Tables is
-- 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
@ -205,8 +245,11 @@ package GNAT.Dynamic_Tables is
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);
@ -236,11 +279,11 @@ package GNAT.Dynamic_Tables is
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

332
gcc/ada/g-table.adb
View file

@ -29,8 +29,6 @@
-- --
------------------------------------------------------------------------------
with GNAT.Heap_Sort_G;
with System; use System;
with System.Memory; use System.Memory;
@ -38,53 +36,20 @@ with Ada.Unchecked_Conversion;
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;
Tab.Allocate (The_Instance, Num);
end Allocate;
if Last_Val > Max then
Reallocate;
end if;
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;
------------
@ -93,7 +58,7 @@ package body GNAT.Table is
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;
----------------
@ -102,9 +67,7 @@ package body GNAT.Table is
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;
--------------------
@ -113,7 +76,7 @@ package body GNAT.Table is
procedure Decrement_Last is
begin
Last_Val := Last_Val - 1;
Tab.Decrement_Last (The_Instance);
end Decrement_Last;
-----------
@ -122,7 +85,7 @@ package body GNAT.Table is
function First return Table_Index_Type is
begin
return Table_Low_Bound;
return Tab.First;
end First;
--------------
@ -130,12 +93,9 @@ package body GNAT.Table is
--------------
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;
----------
@ -144,9 +104,7 @@ package body GNAT.Table is
procedure Free is
begin
Free (To_Address (Table));
Table := null;
Length := 0;
Tab.Free (The_Instance);
end Free;
--------------------
@ -155,201 +113,85 @@ package body GNAT.Table is
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;
----------------
@ -357,69 +199,9 @@ package body GNAT.Table is
----------------
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;

205
gcc/ada/g-table.ads
View file

@ -29,198 +29,117 @@
-- --
------------------------------------------------------------------------------
-- 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:
package Tab is new GNAT.Dynamic_Tables
(Table_Component_Type,
Table_Index_Type,
Table_Low_Bound,
Table_Initial,
Table_Increment,
Release_Threshold);
-- Table : array (Table_Index_Type range Table_Low_Bound .. <>)
-- of Table_Component_Type;
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;
-- 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.
subtype Table_Ptr is Tab.Table_Ptr;
-- 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_Instance : Tab.Instance;
Table : Table_Ptr renames The_Instance.Table;
Locked : Boolean renames The_Instance.Locked;
-- 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.
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;
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);
function Last return Table_Last_Type;
pragma Inline (Last);
procedure Release;
procedure Free;
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;

19
gcc/ada/namet.adb
View file

@ -36,6 +36,7 @@
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;
@ -1093,15 +1094,6 @@ package body Namet is
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 --
----------------
@ -1139,15 +1131,6 @@ package body Namet is
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 --
------------------------

8
gcc/ada/namet.ads
View file

@ -32,7 +32,6 @@
with Alloc;
with Hostparm; use Hostparm;
with Table;
with System; use System;
with Types; use Types;
package Namet is
@ -564,13 +563,6 @@ 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

6
gcc/ada/namet.h
View file

@ -6,7 +6,7 @@
* *
* 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- *
@ -45,11 +45,11 @@ struct Name_Entry
};
/* 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. */

2
gcc/ada/osint.ads
View file

@ -662,7 +662,7 @@ package Osint is
-- 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

12
gcc/ada/scos.h
View file

@ -45,8 +45,10 @@ struct SCO_Unit_Table_Entry
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
@ -74,8 +76,10 @@ struct SCO_Table_Entry
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

207
gcc/ada/sem_elab.adb
View file

@ -65,36 +65,51 @@ package body Sem_Elab is
-- 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;
@ -743,7 +758,7 @@ package body Sem_Elab is
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;
@ -913,17 +928,17 @@ package body Sem_Elab is
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
@ -1151,7 +1166,7 @@ package body Sem_Elab is
-- 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;
@ -1218,8 +1233,8 @@ package body Sem_Elab is
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
@ -1623,14 +1638,22 @@ package body Sem_Elab is
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:
@ -2394,14 +2417,19 @@ package body Sem_Elab is
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
@ -2422,8 +2450,8 @@ package body Sem_Elab is
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;
@ -2579,26 +2607,22 @@ package body Sem_Elab is
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);
@ -2629,12 +2653,15 @@ package body Sem_Elab is
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
@ -2657,8 +2684,8 @@ package body Sem_Elab is
("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,
@ -2697,13 +2724,6 @@ package body Sem_Elab is
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;
---------------------------
@ -2909,32 +2929,32 @@ package body Sem_Elab is
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);
@ -2988,18 +3008,19 @@ package body Sem_Elab is
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.
@ -3008,13 +3029,13 @@ package body Sem_Elab is
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)
@ -3025,7 +3046,7 @@ package body Sem_Elab is
else
Activate_Elaborate_All_Desirable (Call, Scop);
Set_Suppress_Elaboration_Warnings (Scop, True);
Set_Suppress_Elaboration_Warnings (Scop);
return;
end if;
@ -3070,7 +3091,7 @@ package body Sem_Elab is
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;
------------------------
@ -3616,23 +3637,22 @@ package body Sem_Elab is
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))));
@ -3645,17 +3665,16 @@ package body Sem_Elab is
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;

371
gcc/ada/table.adb
View file

@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
@ -29,9 +29,6 @@
-- --
------------------------------------------------------------------------------
with Debug; use Debug;
with Opt; use Opt;
with Output; use Output;
with System; use System;
with Tree_IO; use Tree_IO;
@ -39,370 +36,20 @@ with System.Memory; use System.Memory;
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;
@ -418,15 +65,15 @@ package body Table is
-- 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.
@ -446,11 +93,9 @@ package body Table is
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;

210
gcc/ada/table.ads
View file

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -29,16 +29,20 @@
-- --
------------------------------------------------------------------------------
-- 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;
@ -50,83 +54,30 @@ package Table is
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:
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));
-- Table : array (Table_Index_Type range Table_Low_Bound .. <>)
-- of Table_Component_Type;
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;
-- 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.
subtype Table_Ptr is Tab.Table_Ptr;
-- 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.
Table : Table_Ptr renames Tab.Table;
-- 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;
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
@ -136,110 +87,39 @@ package Table is
-- 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 Is_Empty return Boolean renames Tab.Is_Empty;
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 Init renames Tab.Init;
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.
function First return Table_Index_Type renames Tab.First;
function Last return Table_Last_Type renames Tab.Last;
procedure Free;
-- Free all allocated memory for the table. A call to init is required
-- before any use of this table after calling Free.
procedure Release renames Tab.Release;
First : constant Table_Index_Type := Table_Low_Bound;
-- Export First as synonym for Low_Bound (parallel with use of Last)
procedure Free renames Tab.Free;
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 Set_Last (New_Val : Table_Last_Type) renames Tab.Set_Last;
procedure Increment_Last;
pragma Inline (Increment_Last);
-- Adds 1 to Last (same as Set_Last (Last + 1)
procedure Increment_Last renames Tab.Increment_Last;
procedure Decrement_Last renames Tab.Decrement_Last;
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 Append (New_Val : Table_Component_Type) renames Tab.Append;
procedure Append_All (New_Vals : Table_Type) renames Tab.Append_All;
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.
(Index : Valid_Table_Index_Type;
Item : Table_Component_Type) renames Tab.Set_Item;
type Saved_Table is private;
-- 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 : 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.
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;
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).
private
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).
Max : Int;
-- Subscript of the maximum entry in the currently allocated table
type Saved_Table is record
Last_Val : Int;
Max : Int;
Table : Table_Ptr;
end record;
-- Tree_Write call, also using Tree_IO.
end Table;
end Table;

10
gcc/ada/uintp.h
View file

@ -6,7 +6,7 @@
* *
* 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- *
@ -101,11 +101,11 @@ extern Boolean UI_Lt (Uint, Uint);
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
}

4
gcc/ada/xoscons.adb
View file

@ -6,7 +6,7 @@
-- --
-- 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- --
@ -26,7 +26,7 @@
-- 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