+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,
Post =>
M_Elements_Sorted'Result =
(for all I in 1 .. M.Length (Container) =>
- (for all J in I .. M.Length (Container) =>
- Element (Container, I) = Element (Container, J)
- or Element (Container, I) < Element (Container, J)));
+ (for all J in I .. M.Length (Container) =>
+ Element (Container, I) = Element (Container, J)
+ or Element (Container, I) < Element (Container, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
end Formal_Model;
-- Find --
----------
- function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
+ function Find
+ (Container : K.Sequence;
+ Key : Key_Type) return Count_Type
is
begin
for I in 1 .. K.Length (Container) loop
-- K_Keys_Included --
---------------------
- function K_Keys_Included (Left : K.Sequence;
- Right : K.Sequence) return Boolean
+ function K_Keys_Included
+ (Left : K.Sequence;
+ Right : K.Sequence) return Boolean
is
begin
for I in 1 .. K.Length (Left) loop
Global => null,
Post =>
(if Find'Result > 0 then
- Find'Result <= K.Length (Container)
- and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
+ Find'Result <= K.Length (Container)
+ and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
function K_Keys_Included
(Left : K.Sequence;
Post =>
K_Keys_Included'Result =
(for all I in 1 .. K.Length (Left) =>
- Find (Right, K.Get (Left, I)) > 0
- and then K.Get (Right, Find (Right, K.Get (Left, I))) =
- K.Get (Left, I));
+ Find (Right, K.Get (Left, I)) > 0
+ and then K.Get (Right, Find (Right, K.Get (Left, I))) =
+ K.Get (Left, I));
package P is new Ada.Containers.Functional_Maps
(Key_Type => Cursor,
-- It only contains keys contained in Model
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
and (for all Key of Model (Container) =>
(Find (Keys'Result, Key) > 0
- and then Equivalent_Keys
- (K.Get (Keys'Result, Find (Keys'Result, Key)), Key)))
+ and then Equivalent_Keys
+ (K.Get (Keys'Result, Find (Keys'Result, Key)),
+ Key)))
-- It has no duplicate
(for all J in 1 .. Length (Container) =>
(if Equivalent_Keys
(K.Get (Keys'Result, I), K.Get (Keys'Result, J))
- then I = J)));
+ then
+ I = J)));
pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys);
function Positions (Container : Map) return P.Map with
and then
(for all J of Positions'Result =>
(if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
- then I = J)));
+ then I = J)));
procedure Lift_Abstraction_Level (Container : Map) with
-- Lift_Abstraction_Level is a ghost procedure that does nothing but
-- Key is inserted in Container
- and K.Get (Keys (Container),
- P.Get (Positions (Container), Find (Container, Key))) =
- Key
+ and K.Get
+ (Keys (Container),
+ P.Get (Positions (Container), Find (Container, Key))) = Key
-- Mapping from cursors to keys is preserved
package body Ada.Containers.Formal_Hashed_Sets with
SPARK_Mode => Off
is
-
-----------------------
-- Local Subprograms --
-----------------------
-- All need comments ???
- procedure Difference
- (Left, Right : Set;
- Target : in out Set);
+ procedure Difference (Left : Set; Right : Set; Target : in out Set);
function Equivalent_Keys
(Key : Element_Type;
pragma Inline (Hash_Node);
procedure Insert
- (Container : in out Set;
- New_Item : Element_Type;
- Node : out Count_Type;
- Inserted : out Boolean);
+ (Container : in out Set;
+ New_Item : Element_Type;
+ Node : out Count_Type;
+ Inserted : out Boolean);
procedure Intersection
(Left : Set;
begin
Node := First (Left).Node;
while Node /= 0 loop
- ENode := Find (Container => Right,
- Item => Left.Nodes (Node).Element).Node;
- if ENode = 0 or else
- Right.Nodes (ENode).Element /= Left.Nodes (Node).Element
+ ENode :=
+ Find
+ (Container => Right,
+ Item => Left.Nodes (Node).Element).Node;
+
+ if ENode = 0
+ or else Right.Nodes (ENode).Element /= Left.Nodes (Node).Element
then
return False;
end if;
end loop;
return True;
-
end;
-
end "=";
------------
Capacity : Count_Type := 0) return Set
is
C : constant Count_Type :=
- Count_Type'Max (Capacity, Source.Capacity);
+ Count_Type'Max (Capacity, Source.Capacity);
+ Cu : Cursor;
H : Hash_Type;
N : Count_Type;
Target : Set (C, Source.Modulus);
- Cu : Cursor;
begin
if 0 < Capacity and then Capacity < Source.Capacity then
-- Delete --
------------
- procedure Delete
- (Container : in out Set;
- Item : Element_Type)
- is
+ procedure Delete (Container : in out Set; Item : Element_Type) is
X : Count_Type;
begin
Free (Container, X);
end Delete;
- procedure Delete
- (Container : in out Set;
- Position : in out Cursor)
- is
+ procedure Delete (Container : in out Set; Position : in out Cursor) is
begin
if not Has_Element (Container, Position) then
raise Constraint_Error with "Position cursor has no element";
-- Difference --
----------------
- procedure Difference
- (Target : in out Set;
- Source : Set)
- is
- Tgt_Node, Src_Node, Src_Last, Src_Length : Count_Type;
+ procedure Difference (Target : in out Set; Source : Set) is
+ Src_Last : Count_Type;
+ Src_Length : Count_Type;
+ Src_Node : Count_Type;
+ Tgt_Node : Count_Type;
TN : Nodes_Type renames Target.Nodes;
SN : Nodes_Type renames Source.Nodes;
end loop;
end Difference;
- procedure Difference
- (Left, Right : Set;
- Target : in out Set)
- is
+ procedure Difference (Left : Set; Right : Set; Target : in out Set) is
procedure Process (L_Node : Count_Type);
procedure Iterate is
-------------
procedure Process (L_Node : Count_Type) is
+ B : Boolean;
E : Element_Type renames Left.Nodes (L_Node).Element;
X : Count_Type;
- B : Boolean;
+
begin
if Find (Right, E).Node = 0 then
Insert (Target, E, X, B);
Iterate (Left);
end Difference;
- function Difference (Left, Right : Set) return Set is
+ function Difference (Left : Set; Right : Set) return Set is
C : Count_Type;
H : Hash_Type;
raise Constraint_Error with "Position cursor equals No_Element";
end if;
- pragma Assert (Vet (Container, Position),
- "bad cursor in function Element");
+ pragma Assert
+ (Vet (Container, Position), "bad cursor in function Element");
return Container.Nodes (Position.Node).Element;
end Element;
L_Node : Node_Type) return Boolean
is
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);
RN : Nodes_Type renames R_HT.Nodes;
-- Exclude --
-------------
- procedure Exclude
- (Container : in out Set;
- Item : Element_Type)
- is
+ procedure Exclude (Container : in out Set; Item : Element_Type) is
X : Count_Type;
begin
Element_Keys.Delete_Key_Sans_Free (Container, Item, X);
-- Free --
----------
- procedure Free
- (HT : in out Set;
- X : Count_Type)
- is
+ procedure Free (HT : in out Set; X : Count_Type) is
begin
HT.Nodes (X).Has_Element := False;
HT_Ops.Free (HT, X);
-- Generic_Allocate --
----------------------
- procedure Generic_Allocate
- (HT : in out Set;
- Node : out Count_Type)
- is
+ procedure Generic_Allocate (HT : in out Set; Node : out Count_Type) is
procedure Allocate is new HT_Ops.Generic_Allocate (Set_Element);
begin
Allocate (HT, Node);
-- Local Instantiations --
--------------------------
- package Key_Keys is
- new Hash_Tables.Generic_Bounded_Keys
- (HT_Types => HT_Types,
- Next => Next,
- Set_Next => Set_Next,
- Key_Type => Key_Type,
- Hash => Hash,
- Equivalent_Keys => Equivalent_Key_Node);
+ package Key_Keys is new Hash_Tables.Generic_Bounded_Keys
+ (HT_Types => HT_Types,
+ Next => Next,
+ Set_Next => Set_Next,
+ Key_Type => Key_Type,
+ Hash => Hash,
+ Equivalent_Keys => Equivalent_Key_Node);
--------------
-- Contains --
-- Delete --
------------
- procedure Delete
- (Container : in out Set;
- Key : Key_Type)
- is
+ procedure Delete (Container : in out Set; Key : Key_Type) is
X : Count_Type;
begin
-- Exclude --
-------------
- procedure Exclude
- (Container : in out Set;
- Key : Key_Type)
- is
+ procedure Exclude (Container : in out Set; Key : Key_Type) is
X : Count_Type;
begin
Key_Keys.Delete_Key_Sans_Free (Container, Key, X);
return False;
end if;
end loop;
+
return True;
end M_Included_Except;
function Key (Container : Set; Position : Cursor) return Key_Type is
begin
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";
end if;
pragma Assert
begin
if Node = 0 then
- raise Constraint_Error with
- "attempt to replace key not in set";
+ raise Constraint_Error with "attempt to replace key not in set";
end if;
Replace_Element (Container, Node, New_Item);
-- Include --
-------------
- procedure Include
- (Container : in out Set;
- New_Item : Element_Type)
- is
- Position : Cursor;
+ procedure Include (Container : in out Set; New_Item : Element_Type) is
Inserted : Boolean;
+ Position : Cursor;
begin
Insert (Container, New_Item, Position, Inserted);
Insert (Container, New_Item, Position.Node, Inserted);
end Insert;
- procedure Insert
- (Container : in out Set;
- New_Item : Element_Type)
- is
- Position : Cursor;
+ procedure Insert (Container : in out Set; New_Item : Element_Type) is
Inserted : Boolean;
+ Position : Cursor;
begin
Insert (Container, New_Item, Position, Inserted);
-- Intersection --
------------------
- procedure Intersection
- (Target : in out Set;
- Source : Set)
- is
+ procedure Intersection (Target : in out Set; Source : Set) is
Tgt_Node : Count_Type;
TN : Nodes_Type renames Target.Nodes;
end loop;
end Intersection;
- procedure Intersection
- (Left : Set;
- Right : Set;
- Target : in out Set)
- is
+ procedure Intersection (Left : Set; Right : Set; Target : in out Set) is
procedure Process (L_Node : Count_Type);
procedure Iterate is
Iterate (Left);
end Intersection;
- function Intersection (Left, Right : Set) return Set is
+ function Intersection (Left : Set; Right : Set) return Set is
C : Count_Type;
H : Hash_Type;
return S : Set (C, H) do
if Length (Left) /= 0 and Length (Right) /= 0 then
- Intersection (Left, Right, Target => S);
+ Intersection (Left, Right, Target => S);
end if;
end return;
end Intersection;
end if;
if not Has_Element (Container, Position) then
- raise Constraint_Error
- with "Position has no element";
+ raise Constraint_Error with "Position has no element";
end if;
pragma Assert (Vet (Container, Position), "bad cursor in Next");
-- Replace --
-------------
- procedure Replace
- (Container : in out Set;
- New_Item : Element_Type)
- is
+ procedure Replace (Container : in out Set; New_Item : Element_Type) is
Node : constant Count_Type := Element_Keys.Find (Container, New_Item);
begin
if Node = 0 then
- raise Constraint_Error with
- "attempt to replace element not in set";
+ raise Constraint_Error with "attempt to replace element not in set";
end if;
Container.Nodes (Node).Element := New_Item;
is
begin
if not Has_Element (Container, Position) then
- raise Constraint_Error with
- "Position cursor equals No_Element";
+ raise Constraint_Error with "Position cursor equals No_Element";
end if;
- pragma Assert (Vet (Container, Position),
- "bad cursor in Replace_Element");
+ pragma Assert
+ (Vet (Container, Position), "bad cursor in Replace_Element");
Replace_Element (Container, Position.Node, New_Item);
end Replace_Element;
-- Symmetric_Difference --
--------------------------
- procedure Symmetric_Difference
- (Target : in out Set;
- Source : Set)
- is
+ procedure Symmetric_Difference (Target : in out Set; Source : Set) is
procedure Process (Source_Node : Count_Type);
pragma Inline (Process);
-------------
procedure Process (Source_Node : Count_Type) is
+ B : Boolean;
N : Node_Type renames Source.Nodes (Source_Node);
X : Count_Type;
- B : Boolean;
+
begin
if Is_In (Target, N) then
Delete (Target, N.Element);
Iterate (Source);
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;
H : Hash_Type;
-- Union --
-----------
- procedure Union
- (Target : in out Set;
- Source : Set)
- is
+ procedure Union (Target : in out Set; Source : Set) is
procedure Process (Src_Node : Count_Type);
procedure Iterate is
Insert (Target, E, X, B);
end Process;
- -- Start of processing for Union
+ -- Start of processing for Union
begin
if Target'Address = Source'Address then
Iterate (Source);
end Union;
- function Union (Left, Right : Set) return Set is
+ function Union (Left : Set; Right : Set) return Set is
C : Count_Type;
H : Hash_Type;
with function Hash (Element : Element_Type) return Hash_Type;
- with function Equivalent_Elements (Left, Right : Element_Type)
- return Boolean is "=";
+ with function Equivalent_Elements
+ (Left : Element_Type;
+ Right : Element_Type) return Boolean is "=";
+
package Ada.Containers.Formal_Hashed_Sets with
SPARK_Mode
is
Global => null,
Post =>
(if Find'Result > 0 then
- Find'Result <= E.Length (Container)
- and Equivalent_Elements (Item, E.Get (Container, Find'Result)));
+ Find'Result <= E.Length (Container)
+ and Equivalent_Elements
+ (Item, E.Get (Container, Find'Result)));
function E_Elements_Included
(Left : E.Sequence;
Post =>
E_Elements_Included'Result =
(for all I in 1 .. E.Length (Left) =>
- Find (Right, E.Get (Left, I)) > 0
- and then E.Get (Right, Find (Right, E.Get (Left, I))) =
- E.Get (Left, I));
+ Find (Right, E.Get (Left, I)) > 0
+ and then E.Get (Right, Find (Right, E.Get (Left, I))) =
+ E.Get (Left, I));
pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
function E_Elements_Included
E_Elements_Included'Result =
(for all I in 1 .. E.Length (Left) =>
(if M.Contains (Model, E.Get (Left, I)) then
- Find (Right, E.Get (Left, I)) > 0
- and then E.Get (Right, Find (Right, E.Get (Left, I))) =
- E.Get (Left, I)));
+ Find (Right, E.Get (Left, I)) > 0
+ and then E.Get (Right, Find (Right, E.Get (Left, I))) =
+ E.Get (Left, I)));
pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
function E_Elements_Included
E_Elements_Included'Result =
(for all I in 1 .. E.Length (Container) =>
(if M.Contains (Model, E.Get (Container, I)) then
- Find (Left, E.Get (Container, I)) > 0
- and then E.Get (Left, Find (Left, E.Get (Container, I))) =
- E.Get (Container, I)
+ Find (Left, E.Get (Container, I)) > 0
+ and then E.Get (Left, Find (Left, E.Get (Container, I))) =
+ E.Get (Container, I)
else
- Find (Right, E.Get (Container, I)) > 0
- and then E.Get (Right, Find (Right, E.Get (Container, I))) =
- E.Get (Container, I)));
+ Find (Right, E.Get (Container, I)) > 0
+ and then E.Get
+ (Right, Find (Right, E.Get (Container, I))) =
+ E.Get (Container, I)));
pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
package P is new Ada.Containers.Functional_Maps
and (for all C of P_Left =>
(if C /= Position then
- E.Get (E_Left, P.Get (P_Left, C)) =
- E.Get (E_Right, P.Get (P_Right, C)))));
+ E.Get (E_Left, P.Get (P_Left, C)) =
+ E.Get (E_Right, P.Get (P_Right, C)))));
function Model (Container : Set) return M.Set with
-- The high-level model of a set is a set of elements. Neither cursors
-- It only contains keys contained in Model
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
and (for all Item of Model (Container) =>
(Find (Elements'Result, Item) > 0
- and then Equivalent_Elements
- (E.Get (Elements'Result, Find (Elements'Result, Item)),
- Item)))
+ and then Equivalent_Elements
+ (E.Get (Elements'Result,
+ Find (Elements'Result, Item)),
+ Item)))
-- It has no duplicate
and then
(for all J of Positions'Result =>
(if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
- then I = J)));
+ then I = J)));
procedure Lift_Abstraction_Level (Container : Set) with
-- Lift_Abstraction_Level is a ghost procedure that does nothing but
function "=" (Left, Right : Set) return Boolean with
Global => null,
Post =>
- "="'Result =
- (Length (Left) = Length (Right)
- and E_Elements_Included (Elements (Left), Elements (Right)))
+ "="'Result =
+ (Length (Left) = Length (Right)
+ and E_Elements_Included (Elements (Left), Elements (Right)))
and
"="'Result =
(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
Global => null,
-- Actual elements are preserved
- and
- E_Elements_Included
- (Elements (Container), Elements (Container)'Old)
- and
- E_Elements_Included
- (Elements (Container)'Old, Elements (Container));
+ and E_Elements_Included
+ (Elements (Container), Elements (Container)'Old)
+ and E_Elements_Included
+ (Elements (Container)'Old, Elements (Container));
function Is_Empty (Container : Set) return Boolean with
Global => null,
-- Actual elements are preserved
- and
- E_Elements_Included (Elements (Target), Elements (Source))
- and
- E_Elements_Included (Elements (Source), Elements (Target));
+ and E_Elements_Included (Elements (Target), Elements (Source))
+ and E_Elements_Included (Elements (Source), Elements (Target));
function Copy
(Source : Set;
-- Actual elements are preserved
- and
- E_Elements_Included (Elements (Target), Elements (Source)'Old)
- and
- E_Elements_Included (Elements (Source)'Old, Elements (Target));
+ and E_Elements_Included (Elements (Target), Elements (Source)'Old)
+ and E_Elements_Included (Elements (Source)'Old, Elements (Target));
procedure Insert
(Container : in out Set;
-- Elements of Target come from either Source or Target
- and
- M.Included_In_Union
- (Model (Target), Model (Source), Model (Target)'Old)
+ and M.Included_In_Union
+ (Model (Target), Model (Source), Model (Target)'Old)
-- Actual value of elements come from either Left or Right
- and
- E_Elements_Included
- (Elements (Target),
- Model (Target)'Old,
- Elements (Target)'Old,
- Elements (Source))
- and
- E_Elements_Included
- (Elements (Target)'Old, Model (Target)'Old, Elements (Target))
- and
- E_Elements_Included
- (Elements (Source),
- Model (Target)'Old,
- Elements (Source),
- Elements (Target))
+ and E_Elements_Included
+ (Elements (Target),
+ Model (Target)'Old,
+ Elements (Target)'Old,
+ Elements (Source))
+
+ and E_Elements_Included
+ (Elements (Target)'Old, Model (Target)'Old, Elements (Target))
+
+ and E_Elements_Included
+ (Elements (Source),
+ Model (Target)'Old,
+ Elements (Source),
+ Elements (Target))
-- Mapping from cursors of Target to elements is preserved
-- Actual value of elements come from either Left or Right
- and
- E_Elements_Included
- (Elements (Union'Result),
- Model (Left),
- Elements (Left),
- Elements (Right))
- and
- E_Elements_Included
- (Elements (Left), Model (Left), Elements (Union'Result))
- and
- E_Elements_Included
- (Elements (Right),
- Model (Left),
- Elements (Right),
- Elements (Union'Result));
+ and E_Elements_Included
+ (Elements (Union'Result),
+ Model (Left),
+ Elements (Left),
+ Elements (Right))
+
+ and E_Elements_Included
+ (Elements (Left), Model (Left), Elements (Union'Result))
+
+ and E_Elements_Included
+ (Elements (Right),
+ Model (Left),
+ Elements (Right),
+ Elements (Union'Result));
function "or" (Left, Right : Set) return Set renames Union;
-- Elements both in Source and Target are in the intersection
- and
- M.Includes_Intersection
- (Model (Target), Model (Source), Model (Target)'Old)
+ and M.Includes_Intersection
+ (Model (Target), Model (Source), Model (Target)'Old)
-- Actual value of elements of Target is preserved
and E_Elements_Included (Elements (Target), Elements (Target)'Old)
- and
- E_Elements_Included
- (Elements (Target)'Old, Model (Source), Elements (Target))
+ and E_Elements_Included
+ (Elements (Target)'Old, Model (Source), Elements (Target))
-- Mapping from cursors of Target to elements is preserved
-- Elements both in Left and Right are in the result of Intersection
- and
- M.Includes_Intersection
- (Model (Intersection'Result), Model (Left), Model (Right))
+ and M.Includes_Intersection
+ (Model (Intersection'Result), Model (Left), Model (Right))
-- Actual value of elements come from Left
- and
- E_Elements_Included
- (Elements (Intersection'Result), Elements (Left))
- and
- E_Elements_Included
- (Elements (Left), Model (Right), Elements (Intersection'Result));
+ and E_Elements_Included
+ (Elements (Intersection'Result), Elements (Left))
+
+ and E_Elements_Included
+ (Elements (Left), Model (Right),
+ Elements (Intersection'Result));
function "and" (Left, Right : Set) return Set renames Intersection;
-- Elements in Target but not in Source are in the difference
- and
- M.Included_In_Union
- (Model (Target)'Old, Model (Target), Model (Source))
+ and M.Included_In_Union
+ (Model (Target)'Old, Model (Target), Model (Source))
-- Actual value of elements of Target is preserved
and E_Elements_Included (Elements (Target), Elements (Target)'Old)
- and
- E_Elements_Included
- (Elements (Target)'Old, Model (Target), Elements (Target))
+ and E_Elements_Included
+ (Elements (Target)'Old, Model (Target), Elements (Target))
-- Mapping from cursors of Target to elements is preserved
-- Elements in Left but not in Right are in the difference
- and
- M.Included_In_Union
- (Model (Left), Model (Difference'Result), Model (Right))
+ and M.Included_In_Union
+ (Model (Left), Model (Difference'Result), Model (Right))
-- Actual value of elements come from Left
- and
- E_Elements_Included (Elements (Difference'Result), Elements (Left))
- and
- E_Elements_Included
- (Elements (Left),
- Model (Difference'Result),
- Elements (Difference'Result));
+ and E_Elements_Included
+ (Elements (Difference'Result), Elements (Left))
+
+ and E_Elements_Included
+ (Elements (Left),
+ Model (Difference'Result),
+ Elements (Difference'Result));
function "-" (Left, Right : Set) return Set renames Difference;
-- Elements in Target but not in Source are in the difference
- and
- M.Included_In_Union
- (Model (Target)'Old, Model (Target), Model (Source))
+ and M.Included_In_Union
+ (Model (Target)'Old, Model (Target), Model (Source))
-- Elements in Source but not in Target are in the difference
- and
- M.Included_In_Union
- (Model (Source), Model (Target), Model (Target)'Old)
+ and M.Included_In_Union
+ (Model (Source), Model (Target), Model (Target)'Old)
-- Actual value of elements come from either Left or Right
- and
- E_Elements_Included
- (Elements (Target),
- Model (Target)'Old,
- Elements (Target)'Old,
- Elements (Source))
- and
- E_Elements_Included
- (Elements (Target)'Old, Model (Target), Elements (Target))
- and
- E_Elements_Included
- (Elements (Source), Model (Target), Elements (Target));
+ and E_Elements_Included
+ (Elements (Target),
+ Model (Target)'Old,
+ Elements (Target)'Old,
+ Elements (Source))
+
+ and E_Elements_Included
+ (Elements (Target)'Old, Model (Target), Elements (Target))
+
+ and E_Elements_Included
+ (Elements (Source), Model (Target), Elements (Target));
function Symmetric_Difference (Left, Right : Set) return Set with
Global => null,
-- Elements of the difference were not both in Left and Right
- and
- M.Not_In_Both
- (Model (Symmetric_Difference'Result), Model (Left), Model (Right))
+ and M.Not_In_Both
+ (Model (Symmetric_Difference'Result),
+ Model (Left),
+ Model (Right))
-- Elements in Left but not in Right are in the difference
- and
- M.Included_In_Union
- (Model (Left), Model (Symmetric_Difference'Result), Model (Right))
+ and M.Included_In_Union
+ (Model (Left),
+ Model (Symmetric_Difference'Result),
+ Model (Right))
-- Elements in Right but not in Left are in the difference
- and
- M.Included_In_Union
- (Model (Right), Model (Symmetric_Difference'Result), Model (Left))
+ and M.Included_In_Union
+ (Model (Right),
+ Model (Symmetric_Difference'Result),
+ Model (Left))
-- Actual value of elements come from either Left or Right
- and
- E_Elements_Included
- (Elements (Symmetric_Difference'Result),
- Model (Left),
- Elements (Left),
- Elements (Right))
- and
- E_Elements_Included
- (Elements (Left),
- Model (Symmetric_Difference'Result),
- Elements (Symmetric_Difference'Result))
- and
- E_Elements_Included
- (Elements (Right),
- Model (Symmetric_Difference'Result),
- Elements (Symmetric_Difference'Result));
+ and E_Elements_Included
+ (Elements (Symmetric_Difference'Result),
+ Model (Left),
+ Elements (Left),
+ Elements (Right))
+
+ and E_Elements_Included
+ (Elements (Left),
+ Model (Symmetric_Difference'Result),
+ Elements (Symmetric_Difference'Result))
+
+ and E_Elements_Included
+ (Elements (Right),
+ Model (Symmetric_Difference'Result),
+ Elements (Symmetric_Difference'Result));
function "xor" (Left, Right : Set) return Set
renames Symmetric_Difference;
Post =>
M_Included_Except'Result =
(for all E of Left =>
- Contains (Right, E)
- or Equivalent_Keys (Generic_Keys.Key (E), Key));
+ Contains (Right, E)
+ or Equivalent_Keys (Generic_Keys.Key (E), Key));
end Formal_Model;
use Formal_Model;
-- The key designated by the result of Find is Key
- and
- Equivalent_Keys
- (Generic_Keys.Key (Container, Find'Result), Key));
+ and Equivalent_Keys
+ (Generic_Keys.Key (Container, Find'Result), Key));
function Contains (Container : Set; Key : Key_Type) return Boolean with
Global => null,
Post =>
Contains'Result =
(for some E of Model (Container) =>
- Equivalent_Keys (Key, Generic_Keys.Key (E)));
+ Equivalent_Keys (Key, Generic_Keys.Key (E)));
end Generic_Keys;
function "<" (Left : Holder; Right : Holder) return Boolean is
(E (Left) < E (Right));
- procedure Sort is
- new Generic_Array_Sort
- (Index_Type => Array_Index,
- Element_Type => Holder,
- Array_Type => Elements_Array,
- "<" => "<");
+ procedure Sort is new Generic_Array_Sort
+ (Index_Type => Array_Index,
+ Element_Type => Holder,
+ Array_Type => Elements_Array,
+ "<" => "<");
Len : constant Capacity_Range := Length (Container);
then
Reserve_Capacity
(Container,
- Capacity_Range'Max (Current_Capacity (Container) * Growth_Factor,
- Capacity_Range (New_Length)));
+ Capacity_Range'Max
+ (Current_Capacity (Container) * Growth_Factor,
+ Capacity_Range (New_Length)));
end if;
declare
-- hence we also know that
-- Index - Index_Type'First >= 0
- -- The issue is that even though 0 is guaranteed to be a value in
- -- the type Index_Type'Base, there's no guarantee that the difference
- -- is a value in that type. To prevent overflow we use the wider
- -- of Count_Type'Base and Index_Type'Base to perform intermediate
+ -- The issue is that even though 0 is guaranteed to be a value in the
+ -- type Index_Type'Base, there's no guarantee that the difference is a
+ -- value in that type. To prevent overflow we use the wider of
+ -- Count_Type'Base and Index_Type'Base to perform intermediate
-- calculations.
if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
Count_Type'Base (Index_Type'First);
end if;
- -- The array index subtype for all container element arrays
- -- always starts with 1.
+ -- The array index subtype for all container element arrays always
+ -- starts with 1.
return 1 + Offset;
end To_Array_Index;
Post =>
M_Elements_Sorted'Result =
(for all I in Index_Type'First .. M.Last (Container) =>
- (for all J in I .. M.Last (Container) =>
- Element (Container, I) = Element (Container, J)
- or Element (Container, I) < Element (Container, J)));
+ (for all J in I .. M.Last (Container) =>
+ Element (Container, I) = Element (Container, J)
+ or Element (Container, I) < Element (Container, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
end Formal_Model;
-- Find --
----------
- function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
+ function Find
+ (Container : K.Sequence;
+ Key : Key_Type) return Count_Type
is
begin
for I in 1 .. K.Length (Container) loop
-- for their postconditions.
while Position /= 0 loop
- R := M.Add (Container => R,
- New_Key => Container.Nodes (Position).Key,
- New_Item => Container.Nodes (Position).Element);
+ R :=
+ M.Add
+ (Container => R,
+ New_Key => Container.Nodes (Position).Key,
+ New_Item => Container.Nodes (Position).Element);
+
Position := Tree_Operations.Next (Container, Position);
end loop;
Pre => Position - 1 <= K.Length (Container),
Post =>
K_Is_Find'Result =
+ ((if Position > 0 then
+ K_Bigger_Than_Range (Container, 1, Position - 1, Key))
- ((if Position > 0 then
- K_Bigger_Than_Range (Container, 1, Position - 1, Key))
-
- and (if Position < K.Length (Container) then
- K_Smaller_Than_Range
- (Container,
- Position + 1,
- K.Length (Container),
- Key)));
+ and
+ (if Position < K.Length (Container) then
+ K_Smaller_Than_Range
+ (Container,
+ Position + 1,
+ K.Length (Container),
+ Key)));
pragma Annotate (GNATprove, Inline_For_Proof, K_Is_Find);
function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
Global => null,
Post =>
(if Find'Result > 0 then
- Find'Result <= K.Length (Container)
- and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
+ Find'Result <= K.Length (Container)
+ and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
package P is new Ada.Containers.Functional_Maps
(Key_Type => Cursor,
-- It only contains keys contained in Model
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
and (for all Key of Model (Container) =>
(Find (Keys'Result, Key) > 0
- and then Equivalent_Keys
- (K.Get (Keys'Result, Find (Keys'Result, Key)), Key)))
+ and then Equivalent_Keys
+ (K.Get (Keys'Result, Find (Keys'Result, Key)),
+ Key)))
-- It is sorted in increasing order
and (for all I in 1 .. Length (Container) =>
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);
function Positions (Container : Map) return P.Map with
and then
(for all J of Positions'Result =>
(if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
- then I = J)));
+ then I = J)));
procedure Lift_Abstraction_Level (Container : Map) with
-- Lift_Abstraction_Level is a ghost procedure that does nothing but
Contract_Cases =>
(Position = No_Element
or else P.Get (Positions (Container), Position) = 1
- =>
+ =>
Position = No_Element,
others =>
Contract_Cases =>
(Length (Container) = 0 or else Key < First_Key (Container) =>
Floor'Result = No_Element,
+
others =>
Has_Element (Container, Floor'Result)
and not (Key < K.Get (Keys (Container),
Ceiling'Result = No_Element,
others =>
Has_Element (Container, Ceiling'Result)
- and
- not (K.Get (Keys (Container),
- P.Get (Positions (Container), Ceiling'Result)) < Key)
+ and not (K.Get
+ (Keys (Container),
+ P.Get (Positions (Container), Ceiling'Result)) < Key)
and K_Is_Find
(Keys (Container),
Key,
return False;
end if;
end loop;
+
return True;
end E_Bigger_Than_Range;
end if;
end loop;
end if;
+
return True;
end E_Is_Find;
return False;
end if;
end loop;
+
return True;
end E_Smaller_Than_Range;
return I;
end if;
end loop;
+
return 0;
end Find;
-- Has_Witness --
-----------------
- function Has_Witness (Container : Map; Witness : Count_Type) return Boolean
- is (Witness in 1 .. Length (Container.Keys));
+ function Has_Witness
+ (Container : Map;
+ Witness : Count_Type) return Boolean
+ is
+ (Witness in 1 .. Length (Container.Keys));
--------------
-- Is_Empty --
-- 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
(Get (Container.Elements, Witness));
generic
type Key_Type (<>) is private;
type Element_Type (<>) is private;
+
with function Equivalent_Keys
(Left : Key_Type;
Right : Key_Type) return Boolean is "=";
+
Enable_Handling_Of_Equivalence : Boolean := True;
-- This constant should only be set to False when no particular handling
-- of equivalence over keys is needed, that is, Equivalent_Keys defines a
-- Has_Key returns the same result on all equivalent keys
(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
-- Return the element associated with Key in Container
-- Get returns the same result on all equivalent keys
Get'Result = W_Get (Container, Witness (Container, Key))
- and (for all K of Container =>
- (Equivalent_Keys (K, Key) =
+ and (for all K of Container =>
+ (Equivalent_Keys (K, Key) =
(Witness (Container, Key) = Witness (Container, K)))));
function Length (Container : Map) return Count_Type with
generic
type Element_Type (<>) is private;
+
with function Equivalent_Elements
(Left : Element_Type;
Right : Element_Type) return Boolean is "=";
+
Enable_Handling_Of_Equivalence : Boolean := True;
-- This constant should only be set to False when no particular handling
-- of equivalence over elements is needed, that is, Equivalent_Elements
-- Contains returns the same result on all equivalent elements
(if (for some E of Container => Equivalent_Elements (E, Item)) then
- Contains'Result));
+ Contains'Result));
function Length (Container : Set) return Count_Type with
Global => null;
-- Set inclusion
Global => null,
- Post => "<="'Result = (for all Item of Left => Contains (Right, Item))
- and (if "<="'Result then Length (Left) <= Length (Right));
+ Post => "<="'Result = (for all Item of Left => Contains (Right, Item));
function "=" (Left : Set; Right : Set) return Boolean with
-- Extensional equality over sets
Global => null,
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 --
Init_Assignment :=
Make_Assignment_Statement (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_Assignment_OK (Name (Init_Assignment));
package NCT_Itype_Assoc is new Simple_HTable (
Header_Num => NCT_Header_Num,
- Element => Entity_Id,
+ Element => Node_Or_Entity_Id,
No_Element => Empty,
Key => Entity_Id,
Hash => New_Copy_Hash,
---------------------------
procedure Build_NCT_Hash_Tables is
- Elmt : Elmt_Id;
- Ent : Entity_Id;
+ Assoc : Entity_Id;
+ Elmt : Elmt_Id;
+ Key : Entity_Id;
+ Value : Entity_Id;
begin
if No (Map) then
return;
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);
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);
- NCT_Assoc.Set (Ent, Node (Elmt));
+ Value := Node (Elmt);
- if Is_Type (Ent) then
- declare
- Anode : constant Entity_Id :=
- Associated_Node_For_Itype (Ent);
+ -- Add the pair in the association hash table
- begin
- -- Enter the link between the associated node of the old
- -- Itype and the new Itype, for updating later when node
- -- is copied.
+ NCT_Assoc.Set (Key, Value);
- if Present (Anode) then
- NCT_Itype_Assoc.Set (Anode, Node (Elmt));
- end if;
- end;
+ -- Add a link between the associated node of the old Itype and the
+ -- new Itype, for updating later when node is copied.
+
+ 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;
Next_Elmt (Elmt);
pragma Assert (not Is_Itype (Old_Entity));
pragma Assert (Nkind (Old_Entity) in N_Entity);
- -- Restrict entity creation to declarations of constants, variables
- -- and subtypes. There is no need to duplicate entities declared in
- -- inner scopes.
+ -- Do not duplicate an entity when it is declared within an inner
+ -- scope enclosed by an expression with actions.
- if (not Ekind_In (Old_Entity, E_Constant, E_Variable)
- and then Nkind (Parent (Old_Entity)) /= N_Subtype_Declaration)
- or else EWA_Inner_Scope_Level > 0
- then
+ if EWA_Inner_Scope_Level > 0 then
+ return;
+
+ -- 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;
end if;
New_E := New_Copy (Old_Entity);
- -- The new entity has all the attributes of the old one, and we
- -- just copy the contents of the entity. However, the back-end
- -- needs different names for debugging purposes, so we create a
- -- new internal name for it in all cases.
+ -- The new entity has all the attributes of the old one, however it
+ -- requires a new name for debugging purposes.
Set_Chars (New_E, New_Internal_Name ('T'));
while Present (New_E) loop
-- Skip entities that were not created in the first phase
- -- (that is, old entities specified by the caller in the
- -- set of mappings to be applied to the tree).
+ -- (that is, old entities specified by the caller in the set of
+ -- mappings to be applied to the tree).
if Is_Itype (New_E)
or else No (Map)
projects / gcc.git / commitdiff