From: Hristian Kirtchev Date: Thu, 27 Apr 2017 10:58:25 +0000 (+0000) Subject: exp_util.adb, [...]: Minor reformatting and code cleanups. X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=27eaddda0f838d0c837d902dea4505c48312ef17;p=gcc.git exp_util.adb, [...]: Minor reformatting and code cleanups. 2017-04-27 Hristian Kirtchev * exp_util.adb, a-cfdlli.adb, a-cfdlli.ads, exp_ch9.adb, g-dyntab.adb, sem_dim.adb, a-cfinve.adb, a-cfinve.ads, a-cofove.adb, a-cofove.ads: Minor reformatting and code cleanups. From-SVN: r247319 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index d4025dc378d..d8863a2f816 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,9 @@ +2017-04-27 Hristian Kirtchev + + * exp_util.adb, a-cfdlli.adb, a-cfdlli.ads, exp_ch9.adb, g-dyntab.adb, + sem_dim.adb, a-cfinve.adb, a-cfinve.ads, a-cofove.adb, a-cofove.ads: + Minor reformatting and code cleanups. + 2017-04-27 Ed Schonberg * freeze.adb (Build_Inherited_Condition_Pragmas): New procedure, diff --git a/gcc/ada/a-cfdlli.adb b/gcc/ada/a-cfdlli.adb index 6c9c0b0f93e..7e641339ecb 100644 --- a/gcc/ada/a-cfdlli.adb +++ b/gcc/ada/a-cfdlli.adb @@ -39,9 +39,7 @@ is New_Item : Element_Type; New_Node : out Count_Type); - procedure Free - (Container : in out List; - X : Count_Type); + procedure Free (Container : in out List; X : Count_Type); procedure Insert_Internal (Container : in out List; @@ -109,10 +107,7 @@ is -- Append -- ------------ - procedure Append - (Container : in out List; - New_Item : Element_Type) - is + procedure Append (Container : in out List; New_Item : Element_Type) is begin Insert (Container, No_Element, New_Item, 1); end Append; @@ -164,14 +159,14 @@ is begin if Container.Length = 0 then pragma Assert (Container.First = 0); - pragma Assert (Container.Last = 0); + pragma Assert (Container.Last = 0); return; end if; pragma Assert (Container.First >= 1); - pragma Assert (Container.Last >= 1); + pragma Assert (Container.Last >= 1); pragma Assert (N (Container.First).Prev = 0); - pragma Assert (N (Container.Last).Next = 0); + pragma Assert (N (Container.Last).Next = 0); while Container.Length > 1 loop X := Container.First; @@ -275,9 +270,9 @@ is pragma Assert (Vet (Container, Position), "bad cursor in Delete"); pragma Assert (Container.First >= 1); - pragma Assert (Container.Last >= 1); + pragma Assert (Container.Last >= 1); pragma Assert (N (Container.First).Prev = 0); - pragma Assert (N (Container.Last).Next = 0); + pragma Assert (N (Container.Last).Next = 0); if Position.Node = Container.First then Delete_First (Container, Count); @@ -430,9 +425,7 @@ is From := Container.First; end if; - if Position.Node /= 0 and then - not Has_Element (Container, Position) - then + if Position.Node /= 0 and then not Has_Element (Container, Position) then raise Constraint_Error with "Position cursor has no element"; end if; @@ -496,33 +489,17 @@ is Left : M.Sequence; Right : M.Sequence) return Boolean is - begin - for I in 1 .. M.Length (Container) loop - declare - Found : Boolean := False; - J : Count_Type := 0; - - begin - while not Found and J < M.Length (Left) loop - J := J + 1; - if Element (Container, I) = Element (Left, J) then - Found := True; - end if; - end loop; - - J := 0; + Elem : Element_Type; - while not Found and J < M.Length (Right) loop - J := J + 1; - if Element (Container, I) = Element (Right, J) then - Found := True; - end if; - end loop; + begin + for Index in 1 .. M.Length (Container) loop + Elem := Element (Container, Index); - if not Found then - return False; - end if; - end; + if not M.Contains (Left, 1, M.Length (Left), Elem) + and then not M.Contains (Right, 1, M.Length (Right), Elem) + then + return False; + end if; end loop; return True; @@ -579,8 +556,7 @@ is end if; for I in 1 .. L loop - if Element (Left, I) /= Element (Right, L - I + 1) - then + if Element (Left, I) /= Element (Right, L - I + 1) then return False; end if; end loop; @@ -638,7 +614,7 @@ is end Model; ----------------------- - -- Mapping_preserved -- + -- Mapping_Preserved -- ----------------------- function Mapping_Preserved @@ -748,7 +724,8 @@ is for C of Right loop if not P.Has_Key (Left, C) - or else (C /= X and C /= Y + or else (C /= X + and C /= Y and P.Get (Left, C) /= P.Get (Right, C)) then return False; @@ -933,8 +910,7 @@ is begin if Target'Address = Source'Address then - raise Program_Error with - "Target and Source denote same container"; + raise Program_Error with "Target and Source denote same container"; end if; LI := First (Target); @@ -1540,8 +1516,7 @@ is begin if Target'Address = Source'Address then - raise Program_Error with - "Target and Source denote same container"; + raise Program_Error with "Target and Source denote same container"; end if; if Before.Node /= 0 then @@ -1549,7 +1524,7 @@ is end if; pragma Assert (SN (Source.First).Prev = 0); - pragma Assert (SN (Source.Last).Next = 0); + pragma Assert (SN (Source.Last).Next = 0); if Target.Length > Count_Type'Base'Last - Source.Length then raise Constraint_Error with "new length exceeds maximum"; @@ -1576,8 +1551,7 @@ is begin if Target'Address = Source'Address then - raise Program_Error with - "Target and Source denote same container"; + raise Program_Error with "Target and Source denote same container"; end if; if Position.Node = 0 then @@ -1820,15 +1794,11 @@ is return False; end if; - if N (Position.Node).Prev = 0 - and then Position.Node /= L.First - then + if N (Position.Node).Prev = 0 and then Position.Node /= L.First then return False; end if; - if N (Position.Node).Next = 0 - and then Position.Node /= L.Last - then + if N (Position.Node).Next = 0 and then Position.Node /= L.Last then return False; end if; diff --git a/gcc/ada/a-cfdlli.ads b/gcc/ada/a-cfdlli.ads index 5c07c12b4be..1a83b609499 100644 --- a/gcc/ada/a-cfdlli.ads +++ b/gcc/ada/a-cfdlli.ads @@ -93,8 +93,8 @@ is (for all I in 1 .. M.Length (Container) => (for some J in 1 .. M.Length (Left) => Element (Container, I) = Element (Left, J)) - or (for some J in 1 .. M.Length (Right) => - Element (Container, I) = Element (Right, J))); + or (for some J in 1 .. M.Length (Right) => + Element (Container, I) = Element (Right, J))); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union); function M_Elements_Included @@ -126,11 +126,11 @@ is M_Elements_Reversed'Result = (M.Length (Left) = M.Length (Right) and (for all I in 1 .. M.Length (Left) => - Element (Left, I) = - Element (Right, M.Length (Left) - I + 1)) + Element (Left, I) = + Element (Right, M.Length (Left) - I + 1)) and (for all I in 1 .. M.Length (Left) => - Element (Right, I) = - Element (Left, M.Length (Left) - I + 1))); + Element (Right, I) = + Element (Left, M.Length (Left) - I + 1))); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed); function M_Elements_Swapped @@ -482,11 +482,11 @@ is -- Container contains Count times New_Item at the end and (if Count > 0 then - M.Constant_Range - (Container => Model (Container), - Fst => Length (Container)'Old + 1, - Lst => Length (Container), - Item => New_Item)) + M.Constant_Range + (Container => Model (Container), + Fst => Length (Container)'Old + 1, + Lst => Length (Container), + Item => New_Item)) -- Container contains Count times New_Item at the end @@ -611,9 +611,9 @@ is Post => Length (Container) = Length (Container)'Old + Count, Contract_Cases => (Count = 0 => - Position = Before - and Model (Container) = Model (Container)'Old - and Positions (Container) = Positions (Container)'Old, + Position = Before + and Model (Container) = Model (Container)'Old + and Positions (Container) = Positions (Container)'Old, others => @@ -772,11 +772,11 @@ is -- Container contains Count times New_Item at the end and (if Count > 0 then - M.Constant_Range - (Container => Model (Container), - Fst => Length (Container)'Old + 1, - Lst => Length (Container), - Item => New_Item)) + M.Constant_Range + (Container => Model (Container), + Fst => Length (Container)'Old + 1, + Lst => Length (Container), + Item => New_Item)) -- Count cursors have been inserted at the end of Container @@ -947,9 +947,9 @@ is -- Other cursors are still valid and P.Keys_Included_Except - (Left => Positions (Container)'Old, - Right => Positions (Container)'Old, - New_Key => Last (Container)'Old) + (Left => Positions (Container)'Old, + Right => Positions (Container)'Old, + New_Key => Last (Container)'Old) -- The positions of other cursors are preserved @@ -992,7 +992,8 @@ is Pre => Has_Element (Container, I) and then Has_Element (Container, J), Post => M_Elements_Swapped - (Model (Container)'Old, Model (Container), + (Model (Container)'Old, + Model (Container), X => P.Get (Positions (Container)'Old, I), Y => P.Get (Positions (Container)'Old, J)) @@ -1001,13 +1002,14 @@ is procedure Swap_Links (Container : in out List; I : Cursor; - J : Cursor) + J : Cursor) with Global => null, Pre => Has_Element (Container, I) and then Has_Element (Container, J), Post => M_Elements_Swapped - (Model (Container'Old), Model (Container), + (Model (Container'Old), + Model (Container), X => P.Get (Positions (Container)'Old, I), Y => P.Get (Positions (Container)'Old, J)) and P_Positions_Swapped @@ -1088,7 +1090,8 @@ is and M_Elements_Included (Left => Model (Target), L_Fst => P.Get (Positions (Target)'Old, Before), - L_Lst => P.Get (Positions (Target)'Old, Before) - 1 + + L_Lst => + P.Get (Positions (Target)'Old, Before) - 1 + Length (Source)'Old, Right => Model (Source)'Old, R_Lst => Length (Source)'Old) @@ -1179,9 +1182,10 @@ is -- The element located at Position in Source is moved to Target - and Element (Model (Target), P.Get (Positions (Target), Position)) = - Element (Model (Source)'Old, - P.Get (Positions (Source)'Old, Position'Old)) + and Element (Model (Target), + P.Get (Positions (Target), Position)) = + Element (Model (Source)'Old, + P.Get (Positions (Source)'Old, Position'Old)) -- A new cursor has been inserted at position Position in Target @@ -1227,9 +1231,10 @@ is -- The last element of Container is the one that was previously at -- Position. - and Element (Model (Container), Length (Container)) = - Element (Model (Container)'Old, - P.Get (Positions (Container)'Old, Position)) + and Element (Model (Container), + Length (Container)) = + Element (Model (Container)'Old, + P.Get (Positions (Container)'Old, Position)) -- Cursors from Container continue designating the same elements @@ -1285,10 +1290,12 @@ is -- The element previously at Position is now before Before - and Element (Model (Container), - P.Get (Positions (Container)'Old, Before)) = - Element (Model (Container)'Old, - P.Get (Positions (Container)'Old, Position)) + and Element + (Model (Container), + P.Get (Positions (Container)'Old, Before)) = + Element + (Model (Container)'Old, + P.Get (Positions (Container)'Old, Position)) -- Cursors from Container continue designating the same elements @@ -1422,8 +1429,9 @@ is -- The element designated by the result of Find is Item - and Element (Model (Container), - P.Get (Positions (Container), Find'Result)) = Item + and Element + (Model (Container), + P.Get (Positions (Container), Find'Result)) = Item -- The result of Find is located after Position @@ -1476,9 +1484,9 @@ is -- The element designated by the result of Find is Item - and Element (Model (Container), - P.Get (Positions (Container), - Reverse_Find'Result)) = Item + and Element + (Model (Container), + P.Get (Positions (Container), Reverse_Find'Result)) = Item -- The result of Find is located before Position @@ -1544,14 +1552,16 @@ is Post => Length (Container) = Length (Container)'Old and M_Elements_Sorted (Model (Container)) - and M_Elements_Included (Left => Model (Container)'Old, - L_Lst => Length (Container), - Right => Model (Container), - R_Lst => Length (Container)) - and M_Elements_Included (Left => Model (Container), - L_Lst => Length (Container), - Right => Model (Container)'Old, - R_Lst => Length (Container)); + and M_Elements_Included + (Left => Model (Container)'Old, + L_Lst => Length (Container), + Right => Model (Container), + R_Lst => Length (Container)) + and M_Elements_Included + (Left => Model (Container), + L_Lst => Length (Container), + Right => Model (Container)'Old, + R_Lst => Length (Container)); procedure Merge (Target : in out List; Source : in out List) with -- Target and Source should not be aliased @@ -1562,18 +1572,22 @@ is and Length (Source) = 0 and (if M_Elements_Sorted (Model (Target)'Old) and M_Elements_Sorted (Model (Source)'Old) - then M_Elements_Sorted (Model (Target))) - and M_Elements_Included (Left => Model (Target)'Old, - L_Lst => Length (Target)'Old, - Right => Model (Target), - R_Lst => Length (Target)) - and M_Elements_Included (Left => Model (Source)'Old, - L_Lst => Length (Source)'Old, - Right => Model (Target), - R_Lst => Length (Target)) - and M_Elements_In_Union (Model (Target), - Model (Source)'Old, - Model (Target)'Old); + then + M_Elements_Sorted (Model (Target))) + and M_Elements_Included + (Left => Model (Target)'Old, + L_Lst => Length (Target)'Old, + Right => Model (Target), + R_Lst => Length (Target)) + and M_Elements_Included + (Left => Model (Source)'Old, + L_Lst => Length (Source)'Old, + Right => Model (Target), + R_Lst => Length (Target)) + and M_Elements_In_Union + (Model (Target), + Model (Source)'Old, + Model (Target)'Old); end Generic_Sorting; private diff --git a/gcc/ada/a-cfinve.adb b/gcc/ada/a-cfinve.adb index 8b29f5e549a..e1a979d2edf 100644 --- a/gcc/ada/a-cfinve.adb +++ b/gcc/ada/a-cfinve.adb @@ -33,7 +33,6 @@ with System; use type System.Address; package body Ada.Containers.Formal_Indefinite_Vectors with SPARK_Mode => Off is - function H (New_Item : Element_Type) return Holder renames To_Holder; function E (Container : Holder) return Element_Type renames Get; @@ -44,12 +43,12 @@ is type Int is range System.Min_Int .. System.Max_Int; procedure Free is - new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr); + new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr); type Maximal_Array_Ptr is access all Elements_Array (Array_Index) with Storage_Size => 0; type Maximal_Array_Ptr_Const is access constant Elements_Array (Array_Index) - with Storage_Size => 0; + with Storage_Size => 0; function Elems (Container : in out Vector) return Maximal_Array_Ptr; function Elemsc @@ -81,7 +80,7 @@ is -- "=" -- --------- - function "=" (Left, Right : Vector) return Boolean is + function "=" (Left : Vector; Right : Vector) return Boolean is begin if Left'Address = Right'Address then return True; @@ -117,10 +116,7 @@ is Insert (Container, Container.Last + 1, New_Item); end Append; - procedure Append - (Container : in out Vector; - New_Item : Element_Type) - is + procedure Append (Container : in out Vector; New_Item : Element_Type) is begin Append (Container, New_Item, 1); end Append; @@ -168,8 +164,11 @@ is function Capacity (Container : Vector) return Capacity_Range is begin - return (if Bounded then Container.Capacity - else Capacity_Range'Last); + return + (if Bounded then + Container.Capacity + else + Capacity_Range'Last); end Capacity; ----------- @@ -229,19 +228,18 @@ is function Current_Capacity (Container : Vector) return Capacity_Range is begin - return (if Container.Elements_Ptr = null - then Container.Elements'Length - else Container.Elements_Ptr.all'Length); + return + (if Container.Elements_Ptr = null then + Container.Elements'Length + else + Container.Elements_Ptr.all'Length); end Current_Capacity; ------------ -- Delete -- ------------ - procedure Delete - (Container : in out Vector; - Index : Extended_Index) - is + procedure Delete (Container : in out Vector; Index : Extended_Index) is begin Delete (Container, Index, 1); end Delete; @@ -339,6 +337,7 @@ is declare EA : Maximal_Array_Ptr renames Elems (Container); Idx : constant Count_Type := EA'First + Off; + begin EA (Idx .. Old_Len - Count) := EA (Idx + Count .. Old_Len); Container.Last := New_Last; @@ -349,17 +348,12 @@ is -- Delete_First -- ------------------ - procedure Delete_First - (Container : in out Vector) - is + procedure Delete_First (Container : in out Vector) is begin Delete_First (Container, 1); end Delete_First; - procedure Delete_First - (Container : in out Vector; - Count : Count_Type) - is + procedure Delete_First (Container : in out Vector; Count : Count_Type) is begin if Count = 0 then return; @@ -377,17 +371,12 @@ is -- Delete_Last -- ----------------- - procedure Delete_Last - (Container : in out Vector) - is + procedure Delete_Last (Container : in out Vector) is begin Delete_Last (Container, 1); end Delete_Last; - procedure Delete_Last - (Container : in out Vector; - Count : Count_Type) - is + procedure Delete_Last (Container : in out Vector; Count : Count_Type) is begin if Count = 0 then return; @@ -431,6 +420,7 @@ is declare II : constant Int'Base := Int (Index) - Int (No_Index); I : constant Capacity_Range := Capacity_Range (II); + begin return Get_Element (Container, I); end; @@ -442,17 +432,20 @@ is function Elems (Container : in out Vector) return Maximal_Array_Ptr is begin - return (if Container.Elements_Ptr = null - then Container.Elements'Unrestricted_Access - else Container.Elements_Ptr.all'Unrestricted_Access); + return + (if Container.Elements_Ptr = null then + Container.Elements'Unrestricted_Access + else + Container.Elements_Ptr.all'Unrestricted_Access); end Elems; - function Elemsc - (Container : Vector) return Maximal_Array_Ptr_Const is + function Elemsc (Container : Vector) return Maximal_Array_Ptr_Const is begin - return (if Container.Elements_Ptr = null - then Container.Elements'Unrestricted_Access - else Container.Elements_Ptr.all'Unrestricted_Access); + return + (if Container.Elements_Ptr = null then + Container.Elements'Unrestricted_Access + else + Container.Elements_Ptr.all'Unrestricted_Access); end Elemsc; ---------------- @@ -519,29 +512,15 @@ is Right : M.Sequence) return Boolean is begin - for I in Index_Type'First .. M.Last (Container) loop + for Index in Index_Type'First .. M.Last (Container) loop declare - Found : Boolean := False; - J : Extended_Index := Extended_Index'First; - + Elem : constant Element_Type := Element (Container, Index); begin - while not Found and J < M.Last (Left) loop - J := J + 1; - if Element (Container, I) = Element (Left, J) then - Found := True; - end if; - end loop; - - J := Extended_Index'First; - - while not Found and J < M.Last (Right) loop - J := J + 1; - if Element (Container, I) = Element (Right, J) then - Found := True; - end if; - end loop; - - if not Found then + if not M.Contains (Left, Index_Type'First, M.Last (Left), Elem) + and then + not M.Contains + (Right, Index_Type'First, M.Last (Right), Elem) + then return False; end if; end; @@ -589,8 +568,12 @@ is -- M_Elements_Reversed -- ------------------------- - function M_Elements_Reversed (Left, Right : M.Sequence) return Boolean is + function M_Elements_Reversed + (Left : M.Sequence; + Right : M.Sequence) return Boolean + is L : constant Index_Type := M.Last (Left); + begin if L /= M.Last (Right) then return False; @@ -613,7 +596,8 @@ is function M_Elements_Swapped (Left : M.Sequence; Right : M.Sequence; - X, Y : Index_Type) return Boolean + X : Index_Type; + Y : Index_Type) return Boolean is begin if M.Length (Left) /= M.Length (Right) @@ -640,10 +624,12 @@ is function Model (Container : Vector) return M.Sequence is R : M.Sequence; + begin for Position in 1 .. Length (Container) loop R := M.Add (R, E (Elemsc (Container) (Position))); end loop; + return R; end Model; @@ -661,11 +647,10 @@ is function Is_Sorted (Container : Vector) return Boolean is L : constant Capacity_Range := Length (Container); + begin for J in 1 .. L - 1 loop - if Get_Element (Container, J + 1) < - Get_Element (Container, J) - then + if Get_Element (Container, J + 1) < Get_Element (Container, J) then return False; end if; end loop; @@ -708,19 +693,19 @@ is -- Sort -- ---------- - procedure Sort (Container : in out Vector) - is + procedure Sort (Container : in out Vector) 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, - "<" => "<"); + (Index_Type => Array_Index, + Element_Type => Holder, + Array_Type => Elements_Array, + "<" => "<"); Len : constant Capacity_Range := Length (Container); + begin if Container.Last <= Index_Type'First then return; @@ -733,13 +718,13 @@ is -- Merge -- ----------- - procedure Merge (Target, Source : in out Vector) is - I, J : Count_Type; + procedure Merge (Target : in out Vector; Source : in out Vector) is + I : Count_Type; + J : Count_Type; begin if Target'Address = Source'Address then - raise Program_Error with - "Target and Source denote same container"; + raise Program_Error with "Target and Source denote same container"; end if; if Length (Source) = 0 then @@ -755,15 +740,16 @@ is declare New_Length : constant Count_Type := I + Length (Source); + begin - if not Bounded and then - Current_Capacity (Target) < Capacity_Range (New_Length) + if not Bounded + and then Current_Capacity (Target) < Capacity_Range (New_Length) then Reserve_Capacity (Target, Capacity_Range'Max (Current_Capacity (Target) * Growth_Factor, - Capacity_Range (New_Length))); + Capacity_Range (New_Length))); end if; if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then @@ -778,6 +764,7 @@ is declare TA : Maximal_Array_Ptr renames Elems (Target); SA : Maximal_Array_Ptr renames Elems (Source); + begin J := Length (Target); while Length (Source) /= 0 loop @@ -820,7 +807,9 @@ is ----------------- function Has_Element - (Container : Vector; Position : Extended_Index) return Boolean is + (Container : Vector; + Position : Extended_Index) return Boolean + is begin return Position in First_Index (Container) .. Last_Index (Container); end Has_Element; @@ -997,8 +986,7 @@ is -- worry about if No_Index were less than 0, but that case is -- handled above). - if Index_Type'Last - No_Index >= - Count_Type'Pos (Count_Type'Last) + if Index_Type'Last - No_Index >= Count_Type'Pos (Count_Type'Last) then -- We have determined that range of Index_Type has at least as -- many values as in Count_Type, so Count_Type'Last is the @@ -1064,17 +1052,18 @@ is -- Increase the capacity of container if needed - if not Bounded and then - Current_Capacity (Container) < Capacity_Range (New_Length) + if not Bounded + and then Current_Capacity (Container) < Capacity_Range (New_Length) then Reserve_Capacity (Container, Capacity_Range'Max (Current_Capacity (Container) * Growth_Factor, - Capacity_Range (New_Length))); + Capacity_Range (New_Length))); end if; declare EA : Maximal_Array_Ptr renames Elems (Container); + begin if Before <= Container.Last then @@ -1134,6 +1123,7 @@ is L : constant Int := Int (Container.Last); F : constant Int := Int (Index_Type'First); N : constant Int'Base := L - F + 1; + begin return Capacity_Range (N); end Length; @@ -1142,11 +1132,9 @@ is -- Move -- ---------- - procedure Move - (Target : in out Vector; - Source : in out Vector) - is + procedure Move (Target : in out Vector; Source : in out Vector) is LS : constant Capacity_Range := Length (Source); + begin if Target'Address = Source'Address then return; @@ -1170,10 +1158,7 @@ is Insert (Container, Index_Type'First, New_Item); end Prepend; - procedure Prepend - (Container : in out Vector; - New_Item : Element_Type) - is + procedure Prepend (Container : in out Vector; New_Item : Element_Type) is begin Prepend (Container, New_Item, 1); end Prepend; @@ -1204,6 +1189,7 @@ is declare II : constant Int'Base := Int (Index) - Int (No_Index); I : constant Capacity_Range := Capacity_Range (II); + begin Elems (Container) (I) := H (New_Item); end; @@ -1222,12 +1208,14 @@ is if Capacity > Container.Capacity then raise Constraint_Error with "Capacity is out of range"; end if; + else if Capacity > Current_Capacity (Container) then declare New_Elements : constant Elements_Array_Ptr := new Elements_Array (1 .. Capacity); L : constant Capacity_Range := Length (Container); + begin New_Elements (1 .. L) := Elemsc (Container) (1 .. L); Free (Container.Elements_Ptr); @@ -1248,9 +1236,10 @@ is end if; declare - I, J : Capacity_Range; - E : Elements_Array renames - Elems (Container) (1 .. Length (Container)); + I : Capacity_Range; + J : Capacity_Range; + E : Elements_Array renames + Elems (Container) (1 .. Length (Container)); begin I := 1; @@ -1258,6 +1247,7 @@ is while I < J loop declare EI : constant Holder := E (I); + begin E (I) := E (J); E (J) := EI; @@ -1304,7 +1294,11 @@ is -- Swap -- ---------- - procedure Swap (Container : in out Vector; I, J : Index_Type) is + procedure Swap + (Container : in out Vector; + I : Index_Type; + J : Index_Type) + is begin if I > Container.Last then raise Constraint_Error with "I index is out of range"; @@ -1391,10 +1385,11 @@ is Last := Index_Type (Last_As_Int); - return (Capacity => Length, - Last => Last, - Elements_Ptr => <>, - Elements => (others => H (New_Item))); + return + (Capacity => Length, + Last => Last, + Elements_Ptr => <>, + Elements => (others => H (New_Item))); end; end To_Vector; diff --git a/gcc/ada/a-cfinve.ads b/gcc/ada/a-cfinve.ads index 5ef2b1edd79..9836c5ff960 100644 --- a/gcc/ada/a-cfinve.ads +++ b/gcc/ada/a-cfinve.ads @@ -124,8 +124,8 @@ is (for all I in Index_Type'First .. M.Last (Container) => (for some J in Index_Type'First .. M.Last (Left) => Element (Container, I) = Element (Left, J)) - or (for some J in Index_Type'First .. M.Last (Right) => - Element (Container, I) = Element (Right, J))); + or (for some J in Index_Type'First .. M.Last (Right) => + Element (Container, I) = Element (Right, J))); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union); function M_Elements_Included @@ -157,11 +157,11 @@ is M_Elements_Reversed'Result = (M.Length (Left) = M.Length (Right) and (for all I in Index_Type'First .. M.Last (Left) => - Element (Left, I) = - Element (Right, M.Last (Left) - I + 1)) + Element (Left, I) = + Element (Right, M.Last (Left) - I + 1)) and (for all I in Index_Type'First .. M.Last (Right) => - Element (Right, I) = - Element (Left, M.Last (Left) - I + 1))); + Element (Right, I) = + Element (Left, M.Last (Left) - I + 1))); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed); function M_Elements_Swapped @@ -195,6 +195,7 @@ is I : Index_Type) return Element_Type renames M.Get; -- To improve readability of contracts, we rename the function used to -- access an element in the model to Element. + end Formal_Model; use Formal_Model; @@ -213,16 +214,20 @@ is Global => null, Post => Formal_Indefinite_Vectors.Length (To_Vector'Result) = Length - and M.Constant_Range (Container => Model (To_Vector'Result), - Fst => Index_Type'First, - Lst => Last_Index (To_Vector'Result), - Item => New_Item); + and M.Constant_Range + (Container => Model (To_Vector'Result), + Fst => Index_Type'First, + Lst => Last_Index (To_Vector'Result), + Item => New_Item); function Capacity (Container : Vector) return Capacity_Range with Global => null, Post => - Capacity'Result = (if Bounded then Container.Capacity - else Capacity_Range'Last); + Capacity'Result = + (if Bounded then + Container.Capacity + else + Capacity_Range'Last); pragma Annotate (GNATprove, Inline_For_Proof, Capacity); procedure Reserve_Capacity @@ -257,8 +262,10 @@ is Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)), Post => Model (Copy'Result) = Model (Source) - and (if Capacity = 0 then Copy'Result.Capacity = Length (Source) - else Copy'Result.Capacity = Capacity); + and (if Capacity = 0 then + Copy'Result.Capacity = Length (Source) + else + Copy'Result.Capacity = Capacity); procedure Move (Target : in out Vector; Source : in out Vector) with @@ -305,7 +312,7 @@ is Pre => Length (Container) <= Capacity (Container) - Length (New_Item) and (Before in Index_Type'First .. Last_Index (Container) - or (Before /= No_Index + or (Before /= No_Index and then Before - 1 = Last_Index (Container))), Post => Length (Container) = Length (Container)'Old + Length (New_Item) @@ -321,12 +328,12 @@ is -- Elements of New_Item are inserted at position Before and (if Length (New_Item) > 0 then - M.Range_Shifted - (Left => Model (New_Item), - Right => Model (Container), - Fst => Index_Type'First, - Lst => Last_Index (New_Item), - Offset => Count_Type (Before - Index_Type'First))) + M.Range_Shifted + (Left => Model (New_Item), + Right => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (New_Item), + Offset => Count_Type (Before - Index_Type'First))) -- Elements located after Before in Container are shifted @@ -380,7 +387,7 @@ is Pre => Length (Container) <= Capacity (Container) - Count and (Before in Index_Type'First .. Last_Index (Container) - or (Before /= No_Index + or (Before /= No_Index and then Before - 1 = Last_Index (Container))), Post => Length (Container) = Length (Container)'Old + Count @@ -396,11 +403,11 @@ is -- New_Item is inserted Count times at position Before and (if Count > 0 then - M.Constant_Range - (Container => Model (Container), - Fst => Before, - Lst => Before + Index_Type'Base (Count - 1), - Item => New_Item)) + M.Constant_Range + (Container => Model (Container), + Fst => Before, + Lst => Before + Index_Type'Base (Count - 1), + Item => New_Item)) -- Elements located after Before in Container are shifted @@ -411,10 +418,7 @@ is Lst => Last_Index (Container)'Old, Offset => Count); - procedure Prepend - (Container : in out Vector; - New_Item : Vector) - with + procedure Prepend (Container : in out Vector; New_Item : Vector) with Global => null, Pre => Length (Container) <= Capacity (Container) - Length (New_Item), Post => @@ -437,10 +441,7 @@ is Lst => Last_Index (Container)'Old, Offset => Length (New_Item)); - procedure Prepend - (Container : in out Vector; - New_Item : Element_Type) - with + procedure Prepend (Container : in out Vector; New_Item : Element_Type) with Global => null, Pre => Length (Container) < Capacity (Container), Post => @@ -486,10 +487,7 @@ is Lst => Last_Index (Container)'Old, Offset => Count); - procedure Append - (Container : in out Vector; - New_Item : Vector) - with + procedure Append (Container : in out Vector; New_Item : Vector) with Global => null, Pre => Length (Container) <= Capacity (Container) - Length (New_Item), @@ -503,19 +501,16 @@ is -- Elements of New_Item are inserted at the end of Container and (if Length (New_Item) > 0 then - M.Range_Shifted - (Left => Model (New_Item), - Right => Model (Container), - Fst => Index_Type'First, - Lst => Last_Index (New_Item), - Offset => - Count_Type - (Last_Index (Container)'Old - Index_Type'First + 1))); + M.Range_Shifted + (Left => Model (New_Item), + Right => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (New_Item), + Offset => + Count_Type + (Last_Index (Container)'Old - Index_Type'First + 1))); - procedure Append - (Container : in out Vector; - New_Item : Element_Type) - with + procedure Append (Container : in out Vector; New_Item : Element_Type) with Global => null, Pre => Length (Container) < Capacity (Container), Post => @@ -547,17 +542,14 @@ is -- New_Item is inserted Count times at the end of Container and (if Count > 0 then - M.Constant_Range - (Container => Model (Container), - Fst => Last_Index (Container)'Old + 1, - Lst => - Last_Index (Container)'Old + Index_Type'Base (Count), - Item => New_Item)); + M.Constant_Range + (Container => Model (Container), + Fst => Last_Index (Container)'Old + 1, + Lst => + Last_Index (Container)'Old + Index_Type'Base (Count), + Item => New_Item)); - procedure Delete - (Container : in out Vector; - Index : Extended_Index) - with + procedure Delete (Container : in out Vector; Index : Extended_Index) with Global => null, Pre => Index in First_Index (Container) .. Last_Index (Container), Post => @@ -619,9 +611,7 @@ is Lst => Last_Index (Container), Offset => Count)); - procedure Delete_First - (Container : in out Vector) - with + procedure Delete_First (Container : in out Vector) with Global => null, Pre => Length (Container) > 0, Post => @@ -636,10 +626,7 @@ is Lst => Last_Index (Container), Offset => 1); - procedure Delete_First - (Container : in out Vector; - Count : Count_Type) - with + procedure Delete_First (Container : in out Vector; Count : Count_Type) with Global => null, Contract_Cases => @@ -659,9 +646,7 @@ is Lst => Last_Index (Container), Offset => Count)); - procedure Delete_Last - (Container : in out Vector) - with + procedure Delete_Last (Container : in out Vector) with Global => null, Pre => Length (Container) > 0, Post => @@ -671,10 +656,7 @@ is and Model (Container) < Model (Container)'Old; - procedure Delete_Last - (Container : in out Vector; - Count : Count_Type) - with + procedure Delete_Last (Container : in out Vector; Count : Count_Type) with Global => null, Contract_Cases => @@ -693,10 +675,15 @@ is Global => null, Post => M_Elements_Reversed (Model (Container)'Old, Model (Container)); - procedure Swap (Container : in out Vector; I, J : Index_Type) with + procedure Swap + (Container : in out Vector; + I : Index_Type; + J : Index_Type) + with Global => null, - Pre => I in First_Index (Container) .. Last_Index (Container) - and then J in First_Index (Container) .. Last_Index (Container), + Pre => + I in First_Index (Container) .. Last_Index (Container) + and then J in First_Index (Container) .. Last_Index (Container), Post => M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J); @@ -737,11 +724,11 @@ is -- returns No_Index. (Index > Last_Index (Container) - or else not M.Contains - (Container => Model (Container), - Fst => Index, - Lst => Last_Index (Container), - Item => Item) + or else not M.Contains + (Container => Model (Container), + Fst => Index, + Lst => Last_Index (Container), + Item => Item) => Find_Index'Result = No_Index, @@ -799,8 +786,10 @@ is (Container => Model (Container), Fst => Reverse_Find_Index'Result + 1, Lst => - (if Index <= Last_Index (Container) then Index - else Last_Index (Container)), + (if Index <= Last_Index (Container) then + Index + else + Last_Index (Container)), Item => Item)); function Contains @@ -809,10 +798,12 @@ is with Global => null, Post => - Contains'Result = M.Contains (Container => Model (Container), - Fst => Index_Type'First, - Lst => Last_Index (Container), - Item => Item); + Contains'Result = + M.Contains + (Container => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (Container), + Item => Item); function Has_Element (Container : Vector; @@ -834,8 +825,8 @@ is 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))); + Element (Container, I) = Element (Container, J) + or Element (Container, I) < Element (Container, J))); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted); function Is_Sorted (Container : Vector) return Boolean with @@ -847,14 +838,16 @@ is Post => Length (Container) = Length (Container)'Old and M_Elements_Sorted (Model (Container)) - and M_Elements_Included (Left => Model (Container)'Old, - L_Lst => Last_Index (Container), - Right => Model (Container), - R_Lst => Last_Index (Container)) - and M_Elements_Included (Left => Model (Container), - L_Lst => Last_Index (Container), - Right => Model (Container)'Old, - R_Lst => Last_Index (Container)); + and M_Elements_Included + (Left => Model (Container)'Old, + L_Lst => Last_Index (Container), + Right => Model (Container), + R_Lst => Last_Index (Container)) + and M_Elements_Included + (Left => Model (Container), + L_Lst => Last_Index (Container), + Right => Model (Container)'Old, + R_Lst => Last_Index (Container)); procedure Merge (Target : in out Vector; Source : in out Vector) with -- Target and Source should not be aliased @@ -865,18 +858,22 @@ is and Length (Source) = 0 and (if M_Elements_Sorted (Model (Target)'Old) and M_Elements_Sorted (Model (Source)'Old) - then M_Elements_Sorted (Model (Target))) - and M_Elements_Included (Left => Model (Target)'Old, - L_Lst => Last_Index (Target)'Old, - Right => Model (Target), - R_Lst => Last_Index (Target)) - and M_Elements_Included (Left => Model (Source)'Old, - L_Lst => Last_Index (Source)'Old, - Right => Model (Target), - R_Lst => Last_Index (Target)) - and M_Elements_In_Union (Model (Target), - Model (Source)'Old, - Model (Target)'Old); + then + M_Elements_Sorted (Model (Target))) + and M_Elements_Included + (Left => Model (Target)'Old, + L_Lst => Last_Index (Target)'Old, + Right => Model (Target), + R_Lst => Last_Index (Target)) + and M_Elements_Included + (Left => Model (Source)'Old, + L_Lst => Last_Index (Source)'Old, + Right => Model (Target), + R_Lst => Last_Index (Target)) + and M_Elements_In_Union + (Model (Target), + Model (Source)'Old, + Model (Target)'Old); end Generic_Sorting; private @@ -904,9 +901,11 @@ private type Elements_Array_Ptr is access all Elements_Array; type Vector (Capacity : Capacity_Range) is limited record + -- In the bounded case, the elements are stored in Elements. In the -- unbounded case, the elements are initially stored in Elements, until -- we run out of room, then we switch to Elements_Ptr. + Last : Extended_Index := No_Index; Elements_Ptr : Elements_Array_Ptr := null; Elements : aliased Elements_Array (1 .. Capacity); diff --git a/gcc/ada/a-cofove.adb b/gcc/ada/a-cofove.adb index d1f4b9ce61b..87c1d3d59cb 100644 --- a/gcc/ada/a-cofove.adb +++ b/gcc/ada/a-cofove.adb @@ -41,12 +41,12 @@ is type Int is range System.Min_Int .. System.Max_Int; procedure Free is - new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr); + new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr); type Maximal_Array_Ptr is access all Elements_Array (Array_Index) with Storage_Size => 0; type Maximal_Array_Ptr_Const is access constant Elements_Array (Array_Index) - with Storage_Size => 0; + with Storage_Size => 0; function Elems (Container : in out Vector) return Maximal_Array_Ptr; function Elemsc @@ -78,7 +78,7 @@ is -- "=" -- --------- - function "=" (Left, Right : Vector) return Boolean is + function "=" (Left : Vector; Right : Vector) return Boolean is begin if Left'Address = Right'Address then return True; @@ -114,10 +114,7 @@ is Insert (Container, Container.Last + 1, New_Item); end Append; - procedure Append - (Container : in out Vector; - New_Item : Element_Type) - is + procedure Append (Container : in out Vector; New_Item : Element_Type) is begin Append (Container, New_Item, 1); end Append; @@ -165,8 +162,11 @@ is function Capacity (Container : Vector) return Capacity_Range is begin - return (if Bounded then Container.Capacity - else Capacity_Range'Last); + return + (if Bounded then + Container.Capacity + else + Capacity_Range'Last); end Capacity; ----------- @@ -226,19 +226,18 @@ is function Current_Capacity (Container : Vector) return Capacity_Range is begin - return (if Container.Elements_Ptr = null - then Container.Elements'Length - else Container.Elements_Ptr.all'Length); + return + (if Container.Elements_Ptr = null then + Container.Elements'Length + else + Container.Elements_Ptr.all'Length); end Current_Capacity; ------------ -- Delete -- ------------ - procedure Delete - (Container : in out Vector; - Index : Extended_Index) - is + procedure Delete (Container : in out Vector; Index : Extended_Index) is begin Delete (Container, Index, 1); end Delete; @@ -317,10 +316,10 @@ is end if; -- There are some elements aren't being deleted (the requested count was - -- less than the available count), so we must slide them down to - -- Index. We first calculate the index values of the respective array - -- slices, using the wider of Index_Type'Base and Count_Type'Base as the - -- type for intermediate calculations. + -- less than the available count), so we must slide them down to Index. + -- We first calculate the index values of the respective array slices, + -- using the wider of Index_Type'Base and Count_Type'Base as the type + -- for intermediate calculations. if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then Off := Count_Type'Base (Index - Index_Type'First); @@ -346,17 +345,12 @@ is -- Delete_First -- ------------------ - procedure Delete_First - (Container : in out Vector) - is + procedure Delete_First (Container : in out Vector) is begin Delete_First (Container, 1); end Delete_First; - procedure Delete_First - (Container : in out Vector; - Count : Count_Type) - is + procedure Delete_First (Container : in out Vector; Count : Count_Type) is begin if Count = 0 then return; @@ -374,17 +368,12 @@ is -- Delete_Last -- ----------------- - procedure Delete_Last - (Container : in out Vector) - is + procedure Delete_Last (Container : in out Vector) is begin Delete_Last (Container, 1); end Delete_Last; - procedure Delete_Last - (Container : in out Vector; - Count : Count_Type) - is + procedure Delete_Last (Container : in out Vector; Count : Count_Type) is begin if Count = 0 then return; @@ -439,17 +428,20 @@ is function Elems (Container : in out Vector) return Maximal_Array_Ptr is begin - return (if Container.Elements_Ptr = null - then Container.Elements'Unrestricted_Access - else Container.Elements_Ptr.all'Unrestricted_Access); + return + (if Container.Elements_Ptr = null then + Container.Elements'Unrestricted_Access + else + Container.Elements_Ptr.all'Unrestricted_Access); end Elems; - function Elemsc - (Container : Vector) return Maximal_Array_Ptr_Const is + function Elemsc (Container : Vector) return Maximal_Array_Ptr_Const is begin - return (if Container.Elements_Ptr = null - then Container.Elements'Unrestricted_Access - else Container.Elements_Ptr.all'Unrestricted_Access); + return + (if Container.Elements_Ptr = null then + Container.Elements'Unrestricted_Access + else + Container.Elements_Ptr.all'Unrestricted_Access); end Elemsc; ---------------- @@ -515,33 +507,18 @@ is Left : M.Sequence; Right : M.Sequence) return Boolean is - begin - for I in Index_Type'First .. M.Last (Container) loop - declare - Found : Boolean := False; - J : Extended_Index := Extended_Index'First; - - begin - while not Found and J < M.Last (Left) loop - J := J + 1; - if Element (Container, I) = Element (Left, J) then - Found := True; - end if; - end loop; + Elem : Element_Type; - J := Extended_Index'First; - - while not Found and J < M.Last (Right) loop - J := J + 1; - if Element (Container, I) = Element (Right, J) then - Found := True; - end if; - end loop; + begin + for Index in Index_Type'First .. M.Last (Container) loop + Elem := Element (Container, Index); - if not Found then - return False; - end if; - end; + if not M.Contains (Left, Index_Type'First, M.Last (Left), Elem) + and then + not M.Contains (Right, Index_Type'First, M.Last (Right), Elem) + then + return False; + end if; end loop; return True; @@ -586,8 +563,12 @@ is -- M_Elements_Reversed -- ------------------------- - function M_Elements_Reversed (Left, Right : M.Sequence) return Boolean is + function M_Elements_Reversed + (Left : M.Sequence; + Right : M.Sequence) return Boolean + is L : constant Index_Type := M.Last (Left); + begin if L /= M.Last (Right) then return False; @@ -610,7 +591,8 @@ is function M_Elements_Swapped (Left : M.Sequence; Right : M.Sequence; - X, Y : Index_Type) return Boolean + X : Index_Type; + Y : Index_Type) return Boolean is begin if M.Length (Left) /= M.Length (Right) @@ -637,10 +619,12 @@ is function Model (Container : Vector) return M.Sequence is R : M.Sequence; + begin for Position in 1 .. Length (Container) loop R := M.Add (R, Elemsc (Container) (Position)); end loop; + return R; end Model; @@ -658,6 +642,7 @@ is function Is_Sorted (Container : Vector) return Boolean is L : constant Capacity_Range := Length (Container); + begin for J in 1 .. L - 1 loop if Get_Element (Container, J + 1) < @@ -705,16 +690,16 @@ is -- Sort -- ---------- - procedure Sort (Container : in out Vector) - is + procedure Sort (Container : in out Vector) is procedure Sort is new Generic_Array_Sort - (Index_Type => Array_Index, - Element_Type => Element_Type, - Array_Type => Elements_Array, - "<" => "<"); + (Index_Type => Array_Index, + Element_Type => Element_Type, + Array_Type => Elements_Array, + "<" => "<"); Len : constant Capacity_Range := Length (Container); + begin if Container.Last <= Index_Type'First then return; @@ -727,13 +712,13 @@ is -- Merge -- ----------- - procedure Merge (Target, Source : in out Vector) is - I, J : Count_Type; + procedure Merge (Target : in out Vector; Source : in out Vector) is + I : Count_Type; + J : Count_Type; begin if Target'Address = Source'Address then - raise Program_Error with - "Target and Source denote same container"; + raise Program_Error with "Target and Source denote same container"; end if; if Length (Source) = 0 then @@ -749,15 +734,16 @@ is declare New_Length : constant Count_Type := I + Length (Source); + begin - if not Bounded and then - Current_Capacity (Target) < Capacity_Range (New_Length) + if not Bounded + and then Current_Capacity (Target) < Capacity_Range (New_Length) then Reserve_Capacity (Target, Capacity_Range'Max (Current_Capacity (Target) * Growth_Factor, - Capacity_Range (New_Length))); + Capacity_Range (New_Length))); end if; if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then @@ -772,6 +758,7 @@ is declare TA : Maximal_Array_Ptr renames Elems (Target); SA : Maximal_Array_Ptr renames Elems (Source); + begin J := Length (Target); while Length (Source) /= 0 loop @@ -814,7 +801,9 @@ is ----------------- function Has_Element - (Container : Vector; Position : Extended_Index) return Boolean is + (Container : Vector; + Position : Extended_Index) return Boolean + is begin return Position in First_Index (Container) .. Last_Index (Container); end Has_Element; @@ -870,6 +859,7 @@ is Insert_Space (Container, Before, Count => N); if N = 0 then + -- There's nothing else to do here (vetting of parameters was -- performed already in Insert_Space), so we simply return. @@ -937,9 +927,9 @@ is -- There are two constraints we need to satisfy. The first constraint is -- that a container cannot have more than Count_Type'Last elements, so - -- we must check the sum of the current length and the insertion - -- count. Note that we cannot simply add these values, because of the - -- possibility of overflow. + -- we must check the sum of the current length and the insertion count. + -- Note that the value cannot be simply added because the result may + -- overflow. if Old_Length > Count_Type'Last - Count then raise Constraint_Error with "Count is out of range"; @@ -991,8 +981,7 @@ is -- worry about if No_Index were less than 0, but that case is -- handled above). - if Index_Type'Last - No_Index >= - Count_Type'Pos (Count_Type'Last) + if Index_Type'Last - No_Index >= Count_Type'Pos (Count_Type'Last) then -- We have determined that range of Index_Type has at least as -- many values as in Count_Type, so Count_Type'Last is the @@ -1058,17 +1047,18 @@ is -- Increase the capacity of container if needed - if not Bounded and then - Current_Capacity (Container) < Capacity_Range (New_Length) + if not Bounded + and then Current_Capacity (Container) < Capacity_Range (New_Length) then Reserve_Capacity (Container, Capacity_Range'Max (Current_Capacity (Container) * Growth_Factor, - Capacity_Range (New_Length))); + Capacity_Range (New_Length))); end if; declare EA : Maximal_Array_Ptr renames Elems (Container); + begin if Before <= Container.Last then @@ -1128,6 +1118,7 @@ is L : constant Int := Int (Container.Last); F : constant Int := Int (Index_Type'First); N : constant Int'Base := L - F + 1; + begin return Capacity_Range (N); end Length; @@ -1136,11 +1127,9 @@ is -- Move -- ---------- - procedure Move - (Target : in out Vector; - Source : in out Vector) - is + procedure Move (Target : in out Vector; Source : in out Vector) is LS : constant Capacity_Range := Length (Source); + begin if Target'Address = Source'Address then return; @@ -1164,10 +1153,7 @@ is Insert (Container, Index_Type'First, New_Item); end Prepend; - procedure Prepend - (Container : in out Vector; - New_Item : Element_Type) - is + procedure Prepend (Container : in out Vector; New_Item : Element_Type) is begin Prepend (Container, New_Item, 1); end Prepend; @@ -1198,6 +1184,7 @@ is declare II : constant Int'Base := Int (Index) - Int (No_Index); I : constant Capacity_Range := Capacity_Range (II); + begin Elems (Container) (I) := New_Item; end; @@ -1216,12 +1203,14 @@ is if Capacity > Container.Capacity then raise Constraint_Error with "Capacity is out of range"; end if; + else if Capacity > Formal_Vectors.Current_Capacity (Container) then declare New_Elements : constant Elements_Array_Ptr := new Elements_Array (1 .. Capacity); L : constant Capacity_Range := Length (Container); + begin New_Elements (1 .. L) := Elemsc (Container) (1 .. L); Free (Container.Elements_Ptr); @@ -1252,6 +1241,7 @@ is while I < J loop declare EI : constant Element_Type := E (I); + begin E (I) := E (J); E (J) := EI; @@ -1298,7 +1288,11 @@ is -- Swap -- ---------- - procedure Swap (Container : in out Vector; I, J : Index_Type) is + procedure Swap + (Container : in out Vector; + I : Index_Type; + J : Index_Type) + is begin if I > Container.Last then raise Constraint_Error with "I index is out of range"; @@ -1350,12 +1344,12 @@ is Offset := Count_Type'Base (Index - Index_Type'First); else - Offset := Count_Type'Base (Index) - - Count_Type'Base (Index_Type'First); + Offset := + Count_Type'Base (Index) - 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; @@ -1385,10 +1379,11 @@ is Last := Index_Type (Last_As_Int); - return (Capacity => Length, - Last => Last, - Elements_Ptr => <>, - Elements => (others => New_Item)); + return + (Capacity => Length, + Last => Last, + Elements_Ptr => <>, + Elements => (others => New_Item)); end; end To_Vector; diff --git a/gcc/ada/a-cofove.ads b/gcc/ada/a-cofove.ads index 5ad0e87c377..efa5e9eaea9 100644 --- a/gcc/ada/a-cofove.ads +++ b/gcc/ada/a-cofove.ads @@ -118,8 +118,8 @@ is (for all I in Index_Type'First .. M.Last (Container) => (for some J in Index_Type'First .. M.Last (Left) => Element (Container, I) = Element (Left, J)) - or (for some J in Index_Type'First .. M.Last (Right) => - Element (Container, I) = Element (Right, J))); + or (for some J in Index_Type'First .. M.Last (Right) => + Element (Container, I) = Element (Right, J))); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union); function M_Elements_Included @@ -151,11 +151,11 @@ is M_Elements_Reversed'Result = (M.Length (Left) = M.Length (Right) and (for all I in Index_Type'First .. M.Last (Left) => - Element (Left, I) = - Element (Right, M.Last (Left) - I + 1)) + Element (Left, I) = + Element (Right, M.Last (Left) - I + 1)) and (for all I in Index_Type'First .. M.Last (Right) => - Element (Right, I) = - Element (Left, M.Last (Left) - I + 1))); + Element (Right, I) = + Element (Left, M.Last (Left) - I + 1))); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed); function M_Elements_Swapped @@ -189,6 +189,7 @@ is I : Index_Type) return Element_Type renames M.Get; -- To improve readability of contracts, we rename the function used to -- access an element in the model to Element. + end Formal_Model; use Formal_Model; @@ -207,16 +208,20 @@ is Global => null, Post => Formal_Vectors.Length (To_Vector'Result) = Length - and M.Constant_Range (Container => Model (To_Vector'Result), - Fst => Index_Type'First, - Lst => Last_Index (To_Vector'Result), - Item => New_Item); + and M.Constant_Range + (Container => Model (To_Vector'Result), + Fst => Index_Type'First, + Lst => Last_Index (To_Vector'Result), + Item => New_Item); function Capacity (Container : Vector) return Capacity_Range with Global => null, Post => - Capacity'Result = (if Bounded then Container.Capacity - else Capacity_Range'Last); + Capacity'Result = + (if Bounded then + Container.Capacity + else + Capacity_Range'Last); pragma Annotate (GNATprove, Inline_For_Proof, Capacity); procedure Reserve_Capacity @@ -251,8 +256,10 @@ is Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)), Post => Model (Copy'Result) = Model (Source) - and (if Capacity = 0 then Copy'Result.Capacity = Length (Source) - else Copy'Result.Capacity = Capacity); + and (if Capacity = 0 then + Copy'Result.Capacity = Length (Source) + else + Copy'Result.Capacity = Capacity); procedure Move (Target : in out Vector; Source : in out Vector) with @@ -299,7 +306,7 @@ is Pre => Length (Container) <= Capacity (Container) - Length (New_Item) and (Before in Index_Type'First .. Last_Index (Container) - or (Before /= No_Index + or (Before /= No_Index and then Before - 1 = Last_Index (Container))), Post => Length (Container) = Length (Container)'Old + Length (New_Item) @@ -315,12 +322,12 @@ is -- Elements of New_Item are inserted at position Before and (if Length (New_Item) > 0 then - M.Range_Shifted - (Left => Model (New_Item), - Right => Model (Container), - Fst => Index_Type'First, - Lst => Last_Index (New_Item), - Offset => Count_Type (Before - Index_Type'First))) + M.Range_Shifted + (Left => Model (New_Item), + Right => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (New_Item), + Offset => Count_Type (Before - Index_Type'First))) -- Elements located after Before in Container are shifted @@ -374,7 +381,7 @@ is Pre => Length (Container) <= Capacity (Container) - Count and (Before in Index_Type'First .. Last_Index (Container) - or (Before /= No_Index + or (Before /= No_Index and then Before - 1 = Last_Index (Container))), Post => Length (Container) = Length (Container)'Old + Count @@ -390,11 +397,11 @@ is -- New_Item is inserted Count times at position Before and (if Count > 0 then - M.Constant_Range - (Container => Model (Container), - Fst => Before, - Lst => Before + Index_Type'Base (Count - 1), - Item => New_Item)) + M.Constant_Range + (Container => Model (Container), + Fst => Before, + Lst => Before + Index_Type'Base (Count - 1), + Item => New_Item)) -- Elements located after Before in Container are shifted @@ -405,10 +412,7 @@ is Lst => Last_Index (Container)'Old, Offset => Count); - procedure Prepend - (Container : in out Vector; - New_Item : Vector) - with + procedure Prepend (Container : in out Vector; New_Item : Vector) with Global => null, Pre => Length (Container) <= Capacity (Container) - Length (New_Item), Post => @@ -431,10 +435,7 @@ is Lst => Last_Index (Container)'Old, Offset => Length (New_Item)); - procedure Prepend - (Container : in out Vector; - New_Item : Element_Type) - with + procedure Prepend (Container : in out Vector; New_Item : Element_Type) with Global => null, Pre => Length (Container) < Capacity (Container), Post => @@ -480,10 +481,7 @@ is Lst => Last_Index (Container)'Old, Offset => Count); - procedure Append - (Container : in out Vector; - New_Item : Vector) - with + procedure Append (Container : in out Vector; New_Item : Vector) with Global => null, Pre => Length (Container) <= Capacity (Container) - Length (New_Item), @@ -497,19 +495,16 @@ is -- Elements of New_Item are inserted at the end of Container and (if Length (New_Item) > 0 then - M.Range_Shifted - (Left => Model (New_Item), - Right => Model (Container), - Fst => Index_Type'First, - Lst => Last_Index (New_Item), - Offset => - Count_Type - (Last_Index (Container)'Old - Index_Type'First + 1))); + M.Range_Shifted + (Left => Model (New_Item), + Right => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (New_Item), + Offset => + Count_Type + (Last_Index (Container)'Old - Index_Type'First + 1))); - procedure Append - (Container : in out Vector; - New_Item : Element_Type) - with + procedure Append (Container : in out Vector; New_Item : Element_Type) with Global => null, Pre => Length (Container) < Capacity (Container), Post => @@ -541,17 +536,14 @@ is -- New_Item is inserted Count times at the end of Container and (if Count > 0 then - M.Constant_Range - (Container => Model (Container), - Fst => Last_Index (Container)'Old + 1, - Lst => - Last_Index (Container)'Old + Index_Type'Base (Count), - Item => New_Item)); + M.Constant_Range + (Container => Model (Container), + Fst => Last_Index (Container)'Old + 1, + Lst => + Last_Index (Container)'Old + Index_Type'Base (Count), + Item => New_Item)); - procedure Delete - (Container : in out Vector; - Index : Extended_Index) - with + procedure Delete (Container : in out Vector; Index : Extended_Index) with Global => null, Pre => Index in First_Index (Container) .. Last_Index (Container), Post => @@ -613,9 +605,7 @@ is Lst => Last_Index (Container), Offset => Count)); - procedure Delete_First - (Container : in out Vector) - with + procedure Delete_First (Container : in out Vector) with Global => null, Pre => Length (Container) > 0, Post => @@ -630,10 +620,7 @@ is Lst => Last_Index (Container), Offset => 1); - procedure Delete_First - (Container : in out Vector; - Count : Count_Type) - with + procedure Delete_First (Container : in out Vector; Count : Count_Type) with Global => null, Contract_Cases => @@ -653,9 +640,7 @@ is Lst => Last_Index (Container), Offset => Count)); - procedure Delete_Last - (Container : in out Vector) - with + procedure Delete_Last (Container : in out Vector) with Global => null, Pre => Length (Container) > 0, Post => @@ -665,10 +650,7 @@ is and Model (Container) < Model (Container)'Old; - procedure Delete_Last - (Container : in out Vector; - Count : Count_Type) - with + procedure Delete_Last (Container : in out Vector; Count : Count_Type) with Global => null, Contract_Cases => @@ -687,10 +669,15 @@ is Global => null, Post => M_Elements_Reversed (Model (Container)'Old, Model (Container)); - procedure Swap (Container : in out Vector; I, J : Index_Type) with + procedure Swap + (Container : in out Vector; + I : Index_Type; + J : Index_Type) + with Global => null, - Pre => I in First_Index (Container) .. Last_Index (Container) - and then J in First_Index (Container) .. Last_Index (Container), + Pre => + I in First_Index (Container) .. Last_Index (Container) + and then J in First_Index (Container) .. Last_Index (Container), Post => M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J); @@ -731,11 +718,11 @@ is -- returns No_Index. (Index > Last_Index (Container) - or else not M.Contains - (Container => Model (Container), - Fst => Index, - Lst => Last_Index (Container), - Item => Item) + or else not M.Contains + (Container => Model (Container), + Fst => Index, + Lst => Last_Index (Container), + Item => Item) => Find_Index'Result = No_Index, @@ -780,7 +767,7 @@ is -- Index others => - Reverse_Find_Index'Result in Index_Type'First .. Index + Reverse_Find_Index'Result in Index_Type'First .. Index and Reverse_Find_Index'Result <= Last_Index (Container) -- The element at this index in Container is Item @@ -793,8 +780,10 @@ is (Container => Model (Container), Fst => Reverse_Find_Index'Result + 1, Lst => - (if Index <= Last_Index (Container) then Index - else Last_Index (Container)), + (if Index <= Last_Index (Container) then + Index + else + Last_Index (Container)), Item => Item)); function Contains @@ -803,10 +792,12 @@ is with Global => null, Post => - Contains'Result = M.Contains (Container => Model (Container), - Fst => Index_Type'First, - Lst => Last_Index (Container), - Item => Item); + Contains'Result = + M.Contains + (Container => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (Container), + Item => Item); function Has_Element (Container : Vector; @@ -828,8 +819,8 @@ is 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))); + Element (Container, I) = Element (Container, J) + or Element (Container, I) < Element (Container, J))); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted); function Is_Sorted (Container : Vector) return Boolean with @@ -841,14 +832,16 @@ is Post => Length (Container) = Length (Container)'Old and M_Elements_Sorted (Model (Container)) - and M_Elements_Included (Left => Model (Container)'Old, - L_Lst => Last_Index (Container), - Right => Model (Container), - R_Lst => Last_Index (Container)) - and M_Elements_Included (Left => Model (Container), - L_Lst => Last_Index (Container), - Right => Model (Container)'Old, - R_Lst => Last_Index (Container)); + and M_Elements_Included + (Left => Model (Container)'Old, + L_Lst => Last_Index (Container), + Right => Model (Container), + R_Lst => Last_Index (Container)) + and M_Elements_Included + (Left => Model (Container), + L_Lst => Last_Index (Container), + Right => Model (Container)'Old, + R_Lst => Last_Index (Container)); procedure Merge (Target : in out Vector; Source : in out Vector) with -- Target and Source should not be aliased @@ -859,18 +852,22 @@ is and Length (Source) = 0 and (if M_Elements_Sorted (Model (Target)'Old) and M_Elements_Sorted (Model (Source)'Old) - then M_Elements_Sorted (Model (Target))) - and M_Elements_Included (Left => Model (Target)'Old, - L_Lst => Last_Index (Target)'Old, - Right => Model (Target), - R_Lst => Last_Index (Target)) - and M_Elements_Included (Left => Model (Source)'Old, - L_Lst => Last_Index (Source)'Old, - Right => Model (Target), - R_Lst => Last_Index (Target)) - and M_Elements_In_Union (Model (Target), - Model (Source)'Old, - Model (Target)'Old); + then + M_Elements_Sorted (Model (Target))) + and M_Elements_Included + (Left => Model (Target)'Old, + L_Lst => Last_Index (Target)'Old, + Right => Model (Target), + R_Lst => Last_Index (Target)) + and M_Elements_Included + (Left => Model (Source)'Old, + L_Lst => Last_Index (Source)'Old, + Right => Model (Target), + R_Lst => Last_Index (Target)) + and M_Elements_In_Union + (Model (Target), + Model (Source)'Old, + Model (Target)'Old); end Generic_Sorting; private @@ -891,9 +888,11 @@ private type Elements_Array_Ptr is access all Elements_Array; type Vector (Capacity : Capacity_Range) is limited record + -- In the bounded case, the elements are stored in Elements. In the -- unbounded case, the elements are initially stored in Elements, until -- we run out of room, then we switch to Elements_Ptr. + Last : Extended_Index := No_Index; Elements_Ptr : Elements_Array_Ptr := null; Elements : aliased Elements_Array (1 .. Capacity); diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb index 6a6766d8692..81327c4312a 100644 --- a/gcc/ada/exp_ch9.adb +++ b/gcc/ada/exp_ch9.adb @@ -7509,21 +7509,16 @@ package body Exp_Ch9 is Cancel_Param := Make_Defining_Identifier (Loc, Name_uC); - -- Insert declaration of C in declarations of existing block + -- Insert the declaration of C in the declarations of the existing + -- block. The variable is initialized to something (True or False, + -- does not matter) to prevent CodePeer from complaining about a + -- possible read of an uninitialized variable. Prepend_To (Decls, Make_Object_Declaration (Loc, Defining_Identifier => Cancel_Param, - Object_Definition => - New_Occurrence_Of (Standard_Boolean, Loc), - Expression => - New_Occurrence_Of (Standard_False, Loc), - -- True would work equally well here. This initialization - -- should be dead, but only because of things (e.g., - -- abortion deferral) that CodePeer doesn't know about. - -- We want to avoid CodePeer complaints about a possible read - -- of an uninitialized variable when this variable is read, - -- so we initialize it here. + Object_Definition => New_Occurrence_Of (Standard_Boolean, Loc), + Expression => New_Occurrence_Of (Standard_False, Loc), Has_Init_Expression => True)); -- Remove and save the call to Call_Simple diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 0828c9b5b7f..4d923a09841 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -1114,13 +1114,11 @@ package body Exp_Util is if Present (New_E) then Rewrite (N, New_Occurrence_Of (New_E, Sloc (N))); - -- If the entity is an overridden primitive and we are not - -- in proof mode, we must build a wrapper for the current + -- If the entity is an overridden primitive and we are not in + -- GNATprove mode, we must build a wrapper for the current -- inherited operation. - if Is_Subprogram (New_E) - and then not GNATprove_Mode - then + if Is_Subprogram (New_E) and then not GNATprove_Mode then Needs_Wrapper := True; end if; end if; diff --git a/gcc/ada/g-dyntab.adb b/gcc/ada/g-dyntab.adb index e011ad849ad..8210419844c 100644 --- a/gcc/ada/g-dyntab.adb +++ b/gcc/ada/g-dyntab.adb @@ -280,7 +280,7 @@ package body GNAT.Dynamic_Tables is Old_Table : Old_Alloc_Ptr := To_Old_Alloc_Ptr (T.Table); New_Table : constant Alloc_Ptr := - new Alloc_Type'(Old_Table (Alloc_Type'Range)); + new Alloc_Type'(Old_Table (Alloc_Type'Range)); begin T.P.Last_Allocated := T.P.Last; Free (Old_Table); diff --git a/gcc/ada/sem_dim.adb b/gcc/ada/sem_dim.adb index cac2af53011..1dd8410b000 100644 --- a/gcc/ada/sem_dim.adb +++ b/gcc/ada/sem_dim.adb @@ -2154,9 +2154,9 @@ package body Sem_Dim is if Dim_Of_Expr /= Dim_Of_Etyp then - -- Numeric literal case. Issue a warning if the object type is not - -- dimensionless to indicate the literal is treated as if its - -- dimension matches the type dimension. + -- Numeric literal case. Issue a warning if the object type is + -- not dimensionless to indicate the literal is treated as if + -- its dimension matches the type dimension. if Nkind_In (Original_Node (Expr), N_Real_Literal, N_Integer_Literal) @@ -2171,8 +2171,8 @@ package body Sem_Dim is Set_Dimensions (Id, Dim_Of_Expr); - -- Expression may have been constant-folded. If nominal type - -- has dimensions, verify that expression has same type. + -- Expression may have been constant-folded. If nominal type has + -- dimensions, verify that expression has same type. elsif Exists (Dim_Of_Etyp) and then Etype (Expr) = Etyp then null; @@ -2184,8 +2184,8 @@ package body Sem_Dim is end if; end if; - -- Remove dimensions in expression after checking consistency - -- with given type. + -- Remove dimensions in expression after checking consistency with + -- given type. Remove_Dimensions (Expr); end if;