+2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * exp_util.adb, a-cfdlli.adb, a-cfdlli.ads, exp_ch9.adb, g-dyntab.adb,
+ sem_dim.adb, a-cfinve.adb, a-cfinve.ads, a-cofove.adb, a-cofove.ads:
+ Minor reformatting and code cleanups.
+
2017-04-27 Ed Schonberg <schonberg@adacore.com>
* freeze.adb (Build_Inherited_Condition_Pragmas): New procedure,
New_Item : Element_Type;
New_Node : out Count_Type);
- procedure Free
- (Container : in out List;
- X : Count_Type);
+ procedure Free (Container : in out List; X : Count_Type);
procedure Insert_Internal
(Container : in out List;
-- Append --
------------
- procedure Append
- (Container : in out List;
- New_Item : Element_Type)
- is
+ procedure Append (Container : in out List; New_Item : Element_Type) is
begin
Insert (Container, No_Element, New_Item, 1);
end Append;
begin
if Container.Length = 0 then
pragma Assert (Container.First = 0);
- pragma Assert (Container.Last = 0);
+ pragma Assert (Container.Last = 0);
return;
end if;
pragma Assert (Container.First >= 1);
- pragma Assert (Container.Last >= 1);
+ pragma Assert (Container.Last >= 1);
pragma Assert (N (Container.First).Prev = 0);
- pragma Assert (N (Container.Last).Next = 0);
+ pragma Assert (N (Container.Last).Next = 0);
while Container.Length > 1 loop
X := Container.First;
pragma Assert (Vet (Container, Position), "bad cursor in Delete");
pragma Assert (Container.First >= 1);
- pragma Assert (Container.Last >= 1);
+ pragma Assert (Container.Last >= 1);
pragma Assert (N (Container.First).Prev = 0);
- pragma Assert (N (Container.Last).Next = 0);
+ pragma Assert (N (Container.Last).Next = 0);
if Position.Node = Container.First then
Delete_First (Container, Count);
From := Container.First;
end if;
- if Position.Node /= 0 and then
- not Has_Element (Container, Position)
- then
+ if Position.Node /= 0 and then not Has_Element (Container, Position) then
raise Constraint_Error with "Position cursor has no element";
end if;
Left : M.Sequence;
Right : M.Sequence) return Boolean
is
- begin
- for I in 1 .. M.Length (Container) loop
- declare
- Found : Boolean := False;
- J : Count_Type := 0;
-
- begin
- while not Found and J < M.Length (Left) loop
- J := J + 1;
- if Element (Container, I) = Element (Left, J) then
- Found := True;
- end if;
- end loop;
-
- J := 0;
+ Elem : Element_Type;
- while not Found and J < M.Length (Right) loop
- J := J + 1;
- if Element (Container, I) = Element (Right, J) then
- Found := True;
- end if;
- end loop;
+ begin
+ for Index in 1 .. M.Length (Container) loop
+ Elem := Element (Container, Index);
- if not Found then
- return False;
- end if;
- end;
+ if not M.Contains (Left, 1, M.Length (Left), Elem)
+ and then not M.Contains (Right, 1, M.Length (Right), Elem)
+ then
+ return False;
+ end if;
end loop;
return True;
end if;
for I in 1 .. L loop
- if Element (Left, I) /= Element (Right, L - I + 1)
- then
+ if Element (Left, I) /= Element (Right, L - I + 1) then
return False;
end if;
end loop;
end Model;
-----------------------
- -- Mapping_preserved --
+ -- Mapping_Preserved --
-----------------------
function Mapping_Preserved
for C of Right loop
if not P.Has_Key (Left, C)
- or else (C /= X and C /= Y
+ or else (C /= X
+ and C /= Y
and P.Get (Left, C) /= P.Get (Right, C))
then
return False;
begin
if Target'Address = Source'Address then
- raise Program_Error with
- "Target and Source denote same container";
+ raise Program_Error with "Target and Source denote same container";
end if;
LI := First (Target);
begin
if Target'Address = Source'Address then
- raise Program_Error with
- "Target and Source denote same container";
+ raise Program_Error with "Target and Source denote same container";
end if;
if Before.Node /= 0 then
end if;
pragma Assert (SN (Source.First).Prev = 0);
- pragma Assert (SN (Source.Last).Next = 0);
+ pragma Assert (SN (Source.Last).Next = 0);
if Target.Length > Count_Type'Base'Last - Source.Length then
raise Constraint_Error with "new length exceeds maximum";
begin
if Target'Address = Source'Address then
- raise Program_Error with
- "Target and Source denote same container";
+ raise Program_Error with "Target and Source denote same container";
end if;
if Position.Node = 0 then
return False;
end if;
- if N (Position.Node).Prev = 0
- and then Position.Node /= L.First
- then
+ if N (Position.Node).Prev = 0 and then Position.Node /= L.First then
return False;
end if;
- if N (Position.Node).Next = 0
- and then Position.Node /= L.Last
- then
+ if N (Position.Node).Next = 0 and then Position.Node /= L.Last then
return False;
end if;
(for all I in 1 .. M.Length (Container) =>
(for some J in 1 .. M.Length (Left) =>
Element (Container, I) = Element (Left, J))
- or (for some J in 1 .. M.Length (Right) =>
- Element (Container, I) = Element (Right, J)));
+ or (for some J in 1 .. M.Length (Right) =>
+ Element (Container, I) = Element (Right, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union);
function M_Elements_Included
M_Elements_Reversed'Result =
(M.Length (Left) = M.Length (Right)
and (for all I in 1 .. M.Length (Left) =>
- Element (Left, I) =
- Element (Right, M.Length (Left) - I + 1))
+ Element (Left, I) =
+ Element (Right, M.Length (Left) - I + 1))
and (for all I in 1 .. M.Length (Left) =>
- Element (Right, I) =
- Element (Left, M.Length (Left) - I + 1)));
+ Element (Right, I) =
+ Element (Left, M.Length (Left) - I + 1)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed);
function M_Elements_Swapped
-- Container contains Count times New_Item at the end
and (if Count > 0 then
- M.Constant_Range
- (Container => Model (Container),
- Fst => Length (Container)'Old + 1,
- Lst => Length (Container),
- Item => New_Item))
+ M.Constant_Range
+ (Container => Model (Container),
+ Fst => Length (Container)'Old + 1,
+ Lst => Length (Container),
+ Item => New_Item))
-- Container contains Count times New_Item at the end
Post => Length (Container) = Length (Container)'Old + Count,
Contract_Cases =>
(Count = 0 =>
- Position = Before
- and Model (Container) = Model (Container)'Old
- and Positions (Container) = Positions (Container)'Old,
+ Position = Before
+ and Model (Container) = Model (Container)'Old
+ and Positions (Container) = Positions (Container)'Old,
others =>
-- Container contains Count times New_Item at the end
and (if Count > 0 then
- M.Constant_Range
- (Container => Model (Container),
- Fst => Length (Container)'Old + 1,
- Lst => Length (Container),
- Item => New_Item))
+ M.Constant_Range
+ (Container => Model (Container),
+ Fst => Length (Container)'Old + 1,
+ Lst => Length (Container),
+ Item => New_Item))
-- Count cursors have been inserted at the end of Container
-- Other cursors are still valid
and P.Keys_Included_Except
- (Left => Positions (Container)'Old,
- Right => Positions (Container)'Old,
- New_Key => Last (Container)'Old)
+ (Left => Positions (Container)'Old,
+ Right => Positions (Container)'Old,
+ New_Key => Last (Container)'Old)
-- The positions of other cursors are preserved
Pre => Has_Element (Container, I) and then Has_Element (Container, J),
Post =>
M_Elements_Swapped
- (Model (Container)'Old, Model (Container),
+ (Model (Container)'Old,
+ Model (Container),
X => P.Get (Positions (Container)'Old, I),
Y => P.Get (Positions (Container)'Old, J))
procedure Swap_Links
(Container : in out List;
I : Cursor;
- J : Cursor)
+ J : Cursor)
with
Global => null,
Pre => Has_Element (Container, I) and then Has_Element (Container, J),
Post =>
M_Elements_Swapped
- (Model (Container'Old), Model (Container),
+ (Model (Container'Old),
+ Model (Container),
X => P.Get (Positions (Container)'Old, I),
Y => P.Get (Positions (Container)'Old, J))
and P_Positions_Swapped
and M_Elements_Included
(Left => Model (Target),
L_Fst => P.Get (Positions (Target)'Old, Before),
- L_Lst => P.Get (Positions (Target)'Old, Before) - 1 +
+ L_Lst =>
+ P.Get (Positions (Target)'Old, Before) - 1 +
Length (Source)'Old,
Right => Model (Source)'Old,
R_Lst => Length (Source)'Old)
-- The element located at Position in Source is moved to Target
- and Element (Model (Target), P.Get (Positions (Target), Position)) =
- Element (Model (Source)'Old,
- P.Get (Positions (Source)'Old, Position'Old))
+ and Element (Model (Target),
+ P.Get (Positions (Target), Position)) =
+ Element (Model (Source)'Old,
+ P.Get (Positions (Source)'Old, Position'Old))
-- A new cursor has been inserted at position Position in Target
-- The last element of Container is the one that was previously at
-- Position.
- and Element (Model (Container), Length (Container)) =
- Element (Model (Container)'Old,
- P.Get (Positions (Container)'Old, Position))
+ and Element (Model (Container),
+ Length (Container)) =
+ Element (Model (Container)'Old,
+ P.Get (Positions (Container)'Old, Position))
-- Cursors from Container continue designating the same elements
-- The element previously at Position is now before Before
- and Element (Model (Container),
- P.Get (Positions (Container)'Old, Before)) =
- Element (Model (Container)'Old,
- P.Get (Positions (Container)'Old, Position))
+ and Element
+ (Model (Container),
+ P.Get (Positions (Container)'Old, Before)) =
+ Element
+ (Model (Container)'Old,
+ P.Get (Positions (Container)'Old, Position))
-- Cursors from Container continue designating the same elements
-- The element designated by the result of Find is Item
- and Element (Model (Container),
- P.Get (Positions (Container), Find'Result)) = Item
+ and Element
+ (Model (Container),
+ P.Get (Positions (Container), Find'Result)) = Item
-- The result of Find is located after Position
-- The element designated by the result of Find is Item
- and Element (Model (Container),
- P.Get (Positions (Container),
- Reverse_Find'Result)) = Item
+ and Element
+ (Model (Container),
+ P.Get (Positions (Container), Reverse_Find'Result)) = Item
-- The result of Find is located before Position
Post =>
Length (Container) = Length (Container)'Old
and M_Elements_Sorted (Model (Container))
- and M_Elements_Included (Left => Model (Container)'Old,
- L_Lst => Length (Container),
- Right => Model (Container),
- R_Lst => Length (Container))
- and M_Elements_Included (Left => Model (Container),
- L_Lst => Length (Container),
- Right => Model (Container)'Old,
- R_Lst => Length (Container));
+ and M_Elements_Included
+ (Left => Model (Container)'Old,
+ L_Lst => Length (Container),
+ Right => Model (Container),
+ R_Lst => Length (Container))
+ and M_Elements_Included
+ (Left => Model (Container),
+ L_Lst => Length (Container),
+ Right => Model (Container)'Old,
+ R_Lst => Length (Container));
procedure Merge (Target : in out List; Source : in out List) with
-- Target and Source should not be aliased
and Length (Source) = 0
and (if M_Elements_Sorted (Model (Target)'Old)
and M_Elements_Sorted (Model (Source)'Old)
- then M_Elements_Sorted (Model (Target)))
- and M_Elements_Included (Left => Model (Target)'Old,
- L_Lst => Length (Target)'Old,
- Right => Model (Target),
- R_Lst => Length (Target))
- and M_Elements_Included (Left => Model (Source)'Old,
- L_Lst => Length (Source)'Old,
- Right => Model (Target),
- R_Lst => Length (Target))
- and M_Elements_In_Union (Model (Target),
- Model (Source)'Old,
- Model (Target)'Old);
+ then
+ M_Elements_Sorted (Model (Target)))
+ and M_Elements_Included
+ (Left => Model (Target)'Old,
+ L_Lst => Length (Target)'Old,
+ Right => Model (Target),
+ R_Lst => Length (Target))
+ and M_Elements_Included
+ (Left => Model (Source)'Old,
+ L_Lst => Length (Source)'Old,
+ Right => Model (Target),
+ R_Lst => Length (Target))
+ and M_Elements_In_Union
+ (Model (Target),
+ Model (Source)'Old,
+ Model (Target)'Old);
end Generic_Sorting;
private
package body Ada.Containers.Formal_Indefinite_Vectors with
SPARK_Mode => Off
is
-
function H (New_Item : Element_Type) return Holder renames To_Holder;
function E (Container : Holder) return Element_Type renames Get;
type Int is range System.Min_Int .. System.Max_Int;
procedure Free is
- new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr);
+ new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr);
type Maximal_Array_Ptr is access all Elements_Array (Array_Index)
with Storage_Size => 0;
type Maximal_Array_Ptr_Const is access constant Elements_Array (Array_Index)
- with Storage_Size => 0;
+ with Storage_Size => 0;
function Elems (Container : in out Vector) return Maximal_Array_Ptr;
function Elemsc
-- "=" --
---------
- function "=" (Left, Right : Vector) return Boolean is
+ function "=" (Left : Vector; Right : Vector) return Boolean is
begin
if Left'Address = Right'Address then
return True;
Insert (Container, Container.Last + 1, New_Item);
end Append;
- procedure Append
- (Container : in out Vector;
- New_Item : Element_Type)
- is
+ procedure Append (Container : in out Vector; New_Item : Element_Type) is
begin
Append (Container, New_Item, 1);
end Append;
function Capacity (Container : Vector) return Capacity_Range is
begin
- return (if Bounded then Container.Capacity
- else Capacity_Range'Last);
+ return
+ (if Bounded then
+ Container.Capacity
+ else
+ Capacity_Range'Last);
end Capacity;
-----------
function Current_Capacity (Container : Vector) return Capacity_Range is
begin
- return (if Container.Elements_Ptr = null
- then Container.Elements'Length
- else Container.Elements_Ptr.all'Length);
+ return
+ (if Container.Elements_Ptr = null then
+ Container.Elements'Length
+ else
+ Container.Elements_Ptr.all'Length);
end Current_Capacity;
------------
-- Delete --
------------
- procedure Delete
- (Container : in out Vector;
- Index : Extended_Index)
- is
+ procedure Delete (Container : in out Vector; Index : Extended_Index) is
begin
Delete (Container, Index, 1);
end Delete;
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;
-- Delete_First --
------------------
- procedure Delete_First
- (Container : in out Vector)
- is
+ procedure Delete_First (Container : in out Vector) is
begin
Delete_First (Container, 1);
end Delete_First;
- procedure Delete_First
- (Container : in out Vector;
- Count : Count_Type)
- is
+ procedure Delete_First (Container : in out Vector; Count : Count_Type) is
begin
if Count = 0 then
return;
-- Delete_Last --
-----------------
- procedure Delete_Last
- (Container : in out Vector)
- is
+ procedure Delete_Last (Container : in out Vector) is
begin
Delete_Last (Container, 1);
end Delete_Last;
- procedure Delete_Last
- (Container : in out Vector;
- Count : Count_Type)
- is
+ procedure Delete_Last (Container : in out Vector; Count : Count_Type) is
begin
if Count = 0 then
return;
declare
II : constant Int'Base := Int (Index) - Int (No_Index);
I : constant Capacity_Range := Capacity_Range (II);
+
begin
return Get_Element (Container, I);
end;
function Elems (Container : in out Vector) return Maximal_Array_Ptr is
begin
- return (if Container.Elements_Ptr = null
- then Container.Elements'Unrestricted_Access
- else Container.Elements_Ptr.all'Unrestricted_Access);
+ return
+ (if Container.Elements_Ptr = null then
+ Container.Elements'Unrestricted_Access
+ else
+ Container.Elements_Ptr.all'Unrestricted_Access);
end Elems;
- function Elemsc
- (Container : Vector) return Maximal_Array_Ptr_Const is
+ function Elemsc (Container : Vector) return Maximal_Array_Ptr_Const is
begin
- return (if Container.Elements_Ptr = null
- then Container.Elements'Unrestricted_Access
- else Container.Elements_Ptr.all'Unrestricted_Access);
+ return
+ (if Container.Elements_Ptr = null then
+ Container.Elements'Unrestricted_Access
+ else
+ Container.Elements_Ptr.all'Unrestricted_Access);
end Elemsc;
----------------
Right : M.Sequence) return Boolean
is
begin
- for I in Index_Type'First .. M.Last (Container) loop
+ for Index in Index_Type'First .. M.Last (Container) loop
declare
- Found : Boolean := False;
- J : Extended_Index := Extended_Index'First;
-
+ Elem : constant Element_Type := Element (Container, Index);
begin
- while not Found and J < M.Last (Left) loop
- J := J + 1;
- if Element (Container, I) = Element (Left, J) then
- Found := True;
- end if;
- end loop;
-
- J := Extended_Index'First;
-
- while not Found and J < M.Last (Right) loop
- J := J + 1;
- if Element (Container, I) = Element (Right, J) then
- Found := True;
- end if;
- end loop;
-
- if not Found then
+ if not M.Contains (Left, Index_Type'First, M.Last (Left), Elem)
+ and then
+ not M.Contains
+ (Right, Index_Type'First, M.Last (Right), Elem)
+ then
return False;
end if;
end;
-- M_Elements_Reversed --
-------------------------
- function M_Elements_Reversed (Left, Right : M.Sequence) return Boolean is
+ function M_Elements_Reversed
+ (Left : M.Sequence;
+ Right : M.Sequence) return Boolean
+ is
L : constant Index_Type := M.Last (Left);
+
begin
if L /= M.Last (Right) then
return False;
function M_Elements_Swapped
(Left : M.Sequence;
Right : M.Sequence;
- X, Y : Index_Type) return Boolean
+ X : Index_Type;
+ Y : Index_Type) return Boolean
is
begin
if M.Length (Left) /= M.Length (Right)
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;
function Is_Sorted (Container : Vector) return Boolean is
L : constant Capacity_Range := Length (Container);
+
begin
for J in 1 .. L - 1 loop
- if Get_Element (Container, J + 1) <
- Get_Element (Container, J)
- then
+ if Get_Element (Container, J + 1) < Get_Element (Container, J) then
return False;
end if;
end loop;
-- Sort --
----------
- procedure Sort (Container : in out Vector)
- is
+ procedure Sort (Container : in out Vector) is
function "<" (Left : Holder; Right : Holder) return Boolean is
(E (Left) < E (Right));
procedure Sort is
new Generic_Array_Sort
- (Index_Type => Array_Index,
- Element_Type => Holder,
- Array_Type => Elements_Array,
- "<" => "<");
+ (Index_Type => Array_Index,
+ Element_Type => Holder,
+ Array_Type => Elements_Array,
+ "<" => "<");
Len : constant Capacity_Range := Length (Container);
+
begin
if Container.Last <= Index_Type'First then
return;
-- Merge --
-----------
- procedure Merge (Target, Source : in out Vector) is
- I, J : Count_Type;
+ procedure Merge (Target : in out Vector; Source : in out Vector) is
+ I : Count_Type;
+ J : Count_Type;
begin
if Target'Address = Source'Address then
- raise Program_Error with
- "Target and Source denote same container";
+ raise Program_Error with "Target and Source denote same container";
end if;
if Length (Source) = 0 then
declare
New_Length : constant Count_Type := I + Length (Source);
+
begin
- if not Bounded and then
- Current_Capacity (Target) < Capacity_Range (New_Length)
+ if not Bounded
+ and then Current_Capacity (Target) < Capacity_Range (New_Length)
then
Reserve_Capacity
(Target,
Capacity_Range'Max
(Current_Capacity (Target) * Growth_Factor,
- Capacity_Range (New_Length)));
+ Capacity_Range (New_Length)));
end if;
if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
declare
TA : Maximal_Array_Ptr renames Elems (Target);
SA : Maximal_Array_Ptr renames Elems (Source);
+
begin
J := Length (Target);
while Length (Source) /= 0 loop
-----------------
function Has_Element
- (Container : Vector; Position : Extended_Index) return Boolean is
+ (Container : Vector;
+ Position : Extended_Index) return Boolean
+ is
begin
return Position in First_Index (Container) .. Last_Index (Container);
end Has_Element;
-- worry about if No_Index were less than 0, but that case is
-- handled above).
- if Index_Type'Last - No_Index >=
- Count_Type'Pos (Count_Type'Last)
+ if Index_Type'Last - No_Index >= Count_Type'Pos (Count_Type'Last)
then
-- We have determined that range of Index_Type has at least as
-- many values as in Count_Type, so Count_Type'Last is the
-- Increase the capacity of container if needed
- if not Bounded and then
- Current_Capacity (Container) < Capacity_Range (New_Length)
+ if not Bounded
+ and then Current_Capacity (Container) < Capacity_Range (New_Length)
then
Reserve_Capacity
(Container,
Capacity_Range'Max (Current_Capacity (Container) * Growth_Factor,
- Capacity_Range (New_Length)));
+ Capacity_Range (New_Length)));
end if;
declare
EA : Maximal_Array_Ptr renames Elems (Container);
+
begin
if Before <= Container.Last then
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
+ 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;
Insert (Container, Index_Type'First, New_Item);
end Prepend;
- procedure Prepend
- (Container : in out Vector;
- New_Item : Element_Type)
- is
+ procedure Prepend (Container : in out Vector; New_Item : Element_Type) is
begin
Prepend (Container, New_Item, 1);
end Prepend;
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;
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);
end if;
declare
- I, J : Capacity_Range;
- E : Elements_Array renames
- Elems (Container) (1 .. Length (Container));
+ I : Capacity_Range;
+ J : Capacity_Range;
+ E : Elements_Array renames
+ Elems (Container) (1 .. Length (Container));
begin
I := 1;
while I < J loop
declare
EI : constant Holder := E (I);
+
begin
E (I) := E (J);
E (J) := EI;
-- Swap --
----------
- procedure Swap (Container : in out Vector; I, J : Index_Type) is
+ procedure Swap
+ (Container : in out Vector;
+ I : Index_Type;
+ J : Index_Type)
+ is
begin
if I > Container.Last then
raise Constraint_Error with "I index is out of range";
Last := Index_Type (Last_As_Int);
- return (Capacity => Length,
- Last => Last,
- Elements_Ptr => <>,
- Elements => (others => H (New_Item)));
+ return
+ (Capacity => Length,
+ Last => Last,
+ Elements_Ptr => <>,
+ Elements => (others => H (New_Item)));
end;
end To_Vector;
(for all I in Index_Type'First .. M.Last (Container) =>
(for some J in Index_Type'First .. M.Last (Left) =>
Element (Container, I) = Element (Left, J))
- or (for some J in Index_Type'First .. M.Last (Right) =>
- Element (Container, I) = Element (Right, J)));
+ or (for some J in Index_Type'First .. M.Last (Right) =>
+ Element (Container, I) = Element (Right, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union);
function M_Elements_Included
M_Elements_Reversed'Result =
(M.Length (Left) = M.Length (Right)
and (for all I in Index_Type'First .. M.Last (Left) =>
- Element (Left, I) =
- Element (Right, M.Last (Left) - I + 1))
+ Element (Left, I) =
+ Element (Right, M.Last (Left) - I + 1))
and (for all I in Index_Type'First .. M.Last (Right) =>
- Element (Right, I) =
- Element (Left, M.Last (Left) - I + 1)));
+ Element (Right, I) =
+ Element (Left, M.Last (Left) - I + 1)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed);
function M_Elements_Swapped
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;
Global => null,
Post =>
Formal_Indefinite_Vectors.Length (To_Vector'Result) = Length
- and M.Constant_Range (Container => Model (To_Vector'Result),
- Fst => Index_Type'First,
- Lst => Last_Index (To_Vector'Result),
- Item => New_Item);
+ and M.Constant_Range
+ (Container => Model (To_Vector'Result),
+ Fst => Index_Type'First,
+ Lst => Last_Index (To_Vector'Result),
+ Item => New_Item);
function Capacity (Container : Vector) return Capacity_Range with
Global => null,
Post =>
- Capacity'Result = (if Bounded then Container.Capacity
- else Capacity_Range'Last);
+ Capacity'Result =
+ (if Bounded then
+ Container.Capacity
+ else
+ Capacity_Range'Last);
pragma Annotate (GNATprove, Inline_For_Proof, Capacity);
procedure Reserve_Capacity
Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)),
Post =>
Model (Copy'Result) = Model (Source)
- and (if Capacity = 0 then Copy'Result.Capacity = Length (Source)
- else Copy'Result.Capacity = Capacity);
+ and (if Capacity = 0 then
+ Copy'Result.Capacity = Length (Source)
+ else
+ Copy'Result.Capacity = Capacity);
procedure Move (Target : in out Vector; Source : in out Vector)
with
Pre =>
Length (Container) <= Capacity (Container) - Length (New_Item)
and (Before in Index_Type'First .. Last_Index (Container)
- or (Before /= No_Index
+ or (Before /= No_Index
and then Before - 1 = Last_Index (Container))),
Post =>
Length (Container) = Length (Container)'Old + Length (New_Item)
-- Elements of New_Item are inserted at position Before
and (if Length (New_Item) > 0 then
- M.Range_Shifted
- (Left => Model (New_Item),
- Right => Model (Container),
- Fst => Index_Type'First,
- Lst => Last_Index (New_Item),
- Offset => Count_Type (Before - Index_Type'First)))
+ M.Range_Shifted
+ (Left => Model (New_Item),
+ Right => Model (Container),
+ Fst => Index_Type'First,
+ Lst => Last_Index (New_Item),
+ Offset => Count_Type (Before - Index_Type'First)))
-- Elements located after Before in Container are shifted
Pre =>
Length (Container) <= Capacity (Container) - Count
and (Before in Index_Type'First .. Last_Index (Container)
- or (Before /= No_Index
+ or (Before /= No_Index
and then Before - 1 = Last_Index (Container))),
Post =>
Length (Container) = Length (Container)'Old + Count
-- New_Item is inserted Count times at position Before
and (if Count > 0 then
- M.Constant_Range
- (Container => Model (Container),
- Fst => Before,
- Lst => Before + Index_Type'Base (Count - 1),
- Item => New_Item))
+ M.Constant_Range
+ (Container => Model (Container),
+ Fst => Before,
+ Lst => Before + Index_Type'Base (Count - 1),
+ Item => New_Item))
-- Elements located after Before in Container are shifted
Lst => Last_Index (Container)'Old,
Offset => Count);
- procedure Prepend
- (Container : in out Vector;
- New_Item : Vector)
- with
+ procedure Prepend (Container : in out Vector; New_Item : Vector) with
Global => null,
Pre => Length (Container) <= Capacity (Container) - Length (New_Item),
Post =>
Lst => Last_Index (Container)'Old,
Offset => Length (New_Item));
- procedure Prepend
- (Container : in out Vector;
- New_Item : Element_Type)
- with
+ procedure Prepend (Container : in out Vector; New_Item : Element_Type) with
Global => null,
Pre => Length (Container) < Capacity (Container),
Post =>
Lst => Last_Index (Container)'Old,
Offset => Count);
- procedure Append
- (Container : in out Vector;
- New_Item : Vector)
- with
+ procedure Append (Container : in out Vector; New_Item : Vector) with
Global => null,
Pre =>
Length (Container) <= Capacity (Container) - Length (New_Item),
-- Elements of New_Item are inserted at the end of Container
and (if Length (New_Item) > 0 then
- M.Range_Shifted
- (Left => Model (New_Item),
- Right => Model (Container),
- Fst => Index_Type'First,
- Lst => Last_Index (New_Item),
- Offset =>
- Count_Type
- (Last_Index (Container)'Old - Index_Type'First + 1)));
+ M.Range_Shifted
+ (Left => Model (New_Item),
+ Right => Model (Container),
+ Fst => Index_Type'First,
+ Lst => Last_Index (New_Item),
+ Offset =>
+ Count_Type
+ (Last_Index (Container)'Old - Index_Type'First + 1)));
- procedure Append
- (Container : in out Vector;
- New_Item : Element_Type)
- with
+ procedure Append (Container : in out Vector; New_Item : Element_Type) with
Global => null,
Pre => Length (Container) < Capacity (Container),
Post =>
-- New_Item is inserted Count times at the end of Container
and (if Count > 0 then
- M.Constant_Range
- (Container => Model (Container),
- Fst => Last_Index (Container)'Old + 1,
- Lst =>
- Last_Index (Container)'Old + Index_Type'Base (Count),
- Item => New_Item));
+ M.Constant_Range
+ (Container => Model (Container),
+ Fst => Last_Index (Container)'Old + 1,
+ Lst =>
+ Last_Index (Container)'Old + Index_Type'Base (Count),
+ Item => New_Item));
- procedure Delete
- (Container : in out Vector;
- Index : Extended_Index)
- with
+ procedure Delete (Container : in out Vector; Index : Extended_Index) with
Global => null,
Pre => Index in First_Index (Container) .. Last_Index (Container),
Post =>
Lst => Last_Index (Container),
Offset => Count));
- procedure Delete_First
- (Container : in out Vector)
- with
+ procedure Delete_First (Container : in out Vector) with
Global => null,
Pre => Length (Container) > 0,
Post =>
Lst => Last_Index (Container),
Offset => 1);
- procedure Delete_First
- (Container : in out Vector;
- Count : Count_Type)
- with
+ procedure Delete_First (Container : in out Vector; Count : Count_Type) with
Global => null,
Contract_Cases =>
Lst => Last_Index (Container),
Offset => Count));
- procedure Delete_Last
- (Container : in out Vector)
- with
+ procedure Delete_Last (Container : in out Vector) with
Global => null,
Pre => Length (Container) > 0,
Post =>
and Model (Container) < Model (Container)'Old;
- procedure Delete_Last
- (Container : in out Vector;
- Count : Count_Type)
- with
+ procedure Delete_Last (Container : in out Vector; Count : Count_Type) with
Global => null,
Contract_Cases =>
Global => null,
Post => M_Elements_Reversed (Model (Container)'Old, Model (Container));
- procedure Swap (Container : in out Vector; I, J : Index_Type) with
+ procedure Swap
+ (Container : in out Vector;
+ I : Index_Type;
+ J : Index_Type)
+ with
Global => null,
- Pre => I in First_Index (Container) .. Last_Index (Container)
- and then J in First_Index (Container) .. Last_Index (Container),
+ Pre =>
+ I in First_Index (Container) .. Last_Index (Container)
+ and then J in First_Index (Container) .. Last_Index (Container),
Post =>
M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J);
-- returns No_Index.
(Index > Last_Index (Container)
- or else not M.Contains
- (Container => Model (Container),
- Fst => Index,
- Lst => Last_Index (Container),
- Item => Item)
+ or else not M.Contains
+ (Container => Model (Container),
+ Fst => Index,
+ Lst => Last_Index (Container),
+ Item => Item)
=>
Find_Index'Result = No_Index,
(Container => Model (Container),
Fst => Reverse_Find_Index'Result + 1,
Lst =>
- (if Index <= Last_Index (Container) then Index
- else Last_Index (Container)),
+ (if Index <= Last_Index (Container) then
+ Index
+ else
+ Last_Index (Container)),
Item => Item));
function Contains
with
Global => null,
Post =>
- Contains'Result = M.Contains (Container => Model (Container),
- Fst => Index_Type'First,
- Lst => Last_Index (Container),
- Item => Item);
+ Contains'Result =
+ M.Contains
+ (Container => Model (Container),
+ Fst => Index_Type'First,
+ Lst => Last_Index (Container),
+ Item => Item);
function Has_Element
(Container : Vector;
M_Elements_Sorted'Result =
(for all I in Index_Type'First .. M.Last (Container) =>
(for all J in I .. M.Last (Container) =>
- Element (Container, I) = Element (Container, J)
- or Element (Container, I) < Element (Container, J)));
+ Element (Container, I) = Element (Container, J)
+ or Element (Container, I) < Element (Container, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
function Is_Sorted (Container : Vector) return Boolean with
Post =>
Length (Container) = Length (Container)'Old
and M_Elements_Sorted (Model (Container))
- and M_Elements_Included (Left => Model (Container)'Old,
- L_Lst => Last_Index (Container),
- Right => Model (Container),
- R_Lst => Last_Index (Container))
- and M_Elements_Included (Left => Model (Container),
- L_Lst => Last_Index (Container),
- Right => Model (Container)'Old,
- R_Lst => Last_Index (Container));
+ and M_Elements_Included
+ (Left => Model (Container)'Old,
+ L_Lst => Last_Index (Container),
+ Right => Model (Container),
+ R_Lst => Last_Index (Container))
+ and M_Elements_Included
+ (Left => Model (Container),
+ L_Lst => Last_Index (Container),
+ Right => Model (Container)'Old,
+ R_Lst => Last_Index (Container));
procedure Merge (Target : in out Vector; Source : in out Vector) with
-- Target and Source should not be aliased
and Length (Source) = 0
and (if M_Elements_Sorted (Model (Target)'Old)
and M_Elements_Sorted (Model (Source)'Old)
- then M_Elements_Sorted (Model (Target)))
- and M_Elements_Included (Left => Model (Target)'Old,
- L_Lst => Last_Index (Target)'Old,
- Right => Model (Target),
- R_Lst => Last_Index (Target))
- and M_Elements_Included (Left => Model (Source)'Old,
- L_Lst => Last_Index (Source)'Old,
- Right => Model (Target),
- R_Lst => Last_Index (Target))
- and M_Elements_In_Union (Model (Target),
- Model (Source)'Old,
- Model (Target)'Old);
+ then
+ M_Elements_Sorted (Model (Target)))
+ and M_Elements_Included
+ (Left => Model (Target)'Old,
+ L_Lst => Last_Index (Target)'Old,
+ Right => Model (Target),
+ R_Lst => Last_Index (Target))
+ and M_Elements_Included
+ (Left => Model (Source)'Old,
+ L_Lst => Last_Index (Source)'Old,
+ Right => Model (Target),
+ R_Lst => Last_Index (Target))
+ and M_Elements_In_Union
+ (Model (Target),
+ Model (Source)'Old,
+ Model (Target)'Old);
end Generic_Sorting;
private
type Elements_Array_Ptr is access all Elements_Array;
type Vector (Capacity : Capacity_Range) is limited record
+
-- In the bounded case, the elements are stored in Elements. In the
-- unbounded case, the elements are initially stored in Elements, until
-- we run out of room, then we switch to Elements_Ptr.
+
Last : Extended_Index := No_Index;
Elements_Ptr : Elements_Array_Ptr := null;
Elements : aliased Elements_Array (1 .. Capacity);
type Int is range System.Min_Int .. System.Max_Int;
procedure Free is
- new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr);
+ new Ada.Unchecked_Deallocation (Elements_Array, Elements_Array_Ptr);
type Maximal_Array_Ptr is access all Elements_Array (Array_Index)
with Storage_Size => 0;
type Maximal_Array_Ptr_Const is access constant Elements_Array (Array_Index)
- with Storage_Size => 0;
+ with Storage_Size => 0;
function Elems (Container : in out Vector) return Maximal_Array_Ptr;
function Elemsc
-- "=" --
---------
- function "=" (Left, Right : Vector) return Boolean is
+ function "=" (Left : Vector; Right : Vector) return Boolean is
begin
if Left'Address = Right'Address then
return True;
Insert (Container, Container.Last + 1, New_Item);
end Append;
- procedure Append
- (Container : in out Vector;
- New_Item : Element_Type)
- is
+ procedure Append (Container : in out Vector; New_Item : Element_Type) is
begin
Append (Container, New_Item, 1);
end Append;
function Capacity (Container : Vector) return Capacity_Range is
begin
- return (if Bounded then Container.Capacity
- else Capacity_Range'Last);
+ return
+ (if Bounded then
+ Container.Capacity
+ else
+ Capacity_Range'Last);
end Capacity;
-----------
function Current_Capacity (Container : Vector) return Capacity_Range is
begin
- return (if Container.Elements_Ptr = null
- then Container.Elements'Length
- else Container.Elements_Ptr.all'Length);
+ return
+ (if Container.Elements_Ptr = null then
+ Container.Elements'Length
+ else
+ Container.Elements_Ptr.all'Length);
end Current_Capacity;
------------
-- Delete --
------------
- procedure Delete
- (Container : in out Vector;
- Index : Extended_Index)
- is
+ procedure Delete (Container : in out Vector; Index : Extended_Index) is
begin
Delete (Container, Index, 1);
end Delete;
end if;
-- There are some elements aren't being deleted (the requested count was
- -- less than the available count), so we must slide them down to
- -- Index. We first calculate the index values of the respective array
- -- slices, using the wider of Index_Type'Base and Count_Type'Base as the
- -- type for intermediate calculations.
+ -- less than the available count), so we must slide them down to Index.
+ -- We first calculate the index values of the respective array slices,
+ -- using the wider of Index_Type'Base and Count_Type'Base as the type
+ -- for intermediate calculations.
if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
Off := Count_Type'Base (Index - Index_Type'First);
-- Delete_First --
------------------
- procedure Delete_First
- (Container : in out Vector)
- is
+ procedure Delete_First (Container : in out Vector) is
begin
Delete_First (Container, 1);
end Delete_First;
- procedure Delete_First
- (Container : in out Vector;
- Count : Count_Type)
- is
+ procedure Delete_First (Container : in out Vector; Count : Count_Type) is
begin
if Count = 0 then
return;
-- Delete_Last --
-----------------
- procedure Delete_Last
- (Container : in out Vector)
- is
+ procedure Delete_Last (Container : in out Vector) is
begin
Delete_Last (Container, 1);
end Delete_Last;
- procedure Delete_Last
- (Container : in out Vector;
- Count : Count_Type)
- is
+ procedure Delete_Last (Container : in out Vector; Count : Count_Type) is
begin
if Count = 0 then
return;
function Elems (Container : in out Vector) return Maximal_Array_Ptr is
begin
- return (if Container.Elements_Ptr = null
- then Container.Elements'Unrestricted_Access
- else Container.Elements_Ptr.all'Unrestricted_Access);
+ return
+ (if Container.Elements_Ptr = null then
+ Container.Elements'Unrestricted_Access
+ else
+ Container.Elements_Ptr.all'Unrestricted_Access);
end Elems;
- function Elemsc
- (Container : Vector) return Maximal_Array_Ptr_Const is
+ function Elemsc (Container : Vector) return Maximal_Array_Ptr_Const is
begin
- return (if Container.Elements_Ptr = null
- then Container.Elements'Unrestricted_Access
- else Container.Elements_Ptr.all'Unrestricted_Access);
+ return
+ (if Container.Elements_Ptr = null then
+ Container.Elements'Unrestricted_Access
+ else
+ Container.Elements_Ptr.all'Unrestricted_Access);
end Elemsc;
----------------
Left : M.Sequence;
Right : M.Sequence) return Boolean
is
- begin
- for I in Index_Type'First .. M.Last (Container) loop
- declare
- Found : Boolean := False;
- J : Extended_Index := Extended_Index'First;
-
- begin
- while not Found and J < M.Last (Left) loop
- J := J + 1;
- if Element (Container, I) = Element (Left, J) then
- Found := True;
- end if;
- end loop;
+ Elem : Element_Type;
- J := Extended_Index'First;
-
- while not Found and J < M.Last (Right) loop
- J := J + 1;
- if Element (Container, I) = Element (Right, J) then
- Found := True;
- end if;
- end loop;
+ begin
+ for Index in Index_Type'First .. M.Last (Container) loop
+ Elem := Element (Container, Index);
- if not Found then
- return False;
- end if;
- end;
+ if not M.Contains (Left, Index_Type'First, M.Last (Left), Elem)
+ and then
+ not M.Contains (Right, Index_Type'First, M.Last (Right), Elem)
+ then
+ return False;
+ end if;
end loop;
return True;
-- M_Elements_Reversed --
-------------------------
- function M_Elements_Reversed (Left, Right : M.Sequence) return Boolean is
+ function M_Elements_Reversed
+ (Left : M.Sequence;
+ Right : M.Sequence) return Boolean
+ is
L : constant Index_Type := M.Last (Left);
+
begin
if L /= M.Last (Right) then
return False;
function M_Elements_Swapped
(Left : M.Sequence;
Right : M.Sequence;
- X, Y : Index_Type) return Boolean
+ X : Index_Type;
+ Y : Index_Type) return Boolean
is
begin
if M.Length (Left) /= M.Length (Right)
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;
function Is_Sorted (Container : Vector) return Boolean is
L : constant Capacity_Range := Length (Container);
+
begin
for J in 1 .. L - 1 loop
if Get_Element (Container, J + 1) <
-- Sort --
----------
- procedure Sort (Container : in out Vector)
- is
+ procedure Sort (Container : in out Vector) is
procedure Sort is
new Generic_Array_Sort
- (Index_Type => Array_Index,
- Element_Type => Element_Type,
- Array_Type => Elements_Array,
- "<" => "<");
+ (Index_Type => Array_Index,
+ Element_Type => Element_Type,
+ Array_Type => Elements_Array,
+ "<" => "<");
Len : constant Capacity_Range := Length (Container);
+
begin
if Container.Last <= Index_Type'First then
return;
-- Merge --
-----------
- procedure Merge (Target, Source : in out Vector) is
- I, J : Count_Type;
+ procedure Merge (Target : in out Vector; Source : in out Vector) is
+ I : Count_Type;
+ J : Count_Type;
begin
if Target'Address = Source'Address then
- raise Program_Error with
- "Target and Source denote same container";
+ raise Program_Error with "Target and Source denote same container";
end if;
if Length (Source) = 0 then
declare
New_Length : constant Count_Type := I + Length (Source);
+
begin
- if not Bounded and then
- Current_Capacity (Target) < Capacity_Range (New_Length)
+ if not Bounded
+ and then Current_Capacity (Target) < Capacity_Range (New_Length)
then
Reserve_Capacity
(Target,
Capacity_Range'Max
(Current_Capacity (Target) * Growth_Factor,
- Capacity_Range (New_Length)));
+ Capacity_Range (New_Length)));
end if;
if Index_Type'Base'Last >= Count_Type'Pos (Count_Type'Last) then
declare
TA : Maximal_Array_Ptr renames Elems (Target);
SA : Maximal_Array_Ptr renames Elems (Source);
+
begin
J := Length (Target);
while Length (Source) /= 0 loop
-----------------
function Has_Element
- (Container : Vector; Position : Extended_Index) return Boolean is
+ (Container : Vector;
+ Position : Extended_Index) return Boolean
+ is
begin
return Position in First_Index (Container) .. Last_Index (Container);
end Has_Element;
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.
-- There are two constraints we need to satisfy. The first constraint is
-- that a container cannot have more than Count_Type'Last elements, so
- -- we must check the sum of the current length and the insertion
- -- count. Note that we cannot simply add these values, because of the
- -- possibility of overflow.
+ -- we must check the sum of the current length and the insertion count.
+ -- Note that the value cannot be simply added because the result may
+ -- overflow.
if Old_Length > Count_Type'Last - Count then
raise Constraint_Error with "Count is out of range";
-- worry about if No_Index were less than 0, but that case is
-- handled above).
- if Index_Type'Last - No_Index >=
- Count_Type'Pos (Count_Type'Last)
+ if Index_Type'Last - No_Index >= Count_Type'Pos (Count_Type'Last)
then
-- We have determined that range of Index_Type has at least as
-- many values as in Count_Type, so Count_Type'Last is the
-- Increase the capacity of container if needed
- if not Bounded and then
- Current_Capacity (Container) < Capacity_Range (New_Length)
+ if not Bounded
+ and then Current_Capacity (Container) < Capacity_Range (New_Length)
then
Reserve_Capacity
(Container,
Capacity_Range'Max (Current_Capacity (Container) * Growth_Factor,
- Capacity_Range (New_Length)));
+ Capacity_Range (New_Length)));
end if;
declare
EA : Maximal_Array_Ptr renames Elems (Container);
+
begin
if Before <= Container.Last then
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
+ 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;
Insert (Container, Index_Type'First, New_Item);
end Prepend;
- procedure Prepend
- (Container : in out Vector;
- New_Item : Element_Type)
- is
+ procedure Prepend (Container : in out Vector; New_Item : Element_Type) is
begin
Prepend (Container, New_Item, 1);
end Prepend;
declare
II : constant Int'Base := Int (Index) - Int (No_Index);
I : constant Capacity_Range := Capacity_Range (II);
+
begin
Elems (Container) (I) := New_Item;
end;
if Capacity > Container.Capacity then
raise Constraint_Error with "Capacity is out of range";
end if;
+
else
if Capacity > Formal_Vectors.Current_Capacity (Container) then
declare
New_Elements : constant Elements_Array_Ptr :=
new Elements_Array (1 .. Capacity);
L : constant Capacity_Range := Length (Container);
+
begin
New_Elements (1 .. L) := Elemsc (Container) (1 .. L);
Free (Container.Elements_Ptr);
while I < J loop
declare
EI : constant Element_Type := E (I);
+
begin
E (I) := E (J);
E (J) := EI;
-- Swap --
----------
- procedure Swap (Container : in out Vector; I, J : Index_Type) is
+ procedure Swap
+ (Container : in out Vector;
+ I : Index_Type;
+ J : Index_Type)
+ is
begin
if I > Container.Last then
raise Constraint_Error with "I index is out of range";
Offset := Count_Type'Base (Index - Index_Type'First);
else
- Offset := Count_Type'Base (Index) -
- Count_Type'Base (Index_Type'First);
+ Offset :=
+ Count_Type'Base (Index) - Count_Type'Base (Index_Type'First);
end if;
- -- The array index subtype for all container element arrays
- -- always starts with 1.
+ -- The array index subtype for all container element arrays always
+ -- starts with 1.
return 1 + Offset;
end To_Array_Index;
Last := Index_Type (Last_As_Int);
- return (Capacity => Length,
- Last => Last,
- Elements_Ptr => <>,
- Elements => (others => New_Item));
+ return
+ (Capacity => Length,
+ Last => Last,
+ Elements_Ptr => <>,
+ Elements => (others => New_Item));
end;
end To_Vector;
(for all I in Index_Type'First .. M.Last (Container) =>
(for some J in Index_Type'First .. M.Last (Left) =>
Element (Container, I) = Element (Left, J))
- or (for some J in Index_Type'First .. M.Last (Right) =>
- Element (Container, I) = Element (Right, J)));
+ or (for some J in Index_Type'First .. M.Last (Right) =>
+ Element (Container, I) = Element (Right, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union);
function M_Elements_Included
M_Elements_Reversed'Result =
(M.Length (Left) = M.Length (Right)
and (for all I in Index_Type'First .. M.Last (Left) =>
- Element (Left, I) =
- Element (Right, M.Last (Left) - I + 1))
+ Element (Left, I) =
+ Element (Right, M.Last (Left) - I + 1))
and (for all I in Index_Type'First .. M.Last (Right) =>
- Element (Right, I) =
- Element (Left, M.Last (Left) - I + 1)));
+ Element (Right, I) =
+ Element (Left, M.Last (Left) - I + 1)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed);
function M_Elements_Swapped
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;
Global => null,
Post =>
Formal_Vectors.Length (To_Vector'Result) = Length
- and M.Constant_Range (Container => Model (To_Vector'Result),
- Fst => Index_Type'First,
- Lst => Last_Index (To_Vector'Result),
- Item => New_Item);
+ and M.Constant_Range
+ (Container => Model (To_Vector'Result),
+ Fst => Index_Type'First,
+ Lst => Last_Index (To_Vector'Result),
+ Item => New_Item);
function Capacity (Container : Vector) return Capacity_Range with
Global => null,
Post =>
- Capacity'Result = (if Bounded then Container.Capacity
- else Capacity_Range'Last);
+ Capacity'Result =
+ (if Bounded then
+ Container.Capacity
+ else
+ Capacity_Range'Last);
pragma Annotate (GNATprove, Inline_For_Proof, Capacity);
procedure Reserve_Capacity
Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)),
Post =>
Model (Copy'Result) = Model (Source)
- and (if Capacity = 0 then Copy'Result.Capacity = Length (Source)
- else Copy'Result.Capacity = Capacity);
+ and (if Capacity = 0 then
+ Copy'Result.Capacity = Length (Source)
+ else
+ Copy'Result.Capacity = Capacity);
procedure Move (Target : in out Vector; Source : in out Vector)
with
Pre =>
Length (Container) <= Capacity (Container) - Length (New_Item)
and (Before in Index_Type'First .. Last_Index (Container)
- or (Before /= No_Index
+ or (Before /= No_Index
and then Before - 1 = Last_Index (Container))),
Post =>
Length (Container) = Length (Container)'Old + Length (New_Item)
-- Elements of New_Item are inserted at position Before
and (if Length (New_Item) > 0 then
- M.Range_Shifted
- (Left => Model (New_Item),
- Right => Model (Container),
- Fst => Index_Type'First,
- Lst => Last_Index (New_Item),
- Offset => Count_Type (Before - Index_Type'First)))
+ M.Range_Shifted
+ (Left => Model (New_Item),
+ Right => Model (Container),
+ Fst => Index_Type'First,
+ Lst => Last_Index (New_Item),
+ Offset => Count_Type (Before - Index_Type'First)))
-- Elements located after Before in Container are shifted
Pre =>
Length (Container) <= Capacity (Container) - Count
and (Before in Index_Type'First .. Last_Index (Container)
- or (Before /= No_Index
+ or (Before /= No_Index
and then Before - 1 = Last_Index (Container))),
Post =>
Length (Container) = Length (Container)'Old + Count
-- New_Item is inserted Count times at position Before
and (if Count > 0 then
- M.Constant_Range
- (Container => Model (Container),
- Fst => Before,
- Lst => Before + Index_Type'Base (Count - 1),
- Item => New_Item))
+ M.Constant_Range
+ (Container => Model (Container),
+ Fst => Before,
+ Lst => Before + Index_Type'Base (Count - 1),
+ Item => New_Item))
-- Elements located after Before in Container are shifted
Lst => Last_Index (Container)'Old,
Offset => Count);
- procedure Prepend
- (Container : in out Vector;
- New_Item : Vector)
- with
+ procedure Prepend (Container : in out Vector; New_Item : Vector) with
Global => null,
Pre => Length (Container) <= Capacity (Container) - Length (New_Item),
Post =>
Lst => Last_Index (Container)'Old,
Offset => Length (New_Item));
- procedure Prepend
- (Container : in out Vector;
- New_Item : Element_Type)
- with
+ procedure Prepend (Container : in out Vector; New_Item : Element_Type) with
Global => null,
Pre => Length (Container) < Capacity (Container),
Post =>
Lst => Last_Index (Container)'Old,
Offset => Count);
- procedure Append
- (Container : in out Vector;
- New_Item : Vector)
- with
+ procedure Append (Container : in out Vector; New_Item : Vector) with
Global => null,
Pre =>
Length (Container) <= Capacity (Container) - Length (New_Item),
-- Elements of New_Item are inserted at the end of Container
and (if Length (New_Item) > 0 then
- M.Range_Shifted
- (Left => Model (New_Item),
- Right => Model (Container),
- Fst => Index_Type'First,
- Lst => Last_Index (New_Item),
- Offset =>
- Count_Type
- (Last_Index (Container)'Old - Index_Type'First + 1)));
+ M.Range_Shifted
+ (Left => Model (New_Item),
+ Right => Model (Container),
+ Fst => Index_Type'First,
+ Lst => Last_Index (New_Item),
+ Offset =>
+ Count_Type
+ (Last_Index (Container)'Old - Index_Type'First + 1)));
- procedure Append
- (Container : in out Vector;
- New_Item : Element_Type)
- with
+ procedure Append (Container : in out Vector; New_Item : Element_Type) with
Global => null,
Pre => Length (Container) < Capacity (Container),
Post =>
-- New_Item is inserted Count times at the end of Container
and (if Count > 0 then
- M.Constant_Range
- (Container => Model (Container),
- Fst => Last_Index (Container)'Old + 1,
- Lst =>
- Last_Index (Container)'Old + Index_Type'Base (Count),
- Item => New_Item));
+ M.Constant_Range
+ (Container => Model (Container),
+ Fst => Last_Index (Container)'Old + 1,
+ Lst =>
+ Last_Index (Container)'Old + Index_Type'Base (Count),
+ Item => New_Item));
- procedure Delete
- (Container : in out Vector;
- Index : Extended_Index)
- with
+ procedure Delete (Container : in out Vector; Index : Extended_Index) with
Global => null,
Pre => Index in First_Index (Container) .. Last_Index (Container),
Post =>
Lst => Last_Index (Container),
Offset => Count));
- procedure Delete_First
- (Container : in out Vector)
- with
+ procedure Delete_First (Container : in out Vector) with
Global => null,
Pre => Length (Container) > 0,
Post =>
Lst => Last_Index (Container),
Offset => 1);
- procedure Delete_First
- (Container : in out Vector;
- Count : Count_Type)
- with
+ procedure Delete_First (Container : in out Vector; Count : Count_Type) with
Global => null,
Contract_Cases =>
Lst => Last_Index (Container),
Offset => Count));
- procedure Delete_Last
- (Container : in out Vector)
- with
+ procedure Delete_Last (Container : in out Vector) with
Global => null,
Pre => Length (Container) > 0,
Post =>
and Model (Container) < Model (Container)'Old;
- procedure Delete_Last
- (Container : in out Vector;
- Count : Count_Type)
- with
+ procedure Delete_Last (Container : in out Vector; Count : Count_Type) with
Global => null,
Contract_Cases =>
Global => null,
Post => M_Elements_Reversed (Model (Container)'Old, Model (Container));
- procedure Swap (Container : in out Vector; I, J : Index_Type) with
+ procedure Swap
+ (Container : in out Vector;
+ I : Index_Type;
+ J : Index_Type)
+ with
Global => null,
- Pre => I in First_Index (Container) .. Last_Index (Container)
- and then J in First_Index (Container) .. Last_Index (Container),
+ Pre =>
+ I in First_Index (Container) .. Last_Index (Container)
+ and then J in First_Index (Container) .. Last_Index (Container),
Post =>
M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J);
-- returns No_Index.
(Index > Last_Index (Container)
- or else not M.Contains
- (Container => Model (Container),
- Fst => Index,
- Lst => Last_Index (Container),
- Item => Item)
+ or else not M.Contains
+ (Container => Model (Container),
+ Fst => Index,
+ Lst => Last_Index (Container),
+ Item => Item)
=>
Find_Index'Result = No_Index,
-- Index
others =>
- Reverse_Find_Index'Result in Index_Type'First .. Index
+ Reverse_Find_Index'Result in Index_Type'First .. Index
and Reverse_Find_Index'Result <= Last_Index (Container)
-- The element at this index in Container is Item
(Container => Model (Container),
Fst => Reverse_Find_Index'Result + 1,
Lst =>
- (if Index <= Last_Index (Container) then Index
- else Last_Index (Container)),
+ (if Index <= Last_Index (Container) then
+ Index
+ else
+ Last_Index (Container)),
Item => Item));
function Contains
with
Global => null,
Post =>
- Contains'Result = M.Contains (Container => Model (Container),
- Fst => Index_Type'First,
- Lst => Last_Index (Container),
- Item => Item);
+ Contains'Result =
+ M.Contains
+ (Container => Model (Container),
+ Fst => Index_Type'First,
+ Lst => Last_Index (Container),
+ Item => Item);
function Has_Element
(Container : Vector;
M_Elements_Sorted'Result =
(for all I in Index_Type'First .. M.Last (Container) =>
(for all J in I .. M.Last (Container) =>
- Element (Container, I) = Element (Container, J)
- or Element (Container, I) < Element (Container, J)));
+ Element (Container, I) = Element (Container, J)
+ or Element (Container, I) < Element (Container, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
function Is_Sorted (Container : Vector) return Boolean with
Post =>
Length (Container) = Length (Container)'Old
and M_Elements_Sorted (Model (Container))
- and M_Elements_Included (Left => Model (Container)'Old,
- L_Lst => Last_Index (Container),
- Right => Model (Container),
- R_Lst => Last_Index (Container))
- and M_Elements_Included (Left => Model (Container),
- L_Lst => Last_Index (Container),
- Right => Model (Container)'Old,
- R_Lst => Last_Index (Container));
+ and M_Elements_Included
+ (Left => Model (Container)'Old,
+ L_Lst => Last_Index (Container),
+ Right => Model (Container),
+ R_Lst => Last_Index (Container))
+ and M_Elements_Included
+ (Left => Model (Container),
+ L_Lst => Last_Index (Container),
+ Right => Model (Container)'Old,
+ R_Lst => Last_Index (Container));
procedure Merge (Target : in out Vector; Source : in out Vector) with
-- Target and Source should not be aliased
and Length (Source) = 0
and (if M_Elements_Sorted (Model (Target)'Old)
and M_Elements_Sorted (Model (Source)'Old)
- then M_Elements_Sorted (Model (Target)))
- and M_Elements_Included (Left => Model (Target)'Old,
- L_Lst => Last_Index (Target)'Old,
- Right => Model (Target),
- R_Lst => Last_Index (Target))
- and M_Elements_Included (Left => Model (Source)'Old,
- L_Lst => Last_Index (Source)'Old,
- Right => Model (Target),
- R_Lst => Last_Index (Target))
- and M_Elements_In_Union (Model (Target),
- Model (Source)'Old,
- Model (Target)'Old);
+ then
+ M_Elements_Sorted (Model (Target)))
+ and M_Elements_Included
+ (Left => Model (Target)'Old,
+ L_Lst => Last_Index (Target)'Old,
+ Right => Model (Target),
+ R_Lst => Last_Index (Target))
+ and M_Elements_Included
+ (Left => Model (Source)'Old,
+ L_Lst => Last_Index (Source)'Old,
+ Right => Model (Target),
+ R_Lst => Last_Index (Target))
+ and M_Elements_In_Union
+ (Model (Target),
+ Model (Source)'Old,
+ Model (Target)'Old);
end Generic_Sorting;
private
type Elements_Array_Ptr is access all Elements_Array;
type Vector (Capacity : Capacity_Range) is limited record
+
-- In the bounded case, the elements are stored in Elements. In the
-- unbounded case, the elements are initially stored in Elements, until
-- we run out of room, then we switch to Elements_Ptr.
+
Last : Extended_Index := No_Index;
Elements_Ptr : Elements_Array_Ptr := null;
Elements : aliased Elements_Array (1 .. Capacity);
Cancel_Param := Make_Defining_Identifier (Loc, Name_uC);
- -- Insert declaration of C in declarations of existing block
+ -- Insert the declaration of C in the declarations of the existing
+ -- block. The variable is initialized to something (True or False,
+ -- does not matter) to prevent CodePeer from complaining about a
+ -- possible read of an uninitialized variable.
Prepend_To (Decls,
Make_Object_Declaration (Loc,
Defining_Identifier => Cancel_Param,
- Object_Definition =>
- New_Occurrence_Of (Standard_Boolean, Loc),
- Expression =>
- New_Occurrence_Of (Standard_False, Loc),
- -- True would work equally well here. This initialization
- -- should be dead, but only because of things (e.g.,
- -- abortion deferral) that CodePeer doesn't know about.
- -- We want to avoid CodePeer complaints about a possible read
- -- of an uninitialized variable when this variable is read,
- -- so we initialize it here.
+ Object_Definition => New_Occurrence_Of (Standard_Boolean, Loc),
+ Expression => New_Occurrence_Of (Standard_False, Loc),
Has_Init_Expression => True));
-- Remove and save the call to Call_Simple
if Present (New_E) then
Rewrite (N, New_Occurrence_Of (New_E, Sloc (N)));
- -- If the entity is an overridden primitive and we are not
- -- in proof mode, we must build a wrapper for the current
+ -- If the entity is an overridden primitive and we are not in
+ -- GNATprove mode, we must build a wrapper for the current
-- inherited operation.
- if Is_Subprogram (New_E)
- and then not GNATprove_Mode
- then
+ if Is_Subprogram (New_E) and then not GNATprove_Mode then
Needs_Wrapper := True;
end if;
end if;
Old_Table : Old_Alloc_Ptr := To_Old_Alloc_Ptr (T.Table);
New_Table : constant Alloc_Ptr :=
- new Alloc_Type'(Old_Table (Alloc_Type'Range));
+ new Alloc_Type'(Old_Table (Alloc_Type'Range));
begin
T.P.Last_Allocated := T.P.Last;
Free (Old_Table);
if Dim_Of_Expr /= Dim_Of_Etyp then
- -- Numeric literal case. Issue a warning if the object type is not
- -- dimensionless to indicate the literal is treated as if its
- -- dimension matches the type dimension.
+ -- Numeric literal case. Issue a warning if the object type is
+ -- not dimensionless to indicate the literal is treated as if
+ -- its dimension matches the type dimension.
if Nkind_In (Original_Node (Expr), N_Real_Literal,
N_Integer_Literal)
Set_Dimensions (Id, Dim_Of_Expr);
- -- Expression may have been constant-folded. If nominal type
- -- has dimensions, verify that expression has same type.
+ -- Expression may have been constant-folded. If nominal type has
+ -- dimensions, verify that expression has same type.
elsif Exists (Dim_Of_Etyp) and then Etype (Expr) = Etyp then
null;
end if;
end if;
- -- Remove dimensions in expression after checking consistency
- -- with given type.
+ -- Remove dimensions in expression after checking consistency with
+ -- given type.
Remove_Dimensions (Expr);
end if;
projects / gcc.git / commitdiff