Skip to content

R
riscv-gcc-1
Commit 78f2b7ce by Arnaud Charlet
Options

[multiple changes] 

2017-04-27  Ed Schonberg  <schonberg@adacore.com>

	* freeze.adb: copy-paste typo.

2017-04-27  Yannick Moy  <moy@adacore.com>

	* 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  <dross@adacore.com>

	* 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  <duff@adacore.com>

	* g-dyntab.adb (Release): When allocating the new
	table, use the correct slice of the old table to initialize it.

From-SVN: r247316
parent 02848684
Showing with 3642 additions and 342 deletions
gcc/ada/ChangeLog
2017-04-27 Ed Schonberg <schonberg@adacore.com>
* freeze.adb: copy-paste typo.
2017-04-27 Yannick Moy <moy@adacore.com>
* 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 <dross@adacore.com>
* 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 <duff@adacore.com>
* 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 <ebotcazou@adacore.com> 2017-04-27 Eric Botcazou <ebotcazou@adacore.com>
* einfo.ads: Minor fixes in comments. * einfo.ads: Minor fixes in comments.
......
gcc/ada/a-cfdlli.adb
...@@ -488,54 +488,70 @@ is ...@@ -488,54 +488,70 @@ is
procedure Lift_Abstraction_Level (Container : List) is null; procedure Lift_Abstraction_Level (Container : List) is null;
------------------------- -------------------------
-- M_Elements_Reversed -- -- M_Elements_In_Union --
------------------------- -------------------------
function M_Elements_Reversed function M_Elements_In_Union
(Left : M.Sequence; (Container : M.Sequence;
Right : M.Sequence) return Boolean Left : M.Sequence;
Right : M.Sequence) return Boolean
is is
L : constant Count_Type := M.Length (Left);
begin begin
if L /= M.Length (Right) then for I in 1 .. M.Length (Container) loop
return False; declare
end if; Found : Boolean := False;
J : Count_Type := 0;
for I in 1 .. L loop begin
if Element (Left, I) /= Element (Right, L - I + 1) while not Found and J < M.Length (Left) loop
then J := J + 1;
return False; if Element (Container, I) = Element (Left, J) then
end if; 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; end loop;
return True; return True;
end M_Elements_Reversed; end M_Elements_In_Union;
------------------------- -------------------------
-- M_Elements_Shuffled -- -- M_Elements_Included --
------------------------- -------------------------
function M_Elements_Shuffle function M_Elements_Included
(Left : M.Sequence; (Left : M.Sequence;
Right : M.Sequence; L_Fst : Positive_Count_Type := 1;
Fst : Positive_Count_Type; L_Lst : Count_Type;
Lst : Count_Type; Right : M.Sequence;
Offset : Count_Type'Base) return Boolean R_Fst : Positive_Count_Type := 1;
R_Lst : Count_Type) return Boolean
is is
begin begin
for I in Fst .. Lst loop for I in L_Fst .. L_Lst loop
declare declare
Found : Boolean := False; Found : Boolean := False;
J : Count_Type := Fst; J : Count_Type := R_Fst - 1;
begin begin
while not Found and J <= Lst loop while not Found and J < R_Lst loop
if Element (Left, I) = Element (Right, J + Offset) then J := J + 1;
if Element (Left, I) = Element (Right, J) then
Found := True; Found := True;
end if; end if;
J := J + 1;
end loop; end loop;
if not Found then if not Found then
...@@ -545,7 +561,32 @@ is ...@@ -545,7 +561,32 @@ is
end loop; end loop;
return True; 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 -- -- M_Elements_Swapted --
...@@ -892,7 +933,8 @@ is ...@@ -892,7 +933,8 @@ is
begin begin
if Target'Address = Source'Address then if Target'Address = Source'Address then
return; raise Program_Error with
"Target and Source denote same container";
end if; end if;
LI := First (Target); LI := First (Target);
...@@ -1466,7 +1508,7 @@ is ...@@ -1466,7 +1508,7 @@ is
begin begin
if CFirst = 0 then if CFirst = 0 then
CFirst := Container.First; CFirst := Container.Last;
end if; end if;
if Container.Length = 0 then if Container.Length = 0 then
...@@ -1497,14 +1539,13 @@ is ...@@ -1497,14 +1539,13 @@ is
SN : Node_Array renames Source.Nodes; SN : Node_Array renames Source.Nodes;
begin begin
if Before.Node /= 0 then if Target'Address = Source'Address then
pragma Assert (Vet (Target, Before), "bad cursor in Splice"); raise Program_Error with
"Target and Source denote same container";
end if; end if;
if Target'Address = Source'Address if Before.Node /= 0 then
or else Source.Length = 0 pragma Assert (Vet (Target, Before), "bad cursor in Splice");
then
return;
end if; end if;
pragma Assert (SN (Source.First).Prev = 0); pragma Assert (SN (Source.First).Prev = 0);
...@@ -1535,8 +1576,8 @@ is ...@@ -1535,8 +1576,8 @@ is
begin begin
if Target'Address = Source'Address then if Target'Address = Source'Address then
Splice (Target, Before, Position); raise Program_Error with
return; "Target and Source denote same container";
end if; end if;
if Position.Node = 0 then if Position.Node = 0 then
......
gcc/ada/a-cfdlli.ads
...@@ -81,25 +81,40 @@ is ...@@ -81,25 +81,40 @@ is
(Left : M.Sequence; (Left : M.Sequence;
Right : M.Sequence) return Boolean renames M."<="; Right : M.Sequence) return Boolean renames M."<=";
function M_Elements_Shuffle function M_Elements_In_Union
(Left : M.Sequence; (Container : M.Sequence;
Right : M.Sequence; Left : M.Sequence;
Fst : Positive_Count_Type; Right : M.Sequence) return Boolean
Lst : Count_Type; -- The elements of Container are contained in either Left or Right
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
with with
Global => null, Global => null,
Pre =>
Lst <= M.Length (Left)
and Offset in 1 - Fst .. M.Length (Right) - Lst,
Post => Post =>
M_Elements_Shuffle'Result = M_Elements_In_Union'Result =
(for all J in Fst + Offset .. Lst + Offset => (for all I in 1 .. M.Length (Container) =>
(for some I in Fst .. Lst => (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))); 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 function M_Elements_Reversed
(Left : M.Sequence; (Left : M.Sequence;
...@@ -242,7 +257,7 @@ is ...@@ -242,7 +257,7 @@ is
M.Get (M_Right, P.Get (P_Right, C)))); M.Get (M_Right, P.Get (P_Right, C))));
function Model (Container : List) return M.Sequence with 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. -- not represented in this model.
Ghost, Ghost,
...@@ -279,8 +294,8 @@ is ...@@ -279,8 +294,8 @@ is
-- assume that we can access to the same elements by iterating over -- assume that we can access to the same elements by iterating over
-- positions or cursors. -- positions or cursors.
-- This information is not generally useful except when switching from -- This information is not generally useful except when switching from
-- a lowlevel, cursor aware view of a container, to a highlevel -- a low-level cursor-aware view of a container to a high-level
-- position based view. -- position-based view.
Ghost, Ghost,
Global => null, Global => null,
...@@ -466,6 +481,15 @@ is ...@@ -466,6 +481,15 @@ is
-- Container contains Count times New_Item at the end -- 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 and M.Constant_Range
(Container => Model (Container), (Container => Model (Container),
Fst => Length (Container)'Old + 1, Fst => Length (Container)'Old + 1,
...@@ -747,11 +771,12 @@ is ...@@ -747,11 +771,12 @@ is
-- Container contains Count times New_Item at the end -- Container contains Count times New_Item at the end
and M.Constant_Range and (if Count > 0 then
(Container => Model (Container), M.Constant_Range
Fst => Length (Container)'Old + 1, (Container => Model (Container),
Lst => Length (Container), Fst => Length (Container)'Old + 1,
Item => New_Item) Lst => Length (Container),
Item => New_Item))
-- Count cursors have been inserted at the end of Container -- Count cursors have been inserted at the end of Container
...@@ -782,11 +807,11 @@ is ...@@ -782,11 +807,11 @@ is
-- The elements located after Position are shifted by 1 -- The elements located after Position are shifted by 1
and M.Range_Shifted and M.Range_Shifted
(Left => Model (Container)'Old, (Left => Model (Container),
Right => Model (Container), Right => Model (Container)'Old,
Fst => P.Get (Positions (Container)'Old, Position'Old) + 1, Fst => P.Get (Positions (Container)'Old, Position'Old),
Lst => Length (Container)'Old, Lst => Length (Container),
Offset => -1) Offset => 1)
-- Position has been removed from Container -- Position has been removed from Container
...@@ -840,12 +865,11 @@ is ...@@ -840,12 +865,11 @@ is
-- Other elements are shifted by Count -- Other elements are shifted by Count
and M.Range_Shifted and M.Range_Shifted
(Left => Model (Container)'Old, (Left => Model (Container),
Right => Model (Container), Right => Model (Container)'Old,
Fst => Fst => P.Get (Positions (Container)'Old, Position'Old),
P.Get (Positions (Container)'Old, Position'Old) + Count, Lst => Length (Container),
Lst => Length (Container)'Old, Offset => Count)
Offset => -Count)
-- Count cursors have been removed from Container at Position -- Count cursors have been removed from Container at Position
...@@ -864,11 +888,11 @@ is ...@@ -864,11 +888,11 @@ is
-- The elements of Container are shifted by 1 -- The elements of Container are shifted by 1
and M.Range_Shifted and M.Range_Shifted
(Left => Model (Container)'Old, (Left => Model (Container),
Right => Model (Container), Right => Model (Container)'Old,
Fst => 2, Fst => 1,
Lst => Length (Container)'Old, Lst => Length (Container),
Offset => -1) Offset => 1)
-- The first cursor of Container has been removed -- The first cursor of Container has been removed
...@@ -892,11 +916,11 @@ is ...@@ -892,11 +916,11 @@ is
-- Elements of Container are shifted by Count -- Elements of Container are shifted by Count
and M.Range_Shifted and M.Range_Shifted
(Left => Model (Container)'Old, (Left => Model (Container),
Right => Model (Container), Right => Model (Container)'Old,
Fst => Count + 1, Fst => 1,
Lst => Length (Container)'Old, Lst => Length (Container),
Offset => -Count) Offset => Count)
-- The first Count cursors have been removed from Container -- The first Count cursors have been removed from Container
...@@ -957,7 +981,7 @@ is ...@@ -957,7 +981,7 @@ is
procedure Reverse_Elements (Container : in out List) with procedure Reverse_Elements (Container : in out List) with
Global => null, Global => null,
Post => M_Elements_Reversed (Model (Container'Old), Model (Container)); Post => M_Elements_Reversed (Model (Container)'Old, Model (Container));
procedure Swap procedure Swap
(Container : in out List; (Container : in out List;
...@@ -1017,12 +1041,19 @@ is ...@@ -1017,12 +1041,19 @@ is
-- The elements of Source are appended to target, the order is not -- The elements of Source are appended to target, the order is not
-- specified. -- specified.
and M_Elements_Shuffle and M_Elements_Included
(Left => Model (Source)'Old, (Left => Model (Source)'Old,
L_Lst => Length (Source)'Old,
Right => Model (Target), Right => Model (Target),
Fst => 1, R_Fst => Length (Target)'Old + 1,
Lst => Length (Source)'Old, R_Lst => Length (Target))
Offset => Length (Target)'Old)
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 -- Cursors have been inserted at the end of Target
...@@ -1045,12 +1076,22 @@ is ...@@ -1045,12 +1076,22 @@ is
-- The elements of Source are inserted before Before, the order is -- The elements of Source are inserted before Before, the order is
-- not specified. -- not specified.
and M_Elements_Shuffle and M_Elements_Included
(Left => Model (Source)'Old, (Left => Model (Source)'Old,
Right => Model (Target), L_Lst => Length (Source)'Old,
Fst => 1, Right => Model (Target),
Lst => Length (Source)'Old, R_Fst => P.Get (Positions (Target)'Old, Before),
Offset => P.Get (Positions (Target)'Old, Before) - 1) 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 -- Other elements are shifted by the length of Source
...@@ -1390,7 +1431,7 @@ is ...@@ -1390,7 +1431,7 @@ is
P.Get (Positions (Container), Find'Result) >= P.Get (Positions (Container), Find'Result) >=
P.Get (Positions (Container), Position)) 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 and not M.Contains
(Container => Model (Container), (Container => Model (Container),
...@@ -1445,7 +1486,7 @@ is ...@@ -1445,7 +1486,7 @@ is
P.Get (Positions (Container), Reverse_Find'Result) <= P.Get (Positions (Container), Reverse_Find'Result) <=
P.Get (Positions (Container), Position)) 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 and not M.Contains
(Container => Model (Container), (Container => Model (Container),
...@@ -1489,7 +1530,7 @@ is ...@@ -1489,7 +1530,7 @@ is
Post => Post =>
M_Elements_Sorted'Result = M_Elements_Sorted'Result =
(for all I in 1 .. M.Length (Container) => (for all I in 1 .. M.Length (Container) =>
(for all J in I + 1 .. M.Length (Container) => (for all J in I .. M.Length (Container) =>
Element (Container, I) = Element (Container, J) Element (Container, I) = Element (Container, J)
or Element (Container, I) < Element (Container, J))); or Element (Container, I) < Element (Container, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
...@@ -1502,7 +1543,15 @@ is ...@@ -1502,7 +1543,15 @@ is
Global => null, Global => null,
Post => Post =>
Length (Container) = Length (Container)'Old 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 procedure Merge (Target : in out List; Source : in out List) with
-- Target and Source should not be aliased -- Target and Source should not be aliased
...@@ -1513,7 +1562,18 @@ is ...@@ -1513,7 +1562,18 @@ is
and Length (Source) = 0 and Length (Source) = 0
and (if M_Elements_Sorted (Model (Target)'Old) and (if M_Elements_Sorted (Model (Target)'Old)
and M_Elements_Sorted (Model (Source)'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; end Generic_Sorting;
private private
......
gcc/ada/a-cfinve.adb
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- B o d y -- -- 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 -- -- 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- -- -- terms of the GNU General Public License as published by the Free Soft- --
...@@ -25,6 +25,11 @@ ...@@ -25,6 +25,11 @@
-- <http://www.gnu.org/licenses/>. -- -- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
with Ada.Containers.Generic_Array_Sort;
with Ada.Unchecked_Deallocation;
with System; use type System.Address;
package body Ada.Containers.Formal_Indefinite_Vectors with package body Ada.Containers.Formal_Indefinite_Vectors with
SPARK_Mode => Off SPARK_Mode => Off
is is
...@@ -32,12 +37,68 @@ is ...@@ -32,12 +37,68 @@ is
function H (New_Item : Element_Type) return Holder renames To_Holder; function H (New_Item : Element_Type) return Holder renames To_Holder;
function E (Container : Holder) return Element_Type renames Get; 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 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 -- -- Append --
...@@ -45,7 +106,15 @@ is ...@@ -45,7 +106,15 @@ is
procedure Append (Container : in out Vector; New_Item : Vector) is procedure Append (Container : in out Vector; New_Item : Vector) is
begin 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; end Append;
procedure Append procedure Append
...@@ -53,7 +122,24 @@ is ...@@ -53,7 +122,24 @@ is
New_Item : Element_Type) New_Item : Element_Type)
is is
begin 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; end Append;
------------ ------------
...@@ -61,8 +147,19 @@ is ...@@ -61,8 +147,19 @@ is
------------ ------------
procedure Assign (Target : in out Vector; Source : Vector) is procedure Assign (Target : in out Vector; Source : Vector) is
LS : constant Capacity_Range := Length (Source);
begin 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; end Assign;
-------------- --------------
...@@ -70,7 +167,10 @@ is ...@@ -70,7 +167,10 @@ is
-------------- --------------
function Capacity (Container : Vector) return Capacity_Range 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 -- -- Clear --
...@@ -78,7 +178,11 @@ is ...@@ -78,7 +178,11 @@ is
procedure Clear (Container : in out Vector) is procedure Clear (Container : in out Vector) is
begin 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; end Clear;
-------------- --------------
...@@ -89,7 +193,9 @@ is ...@@ -89,7 +193,9 @@ is
(Container : Vector; (Container : Vector;
Item : Element_Type) return Boolean Item : Element_Type) return Boolean
is is
(Contains (Container.V, H (Item))); begin
return Find_Index (Container, Item) /= No_Index;
end Contains;
---------- ----------
-- Copy -- -- Copy --
...@@ -99,19 +205,173 @@ is ...@@ -99,19 +205,173 @@ is
(Source : Vector; (Source : Vector;
Capacity : Capacity_Range := 0) return Vector Capacity : Capacity_Range := 0) return Vector
is is
((if Capacity = 0 then Length (Source) else Capacity), LS : constant Capacity_Range := Length (Source);
V => Copy (Source.V, Capacity)); C : Capacity_Range;
--------------------- begin
-- Current_To_Last -- if Capacity = 0 then
--------------------- C := LS;
elsif Capacity >= LS then
C := Capacity;
else
raise Capacity_Error;
end if;
function Current_To_Last return Target : Vector (C) do
(Container : Vector; Elems (Target) (1 .. LS) := Elemsc (Source) (1 .. LS);
Current : Index_Type) return Vector is 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 begin
return (Length (Container), Current_To_Last (Container.V, Current)); if Count = 0 then
end Current_To_Last; return;
elsif Count >= Length (Container) then
Clear (Container);
return;
else
Delete (Container, Index_Type'First, Count);
end if;
end Delete_First;
----------------- -----------------
-- Delete_Last -- -- Delete_Last --
...@@ -121,7 +381,38 @@ is ...@@ -121,7 +381,38 @@ is
(Container : in out Vector) (Container : in out Vector)
is is
begin 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; end Delete_Last;
------------- -------------
...@@ -130,8 +421,39 @@ is ...@@ -130,8 +421,39 @@ is
function Element function Element
(Container : Vector; (Container : Vector;
Index : Index_Type) return Element_Type is Index : Index_Type) return Element_Type
(E (Element (Container.V, Index))); 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 -- -- Find_Index --
...@@ -142,32 +464,190 @@ is ...@@ -142,32 +464,190 @@ is
Item : Element_Type; Item : Element_Type;
Index : Index_Type := Index_Type'First) return Extended_Index Index : Index_Type := Index_Type'First) return Extended_Index
is 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 -- -- First_Element --
------------------- -------------------
function First_Element (Container : Vector) return Element_Type is 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 -- -- First_Index --
----------------- -----------------
function First_Index (Container : Vector) return Index_Type is 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 package body Formal_Model is
(Container : Vector;
Current : Index_Type) return Vector is -------------------------
begin -- M_Elements_In_Union --
return (Length (Container), First_To_Previous (Container.V, Current)); -------------------------
end First_To_Previous;
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 -- -- Generic_Sorting --
...@@ -175,65 +655,537 @@ is ...@@ -175,65 +655,537 @@ is
package body Generic_Sorting with SPARK_Mode => Off 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 -- -- Is_Sorted --
--------------- ---------------
function Is_Sorted (Container : Vector) return Boolean is 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 -- -- 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 begin
Sort (Container.V); if Container.Last <= Index_Type'First then
return;
else
Sort (Elems (Container) (1 .. Len));
end if;
end Sort; 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; 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 -- -- Has_Element --
----------------- -----------------
function Has_Element function Has_Element
(Container : Vector; (Container : Vector; Position : Extended_Index) return Boolean is
Position : Extended_Index) return Boolean 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 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 -- -- Is_Empty --
-------------- --------------
function Is_Empty (Container : Vector) return Boolean is 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 -- -- Last_Element --
------------------ ------------------
function Last_Element (Container : Vector) return Element_Type is 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 -- -- Last_Index --
---------------- ----------------
function Last_Index (Container : Vector) return Extended_Index is function Last_Index (Container : Vector) return Extended_Index is
(Last_Index (Container.V)); begin
return Container.Last;
end Last_Index;
------------ ------------
-- Length -- -- Length --
------------ ------------
function Length (Container : Vector) return Capacity_Range is 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 -- -- Replace_Element --
...@@ -245,7 +1197,16 @@ is ...@@ -245,7 +1197,16 @@ is
New_Item : Element_Type) New_Item : Element_Type)
is is
begin 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; end Replace_Element;
---------------------- ----------------------
...@@ -257,7 +1218,23 @@ is ...@@ -257,7 +1218,23 @@ is
Capacity : Capacity_Range) Capacity : Capacity_Range)
is is
begin 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; end Reserve_Capacity;
---------------------- ----------------------
...@@ -266,7 +1243,30 @@ is ...@@ -266,7 +1243,30 @@ is
procedure Reverse_Elements (Container : in out Vector) is procedure Reverse_Elements (Container : in out Vector) is
begin 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; end Reverse_Elements;
------------------------ ------------------------
...@@ -278,7 +1278,27 @@ is ...@@ -278,7 +1278,27 @@ is
Item : Element_Type; Item : Element_Type;
Index : Index_Type := Index_Type'Last) return Extended_Index Index : Index_Type := Index_Type'Last) return Extended_Index
is 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 -- -- Swap --
...@@ -286,9 +1306,66 @@ is ...@@ -286,9 +1306,66 @@ is
procedure Swap (Container : in out Vector; I, J : Index_Type) is procedure Swap (Container : in out Vector; I, J : Index_Type) is
begin 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; 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 -- -- To_Vector --
--------------- ---------------
...@@ -298,7 +1375,27 @@ is ...@@ -298,7 +1375,27 @@ is
Length : Capacity_Range) return Vector Length : Capacity_Range) return Vector
is is
begin 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 To_Vector;
end Ada.Containers.Formal_Indefinite_Vectors; end Ada.Containers.Formal_Indefinite_Vectors;
gcc/ada/a-cfinve.ads
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- S p e c -- -- 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 -- -- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow -- -- GNAT. The copyright notice above, and the license provisions that follow --
...@@ -30,11 +30,10 @@ ...@@ -30,11 +30,10 @@
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
-- Similar to Ada.Containers.Formal_Vectors. The main difference is that -- Similar to Ada.Containers.Formal_Vectors. The main difference is that
-- Element_Type may be indefinite (but not an unconstrained array). In -- Element_Type may be indefinite (but not an unconstrained array).
-- addition, this is simplified by removing less-used functionality.
with Ada.Containers.Bounded_Holders; with Ada.Containers.Bounded_Holders;
with Ada.Containers.Formal_Vectors; with Ada.Containers.Functional_Vectors;
generic generic
type Index_Type is range <>; type Index_Type is range <>;
...@@ -48,8 +47,6 @@ generic ...@@ -48,8 +47,6 @@ generic
-- responsibility of clients to calculate the maximum size of all types in -- responsibility of clients to calculate the maximum size of all types in
-- the class. -- the class.
with function "=" (Left, Right : Element_Type) return Boolean is <>;
Bounded : Boolean := True; Bounded : Boolean := True;
-- If True, the containers are bounded; the initial capacity is the maximum -- If True, the containers are bounded; the initial capacity is the maximum
-- size, and heap allocation will be avoided. If False, the containers can -- size, and heap allocation will be avoided. If False, the containers can
...@@ -58,7 +55,6 @@ generic ...@@ -58,7 +55,6 @@ generic
package Ada.Containers.Formal_Indefinite_Vectors with package Ada.Containers.Formal_Indefinite_Vectors with
SPARK_Mode => On SPARK_Mode => On
is is
pragma Annotate (GNATprove, External_Axiomatization);
pragma Annotate (CodePeer, Skip_Analysis); pragma Annotate (CodePeer, Skip_Analysis);
subtype Extended_Index is Index_Type'Base subtype Extended_Index is Index_Type'Base
...@@ -71,60 +67,203 @@ is ...@@ -71,60 +67,203 @@ is
Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1); Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
type Vector (Capacity : Capacity_Range) is limited private with 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 function Empty_Vector return Vector with
Global => null; Global => null,
Post => Length (Empty_Vector'Result) = 0;
function "=" (Left, Right : Vector) return Boolean with function "=" (Left, Right : Vector) return Boolean with
Global => null; Global => null,
Post => "="'Result = (Model (Left) = Model (Right));
function To_Vector function To_Vector
(New_Item : Element_Type; (New_Item : Element_Type;
Length : Capacity_Range) return Vector Length : Capacity_Range) return Vector
with 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 function Capacity (Container : Vector) return Capacity_Range with
Global => null, 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 procedure Reserve_Capacity
(Container : in out Vector; (Container : in out Vector;
Capacity : Capacity_Range) Capacity : Capacity_Range)
with with
Global => null, Global => null,
Pre => (if Bounded then Capacity <= Container.Capacity); Pre => (if Bounded then Capacity <= Container.Capacity),
Post => Model (Container) = Model (Container)'Old;
function Length (Container : Vector) return Capacity_Range with
Global => null;
function Is_Empty (Container : Vector) return Boolean with 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 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 -- 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 -- 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 procedure Assign (Target : in out Vector; Source : Vector) with
Global => null, 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 function Copy
(Source : Vector; (Source : Vector;
Capacity : Capacity_Range := 0) return Vector Capacity : Capacity_Range := 0) return Vector
with with
Global => null, 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 function Element
(Container : Vector; (Container : Vector;
Index : Index_Type) return Element_Type Index : Index_Type) return Element_Type
with with
Global => null, 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 procedure Replace_Element
(Container : in out Vector; (Container : in out Vector;
...@@ -132,102 +271,602 @@ is ...@@ -132,102 +271,602 @@ is
New_Item : Element_Type) New_Item : Element_Type)
with with
Global => null, 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; (Container : in out Vector;
Before : Extended_Index;
New_Item : Vector) New_Item : Vector)
with with
Global => null, Global => null,
Pre => (if Bounded Pre =>
then Length (Container) + Length (New_Item) <= Length (Container) <= Capacity (Container) - Length (New_Item)
Container.Capacity); 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 procedure Append
(Container : in out Vector; (Container : in out Vector;
New_Item : Element_Type) New_Item : Element_Type)
with with
Global => null, Global => null,
Pre => (if Bounded Pre => Length (Container) < Capacity (Container),
then Length (Container) < Container.Capacity); 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 procedure Delete_Last
(Container : in out Vector) (Container : in out Vector)
with 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 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 procedure Swap (Container : in out Vector; I, J : Index_Type) with
Global => null, Global => null,
Pre => I in First_Index (Container) .. Last_Index (Container) Pre => I in First_Index (Container) .. Last_Index (Container)
and then J in First_Index (Container) .. Last_Index (Container); 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 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 function First_Element (Container : Vector) return Element_Type with
Global => null, 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 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 function Last_Element (Container : Vector) return Element_Type with
Global => null, 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 function Find_Index
(Container : Vector; (Container : Vector;
Item : Element_Type; Item : Element_Type;
Index : Index_Type := Index_Type'First) return Extended_Index Index : Index_Type := Index_Type'First) return Extended_Index
with 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 function Reverse_Find_Index
(Container : Vector; (Container : Vector;
Item : Element_Type; Item : Element_Type;
Index : Index_Type := Index_Type'Last) return Extended_Index Index : Index_Type := Index_Type'Last) return Extended_Index
with 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 function Contains
(Container : Vector; (Container : Vector;
Item : Element_Type) return Boolean Item : Element_Type) return Boolean
with 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 function Has_Element
(Container : Vector; Position : Extended_Index) return Boolean with (Container : Vector;
Global => null; 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 generic
with function "<" (Left, Right : Element_Type) return Boolean is <>; with function "<" (Left, Right : Element_Type) return Boolean is <>;
package Generic_Sorting with SPARK_Mode 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 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 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; 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 private
pragma SPARK_Mode (Off); pragma SPARK_Mode (Off);
...@@ -240,23 +879,39 @@ private ...@@ -240,23 +879,39 @@ private
pragma Inline (Contains); pragma Inline (Contains);
-- The implementation method is to instantiate Bounded_Holders to get a -- The implementation method is to instantiate Bounded_Holders to get a
-- definite type for Element_Type, and then use that Holder type to -- definite type for Element_Type.
-- instantiate Formal_Vectors. All the operations are just wrappers.
package Holders is new Bounded_Holders package Holders is new Bounded_Holders
(Element_Type, Max_Size_In_Storage_Elements, "="); (Element_Type, Max_Size_In_Storage_Elements, "=");
use Holders; use Holders;
package Def is new Formal_Vectors (Index_Type, Holder, "=", Bounded); subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last;
use Def; 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 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; 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 function Empty_Vector return Vector is
((Capacity => 0, V => Def.Empty_Vector)); ((Capacity => 0, others => <>));
end Ada.Containers.Formal_Indefinite_Vectors; end Ada.Containers.Formal_Indefinite_Vectors;
gcc/ada/a-cofove.adb
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- B o d y -- -- 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 -- -- 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- -- -- terms of the GNU General Public License as published by the Free Soft- --
...@@ -39,7 +39,6 @@ is ...@@ -39,7 +39,6 @@ is
-- leads to amortized linear-time copying. -- leads to amortized linear-time copying.
type Int is range System.Min_Int .. System.Max_Int; type Int is range System.Min_Int .. System.Max_Int;
type UInt is mod System.Max_Binary_Modulus;
procedure Free is procedure Free is
new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr); new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr);
...@@ -66,6 +65,15 @@ is ...@@ -66,6 +65,15 @@ is
(Container : Vector; (Container : Vector;
Position : Capacity_Range) return Element_Type; 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 ...@@ -95,34 +103,40 @@ is
procedure Append (Container : in out Vector; New_Item : Vector) is procedure Append (Container : in out Vector; New_Item : Vector) is
begin begin
for X in First_Index (New_Item) .. Last_Index (New_Item) loop if Is_Empty (New_Item) then
Append (Container, Element (New_Item, X)); return;
end loop; 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; end Append;
procedure Append procedure Append
(Container : in out Vector; (Container : in out Vector;
New_Item : Element_Type) New_Item : Element_Type)
is is
New_Length : constant UInt := UInt (Length (Container) + 1);
begin begin
if not Bounded and then Append (Container, New_Item, 1);
Capacity (Container) < Capacity_Range (New_Length) end Append;
then
Reserve_Capacity procedure Append
(Container, (Container : in out Vector;
Capacity_Range'Max (Capacity (Container) * Growth_Factor, New_Item : Element_Type;
Capacity_Range (New_Length))); Count : Count_Type)
is
begin
if Count = 0 then
return;
end if; 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"; raise Constraint_Error with "vector is already at its maximum length";
end if; end if;
-- TODO: should check whether length > max capacity (cnt_t'last) ??? Insert (Container, Container.Last + 1, New_Item, Count);
Container.Last := Container.Last + 1;
Elems (Container) (Length (Container)) := New_Item;
end Append; end Append;
------------ ------------
...@@ -151,9 +165,8 @@ is ...@@ -151,9 +165,8 @@ is
function Capacity (Container : Vector) return Capacity_Range is function Capacity (Container : Vector) return Capacity_Range is
begin begin
return (if Container.Elements_Ptr = null return (if Bounded then Container.Capacity
then Container.Elements'Length else Capacity_Range'Last);
else Container.Elements_Ptr.all'Length);
end Capacity; end Capacity;
----------- -----------
...@@ -207,22 +220,155 @@ is ...@@ -207,22 +220,155 @@ is
end return; end return;
end Copy; end Copy;
--------------------- ----------------------
-- Current_To_Last -- -- Current_Capacity --
--------------------- ----------------------
function Current_To_Last function Current_Capacity (Container : Vector) return Capacity_Range is
(Container : Vector; begin
Current : Index_Type) return Vector 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 is
begin begin
return Result : Vector (Count_Type (Container.Last - Current + 1)) Delete (Container, Index, 1);
do end Delete;
for X in Current .. Container.Last loop
Append (Result, Element (Container, X)); procedure Delete
end loop; (Container : in out Vector;
end return; Index : Extended_Index;
end Current_To_Last; 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 -- -- Delete_Last --
...@@ -231,16 +377,38 @@ is ...@@ -231,16 +377,38 @@ is
procedure Delete_Last procedure Delete_Last
(Container : in out Vector) (Container : in out Vector)
is is
Count : constant Capacity_Range := 1; begin
Index : Int'Base; Delete_Last (Container, 1);
end Delete_Last;
procedure Delete_Last
(Container : in out Vector;
Count : Count_Type)
is
begin 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; 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 else
Container.Last := Index_Type (Index); Container.Last :=
Index_Type'Base (Count_Type'Base (Container.Last) - Count);
end if; end if;
end Delete_Last; end Delete_Last;
...@@ -332,23 +500,151 @@ is ...@@ -332,23 +500,151 @@ is
return Index_Type'First; return Index_Type'First;
end First_Index; end First_Index;
----------------------- ------------------
-- First_To_Previous -- -- Formal_Model --
----------------------- ------------------
function First_To_Previous package body Formal_Model is
(Container : Vector;
Current : Index_Type) return Vector -------------------------
is -- M_Elements_In_Union --
begin -------------------------
return Result : Vector
(Count_Type (Current - First_Index (Container))) function M_Elements_In_Union
do (Container : M.Sequence;
for X in First_Index (Container) .. Current - 1 loop Left : M.Sequence;
Append (Result, Element (Container, X)); 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 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 -- -- Generic_Sorting --
...@@ -374,6 +670,37 @@ is ...@@ -374,6 +670,37 @@ is
return True; return True;
end Is_Sorted; 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 -- -- Sort --
---------- ----------
...@@ -396,6 +723,78 @@ is ...@@ -396,6 +723,78 @@ is
end if; end if;
end Sort; 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; end Generic_Sorting;
----------------- -----------------
...@@ -420,6 +819,276 @@ is ...@@ -420,6 +819,276 @@ is
return Position in First_Index (Container) .. Last_Index (Container); return Position in First_Index (Container) .. Last_Index (Container);
end Has_Element; 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 -- -- Is_Empty --
-------------- --------------
...@@ -456,13 +1125,62 @@ is ...@@ -456,13 +1125,62 @@ is
------------ ------------
function Length (Container : Vector) return Capacity_Range 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); F : constant Int := Int (Index_Type'First);
N : constant Int'Base := L - F + 1; N : constant Int'Base := L - F + 1;
begin begin
return Capacity_Range (N); return Capacity_Range (N);
end Length; 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 -- -- Replace_Element --
--------------------- ---------------------
...@@ -499,7 +1217,7 @@ is ...@@ -499,7 +1217,7 @@ is
raise Constraint_Error with "Capacity is out of range"; raise Constraint_Error with "Capacity is out of range";
end if; end if;
else else
if Capacity > Formal_Vectors.Capacity (Container) then if Capacity > Formal_Vectors.Current_Capacity (Container) then
declare declare
New_Elements : constant Elements_Array_Ptr := New_Elements : constant Elements_Array_Ptr :=
new Elements_Array (1 .. Capacity); new Elements_Array (1 .. Capacity);
...@@ -609,6 +1327,39 @@ is ...@@ -609,6 +1327,39 @@ is
end; end;
end Swap; 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 -- -- To_Vector --
--------------- ---------------
......
gcc/ada/a-cofove.ads
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- S p e c -- -- 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 -- -- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow -- -- GNAT. The copyright notice above, and the license provisions that follow --
...@@ -35,12 +35,12 @@ ...@@ -35,12 +35,12 @@
-- unit compatible with SPARK 2014. Note that the API of this unit may be -- unit compatible with SPARK 2014. Note that the API of this unit may be
-- subject to incompatible changes as SPARK 2014 evolves. -- subject to incompatible changes as SPARK 2014 evolves.
with Ada.Containers.Functional_Vectors;
generic generic
type Index_Type is range <>; type Index_Type is range <>;
type Element_Type is private; type Element_Type is private;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
Bounded : Boolean := True; Bounded : Boolean := True;
-- If True, the containers are bounded; the initial capacity is the maximum -- If True, the containers are bounded; the initial capacity is the maximum
-- size, and heap allocation will be avoided. If False, the containers can -- size, and heap allocation will be avoided. If False, the containers can
...@@ -49,7 +49,6 @@ generic ...@@ -49,7 +49,6 @@ generic
package Ada.Containers.Formal_Vectors with package Ada.Containers.Formal_Vectors with
SPARK_Mode SPARK_Mode
is is
pragma Annotate (GNATprove, External_Axiomatization);
pragma Annotate (CodePeer, Skip_Analysis); pragma Annotate (CodePeer, Skip_Analysis);
subtype Extended_Index is Index_Type'Base subtype Extended_Index is Index_Type'Base
...@@ -73,58 +72,192 @@ is ...@@ -73,58 +72,192 @@ is
-- unbounded case; you can't assign from one object to another if the -- unbounded case; you can't assign from one object to another if the
-- Capacity is different. -- 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 function Empty_Vector return Vector with
Global => null; Global => null,
Post => Length (Empty_Vector'Result) = 0;
function "=" (Left, Right : Vector) return Boolean with function "=" (Left, Right : Vector) return Boolean with
Global => null; Global => null,
Post => "="'Result = (Model (Left) = Model (Right));
function To_Vector function To_Vector
(New_Item : Element_Type; (New_Item : Element_Type;
Length : Capacity_Range) return Vector Length : Capacity_Range) return Vector
with 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 function Capacity (Container : Vector) return Capacity_Range with
Global => null, 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 procedure Reserve_Capacity
(Container : in out Vector; (Container : in out Vector;
Capacity : Capacity_Range) Capacity : Capacity_Range)
with with
Global => null, Global => null,
Pre => (if Bounded then Capacity <= Container.Capacity); Pre => (if Bounded then Capacity <= Container.Capacity),
Post => Model (Container) = Model (Container)'Old;
function Length (Container : Vector) return Capacity_Range with
Global => null;
function Is_Empty (Container : Vector) return Boolean with 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 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 -- 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 -- this before a container goes out of scope in order to avoid storage
-- leaks. In addition, "X := ..." can leak unless you Clear(X) first. -- leaks. In addition, "X := ..." can leak unless you Clear(X) first.
procedure Assign (Target : in out Vector; Source : Vector) with procedure Assign (Target : in out Vector; Source : Vector) with
Global => null, 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 function Copy
(Source : Vector; (Source : Vector;
Capacity : Capacity_Range := 0) return Vector Capacity : Capacity_Range := 0) return Vector
with with
Global => null, 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 function Element
(Container : Vector; (Container : Vector;
Index : Index_Type) return Element_Type Index : Index_Type) return Element_Type
with with
Global => null, 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 procedure Replace_Element
(Container : in out Vector; (Container : in out Vector;
...@@ -132,112 +265,602 @@ is ...@@ -132,112 +265,602 @@ is
New_Item : Element_Type) New_Item : Element_Type)
with with
Global => null, 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; (Container : in out Vector;
Before : Extended_Index;
New_Item : Vector) New_Item : Vector)
with with
Global => null, Global => null,
Pre => (if Bounded then Pre =>
Length (Container) + Length (New_Item) <= Container.Capacity); 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 procedure Append
(Container : in out Vector; (Container : in out Vector;
New_Item : Element_Type) New_Item : Element_Type)
with with
Global => null, Global => null,
Pre => (if Bounded then Pre => Length (Container) < Capacity (Container),
Length (Container) < Container.Capacity); 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 procedure Delete_Last
(Container : in out Vector) (Container : in out Vector)
with 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 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 procedure Swap (Container : in out Vector; I, J : Index_Type) with
Global => null, Global => null,
Pre => I in First_Index (Container) .. Last_Index (Container) Pre => I in First_Index (Container) .. Last_Index (Container)
and then J in First_Index (Container) .. Last_Index (Container); 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 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 function First_Element (Container : Vector) return Element_Type with
Global => null, 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 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 function Last_Element (Container : Vector) return Element_Type with
Global => null, 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 function Find_Index
(Container : Vector; (Container : Vector;
Item : Element_Type; Item : Element_Type;
Index : Index_Type := Index_Type'First) return Extended_Index Index : Index_Type := Index_Type'First) return Extended_Index
with 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 function Reverse_Find_Index
(Container : Vector; (Container : Vector;
Item : Element_Type; Item : Element_Type;
Index : Index_Type := Index_Type'Last) return Extended_Index Index : Index_Type := Index_Type'Last) return Extended_Index
with 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 function Contains
(Container : Vector; (Container : Vector;
Item : Element_Type) return Boolean Item : Element_Type) return Boolean
with 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 function Has_Element
(Container : Vector; (Container : Vector;
Position : Extended_Index) return Boolean Position : Extended_Index) return Boolean
with 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 generic
with function "<" (Left, Right : Element_Type) return Boolean is <>; with function "<" (Left, Right : Element_Type) return Boolean is <>;
package Generic_Sorting with SPARK_Mode 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 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 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; 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 private
pragma SPARK_Mode (Off); pragma SPARK_Mode (Off);
......
gcc/ada/freeze.adb
...@@ -1482,7 +1482,7 @@ package body Freeze is ...@@ -1482,7 +1482,7 @@ package body Freeze is
A_Post := Get_Pragma (Par_Prim, Pragma_Postcondition); A_Post := Get_Pragma (Par_Prim, Pragma_Postcondition);
if Present (A_Post) and then Class_Present (A_Post) then 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 Build_Class_Wide_Expression
(Prag => New_Prag, (Prag => New_Prag,
Subp => Prim, Subp => Prim,
......
gcc/ada/g-dyntab.adb
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
-- -- -- --
-- B o d y -- -- 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 -- -- 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- -- -- terms of the GNU General Public License as published by the Free Soft- --
...@@ -279,7 +279,8 @@ package body GNAT.Dynamic_Tables is ...@@ -279,7 +279,8 @@ package body GNAT.Dynamic_Tables is
new Ada.Unchecked_Conversion (Alloc_Ptr, Table_Ptr); new Ada.Unchecked_Conversion (Alloc_Ptr, Table_Ptr);
Old_Table : Old_Alloc_Ptr := To_Old_Alloc_Ptr (T.Table); 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 begin
T.P.Last_Allocated := T.P.Last; T.P.Last_Allocated := T.P.Last;
Free (Old_Table); Free (Old_Table);
......
gcc/ada/sem_prag.adb
...@@ -24007,16 +24007,20 @@ package body Sem_Prag is ...@@ -24007,16 +24007,20 @@ package body Sem_Prag is
& "of &", Nod, Disp_Typ); & "of &", Nod, Disp_Typ);
end if; end if;
-- Otherwise we have a call to an overridden primitive, and -- Otherwise we have a call to an overridden primitive, and we
-- we will create a common class-wide clone for the body of -- will create a common class-wide clone for the body of
-- original operation and its eventual inherited versions. -- original operation and its eventual inherited versions. If
-- If the original operation dispatches on result it is -- the original operation dispatches on result it is never
-- never inherited and there is no need for a clone. -- 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) elsif not Is_Abstract_Subprogram (Spec_Id)
and then No (Class_Wide_Clone (Spec_Id)) and then No (Class_Wide_Clone (Spec_Id))
and then not Has_Controlling_Result (Spec_Id) and then not Has_Controlling_Result (Spec_Id)
and then SPARK_Mode /= On and then not GNATprove_Mode
then then
Build_Class_Wide_Clone_Decl (Spec_Id); Build_Class_Wide_Clone_Decl (Spec_Id);
end if; end if;
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment