From: Hristian Kirtchev Date: Fri, 28 Apr 2017 13:29:34 +0000 (+0000) Subject: exp_ch6.adb (Expand_N_Extended_Return_Statement): Use New_Copy_Tree instead of Reloca... X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d5fa5335e2171cbfd732a9acba9f22f0df784913;p=gcc.git 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 * 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 * 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 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 6997493e6a5..209e16e50d9 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,20 @@ +2017-04-28 Hristian Kirtchev + + * 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 + + * 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 * exp_util.adb, g-dyntab.adb, par-ch4.adb, sem_util.adb, sem_attr.adb, diff --git a/gcc/ada/a-cfdlli.ads b/gcc/ada/a-cfdlli.ads index e7b7ba7203c..f6638cbb18b 100644 --- a/gcc/ada/a-cfdlli.ads +++ b/gcc/ada/a-cfdlli.ads @@ -1541,9 +1541,9 @@ is 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; diff --git a/gcc/ada/a-cfhama.adb b/gcc/ada/a-cfhama.adb index 4351102adaa..bf782c6c8df 100644 --- a/gcc/ada/a-cfhama.adb +++ b/gcc/ada/a-cfhama.adb @@ -370,7 +370,9 @@ is -- 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 @@ -385,8 +387,9 @@ is -- 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 diff --git a/gcc/ada/a-cfhama.ads b/gcc/ada/a-cfhama.ads index dc60dc8f9f2..e02accc3f52 100644 --- a/gcc/ada/a-cfhama.ads +++ b/gcc/ada/a-cfhama.ads @@ -126,8 +126,8 @@ is 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; @@ -139,9 +139,9 @@ is 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, @@ -203,14 +203,15 @@ is -- 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 @@ -221,7 +222,8 @@ is (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 @@ -246,7 +248,7 @@ is 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 @@ -547,9 +549,9 @@ is -- 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 diff --git a/gcc/ada/a-cfhase.adb b/gcc/ada/a-cfhase.adb index f40fc2fe09b..9b2c9a4bf06 100644 --- a/gcc/ada/a-cfhase.adb +++ b/gcc/ada/a-cfhase.adb @@ -38,16 +38,13 @@ with System; use type System.Address; 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; @@ -68,10 +65,10 @@ is 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; @@ -136,10 +133,13 @@ is 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; @@ -148,9 +148,7 @@ is end loop; return True; - end; - end "="; ------------ @@ -228,11 +226,11 @@ is 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 @@ -276,10 +274,7 @@ is -- 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 @@ -292,10 +287,7 @@ is 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"; @@ -313,11 +305,11 @@ is -- 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; @@ -369,10 +361,7 @@ is 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 @@ -383,9 +372,10 @@ 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); @@ -399,7 +389,7 @@ is 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; @@ -437,8 +427,8 @@ is 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; @@ -466,7 +456,7 @@ is 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; @@ -508,10 +498,7 @@ is -- 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); @@ -771,10 +758,7 @@ is -- 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); @@ -784,10 +768,7 @@ is -- 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); @@ -809,14 +790,13 @@ is -- 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 -- @@ -834,10 +814,7 @@ is -- 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 @@ -884,10 +861,7 @@ is -- 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); @@ -930,6 +904,7 @@ is return False; end if; end loop; + return True; end M_Included_Except; @@ -942,8 +917,7 @@ is 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 @@ -969,8 +943,7 @@ is 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); @@ -1006,12 +979,9 @@ is -- 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); @@ -1035,12 +1005,9 @@ is 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); @@ -1099,10 +1066,7 @@ is -- 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; @@ -1133,11 +1097,7 @@ is 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 @@ -1165,7 +1125,7 @@ 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; @@ -1179,7 +1139,7 @@ is 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; @@ -1301,8 +1261,7 @@ is 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"); @@ -1353,16 +1312,12 @@ is -- 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; @@ -1379,12 +1334,11 @@ is 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; @@ -1425,10 +1379,7 @@ is -- 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); @@ -1439,9 +1390,10 @@ is ------------- 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); @@ -1467,7 +1419,7 @@ is 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; @@ -1512,10 +1464,7 @@ is -- 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 @@ -1536,7 +1485,7 @@ 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 @@ -1546,7 +1495,7 @@ is 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; diff --git a/gcc/ada/a-cfhase.ads b/gcc/ada/a-cfhase.ads index 0f2be8560ba..fd3d007facd 100644 --- a/gcc/ada/a-cfhase.ads +++ b/gcc/ada/a-cfhase.ads @@ -55,8 +55,10 @@ generic 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 @@ -122,8 +124,9 @@ 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; @@ -135,9 +138,9 @@ is 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 @@ -152,9 +155,9 @@ is 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 @@ -171,13 +174,14 @@ is 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 @@ -241,8 +245,8 @@ is 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 @@ -266,15 +270,16 @@ is -- 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 @@ -311,7 +316,7 @@ is 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 @@ -343,13 +348,13 @@ is 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, @@ -378,12 +383,10 @@ is -- 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, @@ -402,10 +405,8 @@ is -- 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; @@ -482,10 +483,8 @@ is -- 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; @@ -769,27 +768,25 @@ is -- 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 @@ -820,21 +817,20 @@ is -- 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; @@ -854,16 +850,14 @@ is -- 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 @@ -886,18 +880,17 @@ is -- 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; @@ -917,16 +910,14 @@ is -- 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 @@ -952,19 +943,18 @@ is -- 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; @@ -984,30 +974,27 @@ is -- 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, @@ -1019,40 +1006,42 @@ is -- 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; @@ -1167,8 +1156,8 @@ is 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; @@ -1309,16 +1298,15 @@ is -- 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; diff --git a/gcc/ada/a-cfinve.adb b/gcc/ada/a-cfinve.adb index 4cb3227934f..8a9d11dccc0 100644 --- a/gcc/ada/a-cfinve.adb +++ b/gcc/ada/a-cfinve.adb @@ -705,12 +705,11 @@ is 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); @@ -1065,8 +1064,9 @@ is 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 @@ -1348,10 +1348,10 @@ is -- 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 @@ -1362,8 +1362,8 @@ is 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; diff --git a/gcc/ada/a-cfinve.ads b/gcc/ada/a-cfinve.ads index e1bc30cf0b5..a7799e556a6 100644 --- a/gcc/ada/a-cfinve.ads +++ b/gcc/ada/a-cfinve.ads @@ -830,9 +830,9 @@ is 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; diff --git a/gcc/ada/a-cforma.adb b/gcc/ada/a-cforma.adb index a7dc514f646..5967973b0fa 100644 --- a/gcc/ada/a-cforma.adb +++ b/gcc/ada/a-cforma.adb @@ -518,7 +518,9 @@ is -- 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 @@ -634,9 +636,12 @@ is -- 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; diff --git a/gcc/ada/a-cforma.ads b/gcc/ada/a-cforma.ads index 6b0597ec2f8..ed4e872f159 100644 --- a/gcc/ada/a-cforma.ads +++ b/gcc/ada/a-cforma.ads @@ -159,16 +159,16 @@ is 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 @@ -178,8 +178,8 @@ is 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, @@ -246,20 +246,21 @@ is -- 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 @@ -284,7 +285,7 @@ is 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 @@ -942,7 +943,7 @@ is Contract_Cases => (Position = No_Element or else P.Get (Positions (Container), Position) = 1 - => + => Position = No_Element, others => @@ -983,6 +984,7 @@ is 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), @@ -999,9 +1001,9 @@ is 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, diff --git a/gcc/ada/a-cforse.adb b/gcc/ada/a-cforse.adb index 47e863bfbd5..b386c5243ba 100644 --- a/gcc/ada/a-cforse.adb +++ b/gcc/ada/a-cforse.adb @@ -608,6 +608,7 @@ is return False; end if; end loop; + return True; end E_Bigger_Than_Range; @@ -700,6 +701,7 @@ is end if; end loop; end if; + return True; end E_Is_Find; @@ -719,6 +721,7 @@ is return False; end if; end loop; + return True; end E_Smaller_Than_Range; @@ -736,6 +739,7 @@ is return I; end if; end loop; + return 0; end Find; diff --git a/gcc/ada/a-cofuma.adb b/gcc/ada/a-cofuma.adb index 487aff46946..93a38b51344 100644 --- a/gcc/ada/a-cofuma.adb +++ b/gcc/ada/a-cofuma.adb @@ -152,8 +152,11 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is -- 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 -- @@ -265,7 +268,9 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is -- 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)); diff --git a/gcc/ada/a-cofuma.ads b/gcc/ada/a-cofuma.ads index ea44dcf9826..f98bfe7b407 100644 --- a/gcc/ada/a-cofuma.ads +++ b/gcc/ada/a-cofuma.ads @@ -35,9 +35,11 @@ private with Ada.Containers.Functional_Base; 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 @@ -77,7 +79,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is -- 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 @@ -90,8 +92,8 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is -- 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 diff --git a/gcc/ada/a-cofuse.ads b/gcc/ada/a-cofuse.ads index 87165d79edc..5eafbc40450 100644 --- a/gcc/ada/a-cofuse.ads +++ b/gcc/ada/a-cofuse.ads @@ -34,9 +34,11 @@ private with Ada.Containers.Functional_Base; 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 @@ -75,7 +77,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is -- 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; @@ -89,8 +91,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is -- 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 @@ -187,7 +188,12 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is 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 -- diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb index fe4735252f1..36f43605fa2 100644 --- a/gcc/ada/exp_ch6.adb +++ b/gcc/ada/exp_ch6.adb @@ -4798,7 +4798,7 @@ package body Exp_Ch6 is 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)); diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 8b1f9c08797..92b33070859 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -17003,7 +17003,7 @@ package body Sem_Util is 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, @@ -17114,37 +17114,45 @@ package body Sem_Util is --------------------------- 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); @@ -17540,23 +17548,29 @@ package body Sem_Util is 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')); @@ -17830,8 +17844,8 @@ package body Sem_Util is 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)