Skip to content

R
riscv-gcc-1
Commit d5fa5335 by Hristian Kirtchev Committed by Arnaud Charlet
Options

exp_ch6.adb (Expand_N_Extended_Return_Statement): Use New_Copy_Tree instead of… 

exp_ch6.adb (Expand_N_Extended_Return_Statement): Use New_Copy_Tree instead of Relocate_Node as any subsequent copies of the...

2017-04-28  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch6.adb (Expand_N_Extended_Return_Statement): Use
	New_Copy_Tree instead of Relocate_Node as any subsequent copies
	of the relocated node will have mangled Parent pointers.
	* sem_util.adb (Build_NCT_Hash_Tables): Reset both hash
	tables used in conjunction with entity and itype replication.
	(Visit_Entity): Rewrite the restriction on which entities
	require duplication.  The restriction now includes all types.

2017-04-28  Hristian Kirtchev  <kirtchev@adacore.com>

	* a-cofuse.ads, a-cfdlli.ads, a-cfhase.adb, a-cfhase.ads, a-cfinve.adb,
	a-cfinve.ads, a-cforma.adb, a-cforma.ads, a-cofuma.adb, a-cofuma.ads,
	a-cfhama.adb, a-cfhama.ads, a-cforse.adb: Minor reformatting and code
	cleanups.

From-SVN: r247384
parent ef952fd5
Showing with 368 additions and 371 deletions
gcc/ada/ChangeLog
2017-04-28 Hristian Kirtchev <kirtchev@adacore.com> 2017-04-28 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch6.adb (Expand_N_Extended_Return_Statement): Use
New_Copy_Tree instead of Relocate_Node as any subsequent copies
of the relocated node will have mangled Parent pointers.
* sem_util.adb (Build_NCT_Hash_Tables): Reset both hash
tables used in conjunction with entity and itype replication.
(Visit_Entity): Rewrite the restriction on which entities
require duplication. The restriction now includes all types.
2017-04-28 Hristian Kirtchev <kirtchev@adacore.com>
* a-cofuse.ads, a-cfdlli.ads, a-cfhase.adb, a-cfhase.ads, a-cfinve.adb,
a-cfinve.ads, a-cforma.adb, a-cforma.ads, a-cofuma.adb, a-cofuma.ads,
a-cfhama.adb, a-cfhama.ads, a-cforse.adb: Minor reformatting and code
cleanups.
2017-04-28 Hristian Kirtchev <kirtchev@adacore.com>
* exp_util.adb, g-dyntab.adb, par-ch4.adb, sem_util.adb, sem_attr.adb, * exp_util.adb, g-dyntab.adb, par-ch4.adb, sem_util.adb, sem_attr.adb,
gnat1drv.adb, exp_disp.adb, namet.adb, alloc.ads: Minor reformatting. gnat1drv.adb, exp_disp.adb, namet.adb, alloc.ads: Minor reformatting.
......
gcc/ada/a-cfdlli.ads
...@@ -1541,9 +1541,9 @@ is ...@@ -1541,9 +1541,9 @@ is
Post => Post =>
M_Elements_Sorted'Result = M_Elements_Sorted'Result =
(for all I in 1 .. M.Length (Container) => (for all I in 1 .. M.Length (Container) =>
(for all J in I .. M.Length (Container) => (for all J in I .. M.Length (Container) =>
Element (Container, I) = Element (Container, J) Element (Container, I) = Element (Container, J)
or Element (Container, I) < Element (Container, J))); or Element (Container, I) < Element (Container, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
end Formal_Model; end Formal_Model;
......
gcc/ada/a-cfhama.adb
...@@ -370,7 +370,9 @@ is ...@@ -370,7 +370,9 @@ is
-- Find -- -- Find --
---------- ----------
function Find (Container : K.Sequence; Key : Key_Type) return Count_Type function Find
(Container : K.Sequence;
Key : Key_Type) return Count_Type
is is
begin begin
for I in 1 .. K.Length (Container) loop for I in 1 .. K.Length (Container) loop
...@@ -385,8 +387,9 @@ is ...@@ -385,8 +387,9 @@ is
-- K_Keys_Included -- -- K_Keys_Included --
--------------------- ---------------------
function K_Keys_Included (Left : K.Sequence; function K_Keys_Included
Right : K.Sequence) return Boolean (Left : K.Sequence;
Right : K.Sequence) return Boolean
is is
begin begin
for I in 1 .. K.Length (Left) loop for I in 1 .. K.Length (Left) loop
......
gcc/ada/a-cfhama.ads
...@@ -126,8 +126,8 @@ is ...@@ -126,8 +126,8 @@ is
Global => null, Global => null,
Post => Post =>
(if Find'Result > 0 then (if Find'Result > 0 then
Find'Result <= K.Length (Container) Find'Result <= K.Length (Container)
and Equivalent_Keys (Key, K.Get (Container, Find'Result))); and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
function K_Keys_Included function K_Keys_Included
(Left : K.Sequence; (Left : K.Sequence;
...@@ -139,9 +139,9 @@ is ...@@ -139,9 +139,9 @@ is
Post => Post =>
K_Keys_Included'Result = K_Keys_Included'Result =
(for all I in 1 .. K.Length (Left) => (for all I in 1 .. K.Length (Left) =>
Find (Right, K.Get (Left, I)) > 0 Find (Right, K.Get (Left, I)) > 0
and then K.Get (Right, Find (Right, K.Get (Left, I))) = and then K.Get (Right, Find (Right, K.Get (Left, I))) =
K.Get (Left, I)); K.Get (Left, I));
package P is new Ada.Containers.Functional_Maps package P is new Ada.Containers.Functional_Maps
(Key_Type => Cursor, (Key_Type => Cursor,
...@@ -203,14 +203,15 @@ is ...@@ -203,14 +203,15 @@ is
-- It only contains keys contained in Model -- It only contains keys contained in Model
and (for all Key of Keys'Result => and (for all Key of Keys'Result =>
M.Has_Key (Model (Container), Key)) M.Has_Key (Model (Container), Key))
-- It contains all the keys contained in Model -- It contains all the keys contained in Model
and (for all Key of Model (Container) => and (for all Key of Model (Container) =>
(Find (Keys'Result, Key) > 0 (Find (Keys'Result, Key) > 0
and then Equivalent_Keys and then Equivalent_Keys
(K.Get (Keys'Result, Find (Keys'Result, Key)), Key))) (K.Get (Keys'Result, Find (Keys'Result, Key)),
Key)))
-- It has no duplicate -- It has no duplicate
...@@ -221,7 +222,8 @@ is ...@@ -221,7 +222,8 @@ is
(for all J in 1 .. Length (Container) => (for all J in 1 .. Length (Container) =>
(if Equivalent_Keys (if Equivalent_Keys
(K.Get (Keys'Result, I), K.Get (Keys'Result, J)) (K.Get (Keys'Result, I), K.Get (Keys'Result, J))
then I = J))); then
I = J)));
pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys); pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys);
function Positions (Container : Map) return P.Map with function Positions (Container : Map) return P.Map with
...@@ -246,7 +248,7 @@ is ...@@ -246,7 +248,7 @@ is
and then and then
(for all J of Positions'Result => (for all J of Positions'Result =>
(if P.Get (Positions'Result, I) = P.Get (Positions'Result, J) (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
then I = J))); then I = J)));
procedure Lift_Abstraction_Level (Container : Map) with procedure Lift_Abstraction_Level (Container : Map) with
-- Lift_Abstraction_Level is a ghost procedure that does nothing but -- Lift_Abstraction_Level is a ghost procedure that does nothing but
...@@ -547,9 +549,9 @@ is ...@@ -547,9 +549,9 @@ is
-- Key is inserted in Container -- Key is inserted in Container
and K.Get (Keys (Container), and K.Get
P.Get (Positions (Container), Find (Container, Key))) = (Keys (Container),
Key P.Get (Positions (Container), Find (Container, Key))) = Key
-- Mapping from cursors to keys is preserved -- Mapping from cursors to keys is preserved
......
gcc/ada/a-cfhase.adb
...@@ -38,16 +38,13 @@ with System; use type System.Address; ...@@ -38,16 +38,13 @@ with System; use type System.Address;
package body Ada.Containers.Formal_Hashed_Sets with package body Ada.Containers.Formal_Hashed_Sets with
SPARK_Mode => Off SPARK_Mode => Off
is is
----------------------- -----------------------
-- Local Subprograms -- -- Local Subprograms --
----------------------- -----------------------
-- All need comments ??? -- All need comments ???
procedure Difference procedure Difference (Left : Set; Right : Set; Target : in out Set);
(Left, Right : Set;
Target : in out Set);
function Equivalent_Keys function Equivalent_Keys
(Key : Element_Type; (Key : Element_Type;
...@@ -68,10 +65,10 @@ is ...@@ -68,10 +65,10 @@ is
pragma Inline (Hash_Node); pragma Inline (Hash_Node);
procedure Insert procedure Insert
(Container : in out Set; (Container : in out Set;
New_Item : Element_Type; New_Item : Element_Type;
Node : out Count_Type; Node : out Count_Type;
Inserted : out Boolean); Inserted : out Boolean);
procedure Intersection procedure Intersection
(Left : Set; (Left : Set;
...@@ -136,10 +133,13 @@ is ...@@ -136,10 +133,13 @@ is
begin begin
Node := First (Left).Node; Node := First (Left).Node;
while Node /= 0 loop while Node /= 0 loop
ENode := Find (Container => Right, ENode :=
Item => Left.Nodes (Node).Element).Node; Find
if ENode = 0 or else (Container => Right,
Right.Nodes (ENode).Element /= Left.Nodes (Node).Element Item => Left.Nodes (Node).Element).Node;
if ENode = 0
or else Right.Nodes (ENode).Element /= Left.Nodes (Node).Element
then then
return False; return False;
end if; end if;
...@@ -148,9 +148,7 @@ is ...@@ -148,9 +148,7 @@ is
end loop; end loop;
return True; return True;
end; end;
end "="; end "=";
------------ ------------
...@@ -228,11 +226,11 @@ is ...@@ -228,11 +226,11 @@ is
Capacity : Count_Type := 0) return Set Capacity : Count_Type := 0) return Set
is is
C : constant Count_Type := C : constant Count_Type :=
Count_Type'Max (Capacity, Source.Capacity); Count_Type'Max (Capacity, Source.Capacity);
Cu : Cursor;
H : Hash_Type; H : Hash_Type;
N : Count_Type; N : Count_Type;
Target : Set (C, Source.Modulus); Target : Set (C, Source.Modulus);
Cu : Cursor;
begin begin
if 0 < Capacity and then Capacity < Source.Capacity then if 0 < Capacity and then Capacity < Source.Capacity then
...@@ -276,10 +274,7 @@ is ...@@ -276,10 +274,7 @@ is
-- Delete -- -- Delete --
------------ ------------
procedure Delete procedure Delete (Container : in out Set; Item : Element_Type) is
(Container : in out Set;
Item : Element_Type)
is
X : Count_Type; X : Count_Type;
begin begin
...@@ -292,10 +287,7 @@ is ...@@ -292,10 +287,7 @@ is
Free (Container, X); Free (Container, X);
end Delete; end Delete;
procedure Delete procedure Delete (Container : in out Set; Position : in out Cursor) is
(Container : in out Set;
Position : in out Cursor)
is
begin begin
if not Has_Element (Container, Position) then if not Has_Element (Container, Position) then
raise Constraint_Error with "Position cursor has no element"; raise Constraint_Error with "Position cursor has no element";
...@@ -313,11 +305,11 @@ is ...@@ -313,11 +305,11 @@ is
-- Difference -- -- Difference --
---------------- ----------------
procedure Difference procedure Difference (Target : in out Set; Source : Set) is
(Target : in out Set; Src_Last : Count_Type;
Source : Set) Src_Length : Count_Type;
is Src_Node : Count_Type;
Tgt_Node, Src_Node, Src_Last, Src_Length : Count_Type; Tgt_Node : Count_Type;
TN : Nodes_Type renames Target.Nodes; TN : Nodes_Type renames Target.Nodes;
SN : Nodes_Type renames Source.Nodes; SN : Nodes_Type renames Source.Nodes;
...@@ -369,10 +361,7 @@ is ...@@ -369,10 +361,7 @@ is
end loop; end loop;
end Difference; end Difference;
procedure Difference procedure Difference (Left : Set; Right : Set; Target : in out Set) is
(Left, Right : Set;
Target : in out Set)
is
procedure Process (L_Node : Count_Type); procedure Process (L_Node : Count_Type);
procedure Iterate is procedure Iterate is
...@@ -383,9 +372,10 @@ is ...@@ -383,9 +372,10 @@ is
------------- -------------
procedure Process (L_Node : Count_Type) is procedure Process (L_Node : Count_Type) is
B : Boolean;
E : Element_Type renames Left.Nodes (L_Node).Element; E : Element_Type renames Left.Nodes (L_Node).Element;
X : Count_Type; X : Count_Type;
B : Boolean;
begin begin
if Find (Right, E).Node = 0 then if Find (Right, E).Node = 0 then
Insert (Target, E, X, B); Insert (Target, E, X, B);
...@@ -399,7 +389,7 @@ is ...@@ -399,7 +389,7 @@ is
Iterate (Left); Iterate (Left);
end Difference; end Difference;
function Difference (Left, Right : Set) return Set is function Difference (Left : Set; Right : Set) return Set is
C : Count_Type; C : Count_Type;
H : Hash_Type; H : Hash_Type;
...@@ -437,8 +427,8 @@ is ...@@ -437,8 +427,8 @@ is
raise Constraint_Error with "Position cursor equals No_Element"; raise Constraint_Error with "Position cursor equals No_Element";
end if; end if;
pragma Assert (Vet (Container, Position), pragma Assert
"bad cursor in function Element"); (Vet (Container, Position), "bad cursor in function Element");
return Container.Nodes (Position.Node).Element; return Container.Nodes (Position.Node).Element;
end Element; end Element;
...@@ -466,7 +456,7 @@ is ...@@ -466,7 +456,7 @@ is
L_Node : Node_Type) return Boolean L_Node : Node_Type) return Boolean
is is
R_Index : constant Hash_Type := R_Index : constant Hash_Type :=
Element_Keys.Index (R_HT, L_Node.Element); Element_Keys.Index (R_HT, L_Node.Element);
R_Node : Count_Type := R_HT.Buckets (R_Index); R_Node : Count_Type := R_HT.Buckets (R_Index);
RN : Nodes_Type renames R_HT.Nodes; RN : Nodes_Type renames R_HT.Nodes;
...@@ -508,10 +498,7 @@ is ...@@ -508,10 +498,7 @@ is
-- Exclude -- -- Exclude --
------------- -------------
procedure Exclude procedure Exclude (Container : in out Set; Item : Element_Type) is
(Container : in out Set;
Item : Element_Type)
is
X : Count_Type; X : Count_Type;
begin begin
Element_Keys.Delete_Key_Sans_Free (Container, Item, X); Element_Keys.Delete_Key_Sans_Free (Container, Item, X);
...@@ -771,10 +758,7 @@ is ...@@ -771,10 +758,7 @@ is
-- Free -- -- Free --
---------- ----------
procedure Free procedure Free (HT : in out Set; X : Count_Type) is
(HT : in out Set;
X : Count_Type)
is
begin begin
HT.Nodes (X).Has_Element := False; HT.Nodes (X).Has_Element := False;
HT_Ops.Free (HT, X); HT_Ops.Free (HT, X);
...@@ -784,10 +768,7 @@ is ...@@ -784,10 +768,7 @@ is
-- Generic_Allocate -- -- Generic_Allocate --
---------------------- ----------------------
procedure Generic_Allocate procedure Generic_Allocate (HT : in out Set; Node : out Count_Type) is
(HT : in out Set;
Node : out Count_Type)
is
procedure Allocate is new HT_Ops.Generic_Allocate (Set_Element); procedure Allocate is new HT_Ops.Generic_Allocate (Set_Element);
begin begin
Allocate (HT, Node); Allocate (HT, Node);
...@@ -809,14 +790,13 @@ is ...@@ -809,14 +790,13 @@ is
-- Local Instantiations -- -- Local Instantiations --
-------------------------- --------------------------
package Key_Keys is package Key_Keys is new Hash_Tables.Generic_Bounded_Keys
new Hash_Tables.Generic_Bounded_Keys (HT_Types => HT_Types,
(HT_Types => HT_Types, Next => Next,
Next => Next, Set_Next => Set_Next,
Set_Next => Set_Next, Key_Type => Key_Type,
Key_Type => Key_Type, Hash => Hash,
Hash => Hash, Equivalent_Keys => Equivalent_Key_Node);
Equivalent_Keys => Equivalent_Key_Node);
-------------- --------------
-- Contains -- -- Contains --
...@@ -834,10 +814,7 @@ is ...@@ -834,10 +814,7 @@ is
-- Delete -- -- Delete --
------------ ------------
procedure Delete procedure Delete (Container : in out Set; Key : Key_Type) is
(Container : in out Set;
Key : Key_Type)
is
X : Count_Type; X : Count_Type;
begin begin
...@@ -884,10 +861,7 @@ is ...@@ -884,10 +861,7 @@ is
-- Exclude -- -- Exclude --
------------- -------------
procedure Exclude procedure Exclude (Container : in out Set; Key : Key_Type) is
(Container : in out Set;
Key : Key_Type)
is
X : Count_Type; X : Count_Type;
begin begin
Key_Keys.Delete_Key_Sans_Free (Container, Key, X); Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
...@@ -930,6 +904,7 @@ is ...@@ -930,6 +904,7 @@ is
return False; return False;
end if; end if;
end loop; end loop;
return True; return True;
end M_Included_Except; end M_Included_Except;
...@@ -942,8 +917,7 @@ is ...@@ -942,8 +917,7 @@ is
function Key (Container : Set; Position : Cursor) return Key_Type is function Key (Container : Set; Position : Cursor) return Key_Type is
begin begin
if not Has_Element (Container, Position) then if not Has_Element (Container, Position) then
raise Constraint_Error with raise Constraint_Error with "Position cursor has no element";
"Position cursor has no element";
end if; end if;
pragma Assert pragma Assert
...@@ -969,8 +943,7 @@ is ...@@ -969,8 +943,7 @@ is
begin begin
if Node = 0 then if Node = 0 then
raise Constraint_Error with raise Constraint_Error with "attempt to replace key not in set";
"attempt to replace key not in set";
end if; end if;
Replace_Element (Container, Node, New_Item); Replace_Element (Container, Node, New_Item);
...@@ -1006,12 +979,9 @@ is ...@@ -1006,12 +979,9 @@ is
-- Include -- -- Include --
------------- -------------
procedure Include procedure Include (Container : in out Set; New_Item : Element_Type) is
(Container : in out Set;
New_Item : Element_Type)
is
Position : Cursor;
Inserted : Boolean; Inserted : Boolean;
Position : Cursor;
begin begin
Insert (Container, New_Item, Position, Inserted); Insert (Container, New_Item, Position, Inserted);
...@@ -1035,12 +1005,9 @@ is ...@@ -1035,12 +1005,9 @@ is
Insert (Container, New_Item, Position.Node, Inserted); Insert (Container, New_Item, Position.Node, Inserted);
end Insert; end Insert;
procedure Insert procedure Insert (Container : in out Set; New_Item : Element_Type) is
(Container : in out Set;
New_Item : Element_Type)
is
Position : Cursor;
Inserted : Boolean; Inserted : Boolean;
Position : Cursor;
begin begin
Insert (Container, New_Item, Position, Inserted); Insert (Container, New_Item, Position, Inserted);
...@@ -1099,10 +1066,7 @@ is ...@@ -1099,10 +1066,7 @@ is
-- Intersection -- -- Intersection --
------------------ ------------------
procedure Intersection procedure Intersection (Target : in out Set; Source : Set) is
(Target : in out Set;
Source : Set)
is
Tgt_Node : Count_Type; Tgt_Node : Count_Type;
TN : Nodes_Type renames Target.Nodes; TN : Nodes_Type renames Target.Nodes;
...@@ -1133,11 +1097,7 @@ is ...@@ -1133,11 +1097,7 @@ is
end loop; end loop;
end Intersection; end Intersection;
procedure Intersection procedure Intersection (Left : Set; Right : Set; Target : in out Set) is
(Left : Set;
Right : Set;
Target : in out Set)
is
procedure Process (L_Node : Count_Type); procedure Process (L_Node : Count_Type);
procedure Iterate is procedure Iterate is
...@@ -1165,7 +1125,7 @@ is ...@@ -1165,7 +1125,7 @@ is
Iterate (Left); Iterate (Left);
end Intersection; end Intersection;
function Intersection (Left, Right : Set) return Set is function Intersection (Left : Set; Right : Set) return Set is
C : Count_Type; C : Count_Type;
H : Hash_Type; H : Hash_Type;
...@@ -1179,7 +1139,7 @@ is ...@@ -1179,7 +1139,7 @@ is
return S : Set (C, H) do return S : Set (C, H) do
if Length (Left) /= 0 and Length (Right) /= 0 then if Length (Left) /= 0 and Length (Right) /= 0 then
Intersection (Left, Right, Target => S); Intersection (Left, Right, Target => S);
end if; end if;
end return; end return;
end Intersection; end Intersection;
...@@ -1301,8 +1261,7 @@ is ...@@ -1301,8 +1261,7 @@ is
end if; end if;
if not Has_Element (Container, Position) then if not Has_Element (Container, Position) then
raise Constraint_Error raise Constraint_Error with "Position has no element";
with "Position has no element";
end if; end if;
pragma Assert (Vet (Container, Position), "bad cursor in Next"); pragma Assert (Vet (Container, Position), "bad cursor in Next");
...@@ -1353,16 +1312,12 @@ is ...@@ -1353,16 +1312,12 @@ is
-- Replace -- -- Replace --
------------- -------------
procedure Replace procedure Replace (Container : in out Set; New_Item : Element_Type) is
(Container : in out Set;
New_Item : Element_Type)
is
Node : constant Count_Type := Element_Keys.Find (Container, New_Item); Node : constant Count_Type := Element_Keys.Find (Container, New_Item);
begin begin
if Node = 0 then if Node = 0 then
raise Constraint_Error with raise Constraint_Error with "attempt to replace element not in set";
"attempt to replace element not in set";
end if; end if;
Container.Nodes (Node).Element := New_Item; Container.Nodes (Node).Element := New_Item;
...@@ -1379,12 +1334,11 @@ is ...@@ -1379,12 +1334,11 @@ is
is is
begin begin
if not Has_Element (Container, Position) then if not Has_Element (Container, Position) then
raise Constraint_Error with raise Constraint_Error with "Position cursor equals No_Element";
"Position cursor equals No_Element";
end if; end if;
pragma Assert (Vet (Container, Position), pragma Assert
"bad cursor in Replace_Element"); (Vet (Container, Position), "bad cursor in Replace_Element");
Replace_Element (Container, Position.Node, New_Item); Replace_Element (Container, Position.Node, New_Item);
end Replace_Element; end Replace_Element;
...@@ -1425,10 +1379,7 @@ is ...@@ -1425,10 +1379,7 @@ is
-- Symmetric_Difference -- -- Symmetric_Difference --
-------------------------- --------------------------
procedure Symmetric_Difference procedure Symmetric_Difference (Target : in out Set; Source : Set) is
(Target : in out Set;
Source : Set)
is
procedure Process (Source_Node : Count_Type); procedure Process (Source_Node : Count_Type);
pragma Inline (Process); pragma Inline (Process);
...@@ -1439,9 +1390,10 @@ is ...@@ -1439,9 +1390,10 @@ is
------------- -------------
procedure Process (Source_Node : Count_Type) is procedure Process (Source_Node : Count_Type) is
B : Boolean;
N : Node_Type renames Source.Nodes (Source_Node); N : Node_Type renames Source.Nodes (Source_Node);
X : Count_Type; X : Count_Type;
B : Boolean;
begin begin
if Is_In (Target, N) then if Is_In (Target, N) then
Delete (Target, N.Element); Delete (Target, N.Element);
...@@ -1467,7 +1419,7 @@ is ...@@ -1467,7 +1419,7 @@ is
Iterate (Source); Iterate (Source);
end Symmetric_Difference; end Symmetric_Difference;
function Symmetric_Difference (Left, Right : Set) return Set is function Symmetric_Difference (Left : Set; Right : Set) return Set is
C : Count_Type; C : Count_Type;
H : Hash_Type; H : Hash_Type;
...@@ -1512,10 +1464,7 @@ is ...@@ -1512,10 +1464,7 @@ is
-- Union -- -- Union --
----------- -----------
procedure Union procedure Union (Target : in out Set; Source : Set) is
(Target : in out Set;
Source : Set)
is
procedure Process (Src_Node : Count_Type); procedure Process (Src_Node : Count_Type);
procedure Iterate is procedure Iterate is
...@@ -1536,7 +1485,7 @@ is ...@@ -1536,7 +1485,7 @@ is
Insert (Target, E, X, B); Insert (Target, E, X, B);
end Process; end Process;
-- Start of processing for Union -- Start of processing for Union
begin begin
if Target'Address = Source'Address then if Target'Address = Source'Address then
...@@ -1546,7 +1495,7 @@ is ...@@ -1546,7 +1495,7 @@ is
Iterate (Source); Iterate (Source);
end Union; end Union;
function Union (Left, Right : Set) return Set is function Union (Left : Set; Right : Set) return Set is
C : Count_Type; C : Count_Type;
H : Hash_Type; H : Hash_Type;
......
gcc/ada/a-cfhase.ads
...@@ -55,8 +55,10 @@ generic ...@@ -55,8 +55,10 @@ generic
with function Hash (Element : Element_Type) return Hash_Type; with function Hash (Element : Element_Type) return Hash_Type;
with function Equivalent_Elements (Left, Right : Element_Type) with function Equivalent_Elements
return Boolean is "="; (Left : Element_Type;
Right : Element_Type) return Boolean is "=";
package Ada.Containers.Formal_Hashed_Sets with package Ada.Containers.Formal_Hashed_Sets with
SPARK_Mode SPARK_Mode
is is
...@@ -122,8 +124,9 @@ is ...@@ -122,8 +124,9 @@ is
Global => null, Global => null,
Post => Post =>
(if Find'Result > 0 then (if Find'Result > 0 then
Find'Result <= E.Length (Container) Find'Result <= E.Length (Container)
and Equivalent_Elements (Item, E.Get (Container, Find'Result))); and Equivalent_Elements
(Item, E.Get (Container, Find'Result)));
function E_Elements_Included function E_Elements_Included
(Left : E.Sequence; (Left : E.Sequence;
...@@ -135,9 +138,9 @@ is ...@@ -135,9 +138,9 @@ is
Post => Post =>
E_Elements_Included'Result = E_Elements_Included'Result =
(for all I in 1 .. E.Length (Left) => (for all I in 1 .. E.Length (Left) =>
Find (Right, E.Get (Left, I)) > 0 Find (Right, E.Get (Left, I)) > 0
and then E.Get (Right, Find (Right, E.Get (Left, I))) = and then E.Get (Right, Find (Right, E.Get (Left, I))) =
E.Get (Left, I)); E.Get (Left, I));
pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included); pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
function E_Elements_Included function E_Elements_Included
...@@ -152,9 +155,9 @@ is ...@@ -152,9 +155,9 @@ is
E_Elements_Included'Result = E_Elements_Included'Result =
(for all I in 1 .. E.Length (Left) => (for all I in 1 .. E.Length (Left) =>
(if M.Contains (Model, E.Get (Left, I)) then (if M.Contains (Model, E.Get (Left, I)) then
Find (Right, E.Get (Left, I)) > 0 Find (Right, E.Get (Left, I)) > 0
and then E.Get (Right, Find (Right, E.Get (Left, I))) = and then E.Get (Right, Find (Right, E.Get (Left, I))) =
E.Get (Left, I))); E.Get (Left, I)));
pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included); pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
function E_Elements_Included function E_Elements_Included
...@@ -171,13 +174,14 @@ is ...@@ -171,13 +174,14 @@ is
E_Elements_Included'Result = E_Elements_Included'Result =
(for all I in 1 .. E.Length (Container) => (for all I in 1 .. E.Length (Container) =>
(if M.Contains (Model, E.Get (Container, I)) then (if M.Contains (Model, E.Get (Container, I)) then
Find (Left, E.Get (Container, I)) > 0 Find (Left, E.Get (Container, I)) > 0
and then E.Get (Left, Find (Left, E.Get (Container, I))) = and then E.Get (Left, Find (Left, E.Get (Container, I))) =
E.Get (Container, I) E.Get (Container, I)
else else
Find (Right, E.Get (Container, I)) > 0 Find (Right, E.Get (Container, I)) > 0
and then E.Get (Right, Find (Right, E.Get (Container, I))) = and then E.Get
E.Get (Container, I))); (Right, Find (Right, E.Get (Container, I))) =
E.Get (Container, I)));
pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included); pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
package P is new Ada.Containers.Functional_Maps package P is new Ada.Containers.Functional_Maps
...@@ -241,8 +245,8 @@ is ...@@ -241,8 +245,8 @@ is
and (for all C of P_Left => and (for all C of P_Left =>
(if C /= Position then (if C /= Position then
E.Get (E_Left, P.Get (P_Left, C)) = E.Get (E_Left, P.Get (P_Left, C)) =
E.Get (E_Right, P.Get (P_Right, C))))); E.Get (E_Right, P.Get (P_Right, C)))));
function Model (Container : Set) return M.Set with function Model (Container : Set) return M.Set with
-- The high-level model of a set is a set of elements. Neither cursors -- The high-level model of a set is a set of elements. Neither cursors
...@@ -266,15 +270,16 @@ is ...@@ -266,15 +270,16 @@ is
-- It only contains keys contained in Model -- It only contains keys contained in Model
and (for all Item of Elements'Result => and (for all Item of Elements'Result =>
M.Contains (Model (Container), Item)) M.Contains (Model (Container), Item))
-- It contains all the elements contained in Model -- It contains all the elements contained in Model
and (for all Item of Model (Container) => and (for all Item of Model (Container) =>
(Find (Elements'Result, Item) > 0 (Find (Elements'Result, Item) > 0
and then Equivalent_Elements and then Equivalent_Elements
(E.Get (Elements'Result, Find (Elements'Result, Item)), (E.Get (Elements'Result,
Item))) Find (Elements'Result, Item)),
Item)))
-- It has no duplicate -- It has no duplicate
...@@ -311,7 +316,7 @@ is ...@@ -311,7 +316,7 @@ is
and then and then
(for all J of Positions'Result => (for all J of Positions'Result =>
(if P.Get (Positions'Result, I) = P.Get (Positions'Result, J) (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
then I = J))); then I = J)));
procedure Lift_Abstraction_Level (Container : Set) with procedure Lift_Abstraction_Level (Container : Set) with
-- Lift_Abstraction_Level is a ghost procedure that does nothing but -- Lift_Abstraction_Level is a ghost procedure that does nothing but
...@@ -343,13 +348,13 @@ is ...@@ -343,13 +348,13 @@ is
function "=" (Left, Right : Set) return Boolean with function "=" (Left, Right : Set) return Boolean with
Global => null, Global => null,
Post => Post =>
"="'Result = "="'Result =
(Length (Left) = Length (Right) (Length (Left) = Length (Right)
and E_Elements_Included (Elements (Left), Elements (Right))) and E_Elements_Included (Elements (Left), Elements (Right)))
and and
"="'Result = "="'Result =
(E_Elements_Included (Elements (Left), Elements (Right)) (E_Elements_Included (Elements (Left), Elements (Right))
and E_Elements_Included (Elements (Right), Elements (Left))); and E_Elements_Included (Elements (Right), Elements (Left)));
function Equivalent_Sets (Left, Right : Set) return Boolean with function Equivalent_Sets (Left, Right : Set) return Boolean with
Global => null, Global => null,
...@@ -378,12 +383,10 @@ is ...@@ -378,12 +383,10 @@ is
-- Actual elements are preserved -- Actual elements are preserved
and and E_Elements_Included
E_Elements_Included (Elements (Container), Elements (Container)'Old)
(Elements (Container), Elements (Container)'Old) and E_Elements_Included
and (Elements (Container)'Old, Elements (Container));
E_Elements_Included
(Elements (Container)'Old, Elements (Container));
function Is_Empty (Container : Set) return Boolean with function Is_Empty (Container : Set) return Boolean with
Global => null, Global => null,
...@@ -402,10 +405,8 @@ is ...@@ -402,10 +405,8 @@ is
-- Actual elements are preserved -- Actual elements are preserved
and and E_Elements_Included (Elements (Target), Elements (Source))
E_Elements_Included (Elements (Target), Elements (Source)) and E_Elements_Included (Elements (Source), Elements (Target));
and
E_Elements_Included (Elements (Source), Elements (Target));
function Copy function Copy
(Source : Set; (Source : Set;
...@@ -482,10 +483,8 @@ is ...@@ -482,10 +483,8 @@ is
-- Actual elements are preserved -- Actual elements are preserved
and and E_Elements_Included (Elements (Target), Elements (Source)'Old)
E_Elements_Included (Elements (Target), Elements (Source)'Old) and E_Elements_Included (Elements (Source)'Old, Elements (Target));
and
E_Elements_Included (Elements (Source)'Old, Elements (Target));
procedure Insert procedure Insert
(Container : in out Set; (Container : in out Set;
...@@ -769,27 +768,25 @@ is ...@@ -769,27 +768,25 @@ is
-- Elements of Target come from either Source or Target -- Elements of Target come from either Source or Target
and and M.Included_In_Union
M.Included_In_Union (Model (Target), Model (Source), Model (Target)'Old)
(Model (Target), Model (Source), Model (Target)'Old)
-- Actual value of elements come from either Left or Right -- Actual value of elements come from either Left or Right
and and E_Elements_Included
E_Elements_Included (Elements (Target),
(Elements (Target), Model (Target)'Old,
Model (Target)'Old, Elements (Target)'Old,
Elements (Target)'Old, Elements (Source))
Elements (Source))
and and E_Elements_Included
E_Elements_Included (Elements (Target)'Old, Model (Target)'Old, Elements (Target))
(Elements (Target)'Old, Model (Target)'Old, Elements (Target))
and and E_Elements_Included
E_Elements_Included (Elements (Source),
(Elements (Source), Model (Target)'Old,
Model (Target)'Old, Elements (Source),
Elements (Source), Elements (Target))
Elements (Target))
-- Mapping from cursors of Target to elements is preserved -- Mapping from cursors of Target to elements is preserved
...@@ -820,21 +817,20 @@ is ...@@ -820,21 +817,20 @@ is
-- Actual value of elements come from either Left or Right -- Actual value of elements come from either Left or Right
and and E_Elements_Included
E_Elements_Included (Elements (Union'Result),
(Elements (Union'Result), Model (Left),
Model (Left), Elements (Left),
Elements (Left), Elements (Right))
Elements (Right))
and and E_Elements_Included
E_Elements_Included (Elements (Left), Model (Left), Elements (Union'Result))
(Elements (Left), Model (Left), Elements (Union'Result))
and and E_Elements_Included
E_Elements_Included (Elements (Right),
(Elements (Right), Model (Left),
Model (Left), Elements (Right),
Elements (Right), Elements (Union'Result));
Elements (Union'Result));
function "or" (Left, Right : Set) return Set renames Union; function "or" (Left, Right : Set) return Set renames Union;
...@@ -854,16 +850,14 @@ is ...@@ -854,16 +850,14 @@ is
-- Elements both in Source and Target are in the intersection -- Elements both in Source and Target are in the intersection
and and M.Includes_Intersection
M.Includes_Intersection (Model (Target), Model (Source), Model (Target)'Old)
(Model (Target), Model (Source), Model (Target)'Old)
-- Actual value of elements of Target is preserved -- Actual value of elements of Target is preserved
and E_Elements_Included (Elements (Target), Elements (Target)'Old) and E_Elements_Included (Elements (Target), Elements (Target)'Old)
and and E_Elements_Included
E_Elements_Included (Elements (Target)'Old, Model (Source), Elements (Target))
(Elements (Target)'Old, Model (Source), Elements (Target))
-- Mapping from cursors of Target to elements is preserved -- Mapping from cursors of Target to elements is preserved
...@@ -886,18 +880,17 @@ is ...@@ -886,18 +880,17 @@ is
-- Elements both in Left and Right are in the result of Intersection -- Elements both in Left and Right are in the result of Intersection
and and M.Includes_Intersection
M.Includes_Intersection (Model (Intersection'Result), Model (Left), Model (Right))
(Model (Intersection'Result), Model (Left), Model (Right))
-- Actual value of elements come from Left -- Actual value of elements come from Left
and and E_Elements_Included
E_Elements_Included (Elements (Intersection'Result), Elements (Left))
(Elements (Intersection'Result), Elements (Left))
and and E_Elements_Included
E_Elements_Included (Elements (Left), Model (Right),
(Elements (Left), Model (Right), Elements (Intersection'Result)); Elements (Intersection'Result));
function "and" (Left, Right : Set) return Set renames Intersection; function "and" (Left, Right : Set) return Set renames Intersection;
...@@ -917,16 +910,14 @@ is ...@@ -917,16 +910,14 @@ is
-- Elements in Target but not in Source are in the difference -- Elements in Target but not in Source are in the difference
and and M.Included_In_Union
M.Included_In_Union (Model (Target)'Old, Model (Target), Model (Source))
(Model (Target)'Old, Model (Target), Model (Source))
-- Actual value of elements of Target is preserved -- Actual value of elements of Target is preserved
and E_Elements_Included (Elements (Target), Elements (Target)'Old) and E_Elements_Included (Elements (Target), Elements (Target)'Old)
and and E_Elements_Included
E_Elements_Included (Elements (Target)'Old, Model (Target), Elements (Target))
(Elements (Target)'Old, Model (Target), Elements (Target))
-- Mapping from cursors of Target to elements is preserved -- Mapping from cursors of Target to elements is preserved
...@@ -952,19 +943,18 @@ is ...@@ -952,19 +943,18 @@ is
-- Elements in Left but not in Right are in the difference -- Elements in Left but not in Right are in the difference
and and M.Included_In_Union
M.Included_In_Union (Model (Left), Model (Difference'Result), Model (Right))
(Model (Left), Model (Difference'Result), Model (Right))
-- Actual value of elements come from Left -- Actual value of elements come from Left
and and E_Elements_Included
E_Elements_Included (Elements (Difference'Result), Elements (Left)) (Elements (Difference'Result), Elements (Left))
and
E_Elements_Included and E_Elements_Included
(Elements (Left), (Elements (Left),
Model (Difference'Result), Model (Difference'Result),
Elements (Difference'Result)); Elements (Difference'Result));
function "-" (Left, Right : Set) return Set renames Difference; function "-" (Left, Right : Set) return Set renames Difference;
...@@ -984,30 +974,27 @@ is ...@@ -984,30 +974,27 @@ is
-- Elements in Target but not in Source are in the difference -- Elements in Target but not in Source are in the difference
and and M.Included_In_Union
M.Included_In_Union (Model (Target)'Old, Model (Target), Model (Source))
(Model (Target)'Old, Model (Target), Model (Source))
-- Elements in Source but not in Target are in the difference -- Elements in Source but not in Target are in the difference
and and M.Included_In_Union
M.Included_In_Union (Model (Source), Model (Target), Model (Target)'Old)
(Model (Source), Model (Target), Model (Target)'Old)
-- Actual value of elements come from either Left or Right -- Actual value of elements come from either Left or Right
and and E_Elements_Included
E_Elements_Included (Elements (Target),
(Elements (Target), Model (Target)'Old,
Model (Target)'Old, Elements (Target)'Old,
Elements (Target)'Old, Elements (Source))
Elements (Source))
and and E_Elements_Included
E_Elements_Included (Elements (Target)'Old, Model (Target), Elements (Target))
(Elements (Target)'Old, Model (Target), Elements (Target))
and and E_Elements_Included
E_Elements_Included (Elements (Source), Model (Target), Elements (Target));
(Elements (Source), Model (Target), Elements (Target));
function Symmetric_Difference (Left, Right : Set) return Set with function Symmetric_Difference (Left, Right : Set) return Set with
Global => null, Global => null,
...@@ -1019,40 +1006,42 @@ is ...@@ -1019,40 +1006,42 @@ is
-- Elements of the difference were not both in Left and Right -- Elements of the difference were not both in Left and Right
and and M.Not_In_Both
M.Not_In_Both (Model (Symmetric_Difference'Result),
(Model (Symmetric_Difference'Result), Model (Left), Model (Right)) Model (Left),
Model (Right))
-- Elements in Left but not in Right are in the difference -- Elements in Left but not in Right are in the difference
and and M.Included_In_Union
M.Included_In_Union (Model (Left),
(Model (Left), Model (Symmetric_Difference'Result), Model (Right)) Model (Symmetric_Difference'Result),
Model (Right))
-- Elements in Right but not in Left are in the difference -- Elements in Right but not in Left are in the difference
and and M.Included_In_Union
M.Included_In_Union (Model (Right),
(Model (Right), Model (Symmetric_Difference'Result), Model (Left)) Model (Symmetric_Difference'Result),
Model (Left))
-- Actual value of elements come from either Left or Right -- Actual value of elements come from either Left or Right
and and E_Elements_Included
E_Elements_Included (Elements (Symmetric_Difference'Result),
(Elements (Symmetric_Difference'Result), Model (Left),
Model (Left), Elements (Left),
Elements (Left), Elements (Right))
Elements (Right))
and and E_Elements_Included
E_Elements_Included (Elements (Left),
(Elements (Left), Model (Symmetric_Difference'Result),
Model (Symmetric_Difference'Result), Elements (Symmetric_Difference'Result))
Elements (Symmetric_Difference'Result))
and and E_Elements_Included
E_Elements_Included (Elements (Right),
(Elements (Right), Model (Symmetric_Difference'Result),
Model (Symmetric_Difference'Result), Elements (Symmetric_Difference'Result));
Elements (Symmetric_Difference'Result));
function "xor" (Left, Right : Set) return Set function "xor" (Left, Right : Set) return Set
renames Symmetric_Difference; renames Symmetric_Difference;
...@@ -1167,8 +1156,8 @@ is ...@@ -1167,8 +1156,8 @@ is
Post => Post =>
M_Included_Except'Result = M_Included_Except'Result =
(for all E of Left => (for all E of Left =>
Contains (Right, E) Contains (Right, E)
or Equivalent_Keys (Generic_Keys.Key (E), Key)); or Equivalent_Keys (Generic_Keys.Key (E), Key));
end Formal_Model; end Formal_Model;
use Formal_Model; use Formal_Model;
...@@ -1309,16 +1298,15 @@ is ...@@ -1309,16 +1298,15 @@ is
-- The key designated by the result of Find is Key -- The key designated by the result of Find is Key
and and Equivalent_Keys
Equivalent_Keys (Generic_Keys.Key (Container, Find'Result), Key));
(Generic_Keys.Key (Container, Find'Result), Key));
function Contains (Container : Set; Key : Key_Type) return Boolean with function Contains (Container : Set; Key : Key_Type) return Boolean with
Global => null, Global => null,
Post => Post =>
Contains'Result = Contains'Result =
(for some E of Model (Container) => (for some E of Model (Container) =>
Equivalent_Keys (Key, Generic_Keys.Key (E))); Equivalent_Keys (Key, Generic_Keys.Key (E)));
end Generic_Keys; end Generic_Keys;
......
gcc/ada/a-cfinve.adb
...@@ -705,12 +705,11 @@ is ...@@ -705,12 +705,11 @@ is
function "<" (Left : Holder; Right : Holder) return Boolean is function "<" (Left : Holder; Right : Holder) return Boolean is
(E (Left) < E (Right)); (E (Left) < E (Right));
procedure Sort is procedure Sort is new Generic_Array_Sort
new Generic_Array_Sort (Index_Type => Array_Index,
(Index_Type => Array_Index, Element_Type => Holder,
Element_Type => Holder, Array_Type => Elements_Array,
Array_Type => Elements_Array, "<" => "<");
"<" => "<");
Len : constant Capacity_Range := Length (Container); Len : constant Capacity_Range := Length (Container);
...@@ -1065,8 +1064,9 @@ is ...@@ -1065,8 +1064,9 @@ is
then then
Reserve_Capacity Reserve_Capacity
(Container, (Container,
Capacity_Range'Max (Current_Capacity (Container) * Growth_Factor, Capacity_Range'Max
Capacity_Range (New_Length))); (Current_Capacity (Container) * Growth_Factor,
Capacity_Range (New_Length)));
end if; end if;
declare declare
...@@ -1348,10 +1348,10 @@ is ...@@ -1348,10 +1348,10 @@ is
-- hence we also know that -- hence we also know that
-- Index - Index_Type'First >= 0 -- Index - Index_Type'First >= 0
-- The issue is that even though 0 is guaranteed to be a value in -- The issue is that even though 0 is guaranteed to be a value in the
-- the type Index_Type'Base, there's no guarantee that the difference -- type Index_Type'Base, there's no guarantee that the difference is a
-- is a value in that type. To prevent overflow we use the wider -- value in that type. To prevent overflow we use the wider of
-- of Count_Type'Base and Index_Type'Base to perform intermediate -- Count_Type'Base and Index_Type'Base to perform intermediate
-- calculations. -- calculations.
if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
...@@ -1362,8 +1362,8 @@ is ...@@ -1362,8 +1362,8 @@ is
Count_Type'Base (Index_Type'First); Count_Type'Base (Index_Type'First);
end if; end if;
-- The array index subtype for all container element arrays -- The array index subtype for all container element arrays always
-- always starts with 1. -- starts with 1.
return 1 + Offset; return 1 + Offset;
end To_Array_Index; end To_Array_Index;
......
gcc/ada/a-cfinve.ads
...@@ -830,9 +830,9 @@ is ...@@ -830,9 +830,9 @@ is
Post => Post =>
M_Elements_Sorted'Result = M_Elements_Sorted'Result =
(for all I in Index_Type'First .. M.Last (Container) => (for all I in Index_Type'First .. M.Last (Container) =>
(for all J in I .. M.Last (Container) => (for all J in I .. M.Last (Container) =>
Element (Container, I) = Element (Container, J) Element (Container, I) = Element (Container, J)
or Element (Container, I) < Element (Container, J))); or Element (Container, I) < Element (Container, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
end Formal_Model; end Formal_Model;
......
gcc/ada/a-cforma.adb
...@@ -518,7 +518,9 @@ is ...@@ -518,7 +518,9 @@ is
-- Find -- -- Find --
---------- ----------
function Find (Container : K.Sequence; Key : Key_Type) return Count_Type function Find
(Container : K.Sequence;
Key : Key_Type) return Count_Type
is is
begin begin
for I in 1 .. K.Length (Container) loop for I in 1 .. K.Length (Container) loop
...@@ -634,9 +636,12 @@ is ...@@ -634,9 +636,12 @@ is
-- for their postconditions. -- for their postconditions.
while Position /= 0 loop while Position /= 0 loop
R := M.Add (Container => R, R :=
New_Key => Container.Nodes (Position).Key, M.Add
New_Item => Container.Nodes (Position).Element); (Container => R,
New_Key => Container.Nodes (Position).Key,
New_Item => Container.Nodes (Position).Element);
Position := Tree_Operations.Next (Container, Position); Position := Tree_Operations.Next (Container, Position);
end loop; end loop;
......
gcc/ada/a-cforma.ads
...@@ -159,16 +159,16 @@ is ...@@ -159,16 +159,16 @@ is
Pre => Position - 1 <= K.Length (Container), Pre => Position - 1 <= K.Length (Container),
Post => Post =>
K_Is_Find'Result = K_Is_Find'Result =
((if Position > 0 then
K_Bigger_Than_Range (Container, 1, Position - 1, Key))
((if Position > 0 then and
K_Bigger_Than_Range (Container, 1, Position - 1, Key)) (if Position < K.Length (Container) then
K_Smaller_Than_Range
and (if Position < K.Length (Container) then (Container,
K_Smaller_Than_Range Position + 1,
(Container, K.Length (Container),
Position + 1, Key)));
K.Length (Container),
Key)));
pragma Annotate (GNATprove, Inline_For_Proof, K_Is_Find); pragma Annotate (GNATprove, Inline_For_Proof, K_Is_Find);
function Find (Container : K.Sequence; Key : Key_Type) return Count_Type function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
...@@ -178,8 +178,8 @@ is ...@@ -178,8 +178,8 @@ is
Global => null, Global => null,
Post => Post =>
(if Find'Result > 0 then (if Find'Result > 0 then
Find'Result <= K.Length (Container) Find'Result <= K.Length (Container)
and Equivalent_Keys (Key, K.Get (Container, Find'Result))); and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
package P is new Ada.Containers.Functional_Maps package P is new Ada.Containers.Functional_Maps
(Key_Type => Cursor, (Key_Type => Cursor,
...@@ -246,20 +246,21 @@ is ...@@ -246,20 +246,21 @@ is
-- It only contains keys contained in Model -- It only contains keys contained in Model
and (for all Key of Keys'Result => and (for all Key of Keys'Result =>
M.Has_Key (Model (Container), Key)) M.Has_Key (Model (Container), Key))
-- It contains all the keys contained in Model -- It contains all the keys contained in Model
and (for all Key of Model (Container) => and (for all Key of Model (Container) =>
(Find (Keys'Result, Key) > 0 (Find (Keys'Result, Key) > 0
and then Equivalent_Keys and then Equivalent_Keys
(K.Get (Keys'Result, Find (Keys'Result, Key)), Key))) (K.Get (Keys'Result, Find (Keys'Result, Key)),
Key)))
-- It is sorted in increasing order -- It is sorted in increasing order
and (for all I in 1 .. Length (Container) => and (for all I in 1 .. Length (Container) =>
Find (Keys'Result, K.Get (Keys'Result, I)) = I Find (Keys'Result, K.Get (Keys'Result, I)) = I
and K_Is_Find (Keys'Result, K.Get (Keys'Result, I), I)); and K_Is_Find (Keys'Result, K.Get (Keys'Result, I), I));
pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys); pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys);
function Positions (Container : Map) return P.Map with function Positions (Container : Map) return P.Map with
...@@ -284,7 +285,7 @@ is ...@@ -284,7 +285,7 @@ is
and then and then
(for all J of Positions'Result => (for all J of Positions'Result =>
(if P.Get (Positions'Result, I) = P.Get (Positions'Result, J) (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
then I = J))); then I = J)));
procedure Lift_Abstraction_Level (Container : Map) with procedure Lift_Abstraction_Level (Container : Map) with
-- Lift_Abstraction_Level is a ghost procedure that does nothing but -- Lift_Abstraction_Level is a ghost procedure that does nothing but
...@@ -942,7 +943,7 @@ is ...@@ -942,7 +943,7 @@ is
Contract_Cases => Contract_Cases =>
(Position = No_Element (Position = No_Element
or else P.Get (Positions (Container), Position) = 1 or else P.Get (Positions (Container), Position) = 1
=> =>
Position = No_Element, Position = No_Element,
others => others =>
...@@ -983,6 +984,7 @@ is ...@@ -983,6 +984,7 @@ is
Contract_Cases => Contract_Cases =>
(Length (Container) = 0 or else Key < First_Key (Container) => (Length (Container) = 0 or else Key < First_Key (Container) =>
Floor'Result = No_Element, Floor'Result = No_Element,
others => others =>
Has_Element (Container, Floor'Result) Has_Element (Container, Floor'Result)
and not (Key < K.Get (Keys (Container), and not (Key < K.Get (Keys (Container),
...@@ -999,9 +1001,9 @@ is ...@@ -999,9 +1001,9 @@ is
Ceiling'Result = No_Element, Ceiling'Result = No_Element,
others => others =>
Has_Element (Container, Ceiling'Result) Has_Element (Container, Ceiling'Result)
and and not (K.Get
not (K.Get (Keys (Container), (Keys (Container),
P.Get (Positions (Container), Ceiling'Result)) < Key) P.Get (Positions (Container), Ceiling'Result)) < Key)
and K_Is_Find and K_Is_Find
(Keys (Container), (Keys (Container),
Key, Key,
......
gcc/ada/a-cforse.adb
...@@ -608,6 +608,7 @@ is ...@@ -608,6 +608,7 @@ is
return False; return False;
end if; end if;
end loop; end loop;
return True; return True;
end E_Bigger_Than_Range; end E_Bigger_Than_Range;
...@@ -700,6 +701,7 @@ is ...@@ -700,6 +701,7 @@ is
end if; end if;
end loop; end loop;
end if; end if;
return True; return True;
end E_Is_Find; end E_Is_Find;
...@@ -719,6 +721,7 @@ is ...@@ -719,6 +721,7 @@ is
return False; return False;
end if; end if;
end loop; end loop;
return True; return True;
end E_Smaller_Than_Range; end E_Smaller_Than_Range;
...@@ -736,6 +739,7 @@ is ...@@ -736,6 +739,7 @@ is
return I; return I;
end if; end if;
end loop; end loop;
return 0; return 0;
end Find; end Find;
......
gcc/ada/a-cofuma.adb
...@@ -152,8 +152,11 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is ...@@ -152,8 +152,11 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
-- Has_Witness -- -- Has_Witness --
----------------- -----------------
function Has_Witness (Container : Map; Witness : Count_Type) return Boolean function Has_Witness
is (Witness in 1 .. Length (Container.Keys)); (Container : Map;
Witness : Count_Type) return Boolean
is
(Witness in 1 .. Length (Container.Keys));
-------------- --------------
-- Is_Empty -- -- Is_Empty --
...@@ -265,7 +268,9 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is ...@@ -265,7 +268,9 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
-- W_Get -- -- W_Get --
----------- -----------
function W_Get (Container : Map; Witness : Count_Type) return Element_Type function W_Get
(Container : Map;
Witness : Count_Type) return Element_Type
is is
(Get (Container.Elements, Witness)); (Get (Container.Elements, Witness));
......
gcc/ada/a-cofuma.ads
...@@ -35,9 +35,11 @@ private with Ada.Containers.Functional_Base; ...@@ -35,9 +35,11 @@ private with Ada.Containers.Functional_Base;
generic generic
type Key_Type (<>) is private; type Key_Type (<>) is private;
type Element_Type (<>) is private; type Element_Type (<>) is private;
with function Equivalent_Keys with function Equivalent_Keys
(Left : Key_Type; (Left : Key_Type;
Right : Key_Type) return Boolean is "="; Right : Key_Type) return Boolean is "=";
Enable_Handling_Of_Equivalence : Boolean := True; Enable_Handling_Of_Equivalence : Boolean := True;
-- This constant should only be set to False when no particular handling -- This constant should only be set to False when no particular handling
-- of equivalence over keys is needed, that is, Equivalent_Keys defines a -- of equivalence over keys is needed, that is, Equivalent_Keys defines a
...@@ -77,7 +79,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is ...@@ -77,7 +79,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
-- Has_Key returns the same result on all equivalent keys -- Has_Key returns the same result on all equivalent keys
(if (for some K of Container => Equivalent_Keys (K, Key)) then (if (for some K of Container => Equivalent_Keys (K, Key)) then
Has_Key'Result)); Has_Key'Result));
function Get (Container : Map; Key : Key_Type) return Element_Type with function Get (Container : Map; Key : Key_Type) return Element_Type with
-- Return the element associated with Key in Container -- Return the element associated with Key in Container
...@@ -90,8 +92,8 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is ...@@ -90,8 +92,8 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
-- Get returns the same result on all equivalent keys -- Get returns the same result on all equivalent keys
Get'Result = W_Get (Container, Witness (Container, Key)) Get'Result = W_Get (Container, Witness (Container, Key))
and (for all K of Container => and (for all K of Container =>
(Equivalent_Keys (K, Key) = (Equivalent_Keys (K, Key) =
(Witness (Container, Key) = Witness (Container, K))))); (Witness (Container, Key) = Witness (Container, K)))));
function Length (Container : Map) return Count_Type with function Length (Container : Map) return Count_Type with
......
gcc/ada/a-cofuse.ads
...@@ -34,9 +34,11 @@ private with Ada.Containers.Functional_Base; ...@@ -34,9 +34,11 @@ private with Ada.Containers.Functional_Base;
generic generic
type Element_Type (<>) is private; type Element_Type (<>) is private;
with function Equivalent_Elements with function Equivalent_Elements
(Left : Element_Type; (Left : Element_Type;
Right : Element_Type) return Boolean is "="; Right : Element_Type) return Boolean is "=";
Enable_Handling_Of_Equivalence : Boolean := True; Enable_Handling_Of_Equivalence : Boolean := True;
-- This constant should only be set to False when no particular handling -- This constant should only be set to False when no particular handling
-- of equivalence over elements is needed, that is, Equivalent_Elements -- of equivalence over elements is needed, that is, Equivalent_Elements
...@@ -75,7 +77,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -75,7 +77,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
-- Contains returns the same result on all equivalent elements -- Contains returns the same result on all equivalent elements
(if (for some E of Container => Equivalent_Elements (E, Item)) then (if (for some E of Container => Equivalent_Elements (E, Item)) then
Contains'Result)); Contains'Result));
function Length (Container : Set) return Count_Type with function Length (Container : Set) return Count_Type with
Global => null; Global => null;
...@@ -89,8 +91,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -89,8 +91,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
-- Set inclusion -- Set inclusion
Global => null, Global => null,
Post => "<="'Result = (for all Item of Left => Contains (Right, Item)) Post => "<="'Result = (for all Item of Left => Contains (Right, Item));
and (if "<="'Result then Length (Left) <= Length (Right));
function "=" (Left : Set; Right : Set) return Boolean with function "=" (Left : Set; Right : Set) return Boolean with
-- Extensional equality over sets -- Extensional equality over sets
...@@ -187,7 +188,12 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -187,7 +188,12 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
Global => null, Global => null,
Post => Post =>
Num_Overlaps'Result = Length (Intersection (Left, Right)); Num_Overlaps'Result = Length (Intersection (Left, Right))
and (if Left <= Right then Num_Overlaps'Result = Length (Left)
else Num_Overlaps'Result < Length (Left))
and (if Right <= Left then Num_Overlaps'Result = Length (Right)
else Num_Overlaps'Result < Length (Right))
and (Num_Overlaps'Result = 0) = No_Overlap (Left, Right);
---------------------------- ----------------------------
-- Construction Functions -- -- Construction Functions --
......
gcc/ada/exp_ch6.adb
...@@ -4798,7 +4798,7 @@ package body Exp_Ch6 is ...@@ -4798,7 +4798,7 @@ package body Exp_Ch6 is
Init_Assignment := Init_Assignment :=
Make_Assignment_Statement (Loc, Make_Assignment_Statement (Loc,
Name => New_Occurrence_Of (Ret_Obj_Id, Loc), Name => New_Occurrence_Of (Ret_Obj_Id, Loc),
Expression => Relocate_Node (Ret_Obj_Expr)); Expression => New_Copy_Tree (Ret_Obj_Expr));
Set_Etype (Name (Init_Assignment), Etype (Ret_Obj_Id)); Set_Etype (Name (Init_Assignment), Etype (Ret_Obj_Id));
Set_Assignment_OK (Name (Init_Assignment)); Set_Assignment_OK (Name (Init_Assignment));
......
gcc/ada/sem_util.adb
...@@ -17003,7 +17003,7 @@ package body Sem_Util is ...@@ -17003,7 +17003,7 @@ package body Sem_Util is
package NCT_Itype_Assoc is new Simple_HTable ( package NCT_Itype_Assoc is new Simple_HTable (
Header_Num => NCT_Header_Num, Header_Num => NCT_Header_Num,
Element => Entity_Id, Element => Node_Or_Entity_Id,
No_Element => Empty, No_Element => Empty,
Key => Entity_Id, Key => Entity_Id,
Hash => New_Copy_Hash, Hash => New_Copy_Hash,
...@@ -17114,37 +17114,45 @@ package body Sem_Util is ...@@ -17114,37 +17114,45 @@ package body Sem_Util is
--------------------------- ---------------------------
procedure Build_NCT_Hash_Tables is procedure Build_NCT_Hash_Tables is
Elmt : Elmt_Id; Assoc : Entity_Id;
Ent : Entity_Id; Elmt : Elmt_Id;
Key : Entity_Id;
Value : Entity_Id;
begin begin
if No (Map) then if No (Map) then
return; return;
end if; end if;
-- Clear both hash tables associated with entry replication since
-- multiple calls to New_Copy_Tree could cause multiple collisions
-- and produce long linked lists in individual buckets.
NCT_Assoc.Reset;
NCT_Itype_Assoc.Reset;
Elmt := First_Elmt (Map); Elmt := First_Elmt (Map);
while Present (Elmt) loop while Present (Elmt) loop
Ent := Node (Elmt);
-- Get new entity, and associate old and new -- Extract a (key, value) pair from the map
Key := Node (Elmt);
Next_Elmt (Elmt); Next_Elmt (Elmt);
NCT_Assoc.Set (Ent, Node (Elmt)); Value := Node (Elmt);
if Is_Type (Ent) then -- Add the pair in the association hash table
declare
Anode : constant Entity_Id :=
Associated_Node_For_Itype (Ent);
begin NCT_Assoc.Set (Key, Value);
-- Enter the link between the associated node of the old
-- Itype and the new Itype, for updating later when node
-- is copied.
if Present (Anode) then -- Add a link between the associated node of the old Itype and the
NCT_Itype_Assoc.Set (Anode, Node (Elmt)); -- new Itype, for updating later when node is copied.
end if;
end; if Is_Type (Key) then
Assoc := Associated_Node_For_Itype (Key);
if Present (Assoc) then
NCT_Itype_Assoc.Set (Assoc, Value);
end if;
end if; end if;
Next_Elmt (Elmt); Next_Elmt (Elmt);
...@@ -17540,23 +17548,29 @@ package body Sem_Util is ...@@ -17540,23 +17548,29 @@ package body Sem_Util is
pragma Assert (not Is_Itype (Old_Entity)); pragma Assert (not Is_Itype (Old_Entity));
pragma Assert (Nkind (Old_Entity) in N_Entity); pragma Assert (Nkind (Old_Entity) in N_Entity);
-- Restrict entity creation to declarations of constants, variables -- Do not duplicate an entity when it is declared within an inner
-- and subtypes. There is no need to duplicate entities declared in -- scope enclosed by an expression with actions.
-- inner scopes.
if (not Ekind_In (Old_Entity, E_Constant, E_Variable) if EWA_Inner_Scope_Level > 0 then
and then Nkind (Parent (Old_Entity)) /= N_Subtype_Declaration) return;
or else EWA_Inner_Scope_Level > 0
then -- Entity duplication is currently performed only for objects and
-- types. Relaxing this restriction leads to a performance penalty.
elsif Ekind_In (Old_Entity, E_Constant, E_Variable) then
null;
elsif Is_Type (Old_Entity) then
null;
else
return; return;
end if; end if;
New_E := New_Copy (Old_Entity); New_E := New_Copy (Old_Entity);
-- The new entity has all the attributes of the old one, and we -- The new entity has all the attributes of the old one, however it
-- just copy the contents of the entity. However, the back-end -- requires a new name for debugging purposes.
-- needs different names for debugging purposes, so we create a
-- new internal name for it in all cases.
Set_Chars (New_E, New_Internal_Name ('T')); Set_Chars (New_E, New_Internal_Name ('T'));
...@@ -17830,8 +17844,8 @@ package body Sem_Util is ...@@ -17830,8 +17844,8 @@ package body Sem_Util is
while Present (New_E) loop while Present (New_E) loop
-- Skip entities that were not created in the first phase -- Skip entities that were not created in the first phase
-- (that is, old entities specified by the caller in the -- (that is, old entities specified by the caller in the set of
-- set of mappings to be applied to the tree). -- mappings to be applied to the tree).
if Is_Itype (New_E) if Is_Itype (New_E)
or else No (Map) or else No (Map)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment