From: Arnaud Charlet Date: Thu, 27 Apr 2017 10:52:44 +0000 (+0200) Subject: [multiple changes] X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=78f2b7ce3aea49818ea97974cb41029f820d0a99;p=gcc.git [multiple changes] 2017-04-27 Ed Schonberg * freeze.adb: copy-paste typo. 2017-04-27 Yannick Moy * sem_prag.adb (Analyze_Pre_Post_In_Decl_Part): Use correct test to detect call in GNATprove mode instead of compilation. 2017-04-27 Claire Dross * a-cfdlli.adb, a-cfdlli.ads (Formal_Model.M_Elements_In_Union): New property function expressing that the element of a sequence are contained in the union of two sequences. (Formal_Model.M_Elements_Included): New property function expressing that the element of a sequence are another sequence. (Generic_Sorting): Use new property functions to state that elements are preserved by Sort and Merge. * a-cofove.adb, a-cofove.ads (=): Generic parameter removed to allow the use of regular equality over elements in contracts. (Formal_Model): Ghost package containing model functions that are used in subprogram contracts. (Capacity): On unbounded containers, return the maximal capacity. (Current_To_Last): Removed, model functions should be used instead. (First_To_Previous): Removed, model functions should be used instead. (Append): Default parameter value replaced by new wrapper to allow more precise contracts. (Insert): Subprogram restored, it seems it was useful to users even if it is inefficient. (Delete): Subprogram restored, it seems it was useful to users even if it is inefficient. (Prepend): Subprogram restored, it seems it was useful to users even if it is inefficient. (Delete_First): Subprogram restored, it seems it was useful to users even if it is inefficient. (Delete_Last): Default parameter value replaced by new wrapper to allow more precise contracts. (Generic_Sorting.Merge): Subprogram restored. * a-cfinve.adb, a-cfinve.ads (=): Generic parameter removed to allow the use of regular equality over elements in contracts. (Formal_Model): Ghost package containing model functions that are used in subprogram contracts. (Capacity): On unbounded containers, return the maximal capacity. (Current_To_Last): Removed, model functions should be used instead. (First_To_Previous): Removed, model functions should be used instead. (Append): Default parameter value replaced by new wrapper to allow more precise contracts. (Insert): Subprogram restored, it seems it was useful to users even if it is inefficient. (Delete): Subprogram restored, it seems it was useful to users even if it is inefficient. (Prepend): Subprogram restored, it seems it was useful to users even if it is inefficient. (Delete_First): Subprogram restored, it seems it was useful to users even if it is inefficient. (Delete_Last): Default parameter value replaced by new wrapper to allow more precise contracts. (Generic_Sorting.Merge): Subprogram restored. (Vector): Do not reuse formal vectors, as it is no longer possible to supply them with an equality function over elements. 2017-04-27 Bob Duff * g-dyntab.adb (Release): When allocating the new table, use the correct slice of the old table to initialize it. From-SVN: r247316 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 88ad07dfa92..f06d94eff59 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,71 @@ +2017-04-27 Ed Schonberg + + * freeze.adb: copy-paste typo. + +2017-04-27 Yannick Moy + + * sem_prag.adb (Analyze_Pre_Post_In_Decl_Part): + Use correct test to detect call in GNATprove mode instead of + compilation. + +2017-04-27 Claire Dross + + * a-cfdlli.adb, a-cfdlli.ads (Formal_Model.M_Elements_In_Union): + New property function expressing that the element of a + sequence are contained in the union of two sequences. + (Formal_Model.M_Elements_Included): New property function + expressing that the element of a sequence are another sequence. + (Generic_Sorting): Use new property functions to state that + elements are preserved by Sort and Merge. + * a-cofove.adb, a-cofove.ads (=): Generic parameter removed to + allow the use of regular equality over elements in contracts. + (Formal_Model): Ghost package containing model functions + that are used in subprogram contracts. (Capacity): + On unbounded containers, return the maximal capacity. + (Current_To_Last): Removed, model functions should be used instead. + (First_To_Previous): Removed, model functions should be used instead. + (Append): Default parameter value replaced + by new wrapper to allow more precise contracts. + (Insert): Subprogram restored, it seems it was useful to users even if + it is inefficient. + (Delete): Subprogram restored, it seems it was useful to users even if + it is inefficient. + (Prepend): Subprogram restored, it seems it was useful to users even + if it is inefficient. + (Delete_First): Subprogram restored, it seems it + was useful to users even if it is inefficient. (Delete_Last): + Default parameter value replaced by new wrapper to allow more + precise contracts. + (Generic_Sorting.Merge): Subprogram restored. + * a-cfinve.adb, a-cfinve.ads (=): Generic parameter removed to + allow the use of regular equality over elements in contracts. + (Formal_Model): Ghost package containing model functions + that are used in subprogram contracts. (Capacity): + On unbounded containers, return the maximal capacity. + (Current_To_Last): Removed, model functions should be used + instead. + (First_To_Previous): Removed, model functions should be used instead. + (Append): Default parameter value replaced + by new wrapper to allow more precise contracts. + (Insert): Subprogram restored, it seems it was useful to users even if + it is inefficient. + (Delete): Subprogram restored, it seems it was useful to users even if + it is inefficient. + (Prepend): Subprogram restored, it seems it was useful to users even + if it is inefficient. + (Delete_First): Subprogram restored, it seems it + was useful to users even if it is inefficient. (Delete_Last): + Default parameter value replaced by new wrapper to allow more + precise contracts. + (Generic_Sorting.Merge): Subprogram restored. + (Vector): Do not reuse formal vectors, as it is no longer possible + to supply them with an equality function over elements. + +2017-04-27 Bob Duff + + * g-dyntab.adb (Release): When allocating the new + table, use the correct slice of the old table to initialize it. + 2017-04-27 Eric Botcazou * einfo.ads: Minor fixes in comments. diff --git a/gcc/ada/a-cfdlli.adb b/gcc/ada/a-cfdlli.adb index 84596ee2850..6c9c0b0f93e 100644 --- a/gcc/ada/a-cfdlli.adb +++ b/gcc/ada/a-cfdlli.adb @@ -488,54 +488,70 @@ is procedure Lift_Abstraction_Level (Container : List) is null; ------------------------- - -- M_Elements_Reversed -- + -- M_Elements_In_Union -- ------------------------- - function M_Elements_Reversed - (Left : M.Sequence; - Right : M.Sequence) return Boolean + function M_Elements_In_Union + (Container : M.Sequence; + Left : M.Sequence; + Right : M.Sequence) return Boolean is - L : constant Count_Type := M.Length (Left); - begin - if L /= M.Length (Right) then - return False; - end if; + for I in 1 .. M.Length (Container) loop + declare + Found : Boolean := False; + J : Count_Type := 0; - for I in 1 .. L loop - if Element (Left, I) /= Element (Right, L - I + 1) - then - return False; - end if; + 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; + + 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; + + if not Found then + return False; + end if; + end; end loop; return True; - end M_Elements_Reversed; + end M_Elements_In_Union; ------------------------- - -- M_Elements_Shuffled -- + -- M_Elements_Included -- ------------------------- - function M_Elements_Shuffle - (Left : M.Sequence; - Right : M.Sequence; - Fst : Positive_Count_Type; - Lst : Count_Type; - Offset : Count_Type'Base) return Boolean + function M_Elements_Included + (Left : M.Sequence; + L_Fst : Positive_Count_Type := 1; + L_Lst : Count_Type; + Right : M.Sequence; + R_Fst : Positive_Count_Type := 1; + R_Lst : Count_Type) return Boolean is begin - for I in Fst .. Lst loop + for I in L_Fst .. L_Lst loop declare Found : Boolean := False; - J : Count_Type := Fst; + J : Count_Type := R_Fst - 1; begin - while not Found and J <= Lst loop - if Element (Left, I) = Element (Right, J + Offset) then + while not Found and J < R_Lst loop + J := J + 1; + if Element (Left, I) = Element (Right, J) then Found := True; end if; - - J := J + 1; end loop; if not Found then @@ -545,7 +561,32 @@ is end loop; return True; - end M_Elements_Shuffle; + end M_Elements_Included; + + ------------------------- + -- M_Elements_Reversed -- + ------------------------- + + function M_Elements_Reversed + (Left : M.Sequence; + Right : M.Sequence) return Boolean + is + L : constant Count_Type := M.Length (Left); + + begin + if L /= M.Length (Right) then + return False; + end if; + + for I in 1 .. L loop + if Element (Left, I) /= Element (Right, L - I + 1) + then + return False; + end if; + end loop; + + return True; + end M_Elements_Reversed; ------------------------ -- M_Elements_Swapted -- @@ -892,7 +933,8 @@ is begin if Target'Address = Source'Address then - return; + raise Program_Error with + "Target and Source denote same container"; end if; LI := First (Target); @@ -1466,7 +1508,7 @@ is begin if CFirst = 0 then - CFirst := Container.First; + CFirst := Container.Last; end if; if Container.Length = 0 then @@ -1497,14 +1539,13 @@ is SN : Node_Array renames Source.Nodes; begin - if Before.Node /= 0 then - pragma Assert (Vet (Target, Before), "bad cursor in Splice"); + if Target'Address = Source'Address then + raise Program_Error with + "Target and Source denote same container"; end if; - if Target'Address = Source'Address - or else Source.Length = 0 - then - return; + if Before.Node /= 0 then + pragma Assert (Vet (Target, Before), "bad cursor in Splice"); end if; pragma Assert (SN (Source.First).Prev = 0); @@ -1535,8 +1576,8 @@ is begin if Target'Address = Source'Address then - Splice (Target, Before, Position); - return; + raise Program_Error with + "Target and Source denote same container"; end if; if Position.Node = 0 then diff --git a/gcc/ada/a-cfdlli.ads b/gcc/ada/a-cfdlli.ads index b60a6fe4b13..5c07c12b4be 100644 --- a/gcc/ada/a-cfdlli.ads +++ b/gcc/ada/a-cfdlli.ads @@ -81,25 +81,40 @@ is (Left : M.Sequence; Right : M.Sequence) return Boolean renames M."<="; - function M_Elements_Shuffle - (Left : M.Sequence; - Right : M.Sequence; - Fst : Positive_Count_Type; - Lst : Count_Type; - Offset : Count_Type'Base) return Boolean - -- The slice from Fst to Lst in Left contains the same elements than the - -- same slide shifted by Offset in Right + function M_Elements_In_Union + (Container : M.Sequence; + Left : M.Sequence; + Right : M.Sequence) return Boolean + -- The elements of Container are contained in either Left or Right with Global => null, - Pre => - Lst <= M.Length (Left) - and Offset in 1 - Fst .. M.Length (Right) - Lst, Post => - M_Elements_Shuffle'Result = - (for all J in Fst + Offset .. Lst + Offset => - (for some I in Fst .. Lst => + M_Elements_In_Union'Result = + (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))); + pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union); + + function M_Elements_Included + (Left : M.Sequence; + L_Fst : Positive_Count_Type := 1; + L_Lst : Count_Type; + Right : M.Sequence; + R_Fst : Positive_Count_Type := 1; + R_Lst : Count_Type) return Boolean + -- The elements of the slice from L_Fst to L_Lst in Left are contained + -- in the slide from R_Fst to R_Lst in Right. + with + Global => null, + Pre => L_Lst <= M.Length (Left) and R_Lst <= M.Length (Right), + Post => + M_Elements_Included'Result = + (for all I in L_Fst .. L_Lst => + (for some J in R_Fst .. R_Lst => Element (Left, I) = Element (Right, J))); - pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Shuffle); + pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Included); function M_Elements_Reversed (Left : M.Sequence; @@ -242,7 +257,7 @@ is M.Get (M_Right, P.Get (P_Right, C)))); function Model (Container : List) return M.Sequence with - -- The highlevel model of a list is a sequence of elements. Cursors are + -- The high-level model of a list is a sequence of elements. Cursors are -- not represented in this model. Ghost, @@ -279,8 +294,8 @@ is -- assume that we can access to the same elements by iterating over -- positions or cursors. -- This information is not generally useful except when switching from - -- a lowlevel, cursor aware view of a container, to a highlevel - -- position based view. + -- a low-level cursor-aware view of a container to a high-level + -- position-based view. Ghost, Global => null, @@ -466,6 +481,15 @@ 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)) + + -- Container contains Count times New_Item at the end + and M.Constant_Range (Container => Model (Container), Fst => Length (Container)'Old + 1, @@ -747,11 +771,12 @@ is -- Container contains Count times New_Item at the end - and M.Constant_Range - (Container => Model (Container), - Fst => Length (Container)'Old + 1, - Lst => Length (Container), - Item => New_Item) + and (if Count > 0 then + 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 @@ -782,11 +807,11 @@ is -- The elements located after Position are shifted by 1 and M.Range_Shifted - (Left => Model (Container)'Old, - Right => Model (Container), - Fst => P.Get (Positions (Container)'Old, Position'Old) + 1, - Lst => Length (Container)'Old, - Offset => -1) + (Left => Model (Container), + Right => Model (Container)'Old, + Fst => P.Get (Positions (Container)'Old, Position'Old), + Lst => Length (Container), + Offset => 1) -- Position has been removed from Container @@ -840,12 +865,11 @@ is -- Other elements are shifted by Count and M.Range_Shifted - (Left => Model (Container)'Old, - Right => Model (Container), - Fst => - P.Get (Positions (Container)'Old, Position'Old) + Count, - Lst => Length (Container)'Old, - Offset => -Count) + (Left => Model (Container), + Right => Model (Container)'Old, + Fst => P.Get (Positions (Container)'Old, Position'Old), + Lst => Length (Container), + Offset => Count) -- Count cursors have been removed from Container at Position @@ -864,11 +888,11 @@ is -- The elements of Container are shifted by 1 and M.Range_Shifted - (Left => Model (Container)'Old, - Right => Model (Container), - Fst => 2, - Lst => Length (Container)'Old, - Offset => -1) + (Left => Model (Container), + Right => Model (Container)'Old, + Fst => 1, + Lst => Length (Container), + Offset => 1) -- The first cursor of Container has been removed @@ -892,11 +916,11 @@ is -- Elements of Container are shifted by Count and M.Range_Shifted - (Left => Model (Container)'Old, - Right => Model (Container), - Fst => Count + 1, - Lst => Length (Container)'Old, - Offset => -Count) + (Left => Model (Container), + Right => Model (Container)'Old, + Fst => 1, + Lst => Length (Container), + Offset => Count) -- The first Count cursors have been removed from Container @@ -957,7 +981,7 @@ is procedure Reverse_Elements (Container : in out List) with Global => null, - Post => M_Elements_Reversed (Model (Container'Old), Model (Container)); + Post => M_Elements_Reversed (Model (Container)'Old, Model (Container)); procedure Swap (Container : in out List; @@ -1017,12 +1041,19 @@ is -- The elements of Source are appended to target, the order is not -- specified. - and M_Elements_Shuffle + and M_Elements_Included (Left => Model (Source)'Old, + L_Lst => Length (Source)'Old, Right => Model (Target), - Fst => 1, - Lst => Length (Source)'Old, - Offset => Length (Target)'Old) + R_Fst => Length (Target)'Old + 1, + R_Lst => Length (Target)) + + and M_Elements_Included + (Left => Model (Target), + L_Fst => Length (Target)'Old + 1, + L_Lst => Length (Target), + Right => Model (Source)'Old, + R_Lst => Length (Source)'Old) -- Cursors have been inserted at the end of Target @@ -1045,12 +1076,22 @@ is -- The elements of Source are inserted before Before, the order is -- not specified. - and M_Elements_Shuffle - (Left => Model (Source)'Old, - Right => Model (Target), - Fst => 1, - Lst => Length (Source)'Old, - Offset => P.Get (Positions (Target)'Old, Before) - 1) + and M_Elements_Included + (Left => Model (Source)'Old, + L_Lst => Length (Source)'Old, + Right => Model (Target), + R_Fst => P.Get (Positions (Target)'Old, Before), + R_Lst => + P.Get (Positions (Target)'Old, Before) - 1 + + Length (Source)'Old) + + and M_Elements_Included + (Left => Model (Target), + L_Fst => P.Get (Positions (Target)'Old, Before), + L_Lst => P.Get (Positions (Target)'Old, Before) - 1 + + Length (Source)'Old, + Right => Model (Source)'Old, + R_Lst => Length (Source)'Old) -- Other elements are shifted by the length of Source @@ -1390,7 +1431,7 @@ is P.Get (Positions (Container), Find'Result) >= P.Get (Positions (Container), Position)) - -- It is the first occurence of Item in this slice + -- It is the first occurrence of Item in this slice and not M.Contains (Container => Model (Container), @@ -1445,7 +1486,7 @@ is P.Get (Positions (Container), Reverse_Find'Result) <= P.Get (Positions (Container), Position)) - -- It is the last occurence of Item in this slice + -- It is the last occurrence of Item in this slice and not M.Contains (Container => Model (Container), @@ -1489,7 +1530,7 @@ is Post => M_Elements_Sorted'Result = (for all I in 1 .. M.Length (Container) => - (for all J in I + 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))); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted); @@ -1502,7 +1543,15 @@ is Global => null, Post => Length (Container) = Length (Container)'Old - and M_Elements_Sorted (Model (Container)); + 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)); procedure Merge (Target : in out List; Source : in out List) with -- Target and Source should not be aliased @@ -1513,7 +1562,18 @@ 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))); + 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 b520d65f020..8b29f5e549a 100644 --- a/gcc/ada/a-cfinve.adb +++ b/gcc/ada/a-cfinve.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2014-2015, Free Software Foundation, Inc. -- +-- Copyright (C) 2010-2017, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -25,6 +25,11 @@ -- . -- ------------------------------------------------------------------------------ +with Ada.Containers.Generic_Array_Sort; +with Ada.Unchecked_Deallocation; + +with System; use type System.Address; + package body Ada.Containers.Formal_Indefinite_Vectors with SPARK_Mode => Off is @@ -32,12 +37,68 @@ is function H (New_Item : Element_Type) return Holder renames To_Holder; function E (Container : Holder) return Element_Type renames Get; + Growth_Factor : constant := 2; + -- When growing a container, multiply current capacity by this. Doubling + -- leads to amortized linear-time copying. + + type Int is range System.Min_Int .. System.Max_Int; + + procedure Free is + 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; + + function Elems (Container : in out Vector) return Maximal_Array_Ptr; + function Elemsc + (Container : Vector) return Maximal_Array_Ptr_Const; + -- Returns a pointer to the Elements array currently in use -- either + -- Container.Elements_Ptr or a pointer to Container.Elements. We work with + -- pointers to a bogus array subtype that is constrained with the maximum + -- possible bounds. This means that the pointer is a thin pointer. This is + -- necessary because 'Unrestricted_Access doesn't work when it produces + -- access-to-unconstrained and is returned from a function. + -- + -- Note that this is dangerous: make sure calls to this use an indexed + -- component or slice that is within the bounds 1 .. Length (Container). + + function Get_Element + (Container : Vector; + Position : Capacity_Range) return Element_Type; + + function To_Array_Index (Index : Index_Type'Base) return Count_Type'Base; + + function Current_Capacity (Container : Vector) return Capacity_Range; + + procedure Insert_Space + (Container : in out Vector; + Before : Extended_Index; + Count : Count_Type := 1); + --------- -- "=" -- --------- function "=" (Left, Right : Vector) return Boolean is - (Left.V = Right.V); + begin + if Left'Address = Right'Address then + return True; + end if; + + if Length (Left) /= Length (Right) then + return False; + end if; + + for J in 1 .. Length (Left) loop + if Get_Element (Left, J) /= Get_Element (Right, J) then + return False; + end if; + end loop; + + return True; + end "="; ------------ -- Append -- @@ -45,7 +106,15 @@ is procedure Append (Container : in out Vector; New_Item : Vector) is begin - Append (Container.V, New_Item.V); + if Is_Empty (New_Item) then + return; + end if; + + if Container.Last >= Index_Type'Last then + raise Constraint_Error with "vector is already at its maximum length"; + end if; + + Insert (Container, Container.Last + 1, New_Item); end Append; procedure Append @@ -53,7 +122,24 @@ is New_Item : Element_Type) is begin - Append (Container.V, H (New_Item)); + Append (Container, New_Item, 1); + end Append; + + procedure Append + (Container : in out Vector; + New_Item : Element_Type; + Count : Count_Type) + is + begin + if Count = 0 then + return; + end if; + + if Container.Last >= Index_Type'Last then + raise Constraint_Error with "vector is already at its maximum length"; + end if; + + Insert (Container, Container.Last + 1, New_Item, Count); end Append; ------------ @@ -61,8 +147,19 @@ is ------------ procedure Assign (Target : in out Vector; Source : Vector) is + LS : constant Capacity_Range := Length (Source); + begin - Assign (Target.V, Source.V); + if Target'Address = Source'Address then + return; + end if; + + if Bounded and then Target.Capacity < LS then + raise Constraint_Error; + end if; + + Clear (Target); + Append (Target, Source); end Assign; -------------- @@ -70,7 +167,10 @@ is -------------- function Capacity (Container : Vector) return Capacity_Range is - (Capacity (Container.V)); + begin + return (if Bounded then Container.Capacity + else Capacity_Range'Last); + end Capacity; ----------- -- Clear -- @@ -78,7 +178,11 @@ is procedure Clear (Container : in out Vector) is begin - Clear (Container.V); + Container.Last := No_Index; + + -- Free element, note that this is OK if Elements_Ptr is null + + Free (Container.Elements_Ptr); end Clear; -------------- @@ -89,7 +193,9 @@ is (Container : Vector; Item : Element_Type) return Boolean is - (Contains (Container.V, H (Item))); + begin + return Find_Index (Container, Item) /= No_Index; + end Contains; ---------- -- Copy -- @@ -99,19 +205,173 @@ is (Source : Vector; Capacity : Capacity_Range := 0) return Vector is - ((if Capacity = 0 then Length (Source) else Capacity), - V => Copy (Source.V, Capacity)); + LS : constant Capacity_Range := Length (Source); + C : Capacity_Range; - --------------------- - -- Current_To_Last -- - --------------------- + begin + if Capacity = 0 then + C := LS; + elsif Capacity >= LS then + C := Capacity; + else + raise Capacity_Error; + end if; - function Current_To_Last - (Container : Vector; - Current : Index_Type) return Vector is + return Target : Vector (C) do + Elems (Target) (1 .. LS) := Elemsc (Source) (1 .. LS); + Target.Last := Source.Last; + end return; + end Copy; + + ---------------------- + -- Current_Capacity -- + ---------------------- + + 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); + end Current_Capacity; + + ------------ + -- Delete -- + ------------ + + procedure Delete + (Container : in out Vector; + Index : Extended_Index) + is + begin + Delete (Container, Index, 1); + end Delete; + + procedure Delete + (Container : in out Vector; + Index : Extended_Index; + Count : Count_Type) + is + Old_Last : constant Index_Type'Base := Container.Last; + Old_Len : constant Count_Type := Length (Container); + New_Last : Index_Type'Base; + Count2 : Count_Type'Base; -- count of items from Index to Old_Last + Off : Count_Type'Base; -- Index expressed as offset from IT'First + + begin + -- Delete removes items from the vector, the number of which is the + -- minimum of the specified Count and the items (if any) that exist from + -- Index to Container.Last. There are no constraints on the specified + -- value of Count (it can be larger than what's available at this + -- position in the vector, for example), but there are constraints on + -- the allowed values of the Index. + + -- As a precondition on the generic actual Index_Type, the base type + -- must include Index_Type'Pred (Index_Type'First); this is the value + -- that Container.Last assumes when the vector is empty. However, we do + -- not allow that as the value for Index when specifying which items + -- should be deleted, so we must manually check. (That the user is + -- allowed to specify the value at all here is a consequence of the + -- declaration of the Extended_Index subtype, which includes the values + -- in the base range that immediately precede and immediately follow the + -- values in the Index_Type.) + + if Index < Index_Type'First then + raise Constraint_Error with "Index is out of range (too small)"; + end if; + + -- We do allow a value greater than Container.Last to be specified as + -- the Index, but only if it's immediately greater. This allows the + -- corner case of deleting no items from the back end of the vector to + -- be treated as a no-op. (It is assumed that specifying an index value + -- greater than Last + 1 indicates some deeper flaw in the caller's + -- algorithm, so that case is treated as a proper error.) + + if Index > Old_Last then + if Index > Old_Last + 1 then + raise Constraint_Error with "Index is out of range (too large)"; + end if; + + return; + end if; + + if Count = 0 then + return; + end if; + + -- We first calculate what's available for deletion starting at + -- Index. Here and elsewhere we use the wider of Index_Type'Base and + -- Count_Type'Base as the type for intermediate values. (See function + -- Length for more information.) + + if Count_Type'Base'Last >= Index_Type'Pos (Index_Type'Base'Last) then + Count2 := Count_Type'Base (Old_Last) - Count_Type'Base (Index) + 1; + else + Count2 := Count_Type'Base (Old_Last - Index + 1); + end if; + + -- If more elements are requested (Count) for deletion than are + -- available (Count2) for deletion beginning at Index, then everything + -- from Index is deleted. There are no elements to slide down, and so + -- all we need to do is set the value of Container.Last. + + if Count >= Count2 then + Container.Last := Index - 1; + return; + end if; + + -- There are some elements that 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. + + if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then + Off := Count_Type'Base (Index - Index_Type'First); + New_Last := Old_Last - Index_Type'Base (Count); + else + Off := Count_Type'Base (Index) - Count_Type'Base (Index_Type'First); + New_Last := Index_Type'Base (Count_Type'Base (Old_Last) - Count); + end if; + + -- The array index values for each slice have already been determined, + -- so we just slide down to Index the elements that weren't deleted. + + 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; + end; + end Delete; + + ------------------ + -- Delete_First -- + ------------------ + + 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 begin - return (Length (Container), Current_To_Last (Container.V, Current)); - end Current_To_Last; + if Count = 0 then + return; + + elsif Count >= Length (Container) then + Clear (Container); + return; + + else + Delete (Container, Index_Type'First, Count); + end if; + end Delete_First; ----------------- -- Delete_Last -- @@ -121,7 +381,38 @@ is (Container : in out Vector) is begin - Delete_Last (Container.V); + Delete_Last (Container, 1); + end Delete_Last; + + procedure Delete_Last + (Container : in out Vector; + Count : Count_Type) + is + begin + if Count = 0 then + return; + end if; + + -- There is no restriction on how large Count can be when deleting + -- items. If it is equal or greater than the current length, then this + -- is equivalent to clearing the vector. (In particular, there's no need + -- for us to actually calculate the new value for Last.) + + -- If the requested count is less than the current length, then we must + -- calculate the new value for Last. For the type we use the widest of + -- Index_Type'Base and Count_Type'Base for the intermediate values of + -- our calculation. (See the comments in Length for more information.) + + if Count >= Length (Container) then + Container.Last := No_Index; + + elsif Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then + Container.Last := Container.Last - Index_Type'Base (Count); + + else + Container.Last := + Index_Type'Base (Count_Type'Base (Container.Last) - Count); + end if; end Delete_Last; ------------- @@ -130,8 +421,39 @@ is function Element (Container : Vector; - Index : Index_Type) return Element_Type is - (E (Element (Container.V, Index))); + Index : Index_Type) return Element_Type + is + begin + if Index > Container.Last then + raise Constraint_Error with "Index is out of range"; + end if; + + declare + II : constant Int'Base := Int (Index) - Int (No_Index); + I : constant Capacity_Range := Capacity_Range (II); + begin + return Get_Element (Container, I); + end; + end Element; + + -------------- + -- Elements -- + -------------- + + 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); + end Elems; + + 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); + end Elemsc; ---------------- -- Find_Index -- @@ -142,32 +464,190 @@ is Item : Element_Type; Index : Index_Type := Index_Type'First) return Extended_Index is - (Find_Index (Container.V, H (Item), Index)); + K : Capacity_Range; + Last : constant Index_Type := Last_Index (Container); + + begin + K := Capacity_Range (Int (Index) - Int (No_Index)); + for Indx in Index .. Last loop + if Get_Element (Container, K) = Item then + return Indx; + end if; + + K := K + 1; + end loop; + + return No_Index; + end Find_Index; ------------------- -- First_Element -- ------------------- function First_Element (Container : Vector) return Element_Type is - (E (First_Element (Container.V))); + begin + if Is_Empty (Container) then + raise Constraint_Error with "Container is empty"; + else + return Get_Element (Container, 1); + end if; + end First_Element; ----------------- -- First_Index -- ----------------- function First_Index (Container : Vector) return Index_Type is - (First_Index (Container.V)); + pragma Unreferenced (Container); + begin + return Index_Type'First; + end First_Index; - ----------------------- - -- First_To_Previous -- - ----------------------- + ------------------ + -- Formal_Model -- + ------------------ - function First_To_Previous - (Container : Vector; - Current : Index_Type) return Vector is - begin - return (Length (Container), First_To_Previous (Container.V, Current)); - end First_To_Previous; + package body Formal_Model is + + ------------------------- + -- M_Elements_In_Union -- + ------------------------- + + function M_Elements_In_Union + (Container : M.Sequence; + 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; + + 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 + return False; + end if; + end; + end loop; + + return True; + end M_Elements_In_Union; + + ------------------------- + -- M_Elements_Included -- + ------------------------- + + function M_Elements_Included + (Left : M.Sequence; + L_Fst : Index_Type := Index_Type'First; + L_Lst : Extended_Index; + Right : M.Sequence; + R_Fst : Index_Type := Index_Type'First; + R_Lst : Extended_Index) return Boolean + is + begin + for I in L_Fst .. L_Lst loop + declare + Found : Boolean := False; + J : Extended_Index := R_Fst - 1; + + begin + while not Found and J < R_Lst loop + J := J + 1; + if Element (Left, I) = Element (Right, J) then + Found := True; + end if; + end loop; + + if not Found then + return False; + end if; + end; + end loop; + + return True; + end M_Elements_Included; + + ------------------------- + -- M_Elements_Reversed -- + ------------------------- + + function M_Elements_Reversed (Left, Right : M.Sequence) return Boolean is + L : constant Index_Type := M.Last (Left); + begin + if L /= M.Last (Right) then + return False; + end if; + + for I in Index_Type'First .. L loop + if Element (Left, I) /= Element (Right, L - I + 1) + then + return False; + end if; + end loop; + + return True; + end M_Elements_Reversed; + + ------------------------ + -- M_Elements_Swapted -- + ------------------------ + + function M_Elements_Swapped + (Left : M.Sequence; + Right : M.Sequence; + X, Y : Index_Type) return Boolean + is + begin + if M.Length (Left) /= M.Length (Right) + or else Element (Left, X) /= Element (Right, Y) + or else Element (Left, Y) /= Element (Right, X) + then + return False; + end if; + + for I in Index_Type'First .. M.Last (Left) loop + if I /= X and then I /= Y + and then Element (Left, I) /= Element (Right, I) + then + return False; + end if; + end loop; + + return True; + end M_Elements_Swapped; + + ----------- + -- Model -- + ----------- + + 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; + + end Formal_Model; --------------------- -- Generic_Sorting -- @@ -175,65 +655,537 @@ is package body Generic_Sorting with SPARK_Mode => Off is - function "<" (X, Y : Holder) return Boolean is (E (X) < E (Y)); - package Def_Sorting is new Def.Generic_Sorting ("<"); - use Def_Sorting; - --------------- -- Is_Sorted -- --------------- function Is_Sorted (Container : Vector) return Boolean is - (Is_Sorted (Container.V)); + 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 + return False; + end if; + end loop; + + return True; + end Is_Sorted; + + ----------------------- + -- M_Elements_Sorted -- + ----------------------- + + function M_Elements_Sorted (Container : M.Sequence) return Boolean is + begin + if M.Length (Container) = 0 then + return True; + end if; + + declare + E1 : Element_Type := Element (Container, Index_Type'First); + + begin + for I in Index_Type'First + 1 .. M.Last (Container) loop + declare + E2 : constant Element_Type := Element (Container, I); + + begin + if E2 < E1 then + return False; + end if; + + E1 := E2; + end; + end loop; + end; + + return True; + end M_Elements_Sorted; ---------- -- 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, + "<" => "<"); + + Len : constant Capacity_Range := Length (Container); begin - Sort (Container.V); + if Container.Last <= Index_Type'First then + return; + else + Sort (Elems (Container) (1 .. Len)); + end if; end Sort; + ----------- + -- Merge -- + ----------- + + procedure Merge (Target, Source : in out Vector) is + I, J : Count_Type; + + begin + if Target'Address = Source'Address then + raise Program_Error with + "Target and Source denote same container"; + end if; + + if Length (Source) = 0 then + return; + end if; + + if Length (Target) = 0 then + Move (Target => Target, Source => Source); + return; + end if; + + I := Length (Target); + + declare + New_Length : constant Count_Type := I + Length (Source); + begin + 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))); + end if; + + if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then + Target.Last := No_Index + Index_Type'Base (New_Length); + + else + Target.Last := + Index_Type'Base (Count_Type'Base (No_Index) + New_Length); + end if; + end; + + declare + TA : Maximal_Array_Ptr renames Elems (Target); + SA : Maximal_Array_Ptr renames Elems (Source); + begin + J := Length (Target); + while Length (Source) /= 0 loop + if I = 0 then + TA (1 .. J) := SA (1 .. Length (Source)); + Source.Last := No_Index; + exit; + end if; + + if E (SA (Length (Source))) < E (TA (I)) then + TA (J) := TA (I); + I := I - 1; + + else + TA (J) := SA (Length (Source)); + Source.Last := Source.Last - 1; + end if; + + J := J - 1; + end loop; + end; + end Merge; + end Generic_Sorting; + ----------------- + -- Get_Element -- + ----------------- + + function Get_Element + (Container : Vector; + Position : Capacity_Range) return Element_Type + is + begin + return E (Elemsc (Container) (Position)); + end Get_Element; + ----------------- -- Has_Element -- ----------------- function Has_Element - (Container : Vector; - Position : Extended_Index) return Boolean + (Container : Vector; Position : Extended_Index) return Boolean is + begin + return Position in First_Index (Container) .. Last_Index (Container); + end Has_Element; + + ------------ + -- Insert -- + ------------ + + procedure Insert + (Container : in out Vector; + Before : Extended_Index; + New_Item : Element_Type) + is + begin + Insert (Container, Before, New_Item, 1); + end Insert; + + procedure Insert + (Container : in out Vector; + Before : Extended_Index; + New_Item : Element_Type; + Count : Count_Type) + is + J : Count_Type'Base; -- scratch + + begin + -- Use Insert_Space to create the "hole" (the destination slice) + + Insert_Space (Container, Before, Count); + + J := To_Array_Index (Before); + + Elems (Container) (J .. J - 1 + Count) := (others => H (New_Item)); + end Insert; + + procedure Insert + (Container : in out Vector; + Before : Extended_Index; + New_Item : Vector) + is + N : constant Count_Type := Length (New_Item); + B : Count_Type; -- index Before converted to Count_Type + + begin + if Container'Address = New_Item'Address then + raise Program_Error with + "Container and New_Item denote same container"; + end if; + + -- Use Insert_Space to create the "hole" (the destination slice) into + -- which we copy the source items. + + 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. + + return; + end if; + + B := To_Array_Index (Before); + + Elems (Container) (B .. B + N - 1) := Elemsc (New_Item) (1 .. N); + end Insert; + + ------------------ + -- Insert_Space -- + ------------------ + + procedure Insert_Space + (Container : in out Vector; + Before : Extended_Index; + Count : Count_Type := 1) is - (Has_Element (Container.V, Position)); + Old_Length : constant Count_Type := Length (Container); + + Max_Length : Count_Type'Base; -- determined from range of Index_Type + New_Length : Count_Type'Base; -- sum of current length and Count + + Index : Index_Type'Base; -- scratch for intermediate values + J : Count_Type'Base; -- scratch + + begin + -- As a precondition on the generic actual Index_Type, the base type + -- must include Index_Type'Pred (Index_Type'First); this is the value + -- that Container.Last assumes when the vector is empty. However, we do + -- not allow that as the value for Index when specifying where the new + -- items should be inserted, so we must manually check. (That the user + -- is allowed to specify the value at all here is a consequence of the + -- declaration of the Extended_Index subtype, which includes the values + -- in the base range that immediately precede and immediately follow the + -- values in the Index_Type.) + + if Before < Index_Type'First then + raise Constraint_Error with + "Before index is out of range (too small)"; + end if; + + -- We do allow a value greater than Container.Last to be specified as + -- the Index, but only if it's immediately greater. This allows for the + -- case of appending items to the back end of the vector. (It is assumed + -- that specifying an index value greater than Last + 1 indicates some + -- deeper flaw in the caller's algorithm, so that case is treated as a + -- proper error.) + + if Before > Container.Last + and then Before - 1 > Container.Last + then + raise Constraint_Error with + "Before index is out of range (too large)"; + end if; + + -- We treat inserting 0 items into the container as a no-op, so we + -- simply return. + + if Count = 0 then + return; + end if; + + -- 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. + + if Old_Length > Count_Type'Last - Count then + raise Constraint_Error with "Count is out of range"; + end if; + + -- It is now safe compute the length of the new vector, without fear of + -- overflow. + + New_Length := Old_Length + Count; + + -- The second constraint is that the new Last index value cannot exceed + -- Index_Type'Last. In each branch below, we calculate the maximum + -- length (computed from the range of values in Index_Type), and then + -- compare the new length to the maximum length. If the new length is + -- acceptable, then we compute the new last index from that. + + if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then + + -- We have to handle the case when there might be more values in the + -- range of Index_Type than in the range of Count_Type. + + if Index_Type'First <= 0 then + + -- We know that No_Index (the same as Index_Type'First - 1) is + -- less than 0, so it is safe to compute the following sum without + -- fear of overflow. + + Index := No_Index + Index_Type'Base (Count_Type'Last); + + if Index <= Index_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 + -- maximum number of items that are allowed. + + Max_Length := Count_Type'Last; + + else + -- The range of Index_Type has fewer values than in Count_Type, + -- so the maximum number of items is computed from the range of + -- the Index_Type. + + Max_Length := Count_Type'Base (Index_Type'Last - No_Index); + end if; + + else + -- No_Index is equal or greater than 0, so we can safely compute + -- the difference without fear of overflow (which we would have to + -- 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) + 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 + -- maximum number of items that are allowed. + + Max_Length := Count_Type'Last; + + else + -- The range of Index_Type has fewer values than in Count_Type, + -- so the maximum number of items is computed from the range of + -- the Index_Type. + + Max_Length := Count_Type'Base (Index_Type'Last - No_Index); + end if; + end if; + + elsif Index_Type'First <= 0 then + + -- We know that No_Index (the same as Index_Type'First - 1) is less + -- than 0, so it is safe to compute the following sum without fear of + -- overflow. + + J := Count_Type'Base (No_Index) + Count_Type'Last; + + if J <= Count_Type'Base (Index_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 maximum + -- number of items that are allowed. + + Max_Length := Count_Type'Last; + + else + -- The range of Index_Type has fewer values than Count_Type does, + -- so the maximum number of items is computed from the range of + -- the Index_Type. + + Max_Length := + Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index); + end if; + + else + -- No_Index is equal or greater than 0, so we can safely compute the + -- difference without fear of overflow (which we would have to worry + -- about if No_Index were less than 0, but that case is handled + -- above). + + Max_Length := + Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index); + end if; + + -- We have just computed the maximum length (number of items). We must + -- now compare the requested length to the maximum length, as we do not + -- allow a vector expand beyond the maximum (because that would create + -- an internal array with a last index value greater than + -- Index_Type'Last, with no way to index those elements). + + if New_Length > Max_Length then + raise Constraint_Error with "Count is out of range"; + end if; + + J := To_Array_Index (Before); + + -- Increase the capacity of container if needed + + 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))); + end if; + + declare + EA : Maximal_Array_Ptr renames Elems (Container); + begin + if Before <= Container.Last then + + -- The new items are being inserted before some existing + -- elements, so we must slide the existing elements up to their + -- new home. + + EA (J + Count .. New_Length) := EA (J .. Old_Length); + end if; + end; + + if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then + Container.Last := No_Index + Index_Type'Base (New_Length); + + else + Container.Last := + Index_Type'Base (Count_Type'Base (No_Index) + New_Length); + end if; + end Insert_Space; -------------- -- Is_Empty -- -------------- function Is_Empty (Container : Vector) return Boolean is - (Is_Empty (Container.V)); + begin + return Last_Index (Container) < Index_Type'First; + end Is_Empty; ------------------ -- Last_Element -- ------------------ function Last_Element (Container : Vector) return Element_Type is - (E (Last_Element (Container.V))); + begin + if Is_Empty (Container) then + raise Constraint_Error with "Container is empty"; + else + return Get_Element (Container, Length (Container)); + end if; + end Last_Element; ---------------- -- Last_Index -- ---------------- function Last_Index (Container : Vector) return Extended_Index is - (Last_Index (Container.V)); + begin + return Container.Last; + end Last_Index; ------------ -- Length -- ------------ function Length (Container : Vector) return Capacity_Range is - (Length (Container.V)); + 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; + + ---------- + -- Move -- + ---------- + + 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; + end if; + + if Bounded and then Target.Capacity < LS then + raise Constraint_Error; + end if; + + Clear (Target); + Append (Target, Source); + Clear (Source); + end Move; + + ------------ + -- Prepend -- + ------------ + + procedure Prepend (Container : in out Vector; New_Item : Vector) is + begin + Insert (Container, Index_Type'First, New_Item); + end Prepend; + + procedure Prepend + (Container : in out Vector; + New_Item : Element_Type) + is + begin + Prepend (Container, New_Item, 1); + end Prepend; + + procedure Prepend + (Container : in out Vector; + New_Item : Element_Type; + Count : Count_Type) + is + begin + Insert (Container, Index_Type'First, New_Item, Count); + end Prepend; --------------------- -- Replace_Element -- @@ -245,7 +1197,16 @@ is New_Item : Element_Type) is begin - Replace_Element (Container.V, Index, H (New_Item)); + if Index > Container.Last then + raise Constraint_Error with "Index is out of range"; + end if; + + 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; end Replace_Element; ---------------------- @@ -257,7 +1218,23 @@ is Capacity : Capacity_Range) is begin - Reserve_Capacity (Container.V, Capacity); + if Bounded then + 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); + Container.Elements_Ptr := New_Elements; + end; + end if; + end if; end Reserve_Capacity; ---------------------- @@ -266,7 +1243,30 @@ is procedure Reverse_Elements (Container : in out Vector) is begin - Reverse_Elements (Container.V); + if Length (Container) <= 1 then + return; + end if; + + declare + I, J : Capacity_Range; + E : Elements_Array renames + Elems (Container) (1 .. Length (Container)); + + begin + I := 1; + J := Length (Container); + while I < J loop + declare + EI : constant Holder := E (I); + begin + E (I) := E (J); + E (J) := EI; + end; + + I := I + 1; + J := J - 1; + end loop; + end; end Reverse_Elements; ------------------------ @@ -278,7 +1278,27 @@ is Item : Element_Type; Index : Index_Type := Index_Type'Last) return Extended_Index is - (Reverse_Find_Index (Container.V, H (Item), Index)); + Last : Index_Type'Base; + K : Capacity_Range; + + begin + if Index > Last_Index (Container) then + Last := Last_Index (Container); + else + Last := Index; + end if; + + K := Capacity_Range (Int (Last) - Int (No_Index)); + for Indx in reverse Index_Type'First .. Last loop + if Get_Element (Container, K) = Item then + return Indx; + end if; + + K := K - 1; + end loop; + + return No_Index; + end Reverse_Find_Index; ---------- -- Swap -- @@ -286,9 +1306,66 @@ is procedure Swap (Container : in out Vector; I, J : Index_Type) is begin - Swap (Container.V, I, J); + if I > Container.Last then + raise Constraint_Error with "I index is out of range"; + end if; + + if J > Container.Last then + raise Constraint_Error with "J index is out of range"; + end if; + + if I = J then + return; + end if; + + declare + II : constant Int'Base := Int (I) - Int (No_Index); + JJ : constant Int'Base := Int (J) - Int (No_Index); + + EI : Holder renames Elems (Container) (Capacity_Range (II)); + EJ : Holder renames Elems (Container) (Capacity_Range (JJ)); + + EI_Copy : constant Holder := EI; + + begin + EI := EJ; + EJ := EI_Copy; + end; end Swap; + -------------------- + -- To_Array_Index -- + -------------------- + + function To_Array_Index (Index : Index_Type'Base) return Count_Type'Base is + Offset : Count_Type'Base; + + begin + -- We know that + -- Index >= Index_Type'First + -- 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 + -- calculations. + + if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then + Offset := Count_Type'Base (Index - Index_Type'First); + + else + 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. + + return 1 + Offset; + end To_Array_Index; + --------------- -- To_Vector -- --------------- @@ -298,7 +1375,27 @@ is Length : Capacity_Range) return Vector is begin - return (Length, To_Vector (H (New_Item), Length)); + if Length = 0 then + return Empty_Vector; + end if; + + declare + First : constant Int := Int (Index_Type'First); + Last_As_Int : constant Int'Base := First + Int (Length) - 1; + Last : Index_Type; + + begin + if Last_As_Int > Index_Type'Pos (Index_Type'Last) then + raise Constraint_Error with "Length is out of range"; -- ??? + end if; + + Last := Index_Type (Last_As_Int); + + return (Capacity => Length, + Last => Last, + Elements_Ptr => <>, + Elements => (others => H (New_Item))); + end; end To_Vector; end Ada.Containers.Formal_Indefinite_Vectors; diff --git a/gcc/ada/a-cfinve.ads b/gcc/ada/a-cfinve.ads index 34abfbbbcff..56aee851444 100644 --- a/gcc/ada/a-cfinve.ads +++ b/gcc/ada/a-cfinve.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2014-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 2014-2017, Free Software Foundation, Inc. -- -- -- -- This specification is derived from the Ada Reference Manual for use with -- -- GNAT. The copyright notice above, and the license provisions that follow -- @@ -30,11 +30,10 @@ ------------------------------------------------------------------------------ -- Similar to Ada.Containers.Formal_Vectors. The main difference is that --- Element_Type may be indefinite (but not an unconstrained array). In --- addition, this is simplified by removing less-used functionality. +-- Element_Type may be indefinite (but not an unconstrained array). with Ada.Containers.Bounded_Holders; -with Ada.Containers.Formal_Vectors; +with Ada.Containers.Functional_Vectors; generic type Index_Type is range <>; @@ -48,8 +47,6 @@ generic -- responsibility of clients to calculate the maximum size of all types in -- the class. - with function "=" (Left, Right : Element_Type) return Boolean is <>; - Bounded : Boolean := True; -- If True, the containers are bounded; the initial capacity is the maximum -- size, and heap allocation will be avoided. If False, the containers can @@ -58,7 +55,6 @@ generic package Ada.Containers.Formal_Indefinite_Vectors with SPARK_Mode => On is - pragma Annotate (GNATprove, External_Axiomatization); pragma Annotate (CodePeer, Skip_Analysis); subtype Extended_Index is Index_Type'Base @@ -71,60 +67,203 @@ is Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1); type Vector (Capacity : Capacity_Range) is limited private with - Default_Initial_Condition; + Default_Initial_Condition => Is_Empty (Vector); + -- In the bounded case, Capacity is the capacity of the container, which + -- never changes. In the unbounded case, Capacity is the initial capacity + -- of the container, and operations such as Reserve_Capacity and Append can + -- increase the capacity. The capacity never shrinks, except in the case of + -- Clear. + -- + -- Note that all objects of type Vector are constrained, including in the + -- unbounded case; you can't assign from one object to another if the + -- Capacity is different. + + function Length (Container : Vector) return Capacity_Range with + Global => null, + Post => Length'Result <= Capacity (Container); + + pragma Unevaluated_Use_Of_Old (Allow); + + package Formal_Model with Ghost is + + package M is new Ada.Containers.Functional_Vectors + (Index_Type => Index_Type, + Element_Type => Element_Type); + + function "=" + (Left : M.Sequence; + Right : M.Sequence) return Boolean renames M."="; + + function "<" + (Left : M.Sequence; + Right : M.Sequence) return Boolean renames M."<"; + + function "<=" + (Left : M.Sequence; + Right : M.Sequence) return Boolean renames M."<="; + + function M_Elements_In_Union + (Container : M.Sequence; + Left : M.Sequence; + Right : M.Sequence) return Boolean + -- The elements of Container are contained in either Left or Right + with + Global => null, + Post => + M_Elements_In_Union'Result = + (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))); + pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union); + + function M_Elements_Included + (Left : M.Sequence; + L_Fst : Index_Type := Index_Type'First; + L_Lst : Extended_Index; + Right : M.Sequence; + R_Fst : Index_Type := Index_Type'First; + R_Lst : Extended_Index) return Boolean + -- The elements of the slice from L_Fst to L_Lst in Left are contained + -- in the slide from R_Fst to R_Lst in Right. + with + Global => null, + Pre => L_Lst <= M.Last (Left) and R_Lst <= M.Last (Right), + Post => + M_Elements_Included'Result = + (for all I in L_Fst .. L_Lst => + (for some J in R_Fst .. R_Lst => + Element (Left, I) = Element (Right, J))); + pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Included); + + function M_Elements_Reversed + (Left : M.Sequence; + Right : M.Sequence) return Boolean + -- Right is Left in reverse order + with + Global => null, + Post => + 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)) + and (for all I in Index_Type'First .. M.Last (Right) => + Element (Right, I) = + Element (Left, M.Last (Left) - I + 1))); + pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed); + + function M_Elements_Swapped + (Left : M.Sequence; + Right : M.Sequence; + X : Index_Type; + Y : Index_Type) return Boolean + -- Elements stored at X and Y are reversed in Left and Right + with + Global => null, + Pre => X <= M.Last (Left) and Y <= M.Last (Left), + Post => + M_Elements_Swapped'Result = + (M.Length (Left) = M.Length (Right) + and Element (Left, X) = Element (Right, Y) + and Element (Left, Y) = Element (Right, X) + and M.Equal_Except (Left, Right, X, Y)); + pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped); + + function Model (Container : Vector) return M.Sequence with + -- The high-level model of a vector is a sequence of elements. The + -- sequence really is similar to the vector itself. However, it is not + -- limited which allows usage of 'Old and 'Loop_Entry attributes. + + Ghost, + Global => null, + Post => M.Length (Model'Result) = Length (Container); + + function Element + (S : M.Sequence; + 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; function Empty_Vector return Vector with - Global => null; + Global => null, + Post => Length (Empty_Vector'Result) = 0; function "=" (Left, Right : Vector) return Boolean with - Global => null; + Global => null, + Post => "="'Result = (Model (Left) = Model (Right)); function To_Vector (New_Item : Element_Type; Length : Capacity_Range) return Vector with - Global => null; + 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); function Capacity (Container : Vector) return Capacity_Range with Global => null, - Post => Capacity'Result >= Container.Capacity; + Post => + Capacity'Result = (if Bounded then Container.Capacity + else Capacity_Range'Last); + pragma Annotate (GNATprove, Inline_For_Proof, Capacity); procedure Reserve_Capacity (Container : in out Vector; Capacity : Capacity_Range) with Global => null, - Pre => (if Bounded then Capacity <= Container.Capacity); - - function Length (Container : Vector) return Capacity_Range with - Global => null; + Pre => (if Bounded then Capacity <= Container.Capacity), + Post => Model (Container) = Model (Container)'Old; function Is_Empty (Container : Vector) return Boolean with - Global => null; + Global => null, + Post => Is_Empty'Result = (Length (Container) = 0); procedure Clear (Container : in out Vector) with - Global => null; + Global => null, + Post => Length (Container) = 0; -- Note that this reclaims storage in the unbounded case. You need to call -- this before a container goes out of scope in order to avoid storage - -- leaks. + -- leaks. In addition, "X := ..." can leak unless you Clear(X) first. procedure Assign (Target : in out Vector; Source : Vector) with Global => null, - Pre => (if Bounded then Length (Source) <= Target.Capacity); + Pre => (if Bounded then Length (Source) <= Target.Capacity), + Post => Model (Target) = Model (Source); function Copy (Source : Vector; Capacity : Capacity_Range := 0) return Vector with Global => null, - Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)); + 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); + + procedure Move (Target : in out Vector; Source : in out Vector) + with + Global => null, + Pre => (if Bounded then Length (Source) <= Capacity (Target)), + Post => Model (Target) = Model (Source)'Old and Length (Source) = 0; function Element (Container : Vector; Index : Index_Type) return Element_Type with Global => null, - Pre => Index in First_Index (Container) .. Last_Index (Container); + Pre => Index in First_Index (Container) .. Last_Index (Container), + Post => Element'Result = Element (Model (Container), Index); + pragma Annotate (GNATprove, Inline_For_Proof, Element); procedure Replace_Element (Container : in out Vector; @@ -132,102 +271,602 @@ is New_Item : Element_Type) with Global => null, - Pre => Index in First_Index (Container) .. Last_Index (Container); + Pre => Index in First_Index (Container) .. Last_Index (Container), + Post => + Length (Container) = Length (Container)'Old - procedure Append + -- Container now has New_Item at index Index + + and Element (Model (Container), Index) = New_Item + + -- All other elements are preserved + + and M.Equal_Except + (Left => Model (Container)'Old, + Right => Model (Container), + Position => Index); + + procedure Insert (Container : in out Vector; + Before : Extended_Index; New_Item : Vector) with Global => null, - Pre => (if Bounded - then Length (Container) + Length (New_Item) <= - Container.Capacity); + Pre => + Length (Container) <= Capacity (Container) - Length (New_Item) + and (Before in Index_Type'First .. Last_Index (Container) + or Before - 1 = Last_Index (Container)), + Post => + Length (Container) = Length (Container)'Old + Length (New_Item) + + -- Elements located before Before in Container are preserved + + and M.Range_Equal + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Before - 1) + + -- 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))) + + -- Elements located after Before in Container are shifted + + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Before, + Lst => Last_Index (Container)'Old, + Offset => Length (New_Item)); + + procedure Insert + (Container : in out Vector; + Before : Extended_Index; + New_Item : Element_Type) + with + Global => null, + Pre => + Length (Container) < Capacity (Container) + and then (Before in Index_Type'First .. Last_Index (Container) + 1), + Post => + Length (Container) = Length (Container)'Old + 1 + + -- Elements located before Before in Container are preserved + + and M.Range_Equal + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Before - 1) + + -- Container now has New_Item at index Before + + and Element (Model (Container), Before) = New_Item + + -- Elements located after Before in Container are shifted by 1 + + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Before, + Lst => Last_Index (Container)'Old, + Offset => 1); + + procedure Insert + (Container : in out Vector; + Before : Extended_Index; + New_Item : Element_Type; + Count : Count_Type) + with + Global => null, + Pre => + Length (Container) <= Capacity (Container) - Count + and (Before in Index_Type'First .. Last_Index (Container) + or Before - 1 = Last_Index (Container)), + Post => + Length (Container) = Length (Container)'Old + Count + + -- Elements located before Before in Container are preserved + + and M.Range_Equal + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Before - 1) + + -- 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)) + + -- Elements located after Before in Container are shifted + + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Before, + Lst => Last_Index (Container)'Old, + Offset => Count); + + procedure Prepend + (Container : in out Vector; + New_Item : Vector) + with + Global => null, + Pre => Length (Container) <= Capacity (Container) - Length (New_Item), + Post => + Length (Container) = Length (Container)'Old + Length (New_Item) + + -- Elements of New_Item are inserted at the beginning of Container + + and M.Range_Equal + (Left => Model (New_Item), + Right => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (New_Item)) + + -- Elements of Container are shifted + + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (Container)'Old, + Offset => Length (New_Item)); + + procedure Prepend + (Container : in out Vector; + New_Item : Element_Type) + with + Global => null, + Pre => Length (Container) < Capacity (Container), + Post => + Length (Container) = Length (Container)'Old + 1 + + -- Container now has New_Item at Index_Type'First + + and Element (Model (Container), Index_Type'First) = New_Item + + -- Elements of Container are shifted by 1 + + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (Container)'Old, + Offset => 1); + + procedure Prepend + (Container : in out Vector; + New_Item : Element_Type; + Count : Count_Type) + with + Global => null, + Pre => Length (Container) <= Capacity (Container) - Count, + Post => + Length (Container) = Length (Container)'Old + Count + + -- New_Item is inserted Count times at the beginning of Container + + and M.Constant_Range + (Container => Model (Container), + Fst => Index_Type'First, + Lst => Index_Type'First + Index_Type'Base (Count - 1), + Item => New_Item) + + -- Elements of Container are shifted + + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (Container)'Old, + Offset => Count); + + procedure Append + (Container : in out Vector; + New_Item : Vector) + with + Global => null, + Pre => + Length (Container) <= Capacity (Container) - Length (New_Item), + Post => + Length (Container) = Length (Container)'Old + Length (New_Item) + + -- The elements of Container are preserved + + and Model (Container)'Old <= Model (Container) + + -- 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))); procedure Append (Container : in out Vector; New_Item : Element_Type) with Global => null, - Pre => (if Bounded - then Length (Container) < Container.Capacity); + Pre => Length (Container) < Capacity (Container), + Post => + Length (Container) = Length (Container)'Old + 1 + + -- Elements of Container are preserved + + and Model (Container)'Old < Model (Container) + + -- Container now has New_Item at the end of Container + + and Element + (Model (Container), Last_Index (Container)'Old + 1) = New_Item; + + procedure Append + (Container : in out Vector; + New_Item : Element_Type; + Count : Count_Type) + with + Global => null, + Pre => Length (Container) <= Capacity (Container) - Count, + Post => + Length (Container) = Length (Container)'Old + Count + + -- Elements of Container are preserved + + and Model (Container)'Old <= Model (Container) + + -- 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)); + + procedure Delete + (Container : in out Vector; + Index : Extended_Index) + with + Global => null, + Pre => Index in First_Index (Container) .. Last_Index (Container), + Post => + Length (Container) = Length (Container)'Old - 1 + + -- Elements located before Index in Container are preserved + + and M.Range_Equal + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Index - 1) + + -- Elements located after Index in Container are shifted by 1 + + and M.Range_Shifted + (Left => Model (Container), + Right => Model (Container)'Old, + Fst => Index, + Lst => Last_Index (Container), + Offset => 1); + + procedure Delete + (Container : in out Vector; + Index : Extended_Index; + Count : Count_Type) + with + Global => null, + Pre => + Index in First_Index (Container) .. Last_Index (Container), + Post => + Length (Container) in + Length (Container)'Old - Count .. Length (Container)'Old + + -- The elements of Container located before Index are preserved. + + and M.Range_Equal + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Index - 1), + + Contract_Cases => + + -- All the elements after Position have been erased + + (Length (Container) - Count <= Count_Type (Index - Index_Type'First) => + Length (Container) = Count_Type (Index - Index_Type'First), + + others => + Length (Container) = Length (Container)'Old - Count + + -- Other elements are shifted by Count + + and M.Range_Shifted + (Left => Model (Container), + Right => Model (Container)'Old, + Fst => Index, + Lst => Last_Index (Container), + Offset => Count)); + + procedure Delete_First + (Container : in out Vector) + with + Global => null, + Pre => Length (Container) > 0, + Post => + Length (Container) = Length (Container)'Old - 1 + + -- Elements of Container are shifted by 1 + + and M.Range_Shifted + (Left => Model (Container), + Right => Model (Container)'Old, + Fst => Index_Type'First, + Lst => Last_Index (Container), + Offset => 1); + + procedure Delete_First + (Container : in out Vector; + Count : Count_Type) + with + Global => null, + Contract_Cases => + + -- All the elements of Container have been erased + + (Length (Container) <= Count => Length (Container) = 0, + + others => + Length (Container) = Length (Container)'Old - Count + + -- Elements of Container are shifted by Count + + and M.Range_Shifted + (Left => Model (Container), + Right => Model (Container)'Old, + Fst => Index_Type'First, + Lst => Last_Index (Container), + Offset => Count)); procedure Delete_Last (Container : in out Vector) with - Global => null; + Global => null, + Pre => Length (Container) > 0, + Post => + Length (Container) = Length (Container)'Old - 1 + + -- Elements of Container are preserved + + and Model (Container) < Model (Container)'Old; + + procedure Delete_Last + (Container : in out Vector; + Count : Count_Type) + with + Global => null, + Contract_Cases => + + -- All the elements after Position have been erased + + (Length (Container) <= Count => Length (Container) = 0, + + others => + Length (Container) = Length (Container)'Old - Count + + -- The elements of Container are preserved + + and Model (Container) <= Model (Container)'Old); procedure Reverse_Elements (Container : in out Vector) with - Global => null; + Global => null, + Post => M_Elements_Reversed (Model (Container)'Old, Model (Container)); procedure Swap (Container : in out Vector; I, 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); + and then J in First_Index (Container) .. Last_Index (Container), + Post => + M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J); function First_Index (Container : Vector) return Index_Type with - Global => null; + Global => null, + Post => First_Index'Result = Index_Type'First; + pragma Annotate (GNATprove, Inline_For_Proof, First_Index); function First_Element (Container : Vector) return Element_Type with Global => null, - Pre => not Is_Empty (Container); + Pre => not Is_Empty (Container), + Post => + First_Element'Result = Element (Model (Container), Index_Type'First); + pragma Annotate (GNATprove, Inline_For_Proof, First_Element); function Last_Index (Container : Vector) return Extended_Index with - Global => null; + Global => null, + Post => Last_Index'Result = M.Last (Model (Container)); + pragma Annotate (GNATprove, Inline_For_Proof, Last_Index); function Last_Element (Container : Vector) return Element_Type with Global => null, - Pre => not Is_Empty (Container); + Pre => not Is_Empty (Container), + Post => + Last_Element'Result = + Element (Model (Container), Last_Index (Container)); + pragma Annotate (GNATprove, Inline_For_Proof, Last_Element); function Find_Index (Container : Vector; Item : Element_Type; Index : Index_Type := Index_Type'First) return Extended_Index with - Global => null; + Global => null, + Contract_Cases => + + -- If Item is not is not contained in Container after Index, Find_Index + -- returns No_Index. + + (Index > Last_Index (Container) + or else not M.Contains + (Container => Model (Container), + Fst => Index, + Lst => Last_Index (Container), + Item => Item) + => + Find_Index'Result = No_Index, + + -- Otherwise, Find_Index returns a valid index greater than Index + + others => + Find_Index'Result in Index .. Last_Index (Container) + + -- The element at this index in Container is Item + + and Element (Model (Container), Find_Index'Result) = Item + + -- It is the first occurrence of Item after Index in Container + + and not M.Contains + (Container => Model (Container), + Fst => Index, + Lst => Find_Index'Result - 1, + Item => Item)); function Reverse_Find_Index (Container : Vector; Item : Element_Type; Index : Index_Type := Index_Type'Last) return Extended_Index with - Global => null; + Global => null, + Contract_Cases => + + -- If Item is not is not contained in Container before Index, + -- Reverse_Find_Index returns No_Index. + + (not M.Contains + (Container => Model (Container), + Fst => Index_Type'First, + Lst => (if Index <= Last_Index (Container) then Index + else Last_Index (Container)), + Item => Item) + => + Reverse_Find_Index'Result = No_Index, + + -- Otherwise, Reverse_Find_Index returns a valid index smaller than + -- Index + + others => + 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 + + and Element (Model (Container), Reverse_Find_Index'Result) = Item + + -- It is the last occurrence of Item before Index in Container + + and not M.Contains + (Container => Model (Container), + Fst => Reverse_Find_Index'Result + 1, + Lst => + (if Index <= Last_Index (Container) then Index + else Last_Index (Container)), + Item => Item)); function Contains (Container : Vector; Item : Element_Type) return Boolean with - Global => null; + Global => null, + Post => + Contains'Result = M.Contains (Container => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (Container), + Item => Item); function Has_Element - (Container : Vector; Position : Extended_Index) return Boolean with - Global => null; + (Container : Vector; + Position : Extended_Index) return Boolean + with + Global => null, + Post => + Has_Element'Result = + (Position in Index_Type'First .. Last_Index (Container)); + pragma Annotate (GNATprove, Inline_For_Proof, Has_Element); generic with function "<" (Left, Right : Element_Type) return Boolean is <>; package Generic_Sorting with SPARK_Mode is + function M_Elements_Sorted (Container : M.Sequence) return Boolean with + Ghost, + Global => null, + 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))); + pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted); function Is_Sorted (Container : Vector) return Boolean with - Global => null; + Global => null, + Post => Is_Sorted'Result = M_Elements_Sorted (Model (Container)); procedure Sort (Container : in out Vector) with - Global => null; - + Global => null, + 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)); + + procedure Merge (Target : in out Vector; Source : in out Vector) with + -- Target and Source should not be aliased + Global => null, + Pre => Length (Source) <= Capacity (Target) - Length (Target), + Post => + Length (Target) = Length (Target)'Old + Length (Source)'Old + 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); end Generic_Sorting; - function First_To_Previous - (Container : Vector; - Current : Index_Type) return Vector - with - Ghost, - Global => null; - - function Current_To_Last - (Container : Vector; - Current : Index_Type) return Vector - with - Ghost, - Global => null; - private pragma SPARK_Mode (Off); @@ -240,23 +879,39 @@ private pragma Inline (Contains); -- The implementation method is to instantiate Bounded_Holders to get a - -- definite type for Element_Type, and then use that Holder type to - -- instantiate Formal_Vectors. All the operations are just wrappers. + -- definite type for Element_Type. package Holders is new Bounded_Holders (Element_Type, Max_Size_In_Storage_Elements, "="); use Holders; - package Def is new Formal_Vectors (Index_Type, Holder, "=", Bounded); - use Def; + subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last; + type Elements_Array is array (Array_Index range <>) of Holder; + function "=" (L, R : Elements_Array) return Boolean is abstract; - -- ????Assert that Def subtypes have the same range + type Elements_Array_Ptr is access all Elements_Array; type Vector (Capacity : Capacity_Range) is limited record - V : Def.Vector (Capacity); + -- 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); end record; + -- The primary reason Vector is limited is that in the unbounded case, once + -- Elements_Ptr is in use, assignment statements won't work. "X := Y;" will + -- cause X and Y to share state; that is, X.Elements_Ptr = Y.Elements_Ptr, + -- so for example "Append (X, ...);" will modify BOTH X and Y. That would + -- allow SPARK to "prove" things that are false. We could fix that by + -- making Vector a controlled type, and override Adjust to make a deep + -- copy, but finalization is not allowed in SPARK. + -- + -- Note that (unfortunately) this means that 'Old and 'Loop_Entry are not + -- allowed on Vectors. + function Empty_Vector return Vector is - ((Capacity => 0, V => Def.Empty_Vector)); + ((Capacity => 0, others => <>)); end Ada.Containers.Formal_Indefinite_Vectors; diff --git a/gcc/ada/a-cofove.adb b/gcc/ada/a-cofove.adb index 529a73b9e25..d1f4b9ce61b 100644 --- a/gcc/ada/a-cofove.adb +++ b/gcc/ada/a-cofove.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2010-2015, Free Software Foundation, Inc. -- +-- Copyright (C) 2010-2017, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -39,7 +39,6 @@ is -- leads to amortized linear-time copying. type Int is range System.Min_Int .. System.Max_Int; - type UInt is mod System.Max_Binary_Modulus; procedure Free is new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr); @@ -66,6 +65,15 @@ is (Container : Vector; Position : Capacity_Range) return Element_Type; + function To_Array_Index (Index : Index_Type'Base) return Count_Type'Base; + + function Current_Capacity (Container : Vector) return Capacity_Range; + + procedure Insert_Space + (Container : in out Vector; + Before : Extended_Index; + Count : Count_Type := 1); + --------- -- "=" -- --------- @@ -95,34 +103,40 @@ is procedure Append (Container : in out Vector; New_Item : Vector) is begin - for X in First_Index (New_Item) .. Last_Index (New_Item) loop - Append (Container, Element (New_Item, X)); - end loop; + if Is_Empty (New_Item) then + return; + end if; + + if Container.Last >= Index_Type'Last then + raise Constraint_Error with "vector is already at its maximum length"; + end if; + + Insert (Container, Container.Last + 1, New_Item); end Append; procedure Append (Container : in out Vector; New_Item : Element_Type) is - New_Length : constant UInt := UInt (Length (Container) + 1); begin - if not Bounded and then - Capacity (Container) < Capacity_Range (New_Length) - then - Reserve_Capacity - (Container, - Capacity_Range'Max (Capacity (Container) * Growth_Factor, - Capacity_Range (New_Length))); + Append (Container, New_Item, 1); + end Append; + + procedure Append + (Container : in out Vector; + New_Item : Element_Type; + Count : Count_Type) + is + begin + if Count = 0 then + return; end if; - if Container.Last = Index_Type'Last then + if Container.Last >= Index_Type'Last then raise Constraint_Error with "vector is already at its maximum length"; end if; - -- TODO: should check whether length > max capacity (cnt_t'last) ??? - - Container.Last := Container.Last + 1; - Elems (Container) (Length (Container)) := New_Item; + Insert (Container, Container.Last + 1, New_Item, Count); end Append; ------------ @@ -151,9 +165,8 @@ is function 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 Bounded then Container.Capacity + else Capacity_Range'Last); end Capacity; ----------- @@ -207,22 +220,155 @@ is end return; end Copy; - --------------------- - -- Current_To_Last -- - --------------------- + ---------------------- + -- Current_Capacity -- + ---------------------- - function Current_To_Last - (Container : Vector; - Current : Index_Type) return Vector + 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); + end Current_Capacity; + + ------------ + -- Delete -- + ------------ + + procedure Delete + (Container : in out Vector; + Index : Extended_Index) is begin - return Result : Vector (Count_Type (Container.Last - Current + 1)) - do - for X in Current .. Container.Last loop - Append (Result, Element (Container, X)); - end loop; - end return; - end Current_To_Last; + Delete (Container, Index, 1); + end Delete; + + procedure Delete + (Container : in out Vector; + Index : Extended_Index; + Count : Count_Type) + is + Old_Last : constant Index_Type'Base := Container.Last; + Old_Len : constant Count_Type := Length (Container); + New_Last : Index_Type'Base; + Count2 : Count_Type'Base; -- count of items from Index to Old_Last + Off : Count_Type'Base; -- Index expressed as offset from IT'First + + begin + -- Delete removes items from the vector, the number of which is the + -- minimum of the specified Count and the items (if any) that exist from + -- Index to Container.Last. There are no constraints on the specified + -- value of Count (it can be larger than what's available at this + -- position in the vector, for example), but there are constraints on + -- the allowed values of the Index. + + -- As a precondition on the generic actual Index_Type, the base type + -- must include Index_Type'Pred (Index_Type'First); this is the value + -- that Container.Last assumes when the vector is empty. However, we do + -- not allow that as the value for Index when specifying which items + -- should be deleted, so we must manually check. (That the user is + -- allowed to specify the value at all here is a consequence of the + -- declaration of the Extended_Index subtype, which includes the values + -- in the base range that immediately precede and immediately follow the + -- values in the Index_Type.) + + if Index < Index_Type'First then + raise Constraint_Error with "Index is out of range (too small)"; + end if; + + -- We do allow a value greater than Container.Last to be specified as + -- the Index, but only if it's immediately greater. This allows the + -- corner case of deleting no items from the back end of the vector to + -- be treated as a no-op. (It is assumed that specifying an index value + -- greater than Last + 1 indicates some deeper flaw in the caller's + -- algorithm, so that case is treated as a proper error.) + + if Index > Old_Last then + if Index > Old_Last + 1 then + raise Constraint_Error with "Index is out of range (too large)"; + end if; + + return; + end if; + + if Count = 0 then + return; + end if; + + -- We first calculate what's available for deletion starting at + -- Index. Here and elsewhere we use the wider of Index_Type'Base and + -- Count_Type'Base as the type for intermediate values. (See function + -- Length for more information.) + + if Count_Type'Base'Last >= Index_Type'Pos (Index_Type'Base'Last) then + Count2 := Count_Type'Base (Old_Last) - Count_Type'Base (Index) + 1; + else + Count2 := Count_Type'Base (Old_Last - Index + 1); + end if; + + -- If more elements are requested (Count) for deletion than are + -- available (Count2) for deletion beginning at Index, then everything + -- from Index is deleted. There are no elements to slide down, and so + -- all we need to do is set the value of Container.Last. + + if Count >= Count2 then + Container.Last := Index - 1; + return; + 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. + + if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then + Off := Count_Type'Base (Index - Index_Type'First); + New_Last := Old_Last - Index_Type'Base (Count); + else + Off := Count_Type'Base (Index) - Count_Type'Base (Index_Type'First); + New_Last := Index_Type'Base (Count_Type'Base (Old_Last) - Count); + end if; + + -- The array index values for each slice have already been determined, + -- so we just slide down to Index the elements that weren't deleted. + + 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; + end; + end Delete; + + ------------------ + -- Delete_First -- + ------------------ + + 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 + begin + if Count = 0 then + return; + + elsif Count >= Length (Container) then + Clear (Container); + return; + + else + Delete (Container, Index_Type'First, Count); + end if; + end Delete_First; ----------------- -- Delete_Last -- @@ -231,16 +377,38 @@ is procedure Delete_Last (Container : in out Vector) is - Count : constant Capacity_Range := 1; - Index : Int'Base; + begin + Delete_Last (Container, 1); + end Delete_Last; + procedure Delete_Last + (Container : in out Vector; + Count : Count_Type) + is begin - Index := Int'Base (Container.Last) - Int'Base (Count); + if Count = 0 then + return; + end if; + + -- There is no restriction on how large Count can be when deleting + -- items. If it is equal or greater than the current length, then this + -- is equivalent to clearing the vector. (In particular, there's no need + -- for us to actually calculate the new value for Last.) - if Index < Index_Type'Pos (Index_Type'First) then + -- If the requested count is less than the current length, then we must + -- calculate the new value for Last. For the type we use the widest of + -- Index_Type'Base and Count_Type'Base for the intermediate values of + -- our calculation. (See the comments in Length for more information.) + + if Count >= Length (Container) then Container.Last := No_Index; + + elsif Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then + Container.Last := Container.Last - Index_Type'Base (Count); + else - Container.Last := Index_Type (Index); + Container.Last := + Index_Type'Base (Count_Type'Base (Container.Last) - Count); end if; end Delete_Last; @@ -332,23 +500,151 @@ is return Index_Type'First; end First_Index; - ----------------------- - -- First_To_Previous -- - ----------------------- + ------------------ + -- Formal_Model -- + ------------------ - function First_To_Previous - (Container : Vector; - Current : Index_Type) return Vector - is - begin - return Result : Vector - (Count_Type (Current - First_Index (Container))) - do - for X in First_Index (Container) .. Current - 1 loop - Append (Result, Element (Container, X)); + package body Formal_Model is + + ------------------------- + -- M_Elements_In_Union -- + ------------------------- + + function M_Elements_In_Union + (Container : M.Sequence; + 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; + + 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 + return False; + end if; + end; end loop; - end return; - end First_To_Previous; + + return True; + end M_Elements_In_Union; + + ------------------------- + -- M_Elements_Included -- + ------------------------- + + function M_Elements_Included + (Left : M.Sequence; + L_Fst : Index_Type := Index_Type'First; + L_Lst : Extended_Index; + Right : M.Sequence; + R_Fst : Index_Type := Index_Type'First; + R_Lst : Extended_Index) return Boolean + is + begin + for I in L_Fst .. L_Lst loop + declare + Found : Boolean := False; + J : Extended_Index := R_Fst - 1; + + begin + while not Found and J < R_Lst loop + J := J + 1; + if Element (Left, I) = Element (Right, J) then + Found := True; + end if; + end loop; + + if not Found then + return False; + end if; + end; + end loop; + + return True; + end M_Elements_Included; + + ------------------------- + -- M_Elements_Reversed -- + ------------------------- + + function M_Elements_Reversed (Left, Right : M.Sequence) return Boolean is + L : constant Index_Type := M.Last (Left); + begin + if L /= M.Last (Right) then + return False; + end if; + + for I in Index_Type'First .. L loop + if Element (Left, I) /= Element (Right, L - I + 1) + then + return False; + end if; + end loop; + + return True; + end M_Elements_Reversed; + + ------------------------ + -- M_Elements_Swapted -- + ------------------------ + + function M_Elements_Swapped + (Left : M.Sequence; + Right : M.Sequence; + X, Y : Index_Type) return Boolean + is + begin + if M.Length (Left) /= M.Length (Right) + or else Element (Left, X) /= Element (Right, Y) + or else Element (Left, Y) /= Element (Right, X) + then + return False; + end if; + + for I in Index_Type'First .. M.Last (Left) loop + if I /= X and then I /= Y + and then Element (Left, I) /= Element (Right, I) + then + return False; + end if; + end loop; + + return True; + end M_Elements_Swapped; + + ----------- + -- Model -- + ----------- + + 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; + + end Formal_Model; --------------------- -- Generic_Sorting -- @@ -374,6 +670,37 @@ is return True; end Is_Sorted; + ----------------------- + -- M_Elements_Sorted -- + ----------------------- + + function M_Elements_Sorted (Container : M.Sequence) return Boolean is + begin + if M.Length (Container) = 0 then + return True; + end if; + + declare + E1 : Element_Type := Element (Container, Index_Type'First); + + begin + for I in Index_Type'First + 1 .. M.Last (Container) loop + declare + E2 : constant Element_Type := Element (Container, I); + + begin + if E2 < E1 then + return False; + end if; + + E1 := E2; + end; + end loop; + end; + + return True; + end M_Elements_Sorted; + ---------- -- Sort -- ---------- @@ -396,6 +723,78 @@ is end if; end Sort; + ----------- + -- Merge -- + ----------- + + procedure Merge (Target, Source : in out Vector) is + I, J : Count_Type; + + begin + if Target'Address = Source'Address then + raise Program_Error with + "Target and Source denote same container"; + end if; + + if Length (Source) = 0 then + return; + end if; + + if Length (Target) = 0 then + Move (Target => Target, Source => Source); + return; + end if; + + I := Length (Target); + + declare + New_Length : constant Count_Type := I + Length (Source); + begin + 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))); + end if; + + if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then + Target.Last := No_Index + Index_Type'Base (New_Length); + + else + Target.Last := + Index_Type'Base (Count_Type'Base (No_Index) + New_Length); + end if; + end; + + declare + TA : Maximal_Array_Ptr renames Elems (Target); + SA : Maximal_Array_Ptr renames Elems (Source); + begin + J := Length (Target); + while Length (Source) /= 0 loop + if I = 0 then + TA (1 .. J) := SA (1 .. Length (Source)); + Source.Last := No_Index; + exit; + end if; + + if SA (Length (Source)) < TA (I) then + TA (J) := TA (I); + I := I - 1; + + else + TA (J) := SA (Length (Source)); + Source.Last := Source.Last - 1; + end if; + + J := J - 1; + end loop; + end; + end Merge; + end Generic_Sorting; ----------------- @@ -420,6 +819,276 @@ is return Position in First_Index (Container) .. Last_Index (Container); end Has_Element; + ------------ + -- Insert -- + ------------ + + procedure Insert + (Container : in out Vector; + Before : Extended_Index; + New_Item : Element_Type) + is + begin + Insert (Container, Before, New_Item, 1); + end Insert; + + procedure Insert + (Container : in out Vector; + Before : Extended_Index; + New_Item : Element_Type; + Count : Count_Type) + is + J : Count_Type'Base; -- scratch + + begin + -- Use Insert_Space to create the "hole" (the destination slice) + + Insert_Space (Container, Before, Count); + + J := To_Array_Index (Before); + + Elems (Container) (J .. J - 1 + Count) := (others => New_Item); + end Insert; + + procedure Insert + (Container : in out Vector; + Before : Extended_Index; + New_Item : Vector) + is + N : constant Count_Type := Length (New_Item); + B : Count_Type; -- index Before converted to Count_Type + + begin + if Container'Address = New_Item'Address then + raise Program_Error with + "Container and New_Item denote same container"; + end if; + + -- Use Insert_Space to create the "hole" (the destination slice) into + -- which we copy the source items. + + 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. + + return; + end if; + + B := To_Array_Index (Before); + + Elems (Container) (B .. B + N - 1) := Elemsc (New_Item) (1 .. N); + end Insert; + + ------------------ + -- Insert_Space -- + ------------------ + + procedure Insert_Space + (Container : in out Vector; + Before : Extended_Index; + Count : Count_Type := 1) + is + Old_Length : constant Count_Type := Length (Container); + + Max_Length : Count_Type'Base; -- determined from range of Index_Type + New_Length : Count_Type'Base; -- sum of current length and Count + + Index : Index_Type'Base; -- scratch for intermediate values + J : Count_Type'Base; -- scratch + + begin + -- As a precondition on the generic actual Index_Type, the base type + -- must include Index_Type'Pred (Index_Type'First); this is the value + -- that Container.Last assumes when the vector is empty. However, we do + -- not allow that as the value for Index when specifying where the new + -- items should be inserted, so we must manually check. (That the user + -- is allowed to specify the value at all here is a consequence of the + -- declaration of the Extended_Index subtype, which includes the values + -- in the base range that immediately precede and immediately follow the + -- values in the Index_Type.) + + if Before < Index_Type'First then + raise Constraint_Error with + "Before index is out of range (too small)"; + end if; + + -- We do allow a value greater than Container.Last to be specified as + -- the Index, but only if it's immediately greater. This allows for the + -- case of appending items to the back end of the vector. (It is assumed + -- that specifying an index value greater than Last + 1 indicates some + -- deeper flaw in the caller's algorithm, so that case is treated as a + -- proper error.) + + if Before > Container.Last + and then Before - 1 > Container.Last + then + raise Constraint_Error with + "Before index is out of range (too large)"; + end if; + + -- We treat inserting 0 items into the container as a no-op, so we + -- simply return. + + if Count = 0 then + return; + end if; + + -- 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. + + if Old_Length > Count_Type'Last - Count then + raise Constraint_Error with "Count is out of range"; + end if; + + -- It is now safe compute the length of the new vector, without fear of + -- overflow. + + New_Length := Old_Length + Count; + + -- The second constraint is that the new Last index value cannot exceed + -- Index_Type'Last. In each branch below, we calculate the maximum + -- length (computed from the range of values in Index_Type), and then + -- compare the new length to the maximum length. If the new length is + -- acceptable, then we compute the new last index from that. + + if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then + + -- We have to handle the case when there might be more values in the + -- range of Index_Type than in the range of Count_Type. + + if Index_Type'First <= 0 then + + -- We know that No_Index (the same as Index_Type'First - 1) is + -- less than 0, so it is safe to compute the following sum without + -- fear of overflow. + + Index := No_Index + Index_Type'Base (Count_Type'Last); + + if Index <= Index_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 + -- maximum number of items that are allowed. + + Max_Length := Count_Type'Last; + + else + -- The range of Index_Type has fewer values than in Count_Type, + -- so the maximum number of items is computed from the range of + -- the Index_Type. + + Max_Length := Count_Type'Base (Index_Type'Last - No_Index); + end if; + + else + -- No_Index is equal or greater than 0, so we can safely compute + -- the difference without fear of overflow (which we would have to + -- 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) + 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 + -- maximum number of items that are allowed. + + Max_Length := Count_Type'Last; + + else + -- The range of Index_Type has fewer values than in Count_Type, + -- so the maximum number of items is computed from the range of + -- the Index_Type. + + Max_Length := Count_Type'Base (Index_Type'Last - No_Index); + end if; + end if; + + elsif Index_Type'First <= 0 then + + -- We know that No_Index (the same as Index_Type'First - 1) is less + -- than 0, so it is safe to compute the following sum without fear of + -- overflow. + + J := Count_Type'Base (No_Index) + Count_Type'Last; + + if J <= Count_Type'Base (Index_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 maximum + -- number of items that are allowed. + + Max_Length := Count_Type'Last; + + else + -- The range of Index_Type has fewer values than Count_Type does, + -- so the maximum number of items is computed from the range of + -- the Index_Type. + + Max_Length := + Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index); + end if; + + else + -- No_Index is equal or greater than 0, so we can safely compute the + -- difference without fear of overflow (which we would have to worry + -- about if No_Index were less than 0, but that case is handled + -- above). + + Max_Length := + Count_Type'Base (Index_Type'Last) - Count_Type'Base (No_Index); + end if; + + -- We have just computed the maximum length (number of items). We must + -- now compare the requested length to the maximum length, as we do not + -- allow a vector expand beyond the maximum (because that would create + -- an internal array with a last index value greater than + -- Index_Type'Last, with no way to index those elements). + + if New_Length > Max_Length then + raise Constraint_Error with "Count is out of range"; + end if; + + J := To_Array_Index (Before); + + -- Increase the capacity of container if needed + + 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))); + end if; + + declare + EA : Maximal_Array_Ptr renames Elems (Container); + begin + if Before <= Container.Last then + + -- The new items are being inserted before some existing + -- elements, so we must slide the existing elements up to their + -- new home. + + EA (J + Count .. New_Length) := EA (J .. Old_Length); + end if; + end; + + if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then + Container.Last := No_Index + Index_Type'Base (New_Length); + + else + Container.Last := + Index_Type'Base (Count_Type'Base (No_Index) + New_Length); + end if; + end Insert_Space; + -------------- -- Is_Empty -- -------------- @@ -456,13 +1125,62 @@ is ------------ function Length (Container : Vector) return Capacity_Range is - L : constant Int := Int (Last_Index (Container)); + 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; + ---------- + -- Move -- + ---------- + + 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; + end if; + + if Bounded and then Target.Capacity < LS then + raise Constraint_Error; + end if; + + Clear (Target); + Append (Target, Source); + Clear (Source); + end Move; + + ------------ + -- Prepend -- + ------------ + + procedure Prepend (Container : in out Vector; New_Item : Vector) is + begin + Insert (Container, Index_Type'First, New_Item); + end Prepend; + + procedure Prepend + (Container : in out Vector; + New_Item : Element_Type) + is + begin + Prepend (Container, New_Item, 1); + end Prepend; + + procedure Prepend + (Container : in out Vector; + New_Item : Element_Type; + Count : Count_Type) + is + begin + Insert (Container, Index_Type'First, New_Item, Count); + end Prepend; + --------------------- -- Replace_Element -- --------------------- @@ -499,7 +1217,7 @@ is raise Constraint_Error with "Capacity is out of range"; end if; else - if Capacity > Formal_Vectors.Capacity (Container) then + if Capacity > Formal_Vectors.Current_Capacity (Container) then declare New_Elements : constant Elements_Array_Ptr := new Elements_Array (1 .. Capacity); @@ -609,6 +1327,39 @@ is end; end Swap; + -------------------- + -- To_Array_Index -- + -------------------- + + function To_Array_Index (Index : Index_Type'Base) return Count_Type'Base is + Offset : Count_Type'Base; + + begin + -- We know that + -- Index >= Index_Type'First + -- 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 + -- calculations. + + if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then + Offset := Count_Type'Base (Index - Index_Type'First); + + else + 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. + + return 1 + Offset; + end To_Array_Index; + --------------- -- To_Vector -- --------------- diff --git a/gcc/ada/a-cofove.ads b/gcc/ada/a-cofove.ads index a97d2d8c10b..c7a93dfd15a 100644 --- a/gcc/ada/a-cofove.ads +++ b/gcc/ada/a-cofove.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2004-2016, Free Software Foundation, Inc. -- +-- Copyright (C) 2004-2017, Free Software Foundation, Inc. -- -- -- -- This specification is derived from the Ada Reference Manual for use with -- -- GNAT. The copyright notice above, and the license provisions that follow -- @@ -35,12 +35,12 @@ -- unit compatible with SPARK 2014. Note that the API of this unit may be -- subject to incompatible changes as SPARK 2014 evolves. +with Ada.Containers.Functional_Vectors; + generic type Index_Type is range <>; type Element_Type is private; - with function "=" (Left, Right : Element_Type) return Boolean is <>; - Bounded : Boolean := True; -- If True, the containers are bounded; the initial capacity is the maximum -- size, and heap allocation will be avoided. If False, the containers can @@ -49,7 +49,6 @@ generic package Ada.Containers.Formal_Vectors with SPARK_Mode is - pragma Annotate (GNATprove, External_Axiomatization); pragma Annotate (CodePeer, Skip_Analysis); subtype Extended_Index is Index_Type'Base @@ -73,58 +72,192 @@ is -- unbounded case; you can't assign from one object to another if the -- Capacity is different. + function Length (Container : Vector) return Capacity_Range with + Global => null, + Post => Length'Result <= Capacity (Container); + + pragma Unevaluated_Use_Of_Old (Allow); + + package Formal_Model with Ghost is + + package M is new Ada.Containers.Functional_Vectors + (Index_Type => Index_Type, + Element_Type => Element_Type); + + function "=" + (Left : M.Sequence; + Right : M.Sequence) return Boolean renames M."="; + + function "<" + (Left : M.Sequence; + Right : M.Sequence) return Boolean renames M."<"; + + function "<=" + (Left : M.Sequence; + Right : M.Sequence) return Boolean renames M."<="; + + function M_Elements_In_Union + (Container : M.Sequence; + Left : M.Sequence; + Right : M.Sequence) return Boolean + -- The elements of Container are contained in either Left or Right + with + Global => null, + Post => + M_Elements_In_Union'Result = + (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))); + pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union); + + function M_Elements_Included + (Left : M.Sequence; + L_Fst : Index_Type := Index_Type'First; + L_Lst : Extended_Index; + Right : M.Sequence; + R_Fst : Index_Type := Index_Type'First; + R_Lst : Extended_Index) return Boolean + -- The elements of the slice from L_Fst to L_Lst in Left are contained + -- in the slide from R_Fst to R_Lst in Right. + with + Global => null, + Pre => L_Lst <= M.Last (Left) and R_Lst <= M.Last (Right), + Post => + M_Elements_Included'Result = + (for all I in L_Fst .. L_Lst => + (for some J in R_Fst .. R_Lst => + Element (Left, I) = Element (Right, J))); + pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Included); + + function M_Elements_Reversed + (Left : M.Sequence; + Right : M.Sequence) return Boolean + -- Right is Left in reverse order + with + Global => null, + Post => + 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)) + and (for all I in Index_Type'First .. M.Last (Right) => + Element (Right, I) = + Element (Left, M.Last (Left) - I + 1))); + pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed); + + function M_Elements_Swapped + (Left : M.Sequence; + Right : M.Sequence; + X : Index_Type; + Y : Index_Type) return Boolean + -- Elements stored at X and Y are reversed in Left and Right + with + Global => null, + Pre => X <= M.Last (Left) and Y <= M.Last (Left), + Post => + M_Elements_Swapped'Result = + (M.Length (Left) = M.Length (Right) + and Element (Left, X) = Element (Right, Y) + and Element (Left, Y) = Element (Right, X) + and M.Equal_Except (Left, Right, X, Y)); + pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped); + + function Model (Container : Vector) return M.Sequence with + -- The high-level model of a vector is a sequence of elements. The + -- sequence really is similar to the vector itself. However, it is not + -- limited which allows usage of 'Old and 'Loop_Entry attributes. + + Ghost, + Global => null, + Post => M.Length (Model'Result) = Length (Container); + + function Element + (S : M.Sequence; + 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; + function Empty_Vector return Vector with - Global => null; + Global => null, + Post => Length (Empty_Vector'Result) = 0; function "=" (Left, Right : Vector) return Boolean with - Global => null; + Global => null, + Post => "="'Result = (Model (Left) = Model (Right)); function To_Vector (New_Item : Element_Type; Length : Capacity_Range) return Vector with - Global => null; + 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); function Capacity (Container : Vector) return Capacity_Range with Global => null, - Post => Capacity'Result >= Container.Capacity; + Post => + Capacity'Result = (if Bounded then Container.Capacity + else Capacity_Range'Last); + pragma Annotate (GNATprove, Inline_For_Proof, Capacity); procedure Reserve_Capacity (Container : in out Vector; Capacity : Capacity_Range) with Global => null, - Pre => (if Bounded then Capacity <= Container.Capacity); - - function Length (Container : Vector) return Capacity_Range with - Global => null; + Pre => (if Bounded then Capacity <= Container.Capacity), + Post => Model (Container) = Model (Container)'Old; function Is_Empty (Container : Vector) return Boolean with - Global => null; + Global => null, + Post => Is_Empty'Result = (Length (Container) = 0); procedure Clear (Container : in out Vector) with - Global => null; + Global => null, + Post => Length (Container) = 0; -- Note that this reclaims storage in the unbounded case. You need to call -- this before a container goes out of scope in order to avoid storage -- leaks. In addition, "X := ..." can leak unless you Clear(X) first. procedure Assign (Target : in out Vector; Source : Vector) with Global => null, - Pre => (if Bounded then Length (Source) <= Target.Capacity); + Pre => (if Bounded then Length (Source) <= Target.Capacity), + Post => Model (Target) = Model (Source); function Copy (Source : Vector; Capacity : Capacity_Range := 0) return Vector with Global => null, - Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)); + 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); + + procedure Move (Target : in out Vector; Source : in out Vector) + with + Global => null, + Pre => (if Bounded then Length (Source) <= Capacity (Target)), + Post => Model (Target) = Model (Source)'Old and Length (Source) = 0; function Element (Container : Vector; Index : Index_Type) return Element_Type with Global => null, - Pre => Index in First_Index (Container) .. Last_Index (Container); + Pre => Index in First_Index (Container) .. Last_Index (Container), + Post => Element'Result = Element (Model (Container), Index); + pragma Annotate (GNATprove, Inline_For_Proof, Element); procedure Replace_Element (Container : in out Vector; @@ -132,112 +265,602 @@ is New_Item : Element_Type) with Global => null, - Pre => Index in First_Index (Container) .. Last_Index (Container); + Pre => Index in First_Index (Container) .. Last_Index (Container), + Post => + Length (Container) = Length (Container)'Old - procedure Append + -- Container now has New_Item at index Index + + and Element (Model (Container), Index) = New_Item + + -- All other elements are preserved + + and M.Equal_Except + (Left => Model (Container)'Old, + Right => Model (Container), + Position => Index); + + procedure Insert (Container : in out Vector; + Before : Extended_Index; New_Item : Vector) with Global => null, - Pre => (if Bounded then - Length (Container) + Length (New_Item) <= Container.Capacity); + Pre => + Length (Container) <= Capacity (Container) - Length (New_Item) + and (Before in Index_Type'First .. Last_Index (Container) + or Before - 1 = Last_Index (Container)), + Post => + Length (Container) = Length (Container)'Old + Length (New_Item) + + -- Elements located before Before in Container are preserved + + and M.Range_Equal + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Before - 1) + + -- 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))) + + -- Elements located after Before in Container are shifted + + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Before, + Lst => Last_Index (Container)'Old, + Offset => Length (New_Item)); + + procedure Insert + (Container : in out Vector; + Before : Extended_Index; + New_Item : Element_Type) + with + Global => null, + Pre => + Length (Container) < Capacity (Container) + and then (Before in Index_Type'First .. Last_Index (Container) + 1), + Post => + Length (Container) = Length (Container)'Old + 1 + + -- Elements located before Before in Container are preserved + + and M.Range_Equal + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Before - 1) + + -- Container now has New_Item at index Before + + and Element (Model (Container), Before) = New_Item + + -- Elements located after Before in Container are shifted by 1 + + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Before, + Lst => Last_Index (Container)'Old, + Offset => 1); + + procedure Insert + (Container : in out Vector; + Before : Extended_Index; + New_Item : Element_Type; + Count : Count_Type) + with + Global => null, + Pre => + Length (Container) <= Capacity (Container) - Count + and (Before in Index_Type'First .. Last_Index (Container) + or Before - 1 = Last_Index (Container)), + Post => + Length (Container) = Length (Container)'Old + Count + + -- Elements located before Before in Container are preserved + + and M.Range_Equal + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Before - 1) + + -- 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)) + + -- Elements located after Before in Container are shifted + + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Before, + Lst => Last_Index (Container)'Old, + Offset => Count); + + procedure Prepend + (Container : in out Vector; + New_Item : Vector) + with + Global => null, + Pre => Length (Container) <= Capacity (Container) - Length (New_Item), + Post => + Length (Container) = Length (Container)'Old + Length (New_Item) + + -- Elements of New_Item are inserted at the beginning of Container + + and M.Range_Equal + (Left => Model (New_Item), + Right => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (New_Item)) + + -- Elements of Container are shifted + + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (Container)'Old, + Offset => Length (New_Item)); + + procedure Prepend + (Container : in out Vector; + New_Item : Element_Type) + with + Global => null, + Pre => Length (Container) < Capacity (Container), + Post => + Length (Container) = Length (Container)'Old + 1 + + -- Container now has New_Item at Index_Type'First + + and Element (Model (Container), Index_Type'First) = New_Item + + -- Elements of Container are shifted by 1 + + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (Container)'Old, + Offset => 1); + + procedure Prepend + (Container : in out Vector; + New_Item : Element_Type; + Count : Count_Type) + with + Global => null, + Pre => Length (Container) <= Capacity (Container) - Count, + Post => + Length (Container) = Length (Container)'Old + Count + + -- New_Item is inserted Count times at the beginning of Container + + and M.Constant_Range + (Container => Model (Container), + Fst => Index_Type'First, + Lst => Index_Type'First + Index_Type'Base (Count - 1), + Item => New_Item) + + -- Elements of Container are shifted + + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (Container)'Old, + Offset => Count); + + procedure Append + (Container : in out Vector; + New_Item : Vector) + with + Global => null, + Pre => + Length (Container) <= Capacity (Container) - Length (New_Item), + Post => + Length (Container) = Length (Container)'Old + Length (New_Item) + + -- The elements of Container are preserved + + and Model (Container)'Old <= Model (Container) + + -- 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))); procedure Append (Container : in out Vector; New_Item : Element_Type) with Global => null, - Pre => (if Bounded then - Length (Container) < Container.Capacity); + Pre => Length (Container) < Capacity (Container), + Post => + Length (Container) = Length (Container)'Old + 1 + + -- Elements of Container are preserved + + and Model (Container)'Old < Model (Container) + + -- Container now has New_Item at the end of Container + + and Element + (Model (Container), Last_Index (Container)'Old + 1) = New_Item; + + procedure Append + (Container : in out Vector; + New_Item : Element_Type; + Count : Count_Type) + with + Global => null, + Pre => Length (Container) <= Capacity (Container) - Count, + Post => + Length (Container) = Length (Container)'Old + Count + + -- Elements of Container are preserved + + and Model (Container)'Old <= Model (Container) + + -- 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)); + + procedure Delete + (Container : in out Vector; + Index : Extended_Index) + with + Global => null, + Pre => Index in First_Index (Container) .. Last_Index (Container), + Post => + Length (Container) = Length (Container)'Old - 1 + + -- Elements located before Index in Container are preserved + + and M.Range_Equal + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Index - 1) + + -- Elements located after Index in Container are shifted by 1 + + and M.Range_Shifted + (Left => Model (Container), + Right => Model (Container)'Old, + Fst => Index, + Lst => Last_Index (Container), + Offset => 1); + + procedure Delete + (Container : in out Vector; + Index : Extended_Index; + Count : Count_Type) + with + Global => null, + Pre => + Index in First_Index (Container) .. Last_Index (Container), + Post => + Length (Container) in + Length (Container)'Old - Count .. Length (Container)'Old + + -- The elements of Container located before Index are preserved. + + and M.Range_Equal + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Index_Type'First, + Lst => Index - 1), + + Contract_Cases => + + -- All the elements after Position have been erased + + (Length (Container) - Count <= Count_Type (Index - Index_Type'First) => + Length (Container) = Count_Type (Index - Index_Type'First), + + others => + Length (Container) = Length (Container)'Old - Count + + -- Other elements are shifted by Count + + and M.Range_Shifted + (Left => Model (Container), + Right => Model (Container)'Old, + Fst => Index, + Lst => Last_Index (Container), + Offset => Count)); + + procedure Delete_First + (Container : in out Vector) + with + Global => null, + Pre => Length (Container) > 0, + Post => + Length (Container) = Length (Container)'Old - 1 + + -- Elements of Container are shifted by 1 + + and M.Range_Shifted + (Left => Model (Container), + Right => Model (Container)'Old, + Fst => Index_Type'First, + Lst => Last_Index (Container), + Offset => 1); + + procedure Delete_First + (Container : in out Vector; + Count : Count_Type) + with + Global => null, + Contract_Cases => + + -- All the elements of Container have been erased + + (Length (Container) <= Count => Length (Container) = 0, + + others => + Length (Container) = Length (Container)'Old - Count + + -- Elements of Container are shifted by Count + + and M.Range_Shifted + (Left => Model (Container), + Right => Model (Container)'Old, + Fst => Index_Type'First, + Lst => Last_Index (Container), + Offset => Count)); procedure Delete_Last (Container : in out Vector) with - Global => null; + Global => null, + Pre => Length (Container) > 0, + Post => + Length (Container) = Length (Container)'Old - 1 + + -- Elements of Container are preserved + + and Model (Container) < Model (Container)'Old; + + procedure Delete_Last + (Container : in out Vector; + Count : Count_Type) + with + Global => null, + Contract_Cases => + + -- All the elements after Position have been erased + + (Length (Container) <= Count => Length (Container) = 0, + + others => + Length (Container) = Length (Container)'Old - Count + + -- The elements of Container are preserved + + and Model (Container) <= Model (Container)'Old); procedure Reverse_Elements (Container : in out Vector) with - Global => null; + Global => null, + Post => M_Elements_Reversed (Model (Container)'Old, Model (Container)); procedure Swap (Container : in out Vector; I, 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); + and then J in First_Index (Container) .. Last_Index (Container), + Post => + M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J); function First_Index (Container : Vector) return Index_Type with - Global => null; + Global => null, + Post => First_Index'Result = Index_Type'First; + pragma Annotate (GNATprove, Inline_For_Proof, First_Index); function First_Element (Container : Vector) return Element_Type with Global => null, - Pre => not Is_Empty (Container); + Pre => not Is_Empty (Container), + Post => + First_Element'Result = Element (Model (Container), Index_Type'First); + pragma Annotate (GNATprove, Inline_For_Proof, First_Element); function Last_Index (Container : Vector) return Extended_Index with - Global => null; + Global => null, + Post => Last_Index'Result = M.Last (Model (Container)); + pragma Annotate (GNATprove, Inline_For_Proof, Last_Index); function Last_Element (Container : Vector) return Element_Type with Global => null, - Pre => not Is_Empty (Container); + Pre => not Is_Empty (Container), + Post => + Last_Element'Result = + Element (Model (Container), Last_Index (Container)); + pragma Annotate (GNATprove, Inline_For_Proof, Last_Element); function Find_Index (Container : Vector; Item : Element_Type; Index : Index_Type := Index_Type'First) return Extended_Index with - Global => null; + Global => null, + Contract_Cases => + + -- If Item is not is not contained in Container after Index, Find_Index + -- returns No_Index. + + (Index > Last_Index (Container) + or else not M.Contains + (Container => Model (Container), + Fst => Index, + Lst => Last_Index (Container), + Item => Item) + => + Find_Index'Result = No_Index, + + -- Otherwise, Find_Index returns a valid index greater than Index + + others => + Find_Index'Result in Index .. Last_Index (Container) + + -- The element at this index in Container is Item + + and Element (Model (Container), Find_Index'Result) = Item + + -- It is the first occurrence of Item after Index in Container + + and not M.Contains + (Container => Model (Container), + Fst => Index, + Lst => Find_Index'Result - 1, + Item => Item)); function Reverse_Find_Index (Container : Vector; Item : Element_Type; Index : Index_Type := Index_Type'Last) return Extended_Index with - Global => null; + Global => null, + Contract_Cases => + + -- If Item is not is not contained in Container before Index, + -- Reverse_Find_Index returns No_Index. + + (not M.Contains + (Container => Model (Container), + Fst => Index_Type'First, + Lst => (if Index <= Last_Index (Container) then Index + else Last_Index (Container)), + Item => Item) + => + Reverse_Find_Index'Result = No_Index, + + -- Otherwise, Reverse_Find_Index returns a valid index smaller than + -- Index + + others => + 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 + + and Element (Model (Container), Reverse_Find_Index'Result) = Item + + -- It is the last occurrence of Item before Index in Container + + and not M.Contains + (Container => Model (Container), + Fst => Reverse_Find_Index'Result + 1, + Lst => + (if Index <= Last_Index (Container) then Index + else Last_Index (Container)), + Item => Item)); function Contains (Container : Vector; Item : Element_Type) return Boolean with - Global => null; + Global => null, + Post => + Contains'Result = M.Contains (Container => Model (Container), + Fst => Index_Type'First, + Lst => Last_Index (Container), + Item => Item); function Has_Element (Container : Vector; Position : Extended_Index) return Boolean with - Global => null; + Global => null, + Post => + Has_Element'Result = + (Position in Index_Type'First .. Last_Index (Container)); + pragma Annotate (GNATprove, Inline_For_Proof, Has_Element); generic with function "<" (Left, Right : Element_Type) return Boolean is <>; package Generic_Sorting with SPARK_Mode is + function M_Elements_Sorted (Container : M.Sequence) return Boolean with + Ghost, + Global => null, + 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))); + pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted); function Is_Sorted (Container : Vector) return Boolean with - Global => null; + Global => null, + Post => Is_Sorted'Result = M_Elements_Sorted (Model (Container)); procedure Sort (Container : in out Vector) with - Global => null; - + Global => null, + 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)); + + procedure Merge (Target : in out Vector; Source : in out Vector) with + -- Target and Source should not be aliased + Global => null, + Pre => Length (Source) <= Capacity (Target) - Length (Target), + Post => + Length (Target) = Length (Target)'Old + Length (Source)'Old + 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); end Generic_Sorting; - function First_To_Previous - (Container : Vector; - Current : Index_Type) return Vector - with - Ghost, - Global => null, - Pre => Current in First_Index (Container) .. Last_Index (Container); - - function Current_To_Last - (Container : Vector; - Current : Index_Type) return Vector - with - Ghost, - Global => null, - Pre => Current in First_Index (Container) .. Last_Index (Container); - -- First_To_Previous returns a container containing all elements preceding - -- Current (excluded) in Container. Current_To_Last returns a container - -- containing all elements following Current (included) in Container. - -- These two new functions can be used to express invariant properties in - -- loops which iterate over containers. First_To_Previous returns the part - -- of the container already scanned and Current_To_Last the part not - -- scanned yet. - private pragma SPARK_Mode (Off); diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index 1c8f9e6fc48..5b0946c3587 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -1482,7 +1482,7 @@ package body Freeze is A_Post := Get_Pragma (Par_Prim, Pragma_Postcondition); if Present (A_Post) and then Class_Present (A_Post) then - New_Prag := New_Copy_Tree (A_Pre); + New_Prag := New_Copy_Tree (A_Post); Build_Class_Wide_Expression (Prag => New_Prag, Subp => Prim, diff --git a/gcc/ada/g-dyntab.adb b/gcc/ada/g-dyntab.adb index a74697dffba..e011ad849ad 100644 --- a/gcc/ada/g-dyntab.adb +++ b/gcc/ada/g-dyntab.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2000-2016, AdaCore -- +-- Copyright (C) 2000-2017, AdaCore -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -279,7 +279,8 @@ package body GNAT.Dynamic_Tables is new Ada.Unchecked_Conversion (Alloc_Ptr, Table_Ptr); Old_Table : Old_Alloc_Ptr := To_Old_Alloc_Ptr (T.Table); - New_Table : constant Alloc_Ptr := new Alloc_Type'(Old_Table.all); + New_Table : constant Alloc_Ptr := + 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_prag.adb b/gcc/ada/sem_prag.adb index 702f4624c08..e4efaabeb44 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -24007,16 +24007,20 @@ package body Sem_Prag is & "of &", Nod, Disp_Typ); end if; - -- Otherwise we have a call to an overridden primitive, and - -- we will create a common class-wide clone for the body of - -- original operation and its eventual inherited versions. - -- If the original operation dispatches on result it is - -- never inherited and there is no need for a clone. + -- Otherwise we have a call to an overridden primitive, and we + -- will create a common class-wide clone for the body of + -- original operation and its eventual inherited versions. If + -- the original operation dispatches on result it is never + -- inherited and there is no need for a clone. There is not + -- need for a clone either in GNATprove mode, as cases that + -- would require it are rejected (when an inherited primitive + -- calls an overridden operation in a class-wide contract), and + -- the clone would make proof impossible in some cases. elsif not Is_Abstract_Subprogram (Spec_Id) and then No (Class_Wide_Clone (Spec_Id)) and then not Has_Controlling_Result (Spec_Id) - and then SPARK_Mode /= On + and then not GNATprove_Mode then Build_Class_Wide_Clone_Decl (Spec_Id); end if;