Skip to content

R
riscv-gcc-1
Commit b63d61f7 by Arnaud Charlet
Options

[multiple changes] 

2017-04-27  Hristian Kirtchev  <kirtchev@adacore.com>

	* a-cofuse.adb, a-cfdlli.adb, a-cofuse.ads, a-cfdlli.ads, a-cofuve.adb,
	a-cofuve.ads, a-cofuma.adb, a-cofuma.ads, sem_eval.adb, a-cofuba.adb:
	Minor reformatting.

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

	* sem_ch4.adb (Analyze_Call): If the return type of a function
	is incomplete in an context in which the full view is available,
	replace the type of the call by the full view, to prevent spurious
	type errors.
	* exp_disp.adb (Check_Premature_Freezing): Disable check on an
	abstract subprogram so that compiler does not reject a parameter
	of a primitive operation of a tagged type being frozen, when
	the untagged type of that parameter cannot be frozen.

2017-04-27  Bob Duff  <duff@adacore.com>

	* sem_attr.adb (Compute_Type_Key): Don't walk
	representation items for irrelevant types, which could be in a
	different source file.

2017-04-27  Steve Baird  <baird@adacore.com>

	* exp_attr.adb (Expand_N_Attribute_Reference):
	Don't expand Image, Wide_Image, Wide_Wide_Image attributes
	for CodePeer.

From-SVN: r247305
parent bb9e2aa2
Showing with 1252 additions and 940 deletions
gcc/ada/ChangeLog
2017-04-27 Hristian Kirtchev <kirtchev@adacore.com>
* a-cofuse.adb, a-cfdlli.adb, a-cofuse.ads, a-cfdlli.ads, a-cofuve.adb,
a-cofuve.ads, a-cofuma.adb, a-cofuma.ads, sem_eval.adb, a-cofuba.adb:
Minor reformatting.
2017-04-27 Ed Schonberg <schonberg@adacore.com>
* sem_ch4.adb (Analyze_Call): If the return type of a function
is incomplete in an context in which the full view is available,
replace the type of the call by the full view, to prevent spurious
type errors.
* exp_disp.adb (Check_Premature_Freezing): Disable check on an
abstract subprogram so that compiler does not reject a parameter
of a primitive operation of a tagged type being frozen, when
the untagged type of that parameter cannot be frozen.
2017-04-27 Bob Duff <duff@adacore.com>
* sem_attr.adb (Compute_Type_Key): Don't walk
representation items for irrelevant types, which could be in a
different source file.
2017-04-27 Steve Baird <baird@adacore.com>
* exp_attr.adb (Expand_N_Attribute_Reference):
Don't expand Image, Wide_Image, Wide_Wide_Image attributes
for CodePeer.
2017-04-27 Yannick Moy <moy@adacore.com> 2017-04-27 Yannick Moy <moy@adacore.com>
* exp_unst.ads: Fix typos in comments. * exp_unst.ads: Fix typos in comments.
......
gcc/ada/a-cfdlli.adb
...@@ -30,7 +30,6 @@ with System; use type System.Address; ...@@ -30,7 +30,6 @@ with System; use type System.Address;
package body Ada.Containers.Formal_Doubly_Linked_Lists with package body Ada.Containers.Formal_Doubly_Linked_Lists with
SPARK_Mode => Off SPARK_Mode => Off
is is
----------------------- -----------------------
-- Local Subprograms -- -- Local Subprograms --
----------------------- -----------------------
...@@ -55,8 +54,9 @@ is ...@@ -55,8 +54,9 @@ is
-- "=" -- -- "=" --
--------- ---------
function "=" (Left, Right : List) return Boolean is function "=" (Left : List; Right : List) return Boolean is
LI, RI : Count_Type; LI : Count_Type;
RI : Count_Type;
begin begin
if Left'Address = Right'Address then if Left'Address = Right'Address then
...@@ -230,10 +230,10 @@ is ...@@ -230,10 +230,10 @@ is
N := N + 1; N := N + 1;
end loop; end loop;
P.Free := Source.Free; P.Free := Source.Free;
P.Length := Source.Length; P.Length := Source.Length;
P.First := Source.First; P.First := Source.First;
P.Last := Source.Last; P.Last := Source.Last;
if P.Free >= 0 then if P.Free >= 0 then
N := Source.Capacity + 1; N := Source.Capacity + 1;
...@@ -250,14 +250,12 @@ is ...@@ -250,14 +250,12 @@ is
-- Delete -- -- Delete --
------------ ------------
procedure Delete procedure Delete (Container : in out List; Position : in out Cursor) is
(Container : in out List;
Position : in out Cursor)
is
begin begin
Delete (Container => Container, Delete
Position => Position, (Container => Container,
Count => 1); Position => Position,
Count => 1);
end Delete; end Delete;
procedure Delete procedure Delete
...@@ -272,8 +270,7 @@ is ...@@ -272,8 +270,7 @@ is
if not Has_Element (Container => Container, if not Has_Element (Container => Container,
Position => Position) Position => Position)
then then
raise Constraint_Error with raise Constraint_Error with "Position cursor has no element";
"Position cursor has no element";
end if; end if;
pragma Assert (Vet (Container, Position), "bad cursor in Delete"); pragma Assert (Vet (Container, Position), "bad cursor in Delete");
...@@ -317,6 +314,7 @@ is ...@@ -317,6 +314,7 @@ is
Free (Container, X); Free (Container, X);
end loop; end loop;
Position := No_Element; Position := No_Element;
end Delete; end Delete;
...@@ -324,17 +322,14 @@ is ...@@ -324,17 +322,14 @@ is
-- Delete_First -- -- Delete_First --
------------------ ------------------
procedure Delete_First (Container : in out List) procedure Delete_First (Container : in out List) is
is
begin begin
Delete_First (Container => Container, Delete_First
Count => 1); (Container => Container,
Count => 1);
end Delete_First; end Delete_First;
procedure Delete_First procedure Delete_First (Container : in out List; Count : Count_Type) is
(Container : in out List;
Count : Count_Type)
is
N : Node_Array renames Container.Nodes; N : Node_Array renames Container.Nodes;
X : Count_Type; X : Count_Type;
...@@ -365,17 +360,14 @@ is ...@@ -365,17 +360,14 @@ is
-- Delete_Last -- -- Delete_Last --
----------------- -----------------
procedure Delete_Last (Container : in out List) procedure Delete_Last (Container : in out List) is
is
begin begin
Delete_Last (Container => Container, Delete_Last
Count => 1); (Container => Container,
Count => 1);
end Delete_Last; end Delete_Last;
procedure Delete_Last procedure Delete_Last (Container : in out List; Count : Count_Type) is
(Container : in out List;
Count : Count_Type)
is
N : Node_Array renames Container.Nodes; N : Node_Array renames Container.Nodes;
X : Count_Type; X : Count_Type;
...@@ -412,8 +404,7 @@ is ...@@ -412,8 +404,7 @@ is
is is
begin begin
if not Has_Element (Container => Container, Position => Position) then if not Has_Element (Container => Container, Position => Position) then
raise Constraint_Error with raise Constraint_Error with "Position cursor has no element";
"Position cursor has no element";
end if; end if;
return Container.Nodes (Position.Node).Element; return Container.Nodes (Position.Node).Element;
...@@ -442,8 +433,7 @@ is ...@@ -442,8 +433,7 @@ is
if Position.Node /= 0 and then if Position.Node /= 0 and then
not Has_Element (Container, Position) not Has_Element (Container, Position)
then then
raise Constraint_Error with raise Constraint_Error with "Position cursor has no element";
"Position cursor has no element";
end if; end if;
while From /= 0 loop while From /= 0 loop
...@@ -476,6 +466,7 @@ is ...@@ -476,6 +466,7 @@ is
function First_Element (Container : List) return Element_Type is function First_Element (Container : List) return Element_Type is
F : constant Count_Type := Container.First; F : constant Count_Type := Container.First;
begin begin
if F = 0 then if F = 0 then
raise Constraint_Error with "list is empty"; raise Constraint_Error with "list is empty";
...@@ -500,8 +491,12 @@ is ...@@ -500,8 +491,12 @@ is
-- M_Elements_Reversed -- -- 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 Count_Type := M.Length (Left); L : constant Count_Type := M.Length (Left);
begin begin
if L /= M.Length (Right) then if L /= M.Length (Right) then
return False; return False;
...@@ -533,11 +528,13 @@ is ...@@ -533,11 +528,13 @@ is
declare declare
Found : Boolean := False; Found : Boolean := False;
J : Count_Type := Fst; J : Count_Type := Fst;
begin begin
while not Found and J <= Lst loop while not Found and J <= Lst loop
if Element (Left, I) = Element (Right, J + Offset) then if Element (Left, I) = Element (Right, J + Offset) then
Found := True; Found := True;
end if; end if;
J := J + 1; J := J + 1;
end loop; end loop;
...@@ -546,6 +543,7 @@ is ...@@ -546,6 +543,7 @@ is
end if; end if;
end; end;
end loop; end loop;
return True; return True;
end M_Elements_Shuffle; end M_Elements_Shuffle;
...@@ -556,7 +554,8 @@ is ...@@ -556,7 +554,8 @@ is
function M_Elements_Swapped function M_Elements_Swapped
(Left : M.Sequence; (Left : M.Sequence;
Right : M.Sequence; Right : M.Sequence;
X, Y : Positive_Count_Type) return Boolean X : Positive_Count_Type;
Y : Positive_Count_Type) return Boolean
is is
begin begin
if M.Length (Left) /= M.Length (Right) if M.Length (Left) /= M.Length (Right)
...@@ -584,13 +583,16 @@ is ...@@ -584,13 +583,16 @@ is
function Model (Container : List) return M.Sequence is function Model (Container : List) return M.Sequence is
Position : Count_Type := Container.First; Position : Count_Type := Container.First;
R : M.Sequence; R : M.Sequence;
begin begin
-- Can't use First, Next or Element here, since they depend -- Can't use First, Next or Element here, since they depend on models
-- on models for their postconditions -- for their postconditions.
while Position /= 0 loop while Position /= 0 loop
R := M.Add (R, Container.Nodes (Position).Element); R := M.Add (R, Container.Nodes (Position).Element);
Position := Container.Nodes (Position).Next; Position := Container.Nodes (Position).Next;
end loop; end loop;
return R; return R;
end Model; end Model;
...@@ -607,10 +609,10 @@ is ...@@ -607,10 +609,10 @@ is
begin begin
for C of P_Left loop for C of P_Left loop
if not P.Has_Key (P_Right, C) if not P.Has_Key (P_Right, C)
or else P.Get (P_Left, C) > M.Length (M_Left) or else P.Get (P_Left, C) > M.Length (M_Left)
or else P.Get (P_Right, C) > M.Length (M_Right) or else P.Get (P_Right, C) > M.Length (M_Right)
or else M.Get (M_Left, P.Get (P_Left, C)) or else M.Get (M_Left, P.Get (P_Left, C)) /=
/= M.Get (M_Right, P.Get (P_Right, C)) M.Get (M_Right, P.Get (P_Right, C))
then then
return False; return False;
end if; end if;
...@@ -645,18 +647,22 @@ is ...@@ -645,18 +647,22 @@ is
for Cu of Big loop for Cu of Big loop
declare declare
Pos : constant Positive_Count_Type := P.Get (Big, Cu); Pos : constant Positive_Count_Type := P.Get (Big, Cu);
begin begin
if Pos < Cut then if Pos < Cut then
if not P.Has_Key (Small, Cu) or else Pos /= P.Get (Small, Cu) if not P.Has_Key (Small, Cu)
or else Pos /= P.Get (Small, Cu)
then then
return False; return False;
end if; end if;
elsif Pos >= Cut + Count then elsif Pos >= Cut + Count then
if not P.Has_Key (Small, Cu) if not P.Has_Key (Small, Cu)
or else Pos /= P.Get (Small, Cu) + Count or else Pos /= P.Get (Small, Cu) + Count
then then
return False; return False;
end if; end if;
else else
if P.Has_Key (Small, Cu) then if P.Has_Key (Small, Cu) then
return False; return False;
...@@ -664,6 +670,7 @@ is ...@@ -664,6 +670,7 @@ is
end if; end if;
end; end;
end loop; end loop;
return True; return True;
end P_Positions_Shifted; end P_Positions_Shifted;
...@@ -674,17 +681,20 @@ is ...@@ -674,17 +681,20 @@ is
function P_Positions_Swapped function P_Positions_Swapped
(Left : P.Map; (Left : P.Map;
Right : P.Map; Right : P.Map;
X, Y : Cursor) return Boolean X : Cursor;
Y : Cursor) return Boolean
is is
begin begin
if not P.Has_Key (Left, X) or not P.Has_Key (Left, Y) if not P.Has_Key (Left, X)
or not P.Has_Key (Right, X) or not P.Has_Key (Right, Y) or not P.Has_Key (Left, Y)
or not P.Has_Key (Right, X)
or not P.Has_Key (Right, Y)
then then
return False; return False;
end if; end if;
if P.Get (Left, X) /= P.Get (Right, Y) if P.Get (Left, X) /= P.Get (Right, Y)
or P.Get (Left, Y) /= P.Get (Right, X) or P.Get (Left, Y) /= P.Get (Right, X)
then then
return False; return False;
end if; end if;
...@@ -698,7 +708,7 @@ is ...@@ -698,7 +708,7 @@ is
for C of Right loop for C of Right loop
if not P.Has_Key (Left, C) 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)) and P.Get (Left, C) /= P.Get (Right, C))
then then
return False; return False;
end if; end if;
...@@ -727,19 +737,24 @@ is ...@@ -727,19 +737,24 @@ is
for Cu of Big loop for Cu of Big loop
declare declare
Pos : constant Positive_Count_Type := P.Get (Big, Cu); Pos : constant Positive_Count_Type := P.Get (Big, Cu);
begin begin
if Pos < Cut then if Pos < Cut then
if not P.Has_Key (Small, Cu) or else Pos /= P.Get (Small, Cu) if not P.Has_Key (Small, Cu)
or else Pos /= P.Get (Small, Cu)
then then
return False; return False;
end if; end if;
elsif Pos >= Cut + Count then elsif Pos >= Cut + Count then
return False; return False;
elsif P.Has_Key (Small, Cu) then elsif P.Has_Key (Small, Cu) then
return False; return False;
end if; end if;
end; end;
end loop; end loop;
return True; return True;
end P_Positions_Truncated; end P_Positions_Truncated;
...@@ -748,18 +763,21 @@ is ...@@ -748,18 +763,21 @@ is
--------------- ---------------
function Positions (Container : List) return P.Map is function Positions (Container : List) return P.Map is
I : Count_Type := 1;
Position : Count_Type := Container.First; Position : Count_Type := Container.First;
R : P.Map; R : P.Map;
I : Count_Type := 1;
begin begin
-- Can't use First, Next or Element here, since they depend -- Can't use First, Next or Element here, since they depend on models
-- on models for their postconditions -- for their postconditions.
while Position /= 0 loop while Position /= 0 loop
R := P.Add (R, (Node => Position), I); R := P.Add (R, (Node => Position), I);
pragma Assert (P.Length (R) = I); pragma Assert (P.Length (R) = I);
Position := Container.Nodes (Position).Next; Position := Container.Nodes (Position).Next;
I := I + 1; I := I + 1;
end loop; end loop;
return R; return R;
end Positions; end Positions;
...@@ -769,10 +787,7 @@ is ...@@ -769,10 +787,7 @@ is
-- Free -- -- Free --
---------- ----------
procedure Free procedure Free (Container : in out List; X : Count_Type) is
(Container : in out List;
X : Count_Type)
is
pragma Assert (X > 0); pragma Assert (X > 0);
pragma Assert (X <= Container.Capacity); pragma Assert (X <= Container.Capacity);
...@@ -846,18 +861,22 @@ is ...@@ -846,18 +861,22 @@ is
declare declare
E1 : Element_Type := Element (Container, 1); E1 : Element_Type := Element (Container, 1);
begin begin
for I in 2 .. M.Length (Container) loop for I in 2 .. M.Length (Container) loop
declare declare
E2 : constant Element_Type := Element (Container, I); E2 : constant Element_Type := Element (Container, I);
begin begin
if E2 < E1 then if E2 < E1 then
return False; return False;
end if; end if;
E1 := E2; E1 := E2;
end; end;
end loop; end loop;
end; end;
return True; return True;
end M_Elements_Sorted; end M_Elements_Sorted;
...@@ -865,10 +884,7 @@ is ...@@ -865,10 +884,7 @@ is
-- Merge -- -- Merge --
----------- -----------
procedure Merge procedure Merge (Target : in out List; Source : in out List) is
(Target : in out List;
Source : in out List)
is
LN : Node_Array renames Target.Nodes; LN : Node_Array renames Target.Nodes;
RN : Node_Array renames Source.Nodes; RN : Node_Array renames Source.Nodes;
LI : Cursor; LI : Cursor;
...@@ -882,18 +898,20 @@ is ...@@ -882,18 +898,20 @@ is
LI := First (Target); LI := First (Target);
RI := First (Source); RI := First (Source);
while RI.Node /= 0 loop while RI.Node /= 0 loop
pragma Assert (RN (RI.Node).Next = 0 pragma Assert
or else not (RN (RN (RI.Node).Next).Element < (RN (RI.Node).Next = 0
RN (RI.Node).Element)); or else not (RN (RN (RI.Node).Next).Element <
RN (RI.Node).Element));
if LI.Node = 0 then if LI.Node = 0 then
Splice (Target, No_Element, Source); Splice (Target, No_Element, Source);
return; return;
end if; end if;
pragma Assert (LN (LI.Node).Next = 0 pragma Assert
or else not (LN (LN (LI.Node).Next).Element < (LN (LI.Node).Next = 0
LN (LI.Node).Element)); or else not (LN (LN (LI.Node).Next).Element <
LN (LI.Node).Element));
if RN (RI.Node).Element < LN (LI.Node).Element then if RN (RI.Node).Element < LN (LI.Node).Element then
declare declare
...@@ -917,14 +935,14 @@ is ...@@ -917,14 +935,14 @@ is
procedure Sort (Container : in out List) is procedure Sort (Container : in out List) is
N : Node_Array renames Container.Nodes; N : Node_Array renames Container.Nodes;
procedure Partition (Pivot, Back : Count_Type); procedure Partition (Pivot : Count_Type; Back : Count_Type);
procedure Sort (Front, Back : Count_Type); procedure Sort (Front : Count_Type; Back : Count_Type);
--------------- ---------------
-- Partition -- -- Partition --
--------------- ---------------
procedure Partition (Pivot, Back : Count_Type) is procedure Partition (Pivot : Count_Type; Back : Count_Type) is
Node : Count_Type; Node : Count_Type;
begin begin
...@@ -968,7 +986,7 @@ is ...@@ -968,7 +986,7 @@ is
-- Sort -- -- Sort --
---------- ----------
procedure Sort (Front, Back : Count_Type) is procedure Sort (Front : Count_Type; Back : Count_Type) is
Pivot : Count_Type; Pivot : Count_Type;
begin begin
...@@ -1060,11 +1078,12 @@ is ...@@ -1060,11 +1078,12 @@ is
Position : out Cursor) Position : out Cursor)
is is
begin begin
Insert (Container => Container, Insert
Before => Before, (Container => Container,
New_Item => New_Item, Before => Before,
Position => Position, New_Item => New_Item,
Count => 1); Position => Position,
Count => 1);
end Insert; end Insert;
procedure Insert procedure Insert
...@@ -1074,6 +1093,7 @@ is ...@@ -1074,6 +1093,7 @@ is
Count : Count_Type) Count : Count_Type)
is is
Position : Cursor; Position : Cursor;
begin begin
Insert (Container, Before, New_Item, Position, Count); Insert (Container, Before, New_Item, Position, Count);
end Insert; end Insert;
...@@ -1084,6 +1104,7 @@ is ...@@ -1084,6 +1104,7 @@ is
New_Item : Element_Type) New_Item : Element_Type)
is is
Position : Cursor; Position : Cursor;
begin begin
Insert (Container, Before, New_Item, Position, 1); Insert (Container, Before, New_Item, Position, 1);
end Insert; end Insert;
...@@ -1171,6 +1192,7 @@ is ...@@ -1171,6 +1192,7 @@ is
function Last_Element (Container : List) return Element_Type is function Last_Element (Container : List) return Element_Type is
L : constant Count_Type := Container.Last; L : constant Count_Type := Container.Last;
begin begin
if L = 0 then if L = 0 then
raise Constraint_Error with "list is empty"; raise Constraint_Error with "list is empty";
...@@ -1192,10 +1214,7 @@ is ...@@ -1192,10 +1214,7 @@ is
-- Move -- -- Move --
---------- ----------
procedure Move procedure Move (Target : in out List; Source : in out List) is
(Target : in out List;
Source : in out List)
is
N : Node_Array renames Source.Nodes; N : Node_Array renames Source.Nodes;
X : Count_Type; X : Count_Type;
...@@ -1295,10 +1314,7 @@ is ...@@ -1295,10 +1314,7 @@ is
-- Prepend -- -- Prepend --
------------- -------------
procedure Prepend procedure Prepend (Container : in out List; New_Item : Element_Type) is
(Container : in out List;
New_Item : Element_Type)
is
begin begin
Insert (Container, First (Container), New_Item, 1); Insert (Container, First (Container), New_Item, 1);
end Prepend; end Prepend;
...@@ -1363,13 +1379,13 @@ is ...@@ -1363,13 +1379,13 @@ is
I : Count_Type := Container.First; I : Count_Type := Container.First;
J : Count_Type := Container.Last; J : Count_Type := Container.Last;
procedure Swap (L, R : Count_Type); procedure Swap (L : Count_Type; R : Count_Type);
---------- ----------
-- Swap -- -- Swap --
---------- ----------
procedure Swap (L, R : Count_Type) is procedure Swap (L : Count_Type; R : Count_Type) is
LN : constant Count_Type := N (L).Next; LN : constant Count_Type := N (L).Next;
LP : constant Count_Type := N (L).Prev; LP : constant Count_Type := N (L).Prev;
...@@ -1414,7 +1430,7 @@ is ...@@ -1414,7 +1430,7 @@ is
pragma Assert (N (Container.Last).Next = 0); pragma Assert (N (Container.Last).Next = 0);
Container.First := J; Container.First := J;
Container.Last := I; Container.Last := I;
loop loop
Swap (L => I, R => J); Swap (L => I, R => J);
...@@ -1642,7 +1658,8 @@ is ...@@ -1642,7 +1658,8 @@ is
procedure Swap procedure Swap
(Container : in out List; (Container : in out List;
I, J : Cursor) I : Cursor;
J : Cursor)
is is
begin begin
if I.Node = 0 then if I.Node = 0 then
...@@ -1679,9 +1696,11 @@ is ...@@ -1679,9 +1696,11 @@ is
procedure Swap_Links procedure Swap_Links
(Container : in out List; (Container : in out List;
I, J : Cursor) I : Cursor;
J : Cursor)
is is
I_Next, J_Next : Cursor; I_Next : Cursor;
J_Next : Cursor;
begin begin
if I.Node = 0 then if I.Node = 0 then
......
gcc/ada/a-cfdlli.ads
...@@ -34,6 +34,7 @@ with Ada.Containers.Functional_Maps; ...@@ -34,6 +34,7 @@ with Ada.Containers.Functional_Maps;
generic generic
type Element_Type is private; type Element_Type is private;
package Ada.Containers.Formal_Doubly_Linked_Lists with package Ada.Containers.Formal_Doubly_Linked_Lists with
SPARK_Mode SPARK_Mode
is is
...@@ -67,17 +68,25 @@ is ...@@ -67,17 +68,25 @@ is
package M is new Ada.Containers.Functional_Vectors package M is new Ada.Containers.Functional_Vectors
(Index_Type => Positive_Count_Type, (Index_Type => Positive_Count_Type,
Element_Type => Element_Type); Element_Type => Element_Type);
function "=" (Left, Right : M.Sequence) return Boolean renames M."=";
function "<" (Left, Right : M.Sequence) return Boolean renames M."<"; function "="
function "<=" (Left, Right : M.Sequence) return Boolean renames M."<="; (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_Shuffle function M_Elements_Shuffle
(Left : M.Sequence; (Left : M.Sequence;
Right : M.Sequence; Right : M.Sequence;
Fst : Positive_Count_Type; Fst : Positive_Count_Type;
Lst : Count_Type; Lst : Count_Type;
Offset : Count_Type'Base) Offset : Count_Type'Base) return Boolean
return Boolean
-- The slice from Fst to Lst in Left contains the same elements than the -- The slice from Fst to Lst in Left contains the same elements than the
-- same slide shifted by Offset in Right -- same slide shifted by Offset in Right
with with
...@@ -87,33 +96,33 @@ is ...@@ -87,33 +96,33 @@ is
and Offset in 1 - Fst .. M.Length (Right) - Lst, and Offset in 1 - Fst .. M.Length (Right) - Lst,
Post => Post =>
M_Elements_Shuffle'Result = M_Elements_Shuffle'Result =
(for all J in Fst + Offset .. Lst + Offset => (for all J in Fst + Offset .. Lst + Offset =>
(for some I in Fst .. Lst => (for some I in Fst .. 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_Shuffle);
function M_Elements_Reversed (Left, Right : M.Sequence) return Boolean function M_Elements_Reversed
(Left : M.Sequence;
Right : M.Sequence) return Boolean
-- Right is Left in reverse order -- Right is Left in reverse order
with with
Global => null, Global => null,
Post => Post =>
M_Elements_Reversed'Result = M_Elements_Reversed'Result =
(M.Length (Left) = M.Length (Right) (M.Length (Left) = M.Length (Right)
and and (for all I in 1 .. M.Length (Left) =>
(for all I in 1 .. M.Length (Left) => Element (Left, I) =
Element (Left, I) Element (Right, M.Length (Left) - I + 1))
= Element (Right, M.Length (Left) - I + 1)) and (for all I in 1 .. M.Length (Left) =>
and Element (Right, I) =
(for all I in 1 .. M.Length (Left) => 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); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed);
function M_Elements_Swapped function M_Elements_Swapped
(Left : M.Sequence; (Left : M.Sequence;
Right : M.Sequence; Right : M.Sequence;
X, Y : Positive_Count_Type) X : Positive_Count_Type;
return Boolean Y : Positive_Count_Type) return Boolean
-- Elements stored at X and Y are reversed in Left and Right -- Elements stored at X and Y are reversed in Left and Right
with with
Global => null, Global => null,
...@@ -121,17 +130,23 @@ is ...@@ -121,17 +130,23 @@ is
Post => Post =>
M_Elements_Swapped'Result = M_Elements_Swapped'Result =
(M.Length (Left) = M.Length (Right) (M.Length (Left) = M.Length (Right)
and Element (Left, X) = Element (Right, Y) and Element (Left, X) = Element (Right, Y)
and Element (Left, Y) = Element (Right, X) and Element (Left, Y) = Element (Right, X)
and M.Equal_Except (Left, Right, X, Y)); and M.Equal_Except (Left, Right, X, Y));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped);
package P is new Ada.Containers.Functional_Maps package P is new Ada.Containers.Functional_Maps
(Key_Type => Cursor, (Key_Type => Cursor,
Element_Type => Positive_Count_Type, Element_Type => Positive_Count_Type,
Equivalent_Keys => "="); Equivalent_Keys => "=");
function "=" (Left, Right : P.Map) return Boolean renames P."=";
function "<=" (Left, Right : P.Map) return Boolean renames P."<="; function "="
(Left : P.Map;
Right : P.Map) return Boolean renames P."=";
function "<="
(Left : P.Map;
Right : P.Map) return Boolean renames P."<=";
function P_Positions_Shifted function P_Positions_Shifted
(Small : P.Map; (Small : P.Map;
...@@ -143,27 +158,31 @@ is ...@@ -143,27 +158,31 @@ is
Post => Post =>
P_Positions_Shifted'Result = P_Positions_Shifted'Result =
-- Big contains all cursors of Small -- Big contains all cursors of Small
(P.Keys_Included (Small, Big)
-- Cursors located before Cut are not moved, cursors located after P.Keys_Included (Small, Big)
-- are shifted by Count.
and
(for all I of Small =>
(if P.Get (Small, I) < Cut
then P.Get (Big, I) = P.Get (Small, I)
else P.Get (Big, I) - Count = P.Get (Small, I)))
-- New cursors of Big (if any) are between Cut and Cut - 1 + Count -- Cursors located before Cut are not moved, cursors located
and -- after are shifted by Count.
(for all I of Big =>
P.Has_Key (Small, I) and (for all I of Small =>
or P.Get (Big, I) - Count in Cut - Count .. Cut - 1)); (if P.Get (Small, I) < Cut then
P.Get (Big, I) = P.Get (Small, I)
else
P.Get (Big, I) - Count = P.Get (Small, I)))
-- New cursors of Big (if any) are between Cut and Cut - 1 +
-- Count.
and (for all I of Big =>
P.Has_Key (Small, I)
or P.Get (Big, I) - Count in Cut - Count .. Cut - 1);
function P_Positions_Swapped function P_Positions_Swapped
(Left : P.Map; (Left : P.Map;
Right : P.Map; Right : P.Map;
X, Y : Cursor) return Boolean X : Cursor;
Y : Cursor) return Boolean
-- Left and Right contain the same cursors, but the positions of X and Y -- Left and Right contain the same cursors, but the positions of X and Y
-- are reversed. -- are reversed.
with with
...@@ -171,11 +190,12 @@ is ...@@ -171,11 +190,12 @@ is
Global => null, Global => null,
Post => Post =>
P_Positions_Swapped'Result = P_Positions_Swapped'Result =
(P.Same_Keys (Left, Right) (P.Same_Keys (Left, Right)
and P.Elements_Equal_Except (Left, Right, X, Y) and P.Elements_Equal_Except (Left, Right, X, Y)
and P.Has_Key (Left, X) and P.Has_Key (Left, Y) and P.Has_Key (Left, X)
and P.Get (Left, X) = P.Get (Right, Y) and P.Has_Key (Left, Y)
and P.Get (Left, Y) = P.Get (Right, X)); and P.Get (Left, X) = P.Get (Right, Y)
and P.Get (Left, Y) = P.Get (Right, X));
function P_Positions_Truncated function P_Positions_Truncated
(Small : P.Map; (Small : P.Map;
...@@ -188,14 +208,16 @@ is ...@@ -188,14 +208,16 @@ is
Post => Post =>
P_Positions_Truncated'Result = P_Positions_Truncated'Result =
-- Big contains all cursors of Small at the same position -- Big contains all cursors of Small at the same position
(Small <= Big
(Small <= Big
-- New cursors of Big (if any) are between Cut and Cut - 1 + Count -- New cursors of Big (if any) are between Cut and Cut - 1 +
and -- Count.
(for all I of Big =>
P.Has_Key (Small, I) and (for all I of Big =>
or P.Get (Big, I) - Count in Cut - Count .. Cut - 1)); P.Has_Key (Small, I)
or P.Get (Big, I) - Count in Cut - Count .. Cut - 1));
function Mapping_Preserved function Mapping_Preserved
(M_Left : M.Sequence; (M_Left : M.Sequence;
...@@ -206,16 +228,18 @@ is ...@@ -206,16 +228,18 @@ is
Ghost, Ghost,
Global => null, Global => null,
Post => Post =>
(if Mapping_Preserved'Result then (if Mapping_Preserved'Result then
-- Left and Right contain the same cursors -- Left and Right contain the same cursors
P.Same_Keys (P_Left, P_Right) P.Same_Keys (P_Left, P_Right)
-- Mappings from cursors to elements induced by M_Left, P_Left -- Mappings from cursors to elements induced by M_Left, P_Left
-- and M_Right, P_Right are the same. -- and M_Right, P_Right are the same.
and (for all C of P_Left =>
M.Get (M_Left, P.Get (P_Left, C)) and (for all C of P_Left =>
= M.Get (M_Right, P.Get (P_Right, C)))); M.Get (M_Left, P.Get (P_Left, 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 highlevel model of a list is a sequence of elements. Cursors are
...@@ -232,19 +256,23 @@ is ...@@ -232,19 +256,23 @@ is
Ghost, Ghost,
Global => null, Global => null,
Post => not P.Has_Key (Positions'Result, No_Element) Post =>
-- Positions of cursors are smaller than the container's length. not P.Has_Key (Positions'Result, No_Element)
and then
(for all I of Positions'Result => -- Positions of cursors are smaller than the container's length.
P.Get (Positions'Result, I) in 1 .. Length (Container)
and then
-- No two cursors have the same position. Note that we do not (for all I of Positions'Result =>
-- state that there is a cursor in the map for each position, P.Get (Positions'Result, I) in 1 .. Length (Container)
-- as it is rarely needed.
and then -- No two cursors have the same position. Note that we do not
(for all J of Positions'Result => -- state that there is a cursor in the map for each position, as
-- it is rarely needed.
and then
(for all J of Positions'Result =>
(if P.Get (Positions'Result, I) = P.Get (Positions'Result, J) (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
then I = J))); then I = J)));
procedure Lift_Abstraction_Level (Container : List) with procedure Lift_Abstraction_Level (Container : List) with
-- Lift_Abstraction_Level is a ghost procedure that does nothing but -- Lift_Abstraction_Level is a ghost procedure that does nothing but
...@@ -257,15 +285,17 @@ is ...@@ -257,15 +285,17 @@ is
Ghost, Ghost,
Global => null, Global => null,
Post => Post =>
(for all Elt of Model (Container) => (for all Elt of Model (Container) =>
(for some I of Positions (Container) => (for some I of Positions (Container) =>
M.Get (Model (Container), P.Get (Positions (Container), I)) M.Get (Model (Container), P.Get (Positions (Container), I)) =
= Elt)); Elt));
function Element (S : M.Sequence; I : Count_Type) return Element_Type function Element
renames M.Get; (S : M.Sequence;
I : Count_Type) return Element_Type renames M.Get;
-- To improve readability of contracts, we rename the function used to -- To improve readability of contracts, we rename the function used to
-- access an element in the model to Element. -- access an element in the model to Element.
end Formal_Model; end Formal_Model;
use Formal_Model; use Formal_Model;
...@@ -289,10 +319,13 @@ is ...@@ -289,10 +319,13 @@ is
function Copy (Source : List; Capacity : Count_Type := 0) return List with function Copy (Source : List; Capacity : Count_Type := 0) return List with
Global => null, Global => null,
Pre => Capacity = 0 or else Capacity >= Source.Capacity, Pre => Capacity = 0 or else Capacity >= Source.Capacity,
Post => Model (Copy'Result) = Model (Source) Post =>
and Positions (Copy'Result) = Positions (Source) Model (Copy'Result) = Model (Source)
and (if Capacity = 0 then Copy'Result.Capacity = Source.Capacity and Positions (Copy'Result) = Positions (Source)
else Copy'Result.Capacity = Capacity); and (if Capacity = 0 then
Copy'Result.Capacity = Source.Capacity
else
Copy'Result.Capacity = Capacity);
function Element function Element
(Container : List; (Container : List;
...@@ -302,8 +335,7 @@ is ...@@ -302,8 +335,7 @@ is
Pre => Has_Element (Container, Position), Pre => Has_Element (Container, Position),
Post => Post =>
Element'Result = Element'Result =
Element (Model (Container), Element (Model (Container), P.Get (Positions (Container), Position));
P.Get (Positions (Container), Position));
pragma Annotate (GNATprove, Inline_For_Proof, Element); pragma Annotate (GNATprove, Inline_For_Proof, Element);
procedure Replace_Element procedure Replace_Element
...@@ -313,25 +345,30 @@ is ...@@ -313,25 +345,30 @@ is
with with
Global => null, Global => null,
Pre => Has_Element (Container, Position), Pre => Has_Element (Container, Position),
Post => Length (Container) = Length (Container)'Old Post =>
Length (Container) = Length (Container)'Old
-- Cursors are preserved
-- Cursors are preserved. and Positions (Container)'Old = Positions (Container)
and Positions (Container)'Old = Positions (Container)
-- The element at the position of Position in Container is New_Item -- The element at the position of Position in Container is New_Item
and Element (Model (Container), P.Get (Positions (Container), Position))
= New_Item
-- Other elements are preserved and Element
and M.Equal_Except (Model (Container)'Old, (Model (Container),
Model (Container), P.Get (Positions (Container), Position)) = New_Item
P.Get (Positions (Container), Position));
-- Other elements are preserved
and M.Equal_Except
(Model (Container)'Old,
Model (Container),
P.Get (Positions (Container), Position));
procedure Move (Target : in out List; Source : in out List) with procedure Move (Target : in out List; Source : in out List) with
Global => null, Global => null,
Pre => Target.Capacity >= Length (Source), Pre => Target.Capacity >= Length (Source),
Post => Model (Target) = Model (Source'Old) Post => Model (Target) = Model (Source'Old) and Length (Source) = 0;
and Length (Source) = 0;
procedure Insert procedure Insert
(Container : in out List; (Container : in out List;
...@@ -340,59 +377,69 @@ is ...@@ -340,59 +377,69 @@ is
with with
Global => null, Global => null,
Pre => Pre =>
Length (Container) < Container.Capacity Length (Container) < Container.Capacity
and then (Has_Element (Container, Before) and then (Has_Element (Container, Before)
or else Before = No_Element), or else Before = No_Element),
Post => Length (Container) = Length (Container)'Old + 1, Post => Length (Container) = Length (Container)'Old + 1,
Contract_Cases => Contract_Cases =>
(Before = No_Element => (Before = No_Element =>
-- Positions contains a new mapping from the last cursor of -- Positions contains a new mapping from the last cursor of
-- Container to its length. -- Container to its length.
P.Get (Positions (Container), Last (Container)) = Length (Container) P.Get (Positions (Container), Last (Container)) = Length (Container)
-- Other cursors come from Container'Old -- Other cursors come from Container'Old
and P.Keys_Included_Except
(Left => Positions (Container), and P.Keys_Included_Except
Right => Positions (Container)'Old, (Left => Positions (Container),
New_Key => Last (Container)) Right => Positions (Container)'Old,
New_Key => Last (Container))
-- Cursors of Container'Old keep the same position -- Cursors of Container'Old keep the same position
and Positions (Container)'Old <= Positions (Container)
-- Model contains a new element New_Item at the end and Positions (Container)'Old <= Positions (Container)
and Element (Model (Container), Length (Container)) = New_Item
-- Elements of Container'Old are preserved -- Model contains a new element New_Item at the end
and Model (Container)'Old <= Model (Container),
others => and Element (Model (Container), Length (Container)) = New_Item
-- Elements of Container'Old are preserved
and Model (Container)'Old <= Model (Container),
others =>
-- The elements of Container located before Before are preserved
-- The elements of Container located before Before are preserved.
M.Range_Equal M.Range_Equal
(Left => Model (Container)'Old, (Left => Model (Container)'Old,
Right => Model (Container), Right => Model (Container),
Fst => 1, Fst => 1,
Lst => P.Get (Positions (Container)'Old, Before) - 1) Lst => P.Get (Positions (Container)'Old, Before) - 1)
-- Other elements are shifted by 1. -- Other elements are shifted by 1
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => P.Get (Positions (Container)'Old, Before),
Lst => Length (Container)'Old,
Offset => 1)
-- New_Item is stored at the previous position of Before in
-- Container
and Element
(Model (Container), P.Get (Positions (Container)'Old, Before))
= New_Item
-- A new cursor has been inserted at position Before in Container and M.Range_Shifted
and P_Positions_Shifted (Left => Model (Container)'Old,
(Positions (Container)'Old, Right => Model (Container),
Positions (Container), Fst => P.Get (Positions (Container)'Old, Before),
Cut => P.Get (Positions (Container)'Old, Before))); Lst => Length (Container)'Old,
Offset => 1)
-- New_Item is stored at the previous position of Before in
-- Container.
and Element
(Model (Container),
P.Get (Positions (Container)'Old, Before)) = New_Item
-- A new cursor has been inserted at position Before in Container
and P_Positions_Shifted
(Positions (Container)'Old,
Positions (Container),
Cut => P.Get (Positions (Container)'Old, Before)));
procedure Insert procedure Insert
(Container : in out List; (Container : in out List;
...@@ -400,66 +447,75 @@ is ...@@ -400,66 +447,75 @@ is
New_Item : Element_Type; New_Item : Element_Type;
Count : Count_Type) Count : Count_Type)
with with
Global => null, Global => null,
Pre => Pre =>
Length (Container) <= Container.Capacity - Count Length (Container) <= Container.Capacity - Count
and then (Has_Element (Container, Before) and then (Has_Element (Container, Before)
or else Before = No_Element), or else Before = No_Element),
Post => Length (Container) = Length (Container)'Old + Count, Post => Length (Container) = Length (Container)'Old + Count,
Contract_Cases => Contract_Cases =>
(Before = No_Element => (Before = No_Element =>
-- The elements of Container are preserved -- The elements of Container are preserved
M.Range_Equal M.Range_Equal
(Left => Model (Container)'Old, (Left => Model (Container)'Old,
Right => Model (Container), Right => Model (Container),
Fst => 1, Fst => 1,
Lst => Length (Container)'Old) Lst => Length (Container)'Old)
-- Container contains Count times New_Item at the end -- Container contains Count times New_Item at the end
and M.Constant_Range
(Container => Model (Container), and 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)
-- A Count cursors have been inserted at the end of Container
and P_Positions_Truncated -- A Count cursors have been inserted at the end of Container
(Positions (Container)'Old,
Positions (Container), and P_Positions_Truncated
Cut => Length (Container)'Old + 1, (Positions (Container)'Old,
Count => Count), Positions (Container),
others => Cut => Length (Container)'Old + 1,
Count => Count),
others =>
-- The elements of Container located before Before are preserved -- The elements of Container located before Before are preserved
M.Range_Equal M.Range_Equal
(Left => Model (Container)'Old, (Left => Model (Container)'Old,
Right => Model (Container), Right => Model (Container),
Fst => 1, Fst => 1,
Lst => P.Get (Positions (Container)'Old, Before) - 1) Lst => P.Get (Positions (Container)'Old, Before) - 1)
-- Other elements are shifted by Count. -- Other elements are shifted by Count
and M.Range_Shifted
(Left => Model (Container)'Old, and M.Range_Shifted
Right => Model (Container), (Left => Model (Container)'Old,
Fst => P.Get (Positions (Container)'Old, Before), Right => Model (Container),
Lst => Length (Container)'Old, Fst => P.Get (Positions (Container)'Old, Before),
Offset => Count) Lst => Length (Container)'Old,
Offset => Count)
-- Container contains Count times New_Item after position Before
and M.Constant_Range -- Container contains Count times New_Item after position Before
(Container => Model (Container),
Fst => P.Get (Positions (Container)'Old, Before), and M.Constant_Range
Lst => (Container => Model (Container),
P.Get (Positions (Container)'Old, Before) - 1 + Count, Fst => P.Get (Positions (Container)'Old, Before),
Item => New_Item) Lst =>
P.Get (Positions (Container)'Old, Before) - 1 + Count,
-- Count cursors have been inserted at position Before in Container Item => New_Item)
and P_Positions_Shifted
(Positions (Container)'Old, -- Count cursors have been inserted at position Before in
Positions (Container), -- Container.
Cut => P.Get (Positions (Container)'Old, Before),
Count => Count)); and P_Positions_Shifted
(Positions (Container)'Old,
Positions (Container),
Cut => P.Get (Positions (Container)'Old, Before),
Count => Count));
procedure Insert procedure Insert
(Container : in out List; (Container : in out List;
...@@ -469,47 +525,52 @@ is ...@@ -469,47 +525,52 @@ is
with with
Global => null, Global => null,
Pre => Pre =>
Length (Container) < Container.Capacity Length (Container) < Container.Capacity
and then (Has_Element (Container, Before) and then (Has_Element (Container, Before)
or else Before = No_Element), or else Before = No_Element),
Post => Post =>
Length (Container) = Length (Container)'Old + 1 Length (Container) = Length (Container)'Old + 1
-- Positions is valid in Container and it is located either before -- Positions is valid in Container and it is located either before
-- Before if it is valid in Container or at the end if it is -- Before if it is valid in Container or at the end if it is
-- No_Element. -- No_Element.
and P.Has_Key (Positions (Container), Position) and P.Has_Key (Positions (Container), Position)
and (if Before = No_Element and (if Before = No_Element then
then P.Get (Positions (Container), Position) P.Get (Positions (Container), Position) = Length (Container)
= Length (Container) else
else P.Get (Positions (Container), Position) P.Get (Positions (Container), Position) =
= P.Get (Positions (Container)'Old, Before)) P.Get (Positions (Container)'Old, Before))
-- The elements of Container located before Position are preserved
-- The elements of Container located before Position are preserved.
and M.Range_Equal and M.Range_Equal
(Left => Model (Container)'Old, (Left => Model (Container)'Old,
Right => Model (Container), Right => Model (Container),
Fst => 1, Fst => 1,
Lst => P.Get (Positions (Container), Position) - 1) Lst => P.Get (Positions (Container), Position) - 1)
-- Other elements are shifted by 1
-- Other elements are shifted by 1.
and M.Range_Shifted and M.Range_Shifted
(Left => Model (Container)'Old, (Left => Model (Container)'Old,
Right => Model (Container), Right => Model (Container),
Fst => P.Get (Positions (Container), Position), Fst => P.Get (Positions (Container), Position),
Lst => Length (Container)'Old, Lst => Length (Container)'Old,
Offset => 1) Offset => 1)
-- New_Item is stored at Position in Container -- New_Item is stored at Position in Container
and Element and Element
(Model (Container), P.Get (Positions (Container), Position)) (Model (Container),
= New_Item P.Get (Positions (Container), Position)) = New_Item
-- A new cursor has been inserted at position Position in Container -- A new cursor has been inserted at position Position in Container
and P_Positions_Shifted and P_Positions_Shifted
(Positions (Container)'Old, (Positions (Container)'Old,
Positions (Container), Positions (Container),
Cut => P.Get (Positions (Container), Position)); Cut => P.Get (Positions (Container), Position));
procedure Insert procedure Insert
(Container : in out List; (Container : in out List;
...@@ -520,80 +581,89 @@ is ...@@ -520,80 +581,89 @@ is
with with
Global => null, Global => null,
Pre => Pre =>
Length (Container) <= Container.Capacity - Count Length (Container) <= Container.Capacity - Count
and then (Has_Element (Container, Before) and then (Has_Element (Container, Before)
or else Before = No_Element), or else Before = No_Element),
Post => Length (Container) = Length (Container)'Old + Count, Post => Length (Container) = Length (Container)'Old + Count,
Contract_Cases => Contract_Cases =>
(Count = 0 => Position = Before (Count = 0 =>
and Model (Container) = Model (Container)'Old Position = Before
and Positions (Container) = Positions (Container)'Old, and Model (Container) = Model (Container)'Old
and Positions (Container) = Positions (Container)'Old,
others =>
others =>
-- Positions is valid in Container and it is located either before -- Positions is valid in Container and it is located either before
-- Before if it is valid in Container or at the end if it is -- Before if it is valid in Container or at the end if it is
-- No_Element. -- No_Element.
P.Has_Key (Positions (Container), Position)
and (if Before = No_Element
then P.Get (Positions (Container), Position)
= Length (Container)'Old + 1
else P.Get (Positions (Container), Position)
= P.Get (Positions (Container)'Old, Before))
-- The elements of Container located before Position are preserved.
and M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => 1,
Lst => P.Get (Positions (Container), Position) - 1)
-- Other elements are shifted by Count.
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => P.Get (Positions (Container), Position),
Lst => Length (Container)'Old,
Offset => Count)
-- Container contains Count times New_Item after position Position
and M.Constant_Range
(Container => Model (Container),
Fst => P.Get (Positions (Container), Position),
Lst => P.Get (Positions (Container), Position) - 1 + Count,
Item => New_Item)
-- Count cursor have been inserted at Position in Container
and P_Positions_Shifted
(Positions (Container)'Old,
Positions (Container),
Cut => P.Get (Positions (Container), Position),
Count => Count));
procedure Prepend P.Has_Key (Positions (Container), Position)
(Container : in out List; and (if Before = No_Element then
New_Item : Element_Type) P.Get (Positions (Container), Position) =
with Length (Container)'Old + 1
else
P.Get (Positions (Container), Position) =
P.Get (Positions (Container)'Old, Before))
-- The elements of Container located before Position are preserved
and M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => 1,
Lst => P.Get (Positions (Container), Position) - 1)
-- Other elements are shifted by Count
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => P.Get (Positions (Container), Position),
Lst => Length (Container)'Old,
Offset => Count)
-- Container contains Count times New_Item after position Position
and M.Constant_Range
(Container => Model (Container),
Fst => P.Get (Positions (Container), Position),
Lst =>
P.Get (Positions (Container), Position) - 1 + Count,
Item => New_Item)
-- Count cursor have been inserted at Position in Container
and P_Positions_Shifted
(Positions (Container)'Old,
Positions (Container),
Cut => P.Get (Positions (Container), Position),
Count => Count));
procedure Prepend (Container : in out List; New_Item : Element_Type) with
Global => null, Global => null,
Pre => Length (Container) < Container.Capacity, Pre => Length (Container) < Container.Capacity,
Post => Post =>
Length (Container) = Length (Container)'Old + 1 Length (Container) = Length (Container)'Old + 1
-- Elements are shifted by 1 -- Elements are shifted by 1
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => 1,
Lst => Length (Container)'Old,
Offset => 1)
-- New_Item is the first element of Container and M.Range_Shifted
and Element (Model (Container), 1) = New_Item (Left => Model (Container)'Old,
Right => Model (Container),
Fst => 1,
Lst => Length (Container)'Old,
Offset => 1)
-- A new cursor has been inserted at the beginning of Container -- New_Item is the first element of Container
and P_Positions_Shifted
(Positions (Container)'Old, and Element (Model (Container), 1) = New_Item
Positions (Container),
Cut => 1); -- A new cursor has been inserted at the beginning of Container
and P_Positions_Shifted
(Positions (Container)'Old,
Positions (Container),
Cut => 1);
procedure Prepend procedure Prepend
(Container : in out List; (Container : in out List;
...@@ -605,55 +675,61 @@ is ...@@ -605,55 +675,61 @@ is
Post => Post =>
Length (Container) = Length (Container)'Old + Count Length (Container) = Length (Container)'Old + Count
-- Elements are shifted by Count. -- Elements are shifted by Count
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => 1,
Lst => Length (Container)'Old,
Offset => Count)
-- Container starts with Count times New_Item
and M.Constant_Range
(Container => Model (Container),
Fst => 1,
Lst => Count,
Item => New_Item)
-- Count cursors have been inserted at the beginning of Container
and P_Positions_Shifted
(Positions (Container)'Old,
Positions (Container),
Cut => 1,
Count => Count);
procedure Append and M.Range_Shifted
(Container : in out List; (Left => Model (Container)'Old,
New_Item : Element_Type) Right => Model (Container),
with Fst => 1,
Lst => Length (Container)'Old,
Offset => Count)
-- Container starts with Count times New_Item
and M.Constant_Range
(Container => Model (Container),
Fst => 1,
Lst => Count,
Item => New_Item)
-- Count cursors have been inserted at the beginning of Container
and P_Positions_Shifted
(Positions (Container)'Old,
Positions (Container),
Cut => 1,
Count => Count);
procedure Append (Container : in out List; New_Item : Element_Type) with
Global => null, Global => null,
Pre => Length (Container) < Container.Capacity, Pre => Length (Container) < Container.Capacity,
Post => Length (Container) = Length (Container)'Old + 1 Post =>
Length (Container) = Length (Container)'Old + 1
-- Positions contains a new mapping from the last cursor of -- Positions contains a new mapping from the last cursor of Container
-- Container to its length. -- to its length.
and P.Get (Positions (Container), Last (Container))
= Length (Container)
-- Other cursors come from Container'Old and P.Get (Positions (Container), Last (Container)) =
and P.Keys_Included_Except Length (Container)
(Left => Positions (Container),
Right => Positions (Container)'Old,
New_Key => Last (Container))
-- Cursors of Container'Old keep the same position -- Other cursors come from Container'Old
and Positions (Container)'Old <= Positions (Container)
-- Model contains a new element New_Item at the end and P.Keys_Included_Except
and Element (Model (Container), Length (Container)) = New_Item (Left => Positions (Container),
Right => Positions (Container)'Old,
New_Key => Last (Container))
-- Elements of Container'Old are preserved -- Cursors of Container'Old keep the same position
and Model (Container)'Old <= Model (Container);
and Positions (Container)'Old <= Positions (Container)
-- Model contains a new element New_Item at the end
and Element (Model (Container), Length (Container)) = New_Item
-- Elements of Container'Old are preserved
and Model (Container)'Old <= Model (Container);
procedure Append procedure Append
(Container : in out List; (Container : in out List;
...@@ -665,55 +741,59 @@ is ...@@ -665,55 +741,59 @@ is
Post => Post =>
Length (Container) = Length (Container)'Old + Count Length (Container) = Length (Container)'Old + Count
-- The elements of Container are preserved -- The elements of Container are preserved
and Model (Container)'Old <= Model (Container)
-- Container contains Count times New_Item at the end
and M.Constant_Range
(Container => Model (Container),
Fst => Length (Container)'Old + 1,
Lst => Length (Container),
Item => New_Item)
-- Count cursors have been inserted at the end of Container
and P_Positions_Truncated
(Positions (Container)'Old,
Positions (Container),
Cut => Length (Container)'Old + 1,
Count => Count);
procedure Delete and Model (Container)'Old <= Model (Container)
(Container : in out List;
Position : in out Cursor) -- Container contains Count times New_Item at the end
with
and 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
and P_Positions_Truncated
(Positions (Container)'Old,
Positions (Container),
Cut => Length (Container)'Old + 1,
Count => Count);
procedure Delete (Container : in out List; Position : in out Cursor) with
Global => null, Global => null,
Pre => Has_Element (Container, Position), Pre => Has_Element (Container, Position),
Post => Post =>
Length (Container) = Length (Container)'Old - 1 Length (Container) = Length (Container)'Old - 1
-- Position is set to No_Element -- Position is set to No_Element
and Position = No_Element
-- The elements of Container located before Position are preserved. and Position = No_Element
and M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => 1,
Lst => P.Get (Positions (Container)'Old, Position'Old) - 1)
-- The elements located after Position are shifted by 1 -- The elements of Container located before Position are preserved.
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => P.Get (Positions (Container)'Old, Position'Old) + 1,
Lst => Length (Container)'Old,
Offset => -1)
-- Position has been removed from Container and M.Range_Equal
and P_Positions_Shifted (Left => Model (Container)'Old,
(Positions (Container), Right => Model (Container),
Positions (Container)'Old, Fst => 1,
Cut => P.Get (Positions (Container)'Old, Position'Old)); Lst => P.Get (Positions (Container)'Old, Position'Old) - 1)
-- The elements located after Position are shifted by 1
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => P.Get (Positions (Container)'Old, Position'Old) + 1,
Lst => Length (Container)'Old,
Offset => -1)
-- Position has been removed from Container
and P_Positions_Shifted
(Positions (Container),
Positions (Container)'Old,
Cut => P.Get (Positions (Container)'Old, Position'Old));
procedure Delete procedure Delete
(Container : in out List; (Container : in out List;
...@@ -723,144 +803,157 @@ is ...@@ -723,144 +803,157 @@ is
Global => null, Global => null,
Pre => Has_Element (Container, Position), Pre => Has_Element (Container, Position),
Post => Post =>
Length (Container) in Length (Container)'Old - Count Length (Container) in
.. Length (Container)'Old Length (Container)'Old - Count .. Length (Container)'Old
-- Position is set to No_Element -- Position is set to No_Element
and Position = No_Element
and Position = No_Element
-- The elements of Container located before Position are preserved.
and M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => 1,
Lst => P.Get (Positions (Container)'Old, Position'Old) - 1),
-- The elements of Container located before Position are preserved.
and M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => 1,
Lst => P.Get (Positions (Container)'Old, Position'Old) - 1),
Contract_Cases => Contract_Cases =>
-- All the elements after Position have been erased -- All the elements after Position have been erased
(Length (Container) - Count < P.Get (Positions (Container), Position)
=>
(Length (Container) - Count < P.Get (Positions (Container), Position) =>
Length (Container) = Length (Container) =
P.Get (Positions (Container)'Old, Position'Old) - 1 P.Get (Positions (Container)'Old, Position'Old) - 1
-- At most Count cursors have been removed at the end of Container -- At most Count cursors have been removed at the end of Container
and P_Positions_Truncated
(Positions (Container), and P_Positions_Truncated
Positions (Container)'Old, (Positions (Container),
Cut => P.Get (Positions (Container)'Old, Position'Old), Positions (Container)'Old,
Count => Count), Cut => P.Get (Positions (Container)'Old, Position'Old),
Count => Count),
others => others =>
Length (Container) = Length (Container)'Old - Count Length (Container) = Length (Container)'Old - Count
-- Other elements are shifted by Count -- Other elements are shifted by Count
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst =>
P.Get (Positions (Container)'Old, Position'Old) + Count,
Lst => Length (Container)'Old,
Offset => -Count)
-- Count cursors have been removed from Container at Position
and P_Positions_Shifted
(Positions (Container),
Positions (Container)'Old,
Cut => P.Get (Positions (Container)'Old, Position'Old),
Count => Count));
procedure Delete_First (Container : in out List) and M.Range_Shifted
with (Left => Model (Container)'Old,
Right => Model (Container),
Fst =>
P.Get (Positions (Container)'Old, Position'Old) + Count,
Lst => Length (Container)'Old,
Offset => -Count)
-- Count cursors have been removed from Container at Position
and P_Positions_Shifted
(Positions (Container),
Positions (Container)'Old,
Cut => P.Get (Positions (Container)'Old, Position'Old),
Count => Count));
procedure Delete_First (Container : in out List) with
Global => null, Global => null,
Pre => not Is_Empty (Container), Pre => not Is_Empty (Container),
Post => Post =>
Length (Container) = Length (Container)'Old - 1 Length (Container) = Length (Container)'Old - 1
-- The elements of Container are shifted by 1 -- The elements of Container are shifted by 1
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => 2,
Lst => Length (Container)'Old,
Offset => -1)
-- The first cursor of Container has been removed and M.Range_Shifted
and P_Positions_Shifted (Left => Model (Container)'Old,
(Positions (Container), Right => Model (Container),
Positions (Container)'Old, Fst => 2,
Cut => 1); Lst => Length (Container)'Old,
Offset => -1)
procedure Delete_First -- The first cursor of Container has been removed
(Container : in out List;
Count : Count_Type) and P_Positions_Shifted
with (Positions (Container),
Positions (Container)'Old,
Cut => 1);
procedure Delete_First (Container : in out List; Count : Count_Type) with
Global => null, Global => null,
Contract_Cases => Contract_Cases =>
-- All the elements of Container have been erased -- All the elements of Container have been erased
(Length (Container) <= Count => Length (Container) = 0,
(Length (Container) <= Count =>
Length (Container) = 0,
others => others =>
Length (Container) = Length (Container)'Old - Count Length (Container) = Length (Container)'Old - Count
-- Elements of Container are shifted by Count -- Elements of Container are shifted by Count
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Count + 1,
Lst => Length (Container)'Old,
Offset => -Count)
-- The first Count cursors have been removed from Container and M.Range_Shifted
and P_Positions_Shifted (Left => Model (Container)'Old,
(Positions (Container), Right => Model (Container),
Positions (Container)'Old, Fst => Count + 1,
Cut => 1, Lst => Length (Container)'Old,
Count => Count)); Offset => -Count)
procedure Delete_Last (Container : in out List) -- The first Count cursors have been removed from Container
with
and P_Positions_Shifted
(Positions (Container),
Positions (Container)'Old,
Cut => 1,
Count => Count));
procedure Delete_Last (Container : in out List) with
Global => null, Global => null,
Pre => not Is_Empty (Container), Pre => not Is_Empty (Container),
Post => Post =>
Length (Container) = Length (Container)'Old - 1 Length (Container) = Length (Container)'Old - 1
-- The elements of Container are preserved. -- The elements of Container are preserved
and Model (Container) <= Model (Container)'Old
-- The last cursor of Container has been removed and Model (Container) <= Model (Container)'Old
and not P.Has_Key (Positions (Container), Last (Container)'Old)
-- Other cursors are still valid -- The last cursor of Container has been removed
and P.Keys_Included_Except
(Left => Positions (Container)'Old,
Right => Positions (Container)'Old,
New_Key => Last (Container)'Old)
-- The positions of other cursors are preserved and not P.Has_Key (Positions (Container), Last (Container)'Old)
and Positions (Container) <= Positions (Container)'Old;
procedure Delete_Last -- Other cursors are still valid
(Container : in out List;
Count : Count_Type) and P.Keys_Included_Except
with (Left => Positions (Container)'Old,
Global => null, Right => Positions (Container)'Old,
New_Key => Last (Container)'Old)
-- The positions of other cursors are preserved
and Positions (Container) <= Positions (Container)'Old;
procedure Delete_Last (Container : in out List; Count : Count_Type) with
Global => null,
Contract_Cases => Contract_Cases =>
-- All the elements of Container have been erased -- All the elements of Container have been erased
(Length (Container) <= Count => Length (Container) = 0,
others =>
(Length (Container) <= Count =>
Length (Container) = 0,
others =>
Length (Container) = Length (Container)'Old - Count Length (Container) = Length (Container)'Old - Count
-- The elements of Container are preserved. -- The elements of Container are preserved
and Model (Container) <= Model (Container)'Old
and Model (Container) <= Model (Container)'Old
-- At most Count cursors have been removed at the end of Container -- At most Count cursors have been removed at the end of Container
and P_Positions_Truncated
(Positions (Container), and P_Positions_Truncated
Positions (Container)'Old, (Positions (Container),
Cut => Length (Container) + 1, Positions (Container)'Old,
Count => Count)); Cut => Length (Container) + 1,
Count => Count));
procedure Reverse_Elements (Container : in out List) with procedure Reverse_Elements (Container : in out List) with
Global => null, Global => null,
...@@ -868,7 +961,8 @@ is ...@@ -868,7 +961,8 @@ is
procedure Swap procedure Swap
(Container : in out List; (Container : in out List;
I, J : Cursor) I : Cursor;
J : Cursor)
with with
Global => null, Global => null,
Pre => Has_Element (Container, I) and then Has_Element (Container, J), Pre => Has_Element (Container, I) and then Has_Element (Container, J),
...@@ -877,11 +971,13 @@ is ...@@ -877,11 +971,13 @@ is
(Model (Container)'Old, Model (Container), (Model (Container)'Old, Model (Container),
X => P.Get (Positions (Container)'Old, I), X => P.Get (Positions (Container)'Old, I),
Y => P.Get (Positions (Container)'Old, J)) Y => P.Get (Positions (Container)'Old, J))
and Positions (Container) = Positions (Container)'Old;
and Positions (Container) = Positions (Container)'Old;
procedure Swap_Links procedure Swap_Links
(Container : in out List; (Container : in out List;
I, J : Cursor) I : Cursor;
J : Cursor)
with with
Global => null, Global => null,
Pre => Has_Element (Container, I) and then Has_Element (Container, J), Pre => Has_Element (Container, I) and then Has_Element (Container, J),
...@@ -890,8 +986,8 @@ is ...@@ -890,8 +986,8 @@ is
(Model (Container'Old), Model (Container), (Model (Container'Old), Model (Container),
X => P.Get (Positions (Container)'Old, I), X => P.Get (Positions (Container)'Old, I),
Y => P.Get (Positions (Container)'Old, J)) Y => P.Get (Positions (Container)'Old, J))
and P_Positions_Swapped and P_Positions_Swapped
(Positions (Container)'Old, Positions (Container), I, J); (Positions (Container)'Old, Positions (Container), I, J);
procedure Splice procedure Splice
(Target : in out List; (Target : in out List;
...@@ -901,69 +997,77 @@ is ...@@ -901,69 +997,77 @@ is
with with
Global => null, Global => null,
Pre => Pre =>
Length (Source) <= Target.Capacity - Length (Target) Length (Source) <= Target.Capacity - Length (Target)
and then (Has_Element (Target, Before) and then (Has_Element (Target, Before)
or else Before = No_Element), or else Before = No_Element),
Post => Post =>
Length (Source) = 0 Length (Source) = 0
and Length (Target) = Length (Target)'Old + Length (Source)'Old, and Length (Target) = Length (Target)'Old + Length (Source)'Old,
Contract_Cases => Contract_Cases =>
(Before = No_Element => (Before = No_Element =>
-- The elements of Target are preserved -- The elements of Target are preserved
M.Range_Equal M.Range_Equal
(Left => Model (Target)'Old, (Left => Model (Target)'Old,
Right => Model (Target), Right => Model (Target),
Fst => 1, Fst => 1,
Lst => Length (Target)'Old) Lst => Length (Target)'Old)
-- 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
(Left => Model (Source)'Old, and M_Elements_Shuffle
Right => Model (Target), (Left => Model (Source)'Old,
Fst => 1, Right => Model (Target),
Lst => Length (Source)'Old, Fst => 1,
Offset => Length (Target)'Old) Lst => Length (Source)'Old,
Offset => Length (Target)'Old)
-- Cursors have been inserted at the end of Target
and P_Positions_Truncated -- Cursors have been inserted at the end of Target
(Positions (Target)'Old,
Positions (Target), and P_Positions_Truncated
Cut => Length (Target)'Old + 1, (Positions (Target)'Old,
Count => Length (Source)'Old), Positions (Target),
others => Cut => Length (Target)'Old + 1,
Count => Length (Source)'Old),
others =>
-- The elements of Target located before Before are preserved -- The elements of Target located before Before are preserved
M.Range_Equal M.Range_Equal
(Left => Model (Target)'Old, (Left => Model (Target)'Old,
Right => Model (Target), Right => Model (Target),
Fst => 1, Fst => 1,
Lst => P.Get (Positions (Target)'Old, Before) - 1) Lst => P.Get (Positions (Target)'Old, Before) - 1)
-- 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_Shuffle
(Left => Model (Source)'Old, (Left => Model (Source)'Old,
Right => Model (Target), Right => Model (Target),
Fst => 1, Fst => 1,
Lst => Length (Source)'Old, Lst => Length (Source)'Old,
Offset => P.Get (Positions (Target)'Old, Before) - 1) Offset => P.Get (Positions (Target)'Old, Before) - 1)
-- Other elements are shifted by the length of Source -- Other elements are shifted by the length of Source
and M.Range_Shifted and M.Range_Shifted
(Left => Model (Target)'Old, (Left => Model (Target)'Old,
Right => Model (Target), Right => Model (Target),
Fst => P.Get (Positions (Target)'Old, Before), Fst => P.Get (Positions (Target)'Old, Before),
Lst => Length (Target)'Old, Lst => Length (Target)'Old,
Offset => Length (Source)'Old) Offset => Length (Source)'Old)
-- Cursors have been inserted at position Before in Target -- Cursors have been inserted at position Before in Target
and P_Positions_Shifted and P_Positions_Shifted
(Positions (Target)'Old, (Positions (Target)'Old,
Positions (Target), Positions (Target),
Cut => P.Get (Positions (Target)'Old, Before), Cut => P.Get (Positions (Target)'Old, Before),
Count => Length (Source)'Old)); Count => Length (Source)'Old));
procedure Splice procedure Splice
(Target : in out List; (Target : in out List;
...@@ -974,70 +1078,76 @@ is ...@@ -974,70 +1078,76 @@ is
with with
Global => null, Global => null,
Pre => Pre =>
(Has_Element (Target, Before) (Has_Element (Target, Before) or else Before = No_Element)
or else Before = No_Element) and then Has_Element (Source, Position)
and then Has_Element (Source, Position) and then Length (Target) < Target.Capacity,
and then Length (Target) < Target.Capacity,
Post => Post =>
Length (Target) = Length (Target)'Old + 1 Length (Target) = Length (Target)'Old + 1
and Length (Source) = Length (Source)'Old - 1 and Length (Source) = Length (Source)'Old - 1
-- The elements of Source located before Position are preserved. -- The elements of Source located before Position are preserved
and M.Range_Equal
(Left => Model (Source)'Old,
Right => Model (Source),
Fst => 1,
Lst => P.Get (Positions (Source)'Old, Position'Old) - 1)
-- The elements located after Position are shifted by 1 and M.Range_Equal
and M.Range_Shifted (Left => Model (Source)'Old,
(Left => Model (Source)'Old, Right => Model (Source),
Right => Model (Source), Fst => 1,
Fst => P.Get (Positions (Source)'Old, Position'Old) + 1, Lst => P.Get (Positions (Source)'Old, Position'Old) - 1)
Lst => Length (Source)'Old,
Offset => -1)
-- Position has been removed from Source -- The elements located after Position are shifted by 1
and P_Positions_Shifted
(Positions (Source),
Positions (Source)'Old,
Cut => P.Get (Positions (Source)'Old, Position'Old))
-- Positions is valid in Target and it is located either before and M.Range_Shifted
-- Before if it is valid in Target or at the end if it is (Left => Model (Source)'Old,
-- No_Element. Right => Model (Source),
and P.Has_Key (Positions (Target), Position) Fst => P.Get (Positions (Source)'Old, Position'Old) + 1,
and (if Before = No_Element Lst => Length (Source)'Old,
then P.Get (Positions (Target), Position) Offset => -1)
= Length (Target)
else P.Get (Positions (Target), Position)
= P.Get (Positions (Target)'Old, Before))
-- The elements of Target located before Position are preserved.
and M.Range_Equal
(Left => Model (Target)'Old,
Right => Model (Target),
Fst => 1,
Lst => P.Get (Positions (Target), Position) - 1)
-- Other elements are shifted by 1. -- Position has been removed from Source
and M.Range_Shifted
(Left => Model (Target)'Old, and P_Positions_Shifted
Right => Model (Target), (Positions (Source),
Fst => P.Get (Positions (Target), Position), Positions (Source)'Old,
Lst => Length (Target)'Old, Cut => P.Get (Positions (Source)'Old, Position'Old))
Offset => 1)
-- Positions is valid in Target and it is located either before
-- The element located at Position in Source is moved to Target -- Before if it is valid in Target or at the end if it is No_Element.
and Element (Model (Target), P.Get (Positions (Target), Position))
= Element (Model (Source)'Old, and P.Has_Key (Positions (Target), Position)
P.Get (Positions (Source)'Old, Position'Old)) and (if Before = No_Element then
P.Get (Positions (Target), Position) = Length (Target)
-- A new cursor has been inserted at position Position in Target else
and P_Positions_Shifted P.Get (Positions (Target), Position) =
(Positions (Target)'Old, P.Get (Positions (Target)'Old, Before))
Positions (Target),
Cut => P.Get (Positions (Target), Position)); -- The elements of Target located before Position are preserved
and M.Range_Equal
(Left => Model (Target)'Old,
Right => Model (Target),
Fst => 1,
Lst => P.Get (Positions (Target), Position) - 1)
-- Other elements are shifted by 1
and M.Range_Shifted
(Left => Model (Target)'Old,
Right => Model (Target),
Fst => P.Get (Positions (Target), Position),
Lst => Length (Target)'Old,
Offset => 1)
-- 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))
-- A new cursor has been inserted at position Position in Target
and P_Positions_Shifted
(Positions (Target)'Old,
Positions (Target),
Cut => P.Get (Positions (Target), Position));
procedure Splice procedure Splice
(Container : in out List; (Container : in out List;
...@@ -1046,17 +1156,18 @@ is ...@@ -1046,17 +1156,18 @@ is
with with
Global => null, Global => null,
Pre => Pre =>
(Has_Element (Container, Before) or else Before = No_Element) (Has_Element (Container, Before) or else Before = No_Element)
and then Has_Element (Container, Position), and then Has_Element (Container, Position),
Post => Length (Container) = Length (Container)'Old, Post => Length (Container) = Length (Container)'Old,
Contract_Cases => Contract_Cases =>
(Before = Position => (Before = Position =>
Model (Container) = Model (Container)'Old Model (Container) = Model (Container)'Old
and Positions (Container) = Positions (Container)'Old, and Positions (Container) = Positions (Container)'Old,
Before = No_Element => Before = No_Element =>
-- The elements located before Position are preserved -- The elements located before Position are preserved
M.Range_Equal M.Range_Equal
(Left => Model (Container)'Old, (Left => Model (Container)'Old,
Right => Model (Container), Right => Model (Container),
...@@ -1064,83 +1175,97 @@ is ...@@ -1064,83 +1175,97 @@ is
Lst => P.Get (Positions (Container)'Old, Position) - 1) Lst => P.Get (Positions (Container)'Old, Position) - 1)
-- 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)'Old,
Right => Model (Container), Right => Model (Container),
Fst => P.Get (Positions (Container)'Old, Position) + 1, Fst => P.Get (Positions (Container)'Old, Position) + 1,
Lst => Length (Container)'Old, Lst => Length (Container)'Old,
Offset => -1) Offset => -1)
-- The last element of Container is the one that was previously -- The last element of Container is the one that was previously at
-- at Position. -- Position.
and Element (Model (Container), Length (Container))
= Element (Model (Container)'Old, and Element (Model (Container), Length (Container)) =
P.Get (Positions (Container)'Old, Position)) Element (Model (Container)'Old,
P.Get (Positions (Container)'Old, Position))
-- Cursors from Container continue designating the same elements -- Cursors from Container continue designating the same elements
and Mapping_Preserved and Mapping_Preserved
(M_Left => Model (Container)'Old, (M_Left => Model (Container)'Old,
M_Right => Model (Container), M_Right => Model (Container),
P_Left => Positions (Container)'Old, P_Left => Positions (Container)'Old,
P_Right => Positions (Container)), P_Right => Positions (Container)),
others => others =>
-- The elements located before Position and Before are preserved -- The elements located before Position and Before are preserved
M.Range_Equal M.Range_Equal
(Left => Model (Container)'Old, (Left => Model (Container)'Old,
Right => Model (Container), Right => Model (Container),
Fst => 1, Fst => 1,
Lst => Count_Type'Min Lst =>
(P.Get (Positions (Container)'Old, Position) - 1, Count_Type'Min
P.Get (Positions (Container)'Old, Before) - 1)) (P.Get (Positions (Container)'Old, Position) - 1,
P.Get (Positions (Container)'Old, Before) - 1))
-- The elements located after Position and Before are preserved
and M.Range_Equal -- The elements located after Position and Before are preserved
(Left => Model (Container)'Old,
Right => Model (Container), and M.Range_Equal
Fst => Count_Type'Max (Left => Model (Container)'Old,
(P.Get (Positions (Container)'Old, Position) + 1, Right => Model (Container),
P.Get (Positions (Container)'Old, Before) + 1), Fst =>
Lst => Length (Container)) Count_Type'Max
(P.Get (Positions (Container)'Old, Position) + 1,
-- The elements located after Before and before Position are shifted P.Get (Positions (Container)'Old, Before) + 1),
-- by 1 to the right. Lst => Length (Container))
and M.Range_Shifted
(Left => Model (Container)'Old, -- The elements located after Before and before Position are
Right => Model (Container), -- shifted by 1 to the right.
Fst => P.Get (Positions (Container)'Old, Before) + 1,
Lst => P.Get (Positions (Container)'Old, Position) - 1, and M.Range_Shifted
Offset => 1) (Left => Model (Container)'Old,
Right => Model (Container),
-- The elements located after Position and before Before are shifted Fst => P.Get (Positions (Container)'Old, Before) + 1,
-- by 1 to the left. Lst => P.Get (Positions (Container)'Old, Position) - 1,
and M.Range_Shifted Offset => 1)
(Left => Model (Container)'Old,
Right => Model (Container), -- The elements located after Position and before Before are
Fst => P.Get (Positions (Container)'Old, Position) + 1, -- shifted by 1 to the left.
Lst => P.Get (Positions (Container)'Old, Before) - 1,
Offset => -1) and M.Range_Shifted
(Left => Model (Container)'Old,
-- The element previously at Position is now before Before Right => Model (Container),
and Element (Model (Container), Fst => P.Get (Positions (Container)'Old, Position) + 1,
P.Get (Positions (Container)'Old, Before)) Lst => P.Get (Positions (Container)'Old, Before) - 1,
= Element (Model (Container)'Old, Offset => -1)
P.Get (Positions (Container)'Old, Position))
-- The element previously at Position is now before Before
-- Cursors from Container continue designating the same elements
and Mapping_Preserved and Element (Model (Container),
(M_Left => Model (Container)'Old, P.Get (Positions (Container)'Old, Before)) =
M_Right => Model (Container), Element (Model (Container)'Old,
P_Left => Positions (Container)'Old, P.Get (Positions (Container)'Old, Position))
P_Right => Positions (Container)));
-- Cursors from Container continue designating the same elements
and Mapping_Preserved
(M_Left => Model (Container)'Old,
M_Right => Model (Container),
P_Left => Positions (Container)'Old,
P_Right => Positions (Container)));
function First (Container : List) return Cursor with function First (Container : List) return Cursor with
Global => null, Global => null,
Contract_Cases => Contract_Cases =>
(Length (Container) = 0 => First'Result = No_Element, (Length (Container) = 0 =>
others => Has_Element (Container, First'Result) First'Result = No_Element,
and P.Get (Positions (Container), First'Result) = 1);
others =>
Has_Element (Container, First'Result)
and P.Get (Positions (Container), First'Result) = 1);
function First_Element (Container : List) return Element_Type with function First_Element (Container : List) return Element_Type with
Global => null, Global => null,
...@@ -1150,65 +1275,79 @@ is ...@@ -1150,65 +1275,79 @@ is
function Last (Container : List) return Cursor with function Last (Container : List) return Cursor with
Global => null, Global => null,
Contract_Cases => Contract_Cases =>
(Length (Container) = 0 => Last'Result = No_Element, (Length (Container) = 0 =>
others => Has_Element (Container, Last'Result) Last'Result = No_Element,
and P.Get (Positions (Container), Last'Result) = Length (Container));
others =>
Has_Element (Container, Last'Result)
and P.Get (Positions (Container), Last'Result) =
Length (Container));
function Last_Element (Container : List) return Element_Type with function Last_Element (Container : List) return Element_Type with
Global => null, Global => null,
Pre => not Is_Empty (Container), Pre => not Is_Empty (Container),
Post => Last_Element'Result Post =>
= M.Get (Model (Container), Length (Container)); Last_Element'Result = M.Get (Model (Container), Length (Container));
function Next (Container : List; Position : Cursor) return Cursor with function Next (Container : List; Position : Cursor) return Cursor with
Global => null, Global => null,
Pre => Has_Element (Container, Position) Pre =>
or else Position = No_Element, Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases => Contract_Cases =>
(Position = No_Element (Position = No_Element
or else P.Get (Positions (Container), Position) = Length (Container) => or else P.Get (Positions (Container), Position) = Length (Container)
Next'Result = No_Element, =>
others => Has_Element (Container, Next'Result) Next'Result = No_Element,
and then P.Get (Positions (Container), Next'Result) =
P.Get (Positions (Container), Position) + 1); others =>
Has_Element (Container, Next'Result)
and then P.Get (Positions (Container), Next'Result) =
P.Get (Positions (Container), Position) + 1);
procedure Next (Container : List; Position : in out Cursor) with procedure Next (Container : List; Position : in out Cursor) with
Global => null, Global => null,
Pre => Has_Element (Container, Position) Pre =>
or else Position = No_Element, Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases => Contract_Cases =>
(Position = No_Element (Position = No_Element
or else P.Get (Positions (Container), Position) = Length (Container) => or else P.Get (Positions (Container), Position) = Length (Container)
Position = No_Element, =>
others => Has_Element (Container, Position) Position = No_Element,
and then P.Get (Positions (Container), Position) =
P.Get (Positions (Container), Position'Old) + 1); others =>
Has_Element (Container, Position)
and then P.Get (Positions (Container), Position) =
P.Get (Positions (Container), Position'Old) + 1);
function Previous (Container : List; Position : Cursor) return Cursor with function Previous (Container : List; Position : Cursor) return Cursor with
Global => null, Global => null,
Pre => Has_Element (Container, Position) Pre =>
or else Position = No_Element, Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases => Contract_Cases =>
(Position = No_Element (Position = No_Element
or else P.Get (Positions (Container), Position) = 1 => or else P.Get (Positions (Container), Position) = 1
=>
Previous'Result = No_Element, Previous'Result = No_Element,
others => others =>
Has_Element (Container, Previous'Result) Has_Element (Container, Previous'Result)
and then P.Get (Positions (Container), Previous'Result) = and then P.Get (Positions (Container), Previous'Result) =
P.Get (Positions (Container), Position) - 1); P.Get (Positions (Container), Position) - 1);
procedure Previous (Container : List; Position : in out Cursor) with procedure Previous (Container : List; Position : in out Cursor) with
Global => null, Global => null,
Pre => Has_Element (Container, Position) Pre =>
or else Position = No_Element, Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases => Contract_Cases =>
(Position = No_Element (Position = No_Element
or else P.Get (Positions (Container), Position) = 1 => or else P.Get (Positions (Container), Position) = 1
=>
Position = No_Element, Position = No_Element,
others => others =>
Has_Element (Container, Position) Has_Element (Container, Position)
and then P.Get (Positions (Container), Position) = and then P.Get (Positions (Container), Position) =
P.Get (Positions (Container), Position'Old) - 1); P.Get (Positions (Container), Position'Old) - 1);
function Find function Find
(Container : List; (Container : List;
...@@ -1217,40 +1356,52 @@ is ...@@ -1217,40 +1356,52 @@ is
with with
Global => null, Global => null,
Pre => Pre =>
Has_Element (Container, Position) or else Position = No_Element, Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases => Contract_Cases =>
-- If Item is not is not contained in Container after Position, Find -- If Item is not is not contained in Container after Position, Find
-- returns No_Element. -- returns No_Element.
(not M.Contains (not M.Contains
(Container => Model (Container), (Container => Model (Container),
Fst => (if Position = No_Element then 1 Fst =>
else P.Get (Positions (Container), Position)), (if Position = No_Element then
Lst => Length (Container), 1
Item => Item) else
P.Get (Positions (Container), Position)),
Lst => Length (Container),
Item => Item)
=> =>
Find'Result = No_Element, Find'Result = No_Element,
-- Otherwise, Find returns a valid cusror in Container -- Otherwise, Find returns a valid cusror in Container
others => others =>
P.Has_Key (Positions (Container), Find'Result) P.Has_Key (Positions (Container), Find'Result)
-- The element designated by the result of Find is Item -- 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 result of Find is located after Position
and (if Position /= No_Element
then P.Get (Positions (Container), Find'Result)
>= P.Get (Positions (Container), Position))
-- It is the first occurence of Item in this slice and (if Position /= No_Element then
and not M.Contains P.Get (Positions (Container), Find'Result) >=
(Container => Model (Container), P.Get (Positions (Container), Position))
Fst => (if Position = No_Element then 1
else P.Get (Positions (Container), Position)), -- It is the first occurence of Item in this slice
Lst => P.Get (Positions (Container), Find'Result) - 1,
Item => Item)); and not M.Contains
(Container => Model (Container),
Fst =>
(if Position = No_Element then
1
else
P.Get (Positions (Container), Position)),
Lst =>
P.Get (Positions (Container), Find'Result) - 1,
Item => Item));
function Reverse_Find function Reverse_Find
(Container : List; (Container : List;
...@@ -1259,40 +1410,54 @@ is ...@@ -1259,40 +1410,54 @@ is
with with
Global => null, Global => null,
Pre => Pre =>
Has_Element (Container, Position) or else Position = No_Element, Has_Element (Container, Position) or else Position = No_Element,
Contract_Cases => Contract_Cases =>
-- If Item is not is not contained in Container before Position, Find -- If Item is not is not contained in Container before Position, Find
-- returns No_Element. -- returns No_Element.
(not M.Contains (not M.Contains
(Container => Model (Container), (Container => Model (Container),
Fst => 1, Fst => 1,
Lst => (if Position = No_Element then Length (Container) Lst =>
else P.Get (Positions (Container), Position)), (if Position = No_Element then
Item => Item) Length (Container)
else
P.Get (Positions (Container), Position)),
Item => Item)
=> =>
Reverse_Find'Result = No_Element, Reverse_Find'Result = No_Element,
-- Otherwise, Find returns a valid cusror in Container -- Otherwise, Find returns a valid cusror in Container
others => others =>
P.Has_Key (Positions (Container), Reverse_Find'Result) P.Has_Key (Positions (Container), Reverse_Find'Result)
-- The element designated by the result of Find is Item -- The element designated by the result of Find is Item
and Element (Model (Container),
P.Get (Positions (Container), Reverse_Find'Result)) = Item
-- The result of Find is located before Position and Element (Model (Container),
and (if Position /= No_Element P.Get (Positions (Container),
then P.Get (Positions (Container), Reverse_Find'Result) Reverse_Find'Result)) = Item
<= P.Get (Positions (Container), Position))
-- It is the last occurence of Item in this slice -- The result of Find is located before Position
and not M.Contains
(Container => Model (Container), and (if Position /= No_Element then
Fst => P.Get (Positions (Container), Reverse_Find'Result) + 1, P.Get (Positions (Container), Reverse_Find'Result) <=
Lst => (if Position = No_Element then Length (Container) P.Get (Positions (Container), Position))
else P.Get (Positions (Container), Position)),
Item => Item)); -- It is the last occurence of Item in this slice
and not M.Contains
(Container => Model (Container),
Fst =>
P.Get (Positions (Container),
Reverse_Find'Result) + 1,
Lst =>
(if Position = No_Element then
Length (Container)
else
P.Get (Positions (Container), Position)),
Item => Item));
function Contains function Contains
(Container : List; (Container : List;
...@@ -1300,29 +1465,33 @@ is ...@@ -1300,29 +1465,33 @@ is
with with
Global => null, Global => null,
Post => Post =>
Contains'Result = M.Contains (Container => Model (Container), Contains'Result = M.Contains (Container => Model (Container),
Fst => 1, Fst => 1,
Lst => Length (Container), Lst => Length (Container),
Item => Item); Item => Item);
function Has_Element (Container : List; Position : Cursor) return Boolean function Has_Element
(Container : List;
Position : Cursor) return Boolean
with with
Global => null, Global => null,
Post => Post =>
Has_Element'Result = P.Has_Key (Positions (Container), Position); Has_Element'Result = P.Has_Key (Positions (Container), Position);
pragma Annotate (GNATprove, Inline_For_Proof, Has_Element); 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 function M_Elements_Sorted (Container : M.Sequence) return Boolean with
Ghost, Ghost,
Global => null, Global => null,
Post => M_Elements_Sorted'Result = Post =>
(for all I in 1 .. M.Length (Container) => M_Elements_Sorted'Result =
(for all J in I + 1 .. M.Length (Container) => (for all I in 1 .. M.Length (Container) =>
Element (Container, I) = Element (Container, J) (for all J in I + 1 .. M.Length (Container) =>
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); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
function Is_Sorted (Container : List) return Boolean with function Is_Sorted (Container : List) return Boolean with
...@@ -1331,18 +1500,20 @@ is ...@@ -1331,18 +1500,20 @@ is
procedure Sort (Container : in out List) with procedure Sort (Container : in out List) with
Global => null, Global => null,
Post => Length (Container) = Length (Container)'Old Post =>
and M_Elements_Sorted (Model (Container)); Length (Container) = Length (Container)'Old
and M_Elements_Sorted (Model (Container));
procedure Merge (Target, 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
Global => null, Global => null,
Pre => Length (Source) <= Target.Capacity - Length (Target), Pre => Length (Source) <= Target.Capacity - Length (Target),
Post => Length (Target) = Length (Target)'Old + Length (Source)'Old Post =>
and Length (Source) = 0 Length (Target) = Length (Target)'Old + Length (Source)'Old
and (if M_Elements_Sorted (Model (Target)'Old) and Length (Source) = 0
and M_Elements_Sorted (Model (Source)'Old) and (if M_Elements_Sorted (Model (Target)'Old)
then M_Elements_Sorted (Model (Target))); and M_Elements_Sorted (Model (Source)'Old)
then M_Elements_Sorted (Model (Target)));
end Generic_Sorting; end Generic_Sorting;
private private
......
gcc/ada/a-cofuba.adb
...@@ -33,14 +33,14 @@ pragma Ada_2012; ...@@ -33,14 +33,14 @@ pragma Ada_2012;
package body Ada.Containers.Functional_Base with SPARK_Mode => Off is package body Ada.Containers.Functional_Base with SPARK_Mode => Off is
function To_Count (Idx : Extended_Index) return Count_Type function To_Count (Idx : Extended_Index) return Count_Type is
is (Count_Type (Count_Type
(Extended_Index'Pos (Idx) - (Extended_Index'Pos (Idx) -
Extended_Index'Pos (Extended_Index'First))); Extended_Index'Pos (Extended_Index'First)));
function To_Index (Position : Count_Type) return Extended_Index function To_Index (Position : Count_Type) return Extended_Index is
is (Extended_Index'Val (Extended_Index'Val
(Position + Extended_Index'Pos (Extended_Index'First))); (Position + Extended_Index'Pos (Extended_Index'First)));
-- Conversion functions between Index_Type and Count_Type -- Conversion functions between Index_Type and Count_Type
function Find (C : Container; E : access Element_Type) return Count_Type; function Find (C : Container; E : access Element_Type) return Count_Type;
......
gcc/ada/a-cofuma.adb
...@@ -93,8 +93,8 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is ...@@ -93,8 +93,8 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
K : constant Key_Type := Get (Left.Keys, I); K : constant Key_Type := Get (Left.Keys, I);
begin begin
if not Equivalent_Keys (K, New_Key) if not Equivalent_Keys (K, New_Key)
and then Get (Right.Elements, Find (Right.Keys, K)) and then Get (Right.Elements, Find (Right.Keys, K)) /=
/= Get (Left.Elements, I) Get (Left.Elements, I)
then then
return False; return False;
end if; end if;
...@@ -106,7 +106,8 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is ...@@ -106,7 +106,8 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
function Elements_Equal_Except function Elements_Equal_Except
(Left : Map; (Left : Map;
Right : Map; Right : Map;
X, Y : Key_Type) return Boolean X : Key_Type;
Y : Key_Type) return Boolean
is is
begin begin
for I in 1 .. Length (Left.Keys) loop for I in 1 .. Length (Left.Keys) loop
...@@ -115,8 +116,8 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is ...@@ -115,8 +116,8 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
begin begin
if not Equivalent_Keys (K, X) if not Equivalent_Keys (K, X)
and then not Equivalent_Keys (K, Y) and then not Equivalent_Keys (K, Y)
and then Get (Right.Elements, Find (Right.Keys, K)) and then Get (Right.Elements, Find (Right.Keys, K)) /=
/= Get (Left.Elements, I) Get (Left.Elements, I)
then then
return False; return False;
end if; end if;
...@@ -167,6 +168,7 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is ...@@ -167,6 +168,7 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
end if; end if;
end; end;
end loop; end loop;
return True; return True;
end Keys_Included; end Keys_Included;
...@@ -191,13 +193,15 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is ...@@ -191,13 +193,15 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
end if; end if;
end; end;
end loop; end loop;
return True; return True;
end Keys_Included_Except; end Keys_Included_Except;
function Keys_Included_Except function Keys_Included_Except
(Left : Map; (Left : Map;
Right : Map; Right : Map;
X, Y : Key_Type) return Boolean X : Key_Type;
Y : Key_Type) return Boolean
is is
begin begin
for I in 1 .. Length (Left.Keys) loop for I in 1 .. Length (Left.Keys) loop
...@@ -212,6 +216,7 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is ...@@ -212,6 +216,7 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
end if; end if;
end; end;
end loop; end loop;
return True; return True;
end Keys_Included_Except; end Keys_Included_Except;
...@@ -229,8 +234,8 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is ...@@ -229,8 +234,8 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
--------------- ---------------
function Same_Keys (Left : Map; Right : Map) return Boolean is function Same_Keys (Left : Map; Right : Map) return Boolean is
(Keys_Included (Left, Right) (Keys_Included (Left, Right)
and Keys_Included (Left => Right, Right => Left)); and Keys_Included (Left => Right, Right => Left));
--------- ---------
-- Set -- -- Set --
...@@ -243,6 +248,6 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is ...@@ -243,6 +248,6 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is
is is
(Keys => Container.Keys, (Keys => Container.Keys,
Elements => Elements =>
Set (Container.Elements, Find (Container.Keys, Key), New_Item)); Set (Container.Elements, Find (Container.Keys, Key), New_Item));
end Ada.Containers.Functional_Maps; end Ada.Containers.Functional_Maps;
gcc/ada/a-cofuma.ads
...@@ -36,6 +36,7 @@ generic ...@@ -36,6 +36,7 @@ generic
type Key_Type (<>) is private; type Key_Type (<>) is private;
type Element_Type (<>) is private; type Element_Type (<>) is private;
with function Equivalent_Keys (Left, Right : Key_Type) return Boolean; with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
package Ada.Containers.Functional_Maps with SPARK_Mode is package Ada.Containers.Functional_Maps with SPARK_Mode is
type Map is private with type Map is private with
...@@ -90,9 +91,9 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is ...@@ -90,9 +91,9 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
Post => Post =>
"="'Result = "="'Result =
((for all Key of Left => ((for all Key of Left =>
Has_Key (Right, Key) Has_Key (Right, Key)
and then Get (Right, Key) = Get (Left, Key)) and then Get (Right, Key) = Get (Left, Key))
and (for all Key of Right => Has_Key (Left, Key))); and (for all Key of Right => Has_Key (Left, Key)));
pragma Warnings (Off, "unused variable ""Key"""); pragma Warnings (Off, "unused variable ""Key""");
function Is_Empty (Container : Map) return Boolean with function Is_Empty (Container : Map) return Boolean with
...@@ -117,8 +118,8 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is ...@@ -117,8 +118,8 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
Global => null, Global => null,
Post => Post =>
Same_Keys'Result = Same_Keys'Result =
(Keys_Included (Left, Right) (Keys_Included (Left, Right)
and Keys_Included (Left => Right, Right => Left)); and Keys_Included (Left => Right, Right => Left));
pragma Annotate (GNATprove, Inline_For_Proof, Same_Keys); pragma Annotate (GNATprove, Inline_For_Proof, Same_Keys);
function Keys_Included_Except function Keys_Included_Except
...@@ -130,24 +131,27 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is ...@@ -130,24 +131,27 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
with with
Global => null, Global => null,
Post => Post =>
Keys_Included_Except'Result = Keys_Included_Except'Result =
(for all Key of Left => (for all Key of Left =>
(if not Equivalent_Keys (Key, New_Key) (if not Equivalent_Keys (Key, New_Key) then
then Has_Key (Right, Key))); Has_Key (Right, Key)));
function Keys_Included_Except function Keys_Included_Except
(Left : Map; (Left : Map;
Right : Map; Right : Map;
X, Y : Key_Type) return Boolean X : Key_Type;
Y : Key_Type) return Boolean
-- Returns True if Left contains only keys of Right and possibly X and Y -- Returns True if Left contains only keys of Right and possibly X and Y
with with
Global => null, Global => null,
Post => Post =>
Keys_Included_Except'Result = Keys_Included_Except'Result =
(for all Key of Left => (for all Key of Left =>
(if not Equivalent_Keys (Key, X) and not Equivalent_Keys (Key, Y) (if not Equivalent_Keys (Key, X)
then Has_Key (Right, Key))); and not Equivalent_Keys (Key, Y)
then
Has_Key (Right, Key)));
function Elements_Equal_Except function Elements_Equal_Except
(Left : Map; (Left : Map;
...@@ -162,13 +166,14 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is ...@@ -162,13 +166,14 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
Post => Post =>
Elements_Equal_Except'Result = Elements_Equal_Except'Result =
(for all Key of Left => (for all Key of Left =>
(if not Equivalent_Keys (Key, New_Key) (if not Equivalent_Keys (Key, New_Key) then
then Get (Left, Key) = Get (Right, Key))); Get (Left, Key) = Get (Right, Key)));
function Elements_Equal_Except function Elements_Equal_Except
(Left : Map; (Left : Map;
Right : Map; Right : Map;
X, Y : Key_Type) return Boolean X : Key_Type;
Y : Key_Type) return Boolean
-- Returns True if all the keys of Left are mapped to the same elements in -- Returns True if all the keys of Left are mapped to the same elements in
-- Left and Right except X and Y. -- Left and Right except X and Y.
...@@ -178,8 +183,10 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is ...@@ -178,8 +183,10 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
Post => Post =>
Elements_Equal_Except'Result = Elements_Equal_Except'Result =
(for all Key of Left => (for all Key of Left =>
(if not Equivalent_Keys (Key, X) and not Equivalent_Keys (Key, Y) (if not Equivalent_Keys (Key, X)
then Get (Left, Key) = Get (Right, Key))); and not Equivalent_Keys (Key, Y)
then
Get (Left, Key) = Get (Right, Key)));
---------------------------- ----------------------------
-- Construction Functions -- -- Construction Functions --
...@@ -192,19 +199,19 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is ...@@ -192,19 +199,19 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
(Container : Map; (Container : Map;
New_Key : Key_Type; New_Key : Key_Type;
New_Item : Element_Type) return Map New_Item : Element_Type) return Map
-- Returns Container augmented with the mapping Key -> New_Item. -- Returns Container augmented with the mapping Key -> New_Item
with with
Global => null, Global => null,
Pre => Pre =>
not Has_Key (Container, New_Key) not Has_Key (Container, New_Key)
and Length (Container) < Count_Type'Last, and Length (Container) < Count_Type'Last,
Post => Post =>
Length (Container) + 1 = Length (Add'Result) Length (Container) + 1 = Length (Add'Result)
and Has_Key (Add'Result, New_Key) and Has_Key (Add'Result, New_Key)
and Get (Add'Result, New_Key) = New_Item and Get (Add'Result, New_Key) = New_Item
and Container <= Add'Result and Container <= Add'Result
and Keys_Included_Except (Add'Result, Container, New_Key); and Keys_Included_Except (Add'Result, Container, New_Key);
function Set function Set
(Container : Map; (Container : Map;
...@@ -218,9 +225,9 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is ...@@ -218,9 +225,9 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is
Pre => Has_Key (Container, Key), Pre => Has_Key (Container, Key),
Post => Post =>
Length (Container) = Length (Set'Result) Length (Container) = Length (Set'Result)
and Get (Set'Result, Key) = New_Item and Get (Set'Result, Key) = New_Item
and Same_Keys (Container, Set'Result) and Same_Keys (Container, Set'Result)
and Elements_Equal_Except (Container, Set'Result, Key); and Elements_Equal_Except (Container, Set'Result, Key);
--------------------------- ---------------------------
-- Iteration Primitives -- -- Iteration Primitives --
...@@ -281,11 +288,15 @@ private ...@@ -281,11 +288,15 @@ private
is is
(Count_Type (Key) in 1 .. Key_Containers.Length (Container.Keys)); (Count_Type (Key) in 1 .. Key_Containers.Length (Container.Keys));
function Iter_Next (Container : Map; Key : Private_Key) return Private_Key function Iter_Next
(Container : Map;
Key : Private_Key) return Private_Key
is is
(if Key = Private_Key'Last then 0 else Key + 1); (if Key = Private_Key'Last then 0 else Key + 1);
function Iter_Element (Container : Map; Key : Private_Key) return Key_Type function Iter_Element
(Container : Map;
Key : Private_Key) return Key_Type
is is
(Key_Containers.Get (Container.Keys, Count_Type (Key))); (Key_Containers.Get (Container.Keys, Count_Type (Key)));
......
gcc/ada/a-cofuse.adb
...@@ -54,7 +54,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is ...@@ -54,7 +54,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
function Add (Container : Set; Item : Element_Type) return Set is function Add (Container : Set; Item : Element_Type) return Set is
(Content => (Content =>
Add (Container.Content, Length (Container.Content) + 1, Item)); Add (Container.Content, Length (Container.Content) + 1, Item));
-------------- --------------
-- Contains -- -- Contains --
...@@ -73,7 +73,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is ...@@ -73,7 +73,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
Item : Element_Type) return Boolean Item : Element_Type) return Boolean
is is
(for all E of Left => (for all E of Left =>
Equivalent_Elements (E, Item) or Contains (Right, E)); Equivalent_Elements (E, Item) or Contains (Right, E));
----------------------- -----------------------
-- Included_In_Union -- -- Included_In_Union --
...@@ -85,7 +85,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is ...@@ -85,7 +85,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
Right : Set) return Boolean Right : Set) return Boolean
is is
(for all Item of Container => (for all Item of Container =>
Contains (Left, Item) or Contains (Right, Item)); Contains (Left, Item) or Contains (Right, Item));
--------------------------- ---------------------------
-- Includes_Intersection -- -- Includes_Intersection --
...@@ -97,7 +97,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is ...@@ -97,7 +97,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
Right : Set) return Boolean Right : Set) return Boolean
is is
(for all Item of Left => (for all Item of Left =>
(if Contains (Right, Item) then Contains (Container, Item))); (if Contains (Right, Item) then Contains (Container, Item)));
------------------ ------------------
-- Intersection -- -- Intersection --
......
gcc/ada/a-cofuse.ads
...@@ -34,8 +34,10 @@ private with Ada.Containers.Functional_Base; ...@@ -34,8 +34,10 @@ private with Ada.Containers.Functional_Base;
generic generic
type Element_Type (<>) is private; type Element_Type (<>) is private;
with with function Equivalent_Elements
function Equivalent_Elements (Left, Right : Element_Type) return Boolean; (Left : Element_Type;
Right : Element_Type) return Boolean;
package Ada.Containers.Functional_Sets with SPARK_Mode is package Ada.Containers.Functional_Sets with SPARK_Mode is
type Set is private with type Set is private with
...@@ -80,8 +82,8 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -80,8 +82,8 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
Global => null, Global => null,
Post => Post =>
"="'Result = "="'Result =
((for all Item of Left => Contains (Right, Item)) (for all Item of Left => Contains (Right, Item))
and (for all Item of Right => Contains (Left, Item))); and (for all Item of Right => Contains (Left, Item));
pragma Warnings (Off, "unused variable ""Item"""); pragma Warnings (Off, "unused variable ""Item""");
function Is_Empty (Container : Set) return Boolean with function Is_Empty (Container : Set) return Boolean with
...@@ -102,8 +104,8 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -102,8 +104,8 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
Global => null, Global => null,
Post => Post =>
Included_Except'Result = Included_Except'Result =
(for all E of Left => (for all E of Left =>
Contains (Right, E) or Equivalent_Elements (E, Item)); Contains (Right, E) or Equivalent_Elements (E, Item));
function Includes_Intersection function Includes_Intersection
(Container : Set; (Container : Set;
...@@ -117,7 +119,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -117,7 +119,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
Post => Post =>
Includes_Intersection'Result = Includes_Intersection'Result =
(for all Item of Left => (for all Item of Left =>
(if Contains (Right, Item) then Contains (Container, Item))); (if Contains (Right, Item) then Contains (Container, Item)));
function Included_In_Union function Included_In_Union
(Container : Set; (Container : Set;
...@@ -130,7 +132,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -130,7 +132,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
Post => Post =>
Included_In_Union'Result = Included_In_Union'Result =
(for all Item of Container => (for all Item of Container =>
Contains (Left, Item) or Contains (Right, Item)); Contains (Left, Item) or Contains (Right, Item));
function Num_Overlaps (Left : Set; Right : Set) return Count_Type with function Num_Overlaps (Left : Set; Right : Set) return Count_Type with
-- Number of elements that are both in Left and Right -- Number of elements that are both in Left and Right
...@@ -158,9 +160,9 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -158,9 +160,9 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
and Length (Container) < Count_Type'Last, and Length (Container) < Count_Type'Last,
Post => Post =>
Length (Add'Result) = Length (Container) + 1 Length (Add'Result) = Length (Container) + 1
and Contains (Add'Result, Item) and Contains (Add'Result, Item)
and Container <= Add'Result and Container <= Add'Result
and Included_Except (Add'Result, Container, Item); and Included_Except (Add'Result, Container, Item);
function Remove (Container : Set; Item : Element_Type) return Set with function Remove (Container : Set; Item : Element_Type) return Set with
-- Return a new set containing all the elements of Container except E -- Return a new set containing all the elements of Container except E
...@@ -169,9 +171,9 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -169,9 +171,9 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
Pre => Contains (Container, Item), Pre => Contains (Container, Item),
Post => Post =>
Length (Remove'Result) = Length (Container) - 1 Length (Remove'Result) = Length (Container) - 1
and not Contains (Remove'Result, Item) and not Contains (Remove'Result, Item)
and Remove'Result <= Container and Remove'Result <= Container
and Included_Except (Container, Remove'Result, Item); and Included_Except (Container, Remove'Result, Item);
function Intersection (Left : Set; Right : Set) return Set with function Intersection (Left : Set; Right : Set) return Set with
-- Returns the intersection of Left and Right -- Returns the intersection of Left and Right
...@@ -188,8 +190,8 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -188,8 +190,8 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
Global => null, Global => null,
Pre => Pre =>
Length (Left) - Num_Overlaps (Left, Right) Length (Left) - Num_Overlaps (Left, Right) <=
<= Count_Type'Last - Length (Right), Count_Type'Last - Length (Right),
Post => Post =>
Length (Union'Result) = Length (Union'Result) =
Length (Left) - Num_Overlaps (Left, Right) + Length (Right) Length (Left) - Num_Overlaps (Left, Right) + Length (Right)
...@@ -212,7 +214,9 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is ...@@ -212,7 +214,9 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is
with with
Global => null; Global => null;
function Iter_Next (Container : Set; Key : Private_Key) return Private_Key function Iter_Next
(Container : Set;
Key : Private_Key) return Private_Key
with with
Global => null, Global => null,
Pre => Iter_Has_Element (Container, Key); Pre => Iter_Has_Element (Container, Key);
...@@ -249,7 +253,9 @@ private ...@@ -249,7 +253,9 @@ private
is is
(Count_Type (Key) in 1 .. Containers.Length (Container.Content)); (Count_Type (Key) in 1 .. Containers.Length (Container.Content));
function Iter_Next (Container : Set; Key : Private_Key) return Private_Key function Iter_Next
(Container : Set;
Key : Private_Key) return Private_Key
is is
(if Key = Private_Key'Last then 0 else Key + 1); (if Key = Private_Key'Last then 0 else Key + 1);
......
gcc/ada/a-cofuve.adb
...@@ -40,7 +40,7 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is ...@@ -40,7 +40,7 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
function "<" (Left : Sequence; Right : Sequence) return Boolean is function "<" (Left : Sequence; Right : Sequence) return Boolean is
(Length (Left.Content) < Length (Right.Content) (Length (Left.Content) < Length (Right.Content)
and then (for all I in Index_Type'First .. Last (Left) => and then (for all I in Index_Type'First .. Last (Left) =>
Get (Left.Content, I) = Get (Right.Content, I))); Get (Left.Content, I) = Get (Right.Content, I)));
---------- ----------
-- "<=" -- -- "<=" --
...@@ -49,7 +49,7 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is ...@@ -49,7 +49,7 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
function "<=" (Left : Sequence; Right : Sequence) return Boolean is function "<=" (Left : Sequence; Right : Sequence) return Boolean is
(Length (Left.Content) <= Length (Right.Content) (Length (Left.Content) <= Length (Right.Content)
and then (for all I in Index_Type'First .. Last (Left) => and then (for all I in Index_Type'First .. Last (Left) =>
Get (Left.Content, I) = Get (Right.Content, I))); Get (Left.Content, I) = Get (Right.Content, I)));
--------- ---------
-- "=" -- -- "=" --
...@@ -62,13 +62,15 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is ...@@ -62,13 +62,15 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
-- Add -- -- Add --
--------- ---------
function Add (Container : Sequence; New_Item : Element_Type) return Sequence function Add
(Container : Sequence;
New_Item : Element_Type) return Sequence
is is
(Content => Add (Container.Content, (Content =>
Index_Type'Val Add (Container.Content,
(Index_Type'Pos (Index_Type'First) + Index_Type'Val (Index_Type'Pos (Index_Type'First) +
Length (Container.Content)), Length (Container.Content)),
New_Item)); New_Item));
function Add function Add
(Container : Sequence; (Container : Sequence;
...@@ -92,6 +94,7 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is ...@@ -92,6 +94,7 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
return False; return False;
end if; end if;
end loop; end loop;
return True; return True;
end Constant_Range; end Constant_Range;
...@@ -111,6 +114,7 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is ...@@ -111,6 +114,7 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
return True; return True;
end if; end if;
end loop; end loop;
return False; return False;
end Contains; end Contains;
...@@ -142,7 +146,8 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is ...@@ -142,7 +146,8 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
function Equal_Except function Equal_Except
(Left : Sequence; (Left : Sequence;
Right : Sequence; Right : Sequence;
X, Y : Index_Type) return Boolean X : Index_Type;
Y : Index_Type) return Boolean
is is
begin begin
if Length (Left.Content) /= Length (Right.Content) then if Length (Left.Content) /= Length (Right.Content) then
...@@ -174,8 +179,8 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is ...@@ -174,8 +179,8 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
---------- ----------
function Last (Container : Sequence) return Extended_Index is function Last (Container : Sequence) return Extended_Index is
(Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) (Index_Type'Val
+ Length (Container))); ((Index_Type'Pos (Index_Type'First) - 1) + Length (Container)));
------------ ------------
-- Length -- -- Length --
...@@ -200,6 +205,7 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is ...@@ -200,6 +205,7 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
return False; return False;
end if; end if;
end loop; end loop;
return True; return True;
end Range_Equal; end Range_Equal;
...@@ -216,8 +222,8 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is ...@@ -216,8 +222,8 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
is is
begin begin
for I in Fst .. Lst loop for I in Fst .. Lst loop
if Get (Left, I) if Get (Left, I) /=
/= Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset)) Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset))
then then
return False; return False;
end if; end if;
...@@ -229,8 +235,9 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is ...@@ -229,8 +235,9 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
-- Remove -- -- Remove --
------------ ------------
function Remove (Container : Sequence; function Remove
Position : Index_Type) return Sequence (Container : Sequence;
Position : Index_Type) return Sequence
is is
(Content => Remove (Container.Content, Position)); (Content => Remove (Container.Content, Position));
......
gcc/ada/a-cofuve.ads
...@@ -38,6 +38,7 @@ generic ...@@ -38,6 +38,7 @@ generic
-- should have at least one more element at the low end than Index_Type. -- should have at least one more element at the low end than Index_Type.
type Element_Type (<>) is private; type Element_Type (<>) is private;
package Ada.Containers.Functional_Vectors with SPARK_Mode is package Ada.Containers.Functional_Vectors with SPARK_Mode is
subtype Extended_Index is Index_Type'Base range subtype Extended_Index is Index_Type'Base range
...@@ -69,7 +70,7 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -69,7 +70,7 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
Global => null, Global => null,
Post => Post =>
(Index_Type'Pos (Index_Type'First) - 1) + Length'Result <= (Index_Type'Pos (Index_Type'First) - 1) + Length'Result <=
Index_Type'Pos (Index_Type'Last); Index_Type'Pos (Index_Type'Last);
function Get function Get
(Container : Sequence; (Container : Sequence;
...@@ -86,8 +87,8 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -86,8 +87,8 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
Global => null, Global => null,
Post => Post =>
Last'Result = Last'Result =
Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) +
+ Length (Container)); Length (Container));
pragma Annotate (GNATprove, Inline_For_Proof, Last); pragma Annotate (GNATprove, Inline_For_Proof, Last);
function First return Extended_Index is (Index_Type'First); function First return Extended_Index is (Index_Type'First);
...@@ -104,8 +105,8 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -104,8 +105,8 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
Post => Post =>
"="'Result = "="'Result =
(Length (Left) = Length (Right) (Length (Left) = Length (Right)
and then (for all N in Index_Type'First .. Last (Left) => and then (for all N in Index_Type'First .. Last (Left) =>
Get (Left, N) = Get (Right, N))); Get (Left, N) = Get (Right, N)));
pragma Annotate (GNATprove, Inline_For_Proof, "="); pragma Annotate (GNATprove, Inline_For_Proof, "=");
function "<" (Left : Sequence; Right : Sequence) return Boolean with function "<" (Left : Sequence; Right : Sequence) return Boolean with
...@@ -115,8 +116,8 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -115,8 +116,8 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
Post => Post =>
"<"'Result = "<"'Result =
(Length (Left) < Length (Right) (Length (Left) < Length (Right)
and then (for all N in Index_Type'First .. Last (Left) => and then (for all N in Index_Type'First .. Last (Left) =>
Get (Left, N) = Get (Right, N))); Get (Left, N) = Get (Right, N)));
pragma Annotate (GNATprove, Inline_For_Proof, "<"); pragma Annotate (GNATprove, Inline_For_Proof, "<");
function "<=" (Left : Sequence; Right : Sequence) return Boolean with function "<=" (Left : Sequence; Right : Sequence) return Boolean with
...@@ -126,16 +127,15 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -126,16 +127,15 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
Post => Post =>
"<="'Result = "<="'Result =
(Length (Left) <= Length (Right) (Length (Left) <= Length (Right)
and then (for all N in Index_Type'First .. Last (Left) => and then (for all N in Index_Type'First .. Last (Left) =>
Get (Left, N) = Get (Right, N))); Get (Left, N) = Get (Right, N)));
pragma Annotate (GNATprove, Inline_For_Proof, "<="); pragma Annotate (GNATprove, Inline_For_Proof, "<=");
function Contains function Contains
(Container : Sequence; (Container : Sequence;
Fst : Index_Type; Fst : Index_Type;
Lst : Extended_Index; Lst : Extended_Index;
Item : Element_Type) Item : Element_Type) return Boolean
return Boolean
-- Returns True if Item occurs in the range from Fst to Lst of Container -- Returns True if Item occurs in the range from Fst to Lst of Container
with with
...@@ -150,8 +150,7 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -150,8 +150,7 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
(Container : Sequence; (Container : Sequence;
Fst : Index_Type; Fst : Index_Type;
Lst : Extended_Index; Lst : Extended_Index;
Item : Element_Type) Item : Element_Type) return Boolean
return Boolean
-- Returns True if every element of the range from Fst to Lst of Container -- Returns True if every element of the range from Fst to Lst of Container
-- is equal to Item. -- is equal to Item.
...@@ -175,14 +174,15 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -175,14 +174,15 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
Post => Post =>
Equal_Except'Result = Equal_Except'Result =
(Length (Left) = Length (Right) (Length (Left) = Length (Right)
and then (for all I in Index_Type'First .. Last (Left) => and then (for all I in Index_Type'First .. Last (Left) =>
(if I /= Position then Get (Left, I) = Get (Right, I)))); (if I /= Position then Get (Left, I) = Get (Right, I))));
pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except); pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
function Equal_Except function Equal_Except
(Left : Sequence; (Left : Sequence;
Right : Sequence; Right : Sequence;
X, Y : Index_Type) return Boolean X : Index_Type;
Y : Index_Type) return Boolean
-- Returns True is Left and Right are the same except at positions X and Y -- Returns True is Left and Right are the same except at positions X and Y
with with
...@@ -191,8 +191,9 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -191,8 +191,9 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
Post => Post =>
Equal_Except'Result = Equal_Except'Result =
(Length (Left) = Length (Right) (Length (Left) = Length (Right)
and then (for all I in Index_Type'First .. Last (Left) => and then (for all I in Index_Type'First .. Last (Left) =>
(if I /= X and I /= Y then Get (Left, I) = Get (Right, I)))); (if I /= X and I /= Y then
Get (Left, I) = Get (Right, I))));
pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except); pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
function Range_Equal function Range_Equal
...@@ -222,21 +223,23 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -222,21 +223,23 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
with with
Global => null, Global => null,
Pre => Lst <= Last (Left) Pre =>
and Offset in Lst <= Last (Left)
Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) .. and Offset in
(Index_Type'Pos (Index_Type'First) - 1) Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) ..
+ Length (Right) - Index_Type'Pos (Lst), (Index_Type'Pos (Index_Type'First) - 1) + Length (Right) -
Index_Type'Pos (Lst),
Post => Post =>
Range_Shifted'Result = Range_Shifted'Result =
((for all I in Fst .. Lst => ((for all I in Fst .. Lst =>
Get (Left, I) Get (Left, I) =
= Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset))) Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset)))
and and
(for all I in Index_Type'Val (Index_Type'Pos (Fst) + Offset) .. (for all I in Index_Type'Val (Index_Type'Pos (Fst) + Offset) ..
Index_Type'Val (Index_Type'Pos (Lst) + Offset) => Index_Type'Val (Index_Type'Pos (Lst) + Offset)
Get (Left, Index_Type'Val (Index_Type'Pos (I) - Offset)) =>
= Get (Right, I))); Get (Left, Index_Type'Val (Index_Type'Pos (I) - Offset)) =
Get (Right, I)));
pragma Annotate (GNATprove, Inline_For_Proof, Range_Shifted); pragma Annotate (GNATprove, Inline_For_Proof, Range_Shifted);
---------------------------- ----------------------------
...@@ -256,8 +259,9 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -256,8 +259,9 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
with with
Global => null, Global => null,
Pre => Position in Index_Type'First .. Last (Container), Pre => Position in Index_Type'First .. Last (Container),
Post => Get (Set'Result, Position) = New_Item Post =>
and then Equal_Except (Container, Set'Result, Position); Get (Set'Result, Position) = New_Item
and then Equal_Except (Container, Set'Result, Position);
function Add (Container : Sequence; New_Item : Element_Type) return Sequence function Add (Container : Sequence; New_Item : Element_Type) return Sequence
-- Returns a new sequence which contains the same elements as Container -- Returns a new sequence which contains the same elements as Container
...@@ -289,17 +293,17 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -289,17 +293,17 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
Post => Post =>
Length (Add'Result) = Length (Container) + 1 Length (Add'Result) = Length (Container) + 1
and then Get (Add'Result, Position) = New_Item and then Get (Add'Result, Position) = New_Item
and then and then Range_Equal
Range_Equal (Left => Container, (Left => Container,
Right => Add'Result, Right => Add'Result,
Fst => Index_Type'First, Fst => Index_Type'First,
Lst => Index_Type'Pred (Position)) Lst => Index_Type'Pred (Position))
and then and then Range_Shifted
Range_Shifted (Left => Container, (Left => Container,
Right => Add'Result, Right => Add'Result,
Fst => Position, Fst => Position,
Lst => Last (Container), Lst => Last (Container),
Offset => 1); Offset => 1);
function Remove function Remove
(Container : Sequence; (Container : Sequence;
...@@ -315,17 +319,17 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -315,17 +319,17 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
and Position in Index_Type'First .. Last (Container), and Position in Index_Type'First .. Last (Container),
Post => Post =>
Length (Remove'Result) = Length (Container) - 1 Length (Remove'Result) = Length (Container) - 1
and then and then Range_Equal
Range_Equal (Left => Container, (Left => Container,
Right => Remove'Result, Right => Remove'Result,
Fst => Index_Type'First, Fst => Index_Type'First,
Lst => Index_Type'Pred (Position)) Lst => Index_Type'Pred (Position))
and then and then Range_Shifted
Range_Shifted (Left => Remove'Result, (Left => Remove'Result,
Right => Container, Right => Container,
Fst => Position, Fst => Position,
Lst => Last (Remove'Result), Lst => Last (Remove'Result),
Offset => 1); Offset => 1);
--------------------------- ---------------------------
-- Iteration Primitives -- -- Iteration Primitives --
...@@ -339,7 +343,8 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is ...@@ -339,7 +343,8 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is
Position : Extended_Index) return Boolean Position : Extended_Index) return Boolean
with with
Global => null, Global => null,
Post => Iter_Has_Element'Result = Post =>
Iter_Has_Element'Result =
(Position in Index_Type'First .. Last (Container)); (Position in Index_Type'First .. Last (Container));
pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element); pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element);
...@@ -364,19 +369,22 @@ private ...@@ -364,19 +369,22 @@ private
function Iter_First (Container : Sequence) return Extended_Index is function Iter_First (Container : Sequence) return Extended_Index is
(Index_Type'First); (Index_Type'First);
function Iter_Next function Iter_Next
(Container : Sequence; (Container : Sequence;
Position : Extended_Index) return Extended_Index Position : Extended_Index) return Extended_Index
is is
(if Position = Extended_Index'Last then Extended_Index'First (if Position = Extended_Index'Last then
else Extended_Index'Succ (Position)); Extended_Index'First
else
Extended_Index'Succ (Position));
function Iter_Has_Element function Iter_Has_Element
(Container : Sequence; (Container : Sequence;
Position : Extended_Index) return Boolean Position : Extended_Index) return Boolean
is is
(Position in Index_Type'First .. (Position in Index_Type'First ..
(Index_Type'Val (Index_Type'Val
((Index_Type'Pos (Index_Type'First) - 1) + Length (Container)))); ((Index_Type'Pos (Index_Type'First) - 1) + Length (Container))));
end Ada.Containers.Functional_Vectors; end Ada.Containers.Functional_Vectors;
gcc/ada/exp_attr.adb
...@@ -3598,6 +3598,14 @@ package body Exp_Attr is ...@@ -3598,6 +3598,14 @@ package body Exp_Attr is
-- Image attribute is handled in separate unit Exp_Imgv -- Image attribute is handled in separate unit Exp_Imgv
when Attribute_Image => when Attribute_Image =>
-- Leave attribute unexpanded in CodePeer mode: the gnat2scil
-- back-end knows how to handle this attribute directly.
if CodePeer_Mode then
return;
end if;
Exp_Imgv.Expand_Image_Attribute (N); Exp_Imgv.Expand_Image_Attribute (N);
--------- ---------
...@@ -6995,6 +7003,14 @@ package body Exp_Attr is ...@@ -6995,6 +7003,14 @@ package body Exp_Attr is
-- Wide_Image attribute is handled in separate unit Exp_Imgv -- Wide_Image attribute is handled in separate unit Exp_Imgv
when Attribute_Wide_Image => when Attribute_Wide_Image =>
-- Leave attribute unexpanded in CodePeer mode: the gnat2scil
-- back-end knows how to handle this attribute directly.
if CodePeer_Mode then
return;
end if;
Exp_Imgv.Expand_Wide_Image_Attribute (N); Exp_Imgv.Expand_Wide_Image_Attribute (N);
--------------------- ---------------------
...@@ -7004,6 +7020,14 @@ package body Exp_Attr is ...@@ -7004,6 +7020,14 @@ package body Exp_Attr is
-- Wide_Wide_Image attribute is handled in separate unit Exp_Imgv -- Wide_Wide_Image attribute is handled in separate unit Exp_Imgv
when Attribute_Wide_Wide_Image => when Attribute_Wide_Wide_Image =>
-- Leave attribute unexpanded in CodePeer mode: the gnat2scil
-- back-end knows how to handle this attribute directly.
if CodePeer_Mode then
return;
end if;
Exp_Imgv.Expand_Wide_Wide_Image_Attribute (N); Exp_Imgv.Expand_Wide_Wide_Image_Attribute (N);
---------------- ----------------
......
gcc/ada/exp_disp.adb
...@@ -4510,10 +4510,13 @@ package body Exp_Disp is ...@@ -4510,10 +4510,13 @@ package body Exp_Disp is
if Building_Static_DT (Typ) then if Building_Static_DT (Typ) then
declare declare
Save : constant Boolean := Freezing_Library_Level_Tagged_Type; Saved_FLLTT : constant Boolean :=
Freezing_Library_Level_Tagged_Type;
Formal : Entity_Id;
Frnodes : List_Id;
Prim : Entity_Id; Prim : Entity_Id;
Prim_Elmt : Elmt_Id; Prim_Elmt : Elmt_Id;
Frnodes : List_Id;
begin begin
Freezing_Library_Level_Tagged_Type := True; Freezing_Library_Level_Tagged_Type := True;
...@@ -4523,18 +4526,21 @@ package body Exp_Disp is ...@@ -4523,18 +4526,21 @@ package body Exp_Disp is
Prim := Node (Prim_Elmt); Prim := Node (Prim_Elmt);
Frnodes := Freeze_Entity (Prim, Typ); Frnodes := Freeze_Entity (Prim, Typ);
declare -- We disable this check for abstract subprograms, given that
F : Entity_Id; -- they cannot be called directly and thus the state of their
-- untagged formals is of no concern. The RM is unclear in any
begin -- case concerning the need for this check, and this topic may
F := First_Formal (Prim); -- go back to the ARG.
while Present (F) loop
Check_Premature_Freezing (Prim, Typ, Etype (F)); if not Is_Abstract_Subprogram (Prim) then
Next_Formal (F); Formal := First_Formal (Prim);
while Present (Formal) loop
Check_Premature_Freezing (Prim, Typ, Etype (Formal));
Next_Formal (Formal);
end loop; end loop;
Check_Premature_Freezing (Prim, Typ, Etype (Prim)); Check_Premature_Freezing (Prim, Typ, Etype (Prim));
end; end if;
if Present (Frnodes) then if Present (Frnodes) then
Append_List_To (Result, Frnodes); Append_List_To (Result, Frnodes);
...@@ -4543,7 +4549,7 @@ package body Exp_Disp is ...@@ -4543,7 +4549,7 @@ package body Exp_Disp is
Next_Elmt (Prim_Elmt); Next_Elmt (Prim_Elmt);
end loop; end loop;
Freezing_Library_Level_Tagged_Type := Save; Freezing_Library_Level_Tagged_Type := Saved_FLLTT;
end; end;
end if; end if;
......
gcc/ada/sem_attr.adb
...@@ -6310,21 +6310,28 @@ package body Sem_Attr is ...@@ -6310,21 +6310,28 @@ package body Sem_Attr is
end; end;
end if; end if;
-- Fold in representation aspects for the type, which appear in if Is_First_Subtype (T) then
-- the same source buffer.
Rep := First_Rep_Item (T); -- Fold in representation aspects for the type, which appear in
-- the same source buffer. If the representation aspects are in
-- a different source file, then skip them; they apply to some
-- other type, perhaps one we're derived from.
while Present (Rep) loop Rep := First_Rep_Item (T);
if Comes_From_Source (Rep) then
Sloc_Range (Rep, P_Min, P_Max);
pragma Assert (SFI = Get_Source_File_Index (P_Min));
pragma Assert (SFI = Get_Source_File_Index (P_Max));
Process_One_Declaration;
end if;
Rep := Next_Rep_Item (Rep); while Present (Rep) loop
end loop; if Comes_From_Source (Rep) then
Sloc_Range (Rep, P_Min, P_Max);
if SFI = Get_Source_File_Index (P_Min) then
pragma Assert (SFI = Get_Source_File_Index (P_Max));
Process_One_Declaration;
end if;
end if;
Rep := Next_Rep_Item (Rep);
end loop;
end if;
end Compute_Type_Key; end Compute_Type_Key;
-- Start of processing for Type_Key -- Start of processing for Type_Key
......
gcc/ada/sem_ch4.adb
...@@ -1463,6 +1463,25 @@ package body Sem_Ch4 is ...@@ -1463,6 +1463,25 @@ package body Sem_Ch4 is
-- actuals. -- actuals.
Check_Function_Writable_Actuals (N); Check_Function_Writable_Actuals (N);
-- The return type of the function may be incomplete. This can be
-- the case if the type is a generic formal, or a limited view. It
-- can also happen when the function declaration appears before the
-- full view of the type (which is legal in Ada 2012) and the call
-- appears in a different unit, in which case the incomplete view
-- must be replaced with the full view to prevent subsequent type
-- errors.
if Is_Incomplete_Type (Etype (N))
and then Present (Full_View (Etype (N)))
then
if Is_Entity_Name (Nam) then
Set_Etype (Nam, Full_View (Etype (N)));
Set_Etype (Entity (Nam), Full_View (Etype (N)));
end if;
Set_Etype (N, Full_View (Etype (N)));
end if;
end if; end if;
end Analyze_Call; end Analyze_Call;
......
gcc/ada/sem_eval.adb
...@@ -630,17 +630,17 @@ package body Sem_Eval is ...@@ -630,17 +630,17 @@ package body Sem_Eval is
-- to discrete and non-discrete types. -- to discrete and non-discrete types.
elsif (Nkind (Choice) = N_Subtype_Indication elsif (Nkind (Choice) = N_Subtype_Indication
or else (Is_Entity_Name (Choice) or else (Is_Entity_Name (Choice)
and then Is_Type (Entity (Choice)))) and then Is_Type (Entity (Choice))))
and then Has_Predicates (Etype (Choice)) and then Has_Predicates (Etype (Choice))
and then Has_Static_Predicate (Etype (Choice)) and then Has_Static_Predicate (Etype (Choice))
then then
if Is_Discrete_Type (Etype (Choice)) then if Is_Discrete_Type (Etype (Choice)) then
return Choices_Match return
(Expr, Static_Discrete_Predicate (Etype (Choice))); Choices_Match
(Expr, Static_Discrete_Predicate (Etype (Choice)));
elsif elsif Real_Or_String_Static_Predicate_Matches (Expr, Etype (Choice))
Real_Or_String_Static_Predicate_Matches (Expr, Etype (Choice))
then then
return Match; return Match;
......
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