diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 29 | ||||
| -rw-r--r-- | gcc/ada/a-cfdlli.adb | 197 | ||||
| -rw-r--r-- | gcc/ada/a-cfdlli.ads | 1529 | ||||
| -rw-r--r-- | gcc/ada/a-cofuba.adb | 16 | ||||
| -rw-r--r-- | gcc/ada/a-cofuma.adb | 23 | ||||
| -rw-r--r-- | gcc/ada/a-cofuma.ads | 73 | ||||
| -rw-r--r-- | gcc/ada/a-cofuse.adb | 8 | ||||
| -rw-r--r-- | gcc/ada/a-cofuse.ads | 42 | ||||
| -rw-r--r-- | gcc/ada/a-cofuve.adb | 37 | ||||
| -rw-r--r-- | gcc/ada/a-cofuve.ads | 122 | ||||
| -rw-r--r-- | gcc/ada/exp_attr.adb | 24 | ||||
| -rw-r--r-- | gcc/ada/exp_disp.adb | 30 | ||||
| -rw-r--r-- | gcc/ada/sem_attr.adb | 31 | ||||
| -rw-r--r-- | gcc/ada/sem_ch4.adb | 19 | ||||
| -rw-r--r-- | gcc/ada/sem_eval.adb | 12 |
15 files changed, 1252 insertions, 940 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index d6f3ec9..3baef3c 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,32 @@ +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> * exp_unst.ads: Fix typos in comments. diff --git a/gcc/ada/a-cfdlli.adb b/gcc/ada/a-cfdlli.adb index d799dcc..84596ee 100644 --- a/gcc/ada/a-cfdlli.adb +++ b/gcc/ada/a-cfdlli.adb @@ -30,7 +30,6 @@ with System; use type System.Address; package body Ada.Containers.Formal_Doubly_Linked_Lists with SPARK_Mode => Off is - ----------------------- -- Local Subprograms -- ----------------------- @@ -55,8 +54,9 @@ is -- "=" -- --------- - function "=" (Left, Right : List) return Boolean is - LI, RI : Count_Type; + function "=" (Left : List; Right : List) return Boolean is + LI : Count_Type; + RI : Count_Type; begin if Left'Address = Right'Address then @@ -230,10 +230,10 @@ is N := N + 1; end loop; - P.Free := Source.Free; + P.Free := Source.Free; P.Length := Source.Length; - P.First := Source.First; - P.Last := Source.Last; + P.First := Source.First; + P.Last := Source.Last; if P.Free >= 0 then N := Source.Capacity + 1; @@ -250,14 +250,12 @@ is -- Delete -- ------------ - procedure Delete - (Container : in out List; - Position : in out Cursor) - is + procedure Delete (Container : in out List; Position : in out Cursor) is begin - Delete (Container => Container, - Position => Position, - Count => 1); + Delete + (Container => Container, + Position => Position, + Count => 1); end Delete; procedure Delete @@ -272,8 +270,7 @@ is if not Has_Element (Container => Container, Position => Position) then - raise Constraint_Error with - "Position cursor has no element"; + raise Constraint_Error with "Position cursor has no element"; end if; pragma Assert (Vet (Container, Position), "bad cursor in Delete"); @@ -317,6 +314,7 @@ is Free (Container, X); end loop; + Position := No_Element; end Delete; @@ -324,17 +322,14 @@ is -- Delete_First -- ------------------ - procedure Delete_First (Container : in out List) - is + procedure Delete_First (Container : in out List) is begin - Delete_First (Container => Container, - Count => 1); + Delete_First + (Container => Container, + Count => 1); end Delete_First; - procedure Delete_First - (Container : in out List; - Count : Count_Type) - is + procedure Delete_First (Container : in out List; Count : Count_Type) is N : Node_Array renames Container.Nodes; X : Count_Type; @@ -365,17 +360,14 @@ is -- Delete_Last -- ----------------- - procedure Delete_Last (Container : in out List) - is + procedure Delete_Last (Container : in out List) is begin - Delete_Last (Container => Container, - Count => 1); + Delete_Last + (Container => Container, + Count => 1); end Delete_Last; - procedure Delete_Last - (Container : in out List; - Count : Count_Type) - is + procedure Delete_Last (Container : in out List; Count : Count_Type) is N : Node_Array renames Container.Nodes; X : Count_Type; @@ -412,8 +404,7 @@ is is begin if not Has_Element (Container => Container, Position => Position) then - raise Constraint_Error with - "Position cursor has no element"; + raise Constraint_Error with "Position cursor has no element"; end if; return Container.Nodes (Position.Node).Element; @@ -442,8 +433,7 @@ is if Position.Node /= 0 and then not Has_Element (Container, Position) then - raise Constraint_Error with - "Position cursor has no element"; + raise Constraint_Error with "Position cursor has no element"; end if; while From /= 0 loop @@ -476,6 +466,7 @@ is function First_Element (Container : List) return Element_Type is F : constant Count_Type := Container.First; + begin if F = 0 then raise Constraint_Error with "list is empty"; @@ -500,8 +491,12 @@ is -- M_Elements_Reversed -- ------------------------- - function M_Elements_Reversed (Left, Right : M.Sequence) return Boolean is + function M_Elements_Reversed + (Left : M.Sequence; + Right : M.Sequence) return Boolean + is L : constant Count_Type := M.Length (Left); + begin if L /= M.Length (Right) then return False; @@ -533,11 +528,13 @@ is declare Found : Boolean := False; J : Count_Type := Fst; + begin while not Found and J <= Lst loop if Element (Left, I) = Element (Right, J + Offset) then Found := True; end if; + J := J + 1; end loop; @@ -546,6 +543,7 @@ is end if; end; end loop; + return True; end M_Elements_Shuffle; @@ -556,7 +554,8 @@ is function M_Elements_Swapped (Left : M.Sequence; Right : M.Sequence; - X, Y : Positive_Count_Type) return Boolean + X : Positive_Count_Type; + Y : Positive_Count_Type) return Boolean is begin if M.Length (Left) /= M.Length (Right) @@ -584,13 +583,16 @@ is function Model (Container : List) return M.Sequence is Position : Count_Type := Container.First; R : M.Sequence; + begin - -- Can't use First, Next or Element here, since they depend - -- on models for their postconditions + -- Can't use First, Next or Element here, since they depend on models + -- for their postconditions. + while Position /= 0 loop R := M.Add (R, Container.Nodes (Position).Element); Position := Container.Nodes (Position).Next; end loop; + return R; end Model; @@ -607,10 +609,10 @@ is begin for C of P_Left loop 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 M.Get (M_Left, P.Get (P_Left, C)) - /= M.Get (M_Right, P.Get (P_Right, C)) + or else M.Get (M_Left, P.Get (P_Left, C)) /= + M.Get (M_Right, P.Get (P_Right, C)) then return False; end if; @@ -645,18 +647,22 @@ is for Cu of Big loop declare Pos : constant Positive_Count_Type := P.Get (Big, Cu); + begin 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 return False; end if; + elsif Pos >= Cut + Count then if not P.Has_Key (Small, Cu) or else Pos /= P.Get (Small, Cu) + Count then return False; end if; + else if P.Has_Key (Small, Cu) then return False; @@ -664,6 +670,7 @@ is end if; end; end loop; + return True; end P_Positions_Shifted; @@ -674,17 +681,20 @@ is function P_Positions_Swapped (Left : P.Map; Right : P.Map; - X, Y : Cursor) return Boolean + X : Cursor; + Y : Cursor) return Boolean is begin - if not P.Has_Key (Left, X) or not P.Has_Key (Left, Y) - or not P.Has_Key (Right, X) or not P.Has_Key (Right, Y) + if not P.Has_Key (Left, X) + or not P.Has_Key (Left, Y) + or not P.Has_Key (Right, X) + or not P.Has_Key (Right, Y) then return False; end if; 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 return False; end if; @@ -698,7 +708,7 @@ is for C of Right loop if not P.Has_Key (Left, C) 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 return False; end if; @@ -727,19 +737,24 @@ is for Cu of Big loop declare Pos : constant Positive_Count_Type := P.Get (Big, Cu); + begin 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 return False; end if; + elsif Pos >= Cut + Count then return False; + elsif P.Has_Key (Small, Cu) then return False; end if; end; end loop; + return True; end P_Positions_Truncated; @@ -748,18 +763,21 @@ is --------------- function Positions (Container : List) return P.Map is + I : Count_Type := 1; Position : Count_Type := Container.First; R : P.Map; - I : Count_Type := 1; + begin - -- Can't use First, Next or Element here, since they depend - -- on models for their postconditions + -- Can't use First, Next or Element here, since they depend on models + -- for their postconditions. + while Position /= 0 loop R := P.Add (R, (Node => Position), I); pragma Assert (P.Length (R) = I); Position := Container.Nodes (Position).Next; I := I + 1; end loop; + return R; end Positions; @@ -769,10 +787,7 @@ is -- Free -- ---------- - procedure Free - (Container : in out List; - X : Count_Type) - is + procedure Free (Container : in out List; X : Count_Type) is pragma Assert (X > 0); pragma Assert (X <= Container.Capacity); @@ -846,18 +861,22 @@ is declare E1 : Element_Type := Element (Container, 1); + begin for I in 2 .. M.Length (Container) loop declare E2 : constant Element_Type := Element (Container, I); + begin if E2 < E1 then return False; end if; + E1 := E2; end; end loop; end; + return True; end M_Elements_Sorted; @@ -865,10 +884,7 @@ is -- Merge -- ----------- - procedure Merge - (Target : in out List; - Source : in out List) - is + procedure Merge (Target : in out List; Source : in out List) is LN : Node_Array renames Target.Nodes; RN : Node_Array renames Source.Nodes; LI : Cursor; @@ -882,18 +898,20 @@ is LI := First (Target); RI := First (Source); while RI.Node /= 0 loop - pragma Assert (RN (RI.Node).Next = 0 - or else not (RN (RN (RI.Node).Next).Element < - RN (RI.Node).Element)); + pragma Assert + (RN (RI.Node).Next = 0 + or else not (RN (RN (RI.Node).Next).Element < + RN (RI.Node).Element)); if LI.Node = 0 then Splice (Target, No_Element, Source); return; end if; - pragma Assert (LN (LI.Node).Next = 0 - or else not (LN (LN (LI.Node).Next).Element < - LN (LI.Node).Element)); + pragma Assert + (LN (LI.Node).Next = 0 + or else not (LN (LN (LI.Node).Next).Element < + LN (LI.Node).Element)); if RN (RI.Node).Element < LN (LI.Node).Element then declare @@ -917,14 +935,14 @@ is procedure Sort (Container : in out List) is N : Node_Array renames Container.Nodes; - procedure Partition (Pivot, Back : Count_Type); - procedure Sort (Front, Back : Count_Type); + procedure Partition (Pivot : Count_Type; Back : Count_Type); + procedure Sort (Front : Count_Type; Back : Count_Type); --------------- -- Partition -- --------------- - procedure Partition (Pivot, Back : Count_Type) is + procedure Partition (Pivot : Count_Type; Back : Count_Type) is Node : Count_Type; begin @@ -968,7 +986,7 @@ is -- Sort -- ---------- - procedure Sort (Front, Back : Count_Type) is + procedure Sort (Front : Count_Type; Back : Count_Type) is Pivot : Count_Type; begin @@ -1060,11 +1078,12 @@ is Position : out Cursor) is begin - Insert (Container => Container, - Before => Before, - New_Item => New_Item, - Position => Position, - Count => 1); + Insert + (Container => Container, + Before => Before, + New_Item => New_Item, + Position => Position, + Count => 1); end Insert; procedure Insert @@ -1074,6 +1093,7 @@ is Count : Count_Type) is Position : Cursor; + begin Insert (Container, Before, New_Item, Position, Count); end Insert; @@ -1084,6 +1104,7 @@ is New_Item : Element_Type) is Position : Cursor; + begin Insert (Container, Before, New_Item, Position, 1); end Insert; @@ -1171,6 +1192,7 @@ is function Last_Element (Container : List) return Element_Type is L : constant Count_Type := Container.Last; + begin if L = 0 then raise Constraint_Error with "list is empty"; @@ -1192,10 +1214,7 @@ is -- Move -- ---------- - procedure Move - (Target : in out List; - Source : in out List) - is + procedure Move (Target : in out List; Source : in out List) is N : Node_Array renames Source.Nodes; X : Count_Type; @@ -1295,10 +1314,7 @@ is -- Prepend -- ------------- - procedure Prepend - (Container : in out List; - New_Item : Element_Type) - is + procedure Prepend (Container : in out List; New_Item : Element_Type) is begin Insert (Container, First (Container), New_Item, 1); end Prepend; @@ -1363,13 +1379,13 @@ is I : Count_Type := Container.First; J : Count_Type := Container.Last; - procedure Swap (L, R : Count_Type); + procedure Swap (L : Count_Type; R : Count_Type); ---------- -- Swap -- ---------- - procedure Swap (L, R : Count_Type) is + procedure Swap (L : Count_Type; R : Count_Type) is LN : constant Count_Type := N (L).Next; LP : constant Count_Type := N (L).Prev; @@ -1414,7 +1430,7 @@ is pragma Assert (N (Container.Last).Next = 0); Container.First := J; - Container.Last := I; + Container.Last := I; loop Swap (L => I, R => J); @@ -1642,7 +1658,8 @@ is procedure Swap (Container : in out List; - I, J : Cursor) + I : Cursor; + J : Cursor) is begin if I.Node = 0 then @@ -1679,9 +1696,11 @@ is procedure Swap_Links (Container : in out List; - I, J : Cursor) + I : Cursor; + J : Cursor) is - I_Next, J_Next : Cursor; + I_Next : Cursor; + J_Next : Cursor; begin if I.Node = 0 then diff --git a/gcc/ada/a-cfdlli.ads b/gcc/ada/a-cfdlli.ads index 0fce673..b60a6fe 100644 --- a/gcc/ada/a-cfdlli.ads +++ b/gcc/ada/a-cfdlli.ads @@ -34,6 +34,7 @@ with Ada.Containers.Functional_Maps; generic type Element_Type is private; + package Ada.Containers.Formal_Doubly_Linked_Lists with SPARK_Mode is @@ -67,17 +68,25 @@ is package M is new Ada.Containers.Functional_Vectors (Index_Type => Positive_Count_Type, Element_Type => Element_Type); - function "=" (Left, Right : M.Sequence) return Boolean renames M."="; - function "<" (Left, Right : M.Sequence) return Boolean renames M."<"; - function "<=" (Left, 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 "<=" + (Left : M.Sequence; + Right : M.Sequence) return Boolean renames M."<="; function M_Elements_Shuffle (Left : M.Sequence; Right : M.Sequence; Fst : Positive_Count_Type; Lst : Count_Type; - Offset : Count_Type'Base) - return Boolean + Offset : Count_Type'Base) return Boolean -- The slice from Fst to Lst in Left contains the same elements than the -- same slide shifted by Offset in Right with @@ -87,33 +96,33 @@ is and Offset in 1 - Fst .. M.Length (Right) - Lst, Post => M_Elements_Shuffle'Result = - (for all J in Fst + Offset .. Lst + Offset => - (for some I in Fst .. Lst => - Element (Left, I) = Element (Right, J))); + (for all J in Fst + Offset .. Lst + Offset => + (for some I in Fst .. Lst => + Element (Left, I) = Element (Right, J))); 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 with Global => null, Post => M_Elements_Reversed'Result = - (M.Length (Left) = M.Length (Right) - and - (for all I in 1 .. M.Length (Left) => - Element (Left, I) - = Element (Right, M.Length (Left) - I + 1)) - and - (for all I in 1 .. M.Length (Left) => - Element (Right, I) - = Element (Left, M.Length (Left) - I + 1))); + (M.Length (Left) = M.Length (Right) + and (for all I in 1 .. M.Length (Left) => + Element (Left, I) = + Element (Right, M.Length (Left) - I + 1)) + and (for all I in 1 .. M.Length (Left) => + Element (Right, I) = + Element (Left, M.Length (Left) - I + 1))); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed); function M_Elements_Swapped (Left : M.Sequence; Right : M.Sequence; - X, Y : Positive_Count_Type) - return Boolean + X : Positive_Count_Type; + Y : Positive_Count_Type) return Boolean -- Elements stored at X and Y are reversed in Left and Right with Global => null, @@ -121,17 +130,23 @@ is Post => M_Elements_Swapped'Result = (M.Length (Left) = M.Length (Right) - and Element (Left, X) = Element (Right, Y) - and Element (Left, Y) = Element (Right, X) - and M.Equal_Except (Left, Right, X, Y)); + and Element (Left, X) = Element (Right, Y) + and Element (Left, Y) = Element (Right, X) + and M.Equal_Except (Left, Right, X, Y)); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped); package P is new Ada.Containers.Functional_Maps (Key_Type => Cursor, Element_Type => Positive_Count_Type, 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 (Small : P.Map; @@ -143,27 +158,31 @@ is Post => P_Positions_Shifted'Result = - -- Big contains all cursors of Small - (P.Keys_Included (Small, Big) + -- Big contains all cursors of Small - -- Cursors located before Cut are not moved, cursors located after - -- 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))) + P.Keys_Included (Small, Big) - -- 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)); + -- Cursors located before Cut are not moved, cursors located + -- after 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. + + 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 (Left : 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 -- are reversed. with @@ -171,11 +190,12 @@ is Global => null, Post => P_Positions_Swapped'Result = - (P.Same_Keys (Left, Right) - and P.Elements_Equal_Except (Left, Right, X, Y) - and P.Has_Key (Left, X) and P.Has_Key (Left, Y) - and P.Get (Left, X) = P.Get (Right, Y) - and P.Get (Left, Y) = P.Get (Right, X)); + (P.Same_Keys (Left, Right) + and P.Elements_Equal_Except (Left, Right, X, Y) + and P.Has_Key (Left, X) + and P.Has_Key (Left, Y) + and P.Get (Left, X) = P.Get (Right, Y) + and P.Get (Left, Y) = P.Get (Right, X)); function P_Positions_Truncated (Small : P.Map; @@ -188,14 +208,16 @@ is Post => P_Positions_Truncated'Result = - -- Big contains all cursors of Small at the same position - (Small <= Big + -- Big contains all cursors of Small at the same position + + (Small <= Big - -- 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)); + -- 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 Mapping_Preserved (M_Left : M.Sequence; @@ -206,16 +228,18 @@ is Ghost, Global => null, Post => - (if Mapping_Preserved'Result then + (if Mapping_Preserved'Result then -- Left and Right contain the same cursors + P.Same_Keys (P_Left, P_Right) - -- Mappings from cursors to elements induced by M_Left, P_Left - -- and M_Right, P_Right are the same. - and (for all C of P_Left => - M.Get (M_Left, P.Get (P_Left, C)) - = M.Get (M_Right, P.Get (P_Right, C)))); + -- Mappings from cursors to elements induced by M_Left, P_Left + -- and M_Right, P_Right are the same. + + and (for all C of P_Left => + 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 -- The highlevel model of a list is a sequence of elements. Cursors are @@ -232,19 +256,23 @@ is Ghost, Global => null, - Post => not P.Has_Key (Positions'Result, No_Element) - -- Positions of cursors are smaller than the container's length. - and then - (for all I of Positions'Result => - P.Get (Positions'Result, I) in 1 .. Length (Container) - - -- No two cursors have the same position. Note that we do not - -- 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 => + Post => + not P.Has_Key (Positions'Result, No_Element) + + -- Positions of cursors are smaller than the container's length. + + and then + (for all I of Positions'Result => + P.Get (Positions'Result, I) in 1 .. Length (Container) + + -- No two cursors have the same position. Note that we do not + -- 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) - then I = J))); + then I = J))); procedure Lift_Abstraction_Level (Container : List) with -- Lift_Abstraction_Level is a ghost procedure that does nothing but @@ -257,15 +285,17 @@ is Ghost, Global => null, Post => - (for all Elt of Model (Container) => - (for some I of Positions (Container) => - M.Get (Model (Container), P.Get (Positions (Container), I)) - = Elt)); - - function Element (S : M.Sequence; I : Count_Type) return Element_Type - renames M.Get; + (for all Elt of Model (Container) => + (for some I of Positions (Container) => + M.Get (Model (Container), P.Get (Positions (Container), I)) = + Elt)); + + function Element + (S : M.Sequence; + I : Count_Type) return Element_Type renames M.Get; -- To improve readability of contracts, we rename the function used to -- access an element in the model to Element. + end Formal_Model; use Formal_Model; @@ -289,10 +319,13 @@ is function Copy (Source : List; Capacity : Count_Type := 0) return List with Global => null, Pre => Capacity = 0 or else Capacity >= Source.Capacity, - Post => Model (Copy'Result) = Model (Source) - and Positions (Copy'Result) = Positions (Source) - and (if Capacity = 0 then Copy'Result.Capacity = Source.Capacity - else Copy'Result.Capacity = Capacity); + Post => + Model (Copy'Result) = Model (Source) + and Positions (Copy'Result) = Positions (Source) + and (if Capacity = 0 then + Copy'Result.Capacity = Source.Capacity + else + Copy'Result.Capacity = Capacity); function Element (Container : List; @@ -302,8 +335,7 @@ is Pre => Has_Element (Container, Position), Post => Element'Result = - Element (Model (Container), - P.Get (Positions (Container), Position)); + Element (Model (Container), P.Get (Positions (Container), Position)); pragma Annotate (GNATprove, Inline_For_Proof, Element); procedure Replace_Element @@ -313,25 +345,30 @@ is with Global => null, 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 - and Element (Model (Container), P.Get (Positions (Container), Position)) - = New_Item + -- The element at the position of Position in Container is New_Item - -- Other elements are preserved - and M.Equal_Except (Model (Container)'Old, - Model (Container), - P.Get (Positions (Container), Position)); + and Element + (Model (Container), + P.Get (Positions (Container), Position)) = New_Item + + -- 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 Global => null, Pre => Target.Capacity >= Length (Source), - Post => Model (Target) = Model (Source'Old) - and Length (Source) = 0; + Post => Model (Target) = Model (Source'Old) and Length (Source) = 0; procedure Insert (Container : in out List; @@ -340,59 +377,69 @@ is with Global => null, Pre => - Length (Container) < Container.Capacity - and then (Has_Element (Container, Before) - or else Before = No_Element), + Length (Container) < Container.Capacity + and then (Has_Element (Container, Before) + or else Before = No_Element), Post => Length (Container) = Length (Container)'Old + 1, Contract_Cases => (Before = No_Element => -- Positions contains a new mapping from the last cursor of -- Container to its length. + P.Get (Positions (Container), Last (Container)) = Length (Container) - -- Other cursors come from Container'Old - and P.Keys_Included_Except - (Left => Positions (Container), - Right => Positions (Container)'Old, - New_Key => Last (Container)) + -- Other cursors come from Container'Old + + and P.Keys_Included_Except + (Left => Positions (Container), + Right => Positions (Container)'Old, + New_Key => Last (Container)) - -- Cursors of Container'Old keep the same position - and Positions (Container)'Old <= Positions (Container) + -- Cursors of Container'Old keep the same position - -- Model contains a new element New_Item at the end - and Element (Model (Container), Length (Container)) = New_Item + and Positions (Container)'Old <= Positions (Container) - -- Elements of Container'Old are preserved - and Model (Container)'Old <= Model (Container), - others => + -- 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), + + others => + + -- The elements of Container located before Before are preserved - -- The elements of Container located before Before are preserved. M.Range_Equal (Left => Model (Container)'Old, Right => Model (Container), Fst => 1, Lst => P.Get (Positions (Container)'Old, Before) - 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 + -- Other elements are shifted by 1 - -- 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))); + 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 P_Positions_Shifted + (Positions (Container)'Old, + Positions (Container), + Cut => P.Get (Positions (Container)'Old, Before))); procedure Insert (Container : in out List; @@ -400,66 +447,75 @@ is New_Item : Element_Type; Count : Count_Type) with - Global => null, - Pre => - Length (Container) <= Container.Capacity - Count - and then (Has_Element (Container, Before) - or else Before = No_Element), + Global => null, + Pre => + Length (Container) <= Container.Capacity - Count + and then (Has_Element (Container, Before) + or else Before = No_Element), Post => Length (Container) = Length (Container)'Old + Count, Contract_Cases => (Before = No_Element => -- The elements of Container are preserved + M.Range_Equal (Left => Model (Container)'Old, Right => Model (Container), Fst => 1, Lst => Length (Container)'Old) - -- 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) - - -- A 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), - others => + -- 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) + + -- A 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), + + others => -- The elements of Container located before Before are preserved + M.Range_Equal (Left => Model (Container)'Old, Right => Model (Container), Fst => 1, Lst => P.Get (Positions (Container)'Old, Before) - 1) - -- Other elements are shifted by Count. - and M.Range_Shifted - (Left => Model (Container)'Old, - Right => Model (Container), - Fst => P.Get (Positions (Container)'Old, Before), - Lst => Length (Container)'Old, - Offset => Count) - - -- Container contains Count times New_Item after position Before - and M.Constant_Range - (Container => Model (Container), - Fst => P.Get (Positions (Container)'Old, Before), - Lst => - P.Get (Positions (Container)'Old, Before) - 1 + Count, - Item => New_Item) - - -- Count cursors have been inserted at position Before in Container - and P_Positions_Shifted - (Positions (Container)'Old, - Positions (Container), - Cut => P.Get (Positions (Container)'Old, Before), - Count => Count)); + -- Other elements are shifted by Count + + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => P.Get (Positions (Container)'Old, Before), + Lst => Length (Container)'Old, + Offset => Count) + + -- Container contains Count times New_Item after position Before + + and M.Constant_Range + (Container => Model (Container), + Fst => P.Get (Positions (Container)'Old, Before), + Lst => + P.Get (Positions (Container)'Old, Before) - 1 + Count, + Item => New_Item) + + -- Count cursors have been inserted at position Before in + -- Container. + + and P_Positions_Shifted + (Positions (Container)'Old, + Positions (Container), + Cut => P.Get (Positions (Container)'Old, Before), + Count => Count)); procedure Insert (Container : in out List; @@ -469,47 +525,52 @@ is with Global => null, Pre => - Length (Container) < Container.Capacity - and then (Has_Element (Container, Before) - or else Before = No_Element), + Length (Container) < Container.Capacity + and then (Has_Element (Container, Before) + or else Before = No_Element), Post => Length (Container) = Length (Container)'Old + 1 -- 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 -- No_Element. + and P.Has_Key (Positions (Container), Position) - and (if Before = No_Element - then P.Get (Positions (Container), Position) - = Length (Container) - else P.Get (Positions (Container), Position) - = P.Get (Positions (Container)'Old, Before)) + and (if Before = No_Element then + P.Get (Positions (Container), Position) = Length (Container) + else + P.Get (Positions (Container), Position) = + 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 - (Left => Model (Container)'Old, - Right => Model (Container), - Fst => 1, - Lst => P.Get (Positions (Container), Position) - 1) + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => 1, + Lst => P.Get (Positions (Container), Position) - 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), Position), - Lst => Length (Container)'Old, - Offset => 1) + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => P.Get (Positions (Container), Position), + Lst => Length (Container)'Old, + Offset => 1) -- New_Item is stored at Position in Container + and Element - (Model (Container), P.Get (Positions (Container), Position)) - = New_Item + (Model (Container), + P.Get (Positions (Container), Position)) = New_Item -- A new cursor has been inserted at position Position in Container + and P_Positions_Shifted - (Positions (Container)'Old, - Positions (Container), - Cut => P.Get (Positions (Container), Position)); + (Positions (Container)'Old, + Positions (Container), + Cut => P.Get (Positions (Container), Position)); procedure Insert (Container : in out List; @@ -520,80 +581,89 @@ is with Global => null, Pre => - Length (Container) <= Container.Capacity - Count - and then (Has_Element (Container, Before) - or else Before = No_Element), + Length (Container) <= Container.Capacity - Count + and then (Has_Element (Container, Before) + or else Before = No_Element), Post => Length (Container) = Length (Container)'Old + Count, Contract_Cases => - (Count = 0 => Position = Before - and Model (Container) = Model (Container)'Old - and Positions (Container) = Positions (Container)'Old, + (Count = 0 => + Position = Before + 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 -- Before if it is valid in Container or at the end if it is -- 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 - (Container : in out List; - New_Item : Element_Type) - with + 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 (Container : in out List; New_Item : Element_Type) with Global => null, Pre => Length (Container) < Container.Capacity, Post => Length (Container) = Length (Container)'Old + 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) + -- Elements are shifted by 1 - -- New_Item is the first element of Container - and Element (Model (Container), 1) = New_Item + and M.Range_Shifted + (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 - and P_Positions_Shifted - (Positions (Container)'Old, - Positions (Container), - Cut => 1); + -- New_Item is the first element of Container + + and Element (Model (Container), 1) = New_Item + + -- A new cursor has been inserted at the beginning of Container + + and P_Positions_Shifted + (Positions (Container)'Old, + Positions (Container), + Cut => 1); procedure Prepend (Container : in out List; @@ -605,55 +675,61 @@ is Post => Length (Container) = Length (Container)'Old + 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); + -- Elements are shifted by Count - procedure Append - (Container : in out List; - New_Item : Element_Type) - with + 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 (Container : in out List; New_Item : Element_Type) with Global => null, 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 - -- Container to its length. - and P.Get (Positions (Container), Last (Container)) - = Length (Container) + -- Positions contains a new mapping from the last cursor of Container + -- to its length. - -- Other cursors come from Container'Old - and P.Keys_Included_Except - (Left => Positions (Container), - Right => Positions (Container)'Old, - New_Key => Last (Container)) + and P.Get (Positions (Container), Last (Container)) = + Length (Container) - -- Cursors of Container'Old keep the same position - and Positions (Container)'Old <= Positions (Container) + -- Other cursors come from Container'Old - -- Model contains a new element New_Item at the end - and Element (Model (Container), Length (Container)) = New_Item + and P.Keys_Included_Except + (Left => Positions (Container), + Right => Positions (Container)'Old, + New_Key => Last (Container)) - -- Elements of Container'Old are preserved - and Model (Container)'Old <= Model (Container); + -- 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 Element (Model (Container), Length (Container)) = New_Item + + -- Elements of Container'Old are preserved + + and Model (Container)'Old <= Model (Container); procedure Append (Container : in out List; @@ -665,55 +741,59 @@ is Post => Length (Container) = Length (Container)'Old + Count - -- 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); + -- The elements of Container are preserved - procedure Delete - (Container : in out List; - Position : in out Cursor) - with + 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 (Container : in out List; Position : in out Cursor) with Global => null, Pre => Has_Element (Container, Position), Post => Length (Container) = Length (Container)'Old - 1 - -- Position is set to No_Element - and Position = No_Element + -- Position is set to 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) + and Position = No_Element - -- 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) + -- The elements of Container located before Position are preserved. - -- Position has been removed from Container - and P_Positions_Shifted - (Positions (Container), - Positions (Container)'Old, - Cut => P.Get (Positions (Container)'Old, Position'Old)); + 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 + + 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 (Container : in out List; @@ -723,144 +803,157 @@ is Global => null, Pre => Has_Element (Container, Position), Post => - Length (Container) in Length (Container)'Old - Count - .. Length (Container)'Old + Length (Container) in + Length (Container)'Old - Count .. Length (Container)'Old - -- Position is set to No_Element - and Position = No_Element + -- Position is set to 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 => -- 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) = P.Get (Positions (Container)'Old, Position'Old) - 1 - -- At most Count cursors have been removed at the end of Container - and P_Positions_Truncated - (Positions (Container), - Positions (Container)'Old, - Cut => P.Get (Positions (Container)'Old, Position'Old), - Count => Count), + -- At most Count cursors have been removed at the end of Container + + and P_Positions_Truncated + (Positions (Container), + Positions (Container)'Old, + Cut => P.Get (Positions (Container)'Old, Position'Old), + Count => Count), + others => Length (Container) = Length (Container)'Old - 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)); + -- Other elements are shifted by Count - procedure Delete_First (Container : in out List) - with + 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) with Global => null, Pre => not Is_Empty (Container), Post => Length (Container) = Length (Container)'Old - 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 elements of Container are shifted by 1 - -- The first cursor of Container has been removed - and P_Positions_Shifted - (Positions (Container), - Positions (Container)'Old, - Cut => 1); + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => 2, + Lst => Length (Container)'Old, + Offset => -1) - procedure Delete_First - (Container : in out List; - Count : Count_Type) - with + -- The first cursor of Container has been removed + + and P_Positions_Shifted + (Positions (Container), + Positions (Container)'Old, + Cut => 1); + + procedure Delete_First (Container : in out List; Count : Count_Type) with Global => null, Contract_Cases => -- All the elements of Container have been erased - (Length (Container) <= Count => Length (Container) = 0, + + (Length (Container) <= Count => + Length (Container) = 0, + others => Length (Container) = Length (Container)'Old - Count - -- Elements of Container are shifted by Count - and M.Range_Shifted - (Left => Model (Container)'Old, - Right => Model (Container), - Fst => Count + 1, - Lst => Length (Container)'Old, - Offset => -Count) + -- Elements of Container are shifted by Count - -- The first Count cursors have been removed from Container - and P_Positions_Shifted - (Positions (Container), - Positions (Container)'Old, - Cut => 1, - Count => Count)); + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => Count + 1, + Lst => Length (Container)'Old, + Offset => -Count) - procedure Delete_Last (Container : in out List) - with + -- The first Count cursors have been removed from Container + + and P_Positions_Shifted + (Positions (Container), + Positions (Container)'Old, + Cut => 1, + Count => Count)); + + procedure Delete_Last (Container : in out List) with Global => null, Pre => not Is_Empty (Container), Post => Length (Container) = Length (Container)'Old - 1 - -- The elements of Container are preserved. - and Model (Container) <= Model (Container)'Old + -- The elements of Container are preserved - -- The last cursor of Container has been removed - and not P.Has_Key (Positions (Container), Last (Container)'Old) + and Model (Container) <= Model (Container)'Old - -- Other cursors are still valid - and P.Keys_Included_Except - (Left => Positions (Container)'Old, - Right => Positions (Container)'Old, - New_Key => Last (Container)'Old) + -- The last cursor of Container has been removed - -- The positions of other cursors are preserved - and Positions (Container) <= Positions (Container)'Old; + and not P.Has_Key (Positions (Container), Last (Container)'Old) - procedure Delete_Last - (Container : in out List; - Count : Count_Type) - with - Global => null, + -- Other cursors are still valid + + 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 Positions (Container) <= Positions (Container)'Old; + + procedure Delete_Last (Container : in out List; Count : Count_Type) with + Global => null, Contract_Cases => -- All the elements of Container have been erased - (Length (Container) <= Count => Length (Container) = 0, - others => + (Length (Container) <= Count => + Length (Container) = 0, + + others => Length (Container) = Length (Container)'Old - Count - -- The elements of Container are preserved. - and Model (Container) <= Model (Container)'Old + -- The elements of Container are preserved + + and Model (Container) <= Model (Container)'Old - -- At most Count cursors have been removed at the end of Container - and P_Positions_Truncated - (Positions (Container), - Positions (Container)'Old, - Cut => Length (Container) + 1, - Count => Count)); + -- At most Count cursors have been removed at the end of Container + + and P_Positions_Truncated + (Positions (Container), + Positions (Container)'Old, + Cut => Length (Container) + 1, + Count => Count)); procedure Reverse_Elements (Container : in out List) with Global => null, @@ -868,7 +961,8 @@ is procedure Swap (Container : in out List; - I, J : Cursor) + I : Cursor; + J : Cursor) with Global => null, Pre => Has_Element (Container, I) and then Has_Element (Container, J), @@ -877,11 +971,13 @@ is (Model (Container)'Old, Model (Container), X => P.Get (Positions (Container)'Old, I), Y => P.Get (Positions (Container)'Old, J)) - and Positions (Container) = Positions (Container)'Old; + + and Positions (Container) = Positions (Container)'Old; procedure Swap_Links (Container : in out List; - I, J : Cursor) + I : Cursor; + J : Cursor) with Global => null, Pre => Has_Element (Container, I) and then Has_Element (Container, J), @@ -890,8 +986,8 @@ is (Model (Container'Old), Model (Container), X => P.Get (Positions (Container)'Old, I), Y => P.Get (Positions (Container)'Old, J)) - and P_Positions_Swapped - (Positions (Container)'Old, Positions (Container), I, J); + and P_Positions_Swapped + (Positions (Container)'Old, Positions (Container), I, J); procedure Splice (Target : in out List; @@ -901,69 +997,77 @@ is with Global => null, Pre => - Length (Source) <= Target.Capacity - Length (Target) + Length (Source) <= Target.Capacity - Length (Target) and then (Has_Element (Target, Before) - or else Before = No_Element), + or else Before = No_Element), Post => Length (Source) = 0 - and Length (Target) = Length (Target)'Old + Length (Source)'Old, + and Length (Target) = Length (Target)'Old + Length (Source)'Old, Contract_Cases => (Before = No_Element => -- The elements of Target are preserved + M.Range_Equal (Left => Model (Target)'Old, Right => Model (Target), Fst => 1, Lst => Length (Target)'Old) - -- The elements of Source are appended to target, the order is not - -- specified. - and M_Elements_Shuffle - (Left => Model (Source)'Old, - Right => Model (Target), - Fst => 1, - Lst => Length (Source)'Old, - Offset => Length (Target)'Old) - - -- Cursors have been inserted at the end of Target - and P_Positions_Truncated - (Positions (Target)'Old, - Positions (Target), - Cut => Length (Target)'Old + 1, - Count => Length (Source)'Old), - others => + -- The elements of Source are appended to target, the order is not + -- specified. + + and M_Elements_Shuffle + (Left => Model (Source)'Old, + Right => Model (Target), + Fst => 1, + Lst => Length (Source)'Old, + Offset => Length (Target)'Old) + + -- Cursors have been inserted at the end of Target + + and P_Positions_Truncated + (Positions (Target)'Old, + Positions (Target), + Cut => Length (Target)'Old + 1, + Count => Length (Source)'Old), + + others => -- The elements of Target located before Before are preserved + M.Range_Equal (Left => Model (Target)'Old, Right => Model (Target), Fst => 1, Lst => P.Get (Positions (Target)'Old, Before) - 1) - -- The elements of Source are inserted before Before, the order is - -- not specified. + -- The elements of Source are inserted before Before, the order is + -- not specified. + and M_Elements_Shuffle - (Left => Model (Source)'Old, - Right => Model (Target), - Fst => 1, - Lst => Length (Source)'Old, - Offset => P.Get (Positions (Target)'Old, Before) - 1) + (Left => Model (Source)'Old, + Right => Model (Target), + Fst => 1, + Lst => Length (Source)'Old, + Offset => P.Get (Positions (Target)'Old, Before) - 1) -- Other elements are shifted by the length of Source + and M.Range_Shifted - (Left => Model (Target)'Old, - Right => Model (Target), - Fst => P.Get (Positions (Target)'Old, Before), - Lst => Length (Target)'Old, - Offset => Length (Source)'Old) + (Left => Model (Target)'Old, + Right => Model (Target), + Fst => P.Get (Positions (Target)'Old, Before), + Lst => Length (Target)'Old, + Offset => Length (Source)'Old) -- Cursors have been inserted at position Before in Target + and P_Positions_Shifted - (Positions (Target)'Old, - Positions (Target), - Cut => P.Get (Positions (Target)'Old, Before), - Count => Length (Source)'Old)); + (Positions (Target)'Old, + Positions (Target), + Cut => P.Get (Positions (Target)'Old, Before), + Count => Length (Source)'Old)); procedure Splice (Target : in out List; @@ -974,70 +1078,76 @@ is with Global => null, Pre => - (Has_Element (Target, Before) - or else Before = No_Element) - and then Has_Element (Source, Position) - and then Length (Target) < Target.Capacity, + (Has_Element (Target, Before) or else Before = No_Element) + and then Has_Element (Source, Position) + and then Length (Target) < Target.Capacity, Post => - Length (Target) = Length (Target)'Old + 1 - and Length (Source) = Length (Source)'Old - 1 + Length (Target) = Length (Target)'Old + 1 + and Length (Source) = Length (Source)'Old - 1 - -- 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 of Source located before Position are preserved - -- The elements located after Position are shifted by 1 - and M.Range_Shifted - (Left => Model (Source)'Old, - Right => Model (Source), - Fst => P.Get (Positions (Source)'Old, Position'Old) + 1, - Lst => Length (Source)'Old, - Offset => -1) + and M.Range_Equal + (Left => Model (Source)'Old, + Right => Model (Source), + Fst => 1, + Lst => P.Get (Positions (Source)'Old, Position'Old) - 1) - -- Position has been removed from Source - and P_Positions_Shifted - (Positions (Source), - Positions (Source)'Old, - Cut => P.Get (Positions (Source)'Old, Position'Old)) + -- The elements located after Position are shifted by 1 - -- Positions is valid in Target and it is located either before - -- Before if it is valid in Target or at the end if it is - -- No_Element. - and P.Has_Key (Positions (Target), Position) - and (if Before = No_Element - then P.Get (Positions (Target), Position) - = 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) + and M.Range_Shifted + (Left => Model (Source)'Old, + Right => Model (Source), + Fst => P.Get (Positions (Source)'Old, Position'Old) + 1, + Lst => Length (Source)'Old, + Offset => -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)); + -- Position has been removed from Source + + 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 + -- Before if it is valid in Target or at the end if it is No_Element. + + and P.Has_Key (Positions (Target), Position) + and (if Before = No_Element then + P.Get (Positions (Target), Position) = 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 + + 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 (Container : in out List; @@ -1046,17 +1156,18 @@ is with Global => null, 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), Post => Length (Container) = Length (Container)'Old, Contract_Cases => - (Before = Position => + (Before = Position => Model (Container) = Model (Container)'Old - and Positions (Container) = Positions (Container)'Old, + and Positions (Container) = Positions (Container)'Old, Before = No_Element => -- The elements located before Position are preserved + M.Range_Equal (Left => Model (Container)'Old, Right => Model (Container), @@ -1064,83 +1175,97 @@ is Lst => P.Get (Positions (Container)'Old, Position) - 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) + 1, - Lst => Length (Container)'Old, - Offset => -1) - - -- The last element of Container is the one that was previously - -- at Position. - and Element (Model (Container), Length (Container)) - = Element (Model (Container)'Old, - P.Get (Positions (Container)'Old, Position)) + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => P.Get (Positions (Container)'Old, Position) + 1, + Lst => Length (Container)'Old, + Offset => -1) + + -- The last element of Container is the one that was previously at + -- Position. + + and Element (Model (Container), Length (Container)) = + Element (Model (Container)'Old, + P.Get (Positions (Container)'Old, Position)) -- 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)), + (M_Left => Model (Container)'Old, + M_Right => Model (Container), + P_Left => Positions (Container)'Old, + P_Right => Positions (Container)), - others => + others => -- The elements located before Position and Before are preserved + M.Range_Equal (Left => Model (Container)'Old, Right => Model (Container), Fst => 1, - Lst => Count_Type'Min - (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 - (Left => Model (Container)'Old, - Right => Model (Container), - Fst => Count_Type'Max - (P.Get (Positions (Container)'Old, Position) + 1, - P.Get (Positions (Container)'Old, Before) + 1), - Lst => Length (Container)) - - -- The elements located after Before and before Position are shifted - -- by 1 to the right. - and M.Range_Shifted - (Left => Model (Container)'Old, - Right => Model (Container), - Fst => P.Get (Positions (Container)'Old, Before) + 1, - Lst => P.Get (Positions (Container)'Old, Position) - 1, - Offset => 1) - - -- The elements located after Position and before Before are shifted - -- by 1 to the left. - and M.Range_Shifted - (Left => Model (Container)'Old, - Right => Model (Container), - Fst => P.Get (Positions (Container)'Old, Position) + 1, - Lst => P.Get (Positions (Container)'Old, Before) - 1, - Offset => -1) - - -- The element previously at Position is now before Before - and Element (Model (Container), - P.Get (Positions (Container)'Old, Before)) - = Element (Model (Container)'Old, - P.Get (Positions (Container)'Old, Position)) - - -- 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))); + Lst => + Count_Type'Min + (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 + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => + Count_Type'Max + (P.Get (Positions (Container)'Old, Position) + 1, + P.Get (Positions (Container)'Old, Before) + 1), + Lst => Length (Container)) + + -- The elements located after Before and before Position are + -- shifted by 1 to the right. + + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => P.Get (Positions (Container)'Old, Before) + 1, + Lst => P.Get (Positions (Container)'Old, Position) - 1, + Offset => 1) + + -- The elements located after Position and before Before are + -- shifted by 1 to the left. + + and M.Range_Shifted + (Left => Model (Container)'Old, + Right => Model (Container), + Fst => P.Get (Positions (Container)'Old, Position) + 1, + Lst => P.Get (Positions (Container)'Old, Before) - 1, + Offset => -1) + + -- The element previously at Position is now before Before + + and Element (Model (Container), + P.Get (Positions (Container)'Old, Before)) = + Element (Model (Container)'Old, + P.Get (Positions (Container)'Old, Position)) + + -- 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 Global => null, Contract_Cases => - (Length (Container) = 0 => First'Result = No_Element, - others => Has_Element (Container, First'Result) - and P.Get (Positions (Container), First'Result) = 1); + (Length (Container) = 0 => + First'Result = No_Element, + + others => + Has_Element (Container, First'Result) + and P.Get (Positions (Container), First'Result) = 1); function First_Element (Container : List) return Element_Type with Global => null, @@ -1150,65 +1275,79 @@ is function Last (Container : List) return Cursor with Global => null, Contract_Cases => - (Length (Container) = 0 => Last'Result = No_Element, - others => Has_Element (Container, Last'Result) - and P.Get (Positions (Container), Last'Result) = Length (Container)); + (Length (Container) = 0 => + Last'Result = No_Element, + + others => + Has_Element (Container, Last'Result) + and P.Get (Positions (Container), Last'Result) = + Length (Container)); function Last_Element (Container : List) return Element_Type with Global => null, Pre => not Is_Empty (Container), - Post => Last_Element'Result - = M.Get (Model (Container), Length (Container)); + Post => + Last_Element'Result = M.Get (Model (Container), Length (Container)); function Next (Container : List; Position : Cursor) return Cursor with Global => null, - Pre => Has_Element (Container, Position) - or else Position = No_Element, + Pre => + Has_Element (Container, Position) or else Position = No_Element, Contract_Cases => (Position = No_Element - or else P.Get (Positions (Container), Position) = Length (Container) => - Next'Result = No_Element, - others => Has_Element (Container, Next'Result) - and then P.Get (Positions (Container), Next'Result) = - P.Get (Positions (Container), Position) + 1); + or else P.Get (Positions (Container), Position) = Length (Container) + => + Next'Result = No_Element, + + 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 Global => null, - Pre => Has_Element (Container, Position) - or else Position = No_Element, + Pre => + Has_Element (Container, Position) or else Position = No_Element, Contract_Cases => (Position = No_Element - or else P.Get (Positions (Container), Position) = Length (Container) => - Position = No_Element, - others => Has_Element (Container, Position) - and then P.Get (Positions (Container), Position) = - P.Get (Positions (Container), Position'Old) + 1); + or else P.Get (Positions (Container), Position) = Length (Container) + => + Position = No_Element, + + 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 Global => null, - Pre => Has_Element (Container, Position) - or else Position = No_Element, + Pre => + Has_Element (Container, Position) or else Position = No_Element, Contract_Cases => (Position = No_Element - or else P.Get (Positions (Container), Position) = 1 => + or else P.Get (Positions (Container), Position) = 1 + => Previous'Result = No_Element, + others => Has_Element (Container, Previous'Result) - and then P.Get (Positions (Container), Previous'Result) = - P.Get (Positions (Container), Position) - 1); + and then P.Get (Positions (Container), Previous'Result) = + P.Get (Positions (Container), Position) - 1); procedure Previous (Container : List; Position : in out Cursor) with Global => null, - Pre => Has_Element (Container, Position) - or else Position = No_Element, + Pre => + Has_Element (Container, Position) or else Position = No_Element, Contract_Cases => (Position = No_Element - or else P.Get (Positions (Container), Position) = 1 => + or else P.Get (Positions (Container), Position) = 1 + => Position = No_Element, + others => Has_Element (Container, Position) - and then P.Get (Positions (Container), Position) = - P.Get (Positions (Container), Position'Old) - 1); + and then P.Get (Positions (Container), Position) = + P.Get (Positions (Container), Position'Old) - 1); function Find (Container : List; @@ -1217,40 +1356,52 @@ is with Global => null, Pre => - Has_Element (Container, Position) or else Position = No_Element, + Has_Element (Container, Position) or else Position = No_Element, Contract_Cases => -- If Item is not is not contained in Container after Position, Find -- returns No_Element. + (not M.Contains - (Container => Model (Container), - Fst => (if Position = No_Element then 1 - else P.Get (Positions (Container), Position)), - Lst => Length (Container), - Item => Item) + (Container => Model (Container), + Fst => + (if Position = No_Element then + 1 + else + P.Get (Positions (Container), Position)), + Lst => Length (Container), + Item => Item) => Find'Result = No_Element, -- Otherwise, Find returns a valid cusror in Container + others => P.Has_Key (Positions (Container), Find'Result) - -- The element designated by the result of Find is Item - and Element (Model (Container), - P.Get (Positions (Container), Find'Result)) = Item + -- The element designated by the result of Find is Item + + and Element (Model (Container), + P.Get (Positions (Container), Find'Result)) = Item - -- 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)) + -- The result of Find is located after Position - -- It is the first occurence of Item in this slice - 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)); + 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 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 (Container : List; @@ -1259,40 +1410,54 @@ is with Global => null, Pre => - Has_Element (Container, Position) or else Position = No_Element, + Has_Element (Container, Position) or else Position = No_Element, Contract_Cases => -- If Item is not is not contained in Container before Position, Find -- returns No_Element. + (not M.Contains - (Container => Model (Container), - Fst => 1, - Lst => (if Position = No_Element then Length (Container) - else P.Get (Positions (Container), Position)), - Item => Item) + (Container => Model (Container), + Fst => 1, + Lst => + (if Position = No_Element then + Length (Container) + else + P.Get (Positions (Container), Position)), + Item => Item) => Reverse_Find'Result = No_Element, -- Otherwise, Find returns a valid cusror in Container + others => P.Has_Key (Positions (Container), Reverse_Find'Result) - -- The element designated by the result of Find is Item - and Element (Model (Container), - P.Get (Positions (Container), Reverse_Find'Result)) = Item + -- The element designated by the result of Find is Item - -- The result of Find is located before Position - and (if Position /= No_Element - then P.Get (Positions (Container), Reverse_Find'Result) - <= P.Get (Positions (Container), Position)) + and Element (Model (Container), + P.Get (Positions (Container), + Reverse_Find'Result)) = 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)); + -- The result of Find is located before Position + + and (if Position /= No_Element then + P.Get (Positions (Container), Reverse_Find'Result) <= + P.Get (Positions (Container), Position)) + + -- 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 (Container : List; @@ -1300,29 +1465,33 @@ is with Global => null, Post => - Contains'Result = M.Contains (Container => Model (Container), - Fst => 1, - Lst => Length (Container), - Item => Item); + Contains'Result = M.Contains (Container => Model (Container), + Fst => 1, + Lst => Length (Container), + Item => Item); - function Has_Element (Container : List; Position : Cursor) return Boolean + function Has_Element + (Container : List; + Position : Cursor) return Boolean with Global => null, 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); generic with function "<" (Left, Right : Element_Type) return Boolean is <>; + package Generic_Sorting with SPARK_Mode is function M_Elements_Sorted (Container : M.Sequence) return Boolean with Ghost, Global => null, - Post => M_Elements_Sorted'Result = - (for all I in 1 .. M.Length (Container) => - (for all J in I + 1 .. M.Length (Container) => - Element (Container, I) = Element (Container, J) - or Element (Container, I) < Element (Container, J))); + Post => + M_Elements_Sorted'Result = + (for all I in 1 .. M.Length (Container) => + (for all J in I + 1 .. M.Length (Container) => + Element (Container, I) = Element (Container, J) + or Element (Container, I) < Element (Container, J))); pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted); function Is_Sorted (Container : List) return Boolean with @@ -1331,18 +1500,20 @@ is procedure Sort (Container : in out List) with Global => null, - Post => Length (Container) = Length (Container)'Old - and M_Elements_Sorted (Model (Container)); + Post => + 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 Global => null, Pre => Length (Source) <= Target.Capacity - Length (Target), - Post => Length (Target) = Length (Target)'Old + Length (Source)'Old - and Length (Source) = 0 - and (if M_Elements_Sorted (Model (Target)'Old) - and M_Elements_Sorted (Model (Source)'Old) - then M_Elements_Sorted (Model (Target))); + Post => + Length (Target) = Length (Target)'Old + Length (Source)'Old + and Length (Source) = 0 + and (if M_Elements_Sorted (Model (Target)'Old) + and M_Elements_Sorted (Model (Source)'Old) + then M_Elements_Sorted (Model (Target))); end Generic_Sorting; private diff --git a/gcc/ada/a-cofuba.adb b/gcc/ada/a-cofuba.adb index 02d354e..4e7ac38c 100644 --- a/gcc/ada/a-cofuba.adb +++ b/gcc/ada/a-cofuba.adb @@ -33,14 +33,14 @@ pragma Ada_2012; package body Ada.Containers.Functional_Base with SPARK_Mode => Off is - function To_Count (Idx : Extended_Index) return Count_Type - is (Count_Type - (Extended_Index'Pos (Idx) - - Extended_Index'Pos (Extended_Index'First))); - - function To_Index (Position : Count_Type) return Extended_Index - is (Extended_Index'Val - (Position + Extended_Index'Pos (Extended_Index'First))); + function To_Count (Idx : Extended_Index) return Count_Type is + (Count_Type + (Extended_Index'Pos (Idx) - + Extended_Index'Pos (Extended_Index'First))); + + function To_Index (Position : Count_Type) return Extended_Index is + (Extended_Index'Val + (Position + Extended_Index'Pos (Extended_Index'First))); -- Conversion functions between Index_Type and Count_Type function Find (C : Container; E : access Element_Type) return Count_Type; diff --git a/gcc/ada/a-cofuma.adb b/gcc/ada/a-cofuma.adb index 39759f4..e4ee198 100644 --- a/gcc/ada/a-cofuma.adb +++ b/gcc/ada/a-cofuma.adb @@ -93,8 +93,8 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is K : constant Key_Type := Get (Left.Keys, I); begin if not Equivalent_Keys (K, New_Key) - and then Get (Right.Elements, Find (Right.Keys, K)) - /= Get (Left.Elements, I) + and then Get (Right.Elements, Find (Right.Keys, K)) /= + Get (Left.Elements, I) then return False; end if; @@ -106,7 +106,8 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is function Elements_Equal_Except (Left : Map; Right : Map; - X, Y : Key_Type) return Boolean + X : Key_Type; + Y : Key_Type) return Boolean is begin for I in 1 .. Length (Left.Keys) loop @@ -115,8 +116,8 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is begin if not Equivalent_Keys (K, X) and then not Equivalent_Keys (K, Y) - and then Get (Right.Elements, Find (Right.Keys, K)) - /= Get (Left.Elements, I) + and then Get (Right.Elements, Find (Right.Keys, K)) /= + Get (Left.Elements, I) then return False; end if; @@ -167,6 +168,7 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is end if; end; end loop; + return True; end Keys_Included; @@ -191,13 +193,15 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is end if; end; end loop; + return True; end Keys_Included_Except; function Keys_Included_Except (Left : Map; Right : Map; - X, Y : Key_Type) return Boolean + X : Key_Type; + Y : Key_Type) return Boolean is begin for I in 1 .. Length (Left.Keys) loop @@ -212,6 +216,7 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is end if; end; end loop; + return True; end Keys_Included_Except; @@ -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 - (Keys_Included (Left, Right) - and Keys_Included (Left => Right, Right => Left)); + (Keys_Included (Left, Right) + and Keys_Included (Left => Right, Right => Left)); --------- -- Set -- @@ -243,6 +248,6 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is is (Keys => Container.Keys, Elements => - Set (Container.Elements, Find (Container.Keys, Key), New_Item)); + Set (Container.Elements, Find (Container.Keys, Key), New_Item)); end Ada.Containers.Functional_Maps; diff --git a/gcc/ada/a-cofuma.ads b/gcc/ada/a-cofuma.ads index 89adcb2..9d3bb97 100644 --- a/gcc/ada/a-cofuma.ads +++ b/gcc/ada/a-cofuma.ads @@ -36,6 +36,7 @@ generic type Key_Type (<>) is private; type Element_Type (<>) is private; with function Equivalent_Keys (Left, Right : Key_Type) return Boolean; + package Ada.Containers.Functional_Maps with SPARK_Mode is type Map is private with @@ -90,9 +91,9 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is Post => "="'Result = ((for all Key of Left => - Has_Key (Right, Key) - and then Get (Right, Key) = Get (Left, Key)) - and (for all Key of Right => Has_Key (Left, Key))); + Has_Key (Right, Key) + and then Get (Right, Key) = Get (Left, Key)) + and (for all Key of Right => Has_Key (Left, Key))); pragma Warnings (Off, "unused variable ""Key"""); function Is_Empty (Container : Map) return Boolean with @@ -117,8 +118,8 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is Global => null, Post => Same_Keys'Result = - (Keys_Included (Left, Right) - and Keys_Included (Left => Right, Right => Left)); + (Keys_Included (Left, Right) + and Keys_Included (Left => Right, Right => Left)); pragma Annotate (GNATprove, Inline_For_Proof, Same_Keys); function Keys_Included_Except @@ -130,24 +131,27 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is with Global => null, Post => - Keys_Included_Except'Result = - (for all Key of Left => - (if not Equivalent_Keys (Key, New_Key) - then Has_Key (Right, Key))); + Keys_Included_Except'Result = + (for all Key of Left => + (if not Equivalent_Keys (Key, New_Key) then + Has_Key (Right, Key))); function Keys_Included_Except (Left : 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 with Global => null, Post => - Keys_Included_Except'Result = - (for all Key of Left => - (if not Equivalent_Keys (Key, X) and not Equivalent_Keys (Key, Y) - then Has_Key (Right, Key))); + Keys_Included_Except'Result = + (for all Key of Left => + (if not Equivalent_Keys (Key, X) + and not Equivalent_Keys (Key, Y) + then + Has_Key (Right, Key))); function Elements_Equal_Except (Left : Map; @@ -162,13 +166,14 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is Post => Elements_Equal_Except'Result = (for all Key of Left => - (if not Equivalent_Keys (Key, New_Key) - then Get (Left, Key) = Get (Right, Key))); + (if not Equivalent_Keys (Key, New_Key) then + Get (Left, Key) = Get (Right, Key))); function Elements_Equal_Except (Left : 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 -- Left and Right except X and Y. @@ -178,8 +183,10 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is Post => Elements_Equal_Except'Result = (for all Key of Left => - (if not Equivalent_Keys (Key, X) and not Equivalent_Keys (Key, Y) - then Get (Left, Key) = Get (Right, Key))); + (if not Equivalent_Keys (Key, X) + and not Equivalent_Keys (Key, Y) + then + Get (Left, Key) = Get (Right, Key))); ---------------------------- -- Construction Functions -- @@ -192,19 +199,19 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is (Container : Map; New_Key : Key_Type; 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 Global => null, Pre => - not Has_Key (Container, New_Key) - and Length (Container) < Count_Type'Last, + not Has_Key (Container, New_Key) + and Length (Container) < Count_Type'Last, Post => Length (Container) + 1 = Length (Add'Result) - and Has_Key (Add'Result, New_Key) - and Get (Add'Result, New_Key) = New_Item - and Container <= Add'Result - and Keys_Included_Except (Add'Result, Container, New_Key); + and Has_Key (Add'Result, New_Key) + and Get (Add'Result, New_Key) = New_Item + and Container <= Add'Result + and Keys_Included_Except (Add'Result, Container, New_Key); function Set (Container : Map; @@ -218,9 +225,9 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is Pre => Has_Key (Container, Key), Post => Length (Container) = Length (Set'Result) - and Get (Set'Result, Key) = New_Item - and Same_Keys (Container, Set'Result) - and Elements_Equal_Except (Container, Set'Result, Key); + and Get (Set'Result, Key) = New_Item + and Same_Keys (Container, Set'Result) + and Elements_Equal_Except (Container, Set'Result, Key); --------------------------- -- Iteration Primitives -- @@ -281,11 +288,15 @@ private is (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 (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 (Key_Containers.Get (Container.Keys, Count_Type (Key))); diff --git a/gcc/ada/a-cofuse.adb b/gcc/ada/a-cofuse.adb index d9b4c1d..e0ea2ff 100644 --- a/gcc/ada/a-cofuse.adb +++ b/gcc/ada/a-cofuse.adb @@ -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 (Content => - Add (Container.Content, Length (Container.Content) + 1, Item)); + Add (Container.Content, Length (Container.Content) + 1, Item)); -------------- -- Contains -- @@ -73,7 +73,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is Item : Element_Type) return Boolean is (for all E of Left => - Equivalent_Elements (E, Item) or Contains (Right, E)); + Equivalent_Elements (E, Item) or Contains (Right, E)); ----------------------- -- Included_In_Union -- @@ -85,7 +85,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is Right : Set) return Boolean is (for all Item of Container => - Contains (Left, Item) or Contains (Right, Item)); + Contains (Left, Item) or Contains (Right, Item)); --------------------------- -- Includes_Intersection -- @@ -97,7 +97,7 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is Right : Set) return Boolean is (for all Item of Left => - (if Contains (Right, Item) then Contains (Container, Item))); + (if Contains (Right, Item) then Contains (Container, Item))); ------------------ -- Intersection -- diff --git a/gcc/ada/a-cofuse.ads b/gcc/ada/a-cofuse.ads index f9848f9..16a4a4d 100644 --- a/gcc/ada/a-cofuse.ads +++ b/gcc/ada/a-cofuse.ads @@ -34,8 +34,10 @@ private with Ada.Containers.Functional_Base; generic type Element_Type (<>) is private; - with - function Equivalent_Elements (Left, Right : Element_Type) return Boolean; + with function Equivalent_Elements + (Left : Element_Type; + Right : Element_Type) return Boolean; + package Ada.Containers.Functional_Sets with SPARK_Mode is type Set is private with @@ -80,8 +82,8 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is Global => null, Post => "="'Result = - ((for all Item of Left => Contains (Right, Item)) - and (for all Item of Right => Contains (Left, Item))); + (for all Item of Left => Contains (Right, Item)) + and (for all Item of Right => Contains (Left, Item)); pragma Warnings (Off, "unused variable ""Item"""); function Is_Empty (Container : Set) return Boolean with @@ -102,8 +104,8 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is Global => null, Post => Included_Except'Result = - (for all E of Left => - Contains (Right, E) or Equivalent_Elements (E, Item)); + (for all E of Left => + Contains (Right, E) or Equivalent_Elements (E, Item)); function Includes_Intersection (Container : Set; @@ -117,7 +119,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is Post => Includes_Intersection'Result = (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 (Container : Set; @@ -130,7 +132,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is Post => Included_In_Union'Result = (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 -- Number of elements that are both in Left and Right @@ -158,9 +160,9 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is and Length (Container) < Count_Type'Last, Post => Length (Add'Result) = Length (Container) + 1 - and Contains (Add'Result, Item) - and Container <= Add'Result - and Included_Except (Add'Result, Container, Item); + and Contains (Add'Result, Item) + and Container <= Add'Result + and Included_Except (Add'Result, Container, Item); function Remove (Container : Set; Item : Element_Type) return Set with -- 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 Pre => Contains (Container, Item), Post => Length (Remove'Result) = Length (Container) - 1 - and not Contains (Remove'Result, Item) - and Remove'Result <= Container - and Included_Except (Container, Remove'Result, Item); + and not Contains (Remove'Result, Item) + and Remove'Result <= Container + and Included_Except (Container, Remove'Result, Item); function Intersection (Left : Set; Right : Set) return Set with -- Returns the intersection of Left and Right @@ -188,8 +190,8 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is Global => null, Pre => - Length (Left) - Num_Overlaps (Left, Right) - <= Count_Type'Last - Length (Right), + Length (Left) - Num_Overlaps (Left, Right) <= + Count_Type'Last - Length (Right), Post => Length (Union'Result) = Length (Left) - Num_Overlaps (Left, Right) + Length (Right) @@ -212,7 +214,9 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is with 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 Global => null, Pre => Iter_Has_Element (Container, Key); @@ -249,7 +253,9 @@ private is (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 (if Key = Private_Key'Last then 0 else Key + 1); diff --git a/gcc/ada/a-cofuve.adb b/gcc/ada/a-cofuve.adb index e8f8757..2984bcc 100644 --- a/gcc/ada/a-cofuve.adb +++ b/gcc/ada/a-cofuve.adb @@ -40,7 +40,7 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is function "<" (Left : Sequence; Right : Sequence) return Boolean is (Length (Left.Content) < Length (Right.Content) 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 function "<=" (Left : Sequence; Right : Sequence) return Boolean is (Length (Left.Content) <= Length (Right.Content) 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 -- Add -- --------- - function Add (Container : Sequence; New_Item : Element_Type) return Sequence + function Add + (Container : Sequence; + New_Item : Element_Type) return Sequence is - (Content => Add (Container.Content, - Index_Type'Val - (Index_Type'Pos (Index_Type'First) + - Length (Container.Content)), - New_Item)); + (Content => + Add (Container.Content, + Index_Type'Val (Index_Type'Pos (Index_Type'First) + + Length (Container.Content)), + New_Item)); function Add (Container : Sequence; @@ -92,6 +94,7 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is return False; end if; end loop; + return True; end Constant_Range; @@ -111,6 +114,7 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is return True; end if; end loop; + return False; end Contains; @@ -142,7 +146,8 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is function Equal_Except (Left : Sequence; Right : Sequence; - X, Y : Index_Type) return Boolean + X : Index_Type; + Y : Index_Type) return Boolean is begin if Length (Left.Content) /= Length (Right.Content) then @@ -174,8 +179,8 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is ---------- function Last (Container : Sequence) return Extended_Index is - (Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) - + Length (Container))); + (Index_Type'Val + ((Index_Type'Pos (Index_Type'First) - 1) + Length (Container))); ------------ -- Length -- @@ -200,6 +205,7 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is return False; end if; end loop; + return True; end Range_Equal; @@ -216,8 +222,8 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is is begin for I in Fst .. Lst loop - if Get (Left, I) - /= Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset)) + if Get (Left, I) /= + Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset)) then return False; end if; @@ -229,8 +235,9 @@ package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is -- Remove -- ------------ - function Remove (Container : Sequence; - Position : Index_Type) return Sequence + function Remove + (Container : Sequence; + Position : Index_Type) return Sequence is (Content => Remove (Container.Content, Position)); diff --git a/gcc/ada/a-cofuve.ads b/gcc/ada/a-cofuve.ads index ad359b4..d02864e 100644 --- a/gcc/ada/a-cofuve.ads +++ b/gcc/ada/a-cofuve.ads @@ -38,6 +38,7 @@ generic -- should have at least one more element at the low end than Index_Type. type Element_Type (<>) is private; + package Ada.Containers.Functional_Vectors with SPARK_Mode is subtype Extended_Index is Index_Type'Base range @@ -69,7 +70,7 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is Global => null, Post => (Index_Type'Pos (Index_Type'First) - 1) + Length'Result <= - Index_Type'Pos (Index_Type'Last); + Index_Type'Pos (Index_Type'Last); function Get (Container : Sequence; @@ -86,8 +87,8 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is Global => null, Post => Last'Result = - Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) - + Length (Container)); + Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) + + Length (Container)); pragma Annotate (GNATprove, Inline_For_Proof, Last); function First return Extended_Index is (Index_Type'First); @@ -104,8 +105,8 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is Post => "="'Result = (Length (Left) = Length (Right) - and then (for all N in Index_Type'First .. Last (Left) => - Get (Left, N) = Get (Right, N))); + and then (for all N in Index_Type'First .. Last (Left) => + Get (Left, N) = Get (Right, N))); pragma Annotate (GNATprove, Inline_For_Proof, "="); function "<" (Left : Sequence; Right : Sequence) return Boolean with @@ -115,8 +116,8 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is Post => "<"'Result = (Length (Left) < Length (Right) - and then (for all N in Index_Type'First .. Last (Left) => - Get (Left, N) = Get (Right, N))); + and then (for all N in Index_Type'First .. Last (Left) => + Get (Left, N) = Get (Right, N))); pragma Annotate (GNATprove, Inline_For_Proof, "<"); function "<=" (Left : Sequence; Right : Sequence) return Boolean with @@ -126,16 +127,15 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is Post => "<="'Result = (Length (Left) <= Length (Right) - and then (for all N in Index_Type'First .. Last (Left) => - Get (Left, N) = Get (Right, N))); + and then (for all N in Index_Type'First .. Last (Left) => + Get (Left, N) = Get (Right, N))); pragma Annotate (GNATprove, Inline_For_Proof, "<="); function Contains (Container : Sequence; Fst : Index_Type; Lst : Extended_Index; - Item : Element_Type) - return Boolean + Item : Element_Type) return Boolean -- Returns True if Item occurs in the range from Fst to Lst of Container with @@ -150,8 +150,7 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is (Container : Sequence; Fst : Index_Type; Lst : Extended_Index; - Item : Element_Type) - return Boolean + Item : Element_Type) return Boolean -- Returns True if every element of the range from Fst to Lst of Container -- is equal to Item. @@ -175,14 +174,15 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is Post => Equal_Except'Result = (Length (Left) = Length (Right) - and then (for all I in Index_Type'First .. Last (Left) => - (if I /= Position then Get (Left, I) = Get (Right, I)))); + and then (for all I in Index_Type'First .. Last (Left) => + (if I /= Position then Get (Left, I) = Get (Right, I)))); pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except); function Equal_Except (Left : 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 with @@ -191,8 +191,9 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is Post => Equal_Except'Result = (Length (Left) = Length (Right) - and then (for all I in Index_Type'First .. Last (Left) => - (if I /= X and I /= Y then Get (Left, I) = Get (Right, I)))); + and then (for all I in Index_Type'First .. Last (Left) => + (if I /= X and I /= Y then + Get (Left, I) = Get (Right, I)))); pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except); function Range_Equal @@ -222,21 +223,23 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is with Global => null, - Pre => Lst <= Last (Left) - and Offset in - Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) .. - (Index_Type'Pos (Index_Type'First) - 1) - + Length (Right) - Index_Type'Pos (Lst), + Pre => + Lst <= Last (Left) + and Offset in + Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) .. + (Index_Type'Pos (Index_Type'First) - 1) + Length (Right) - + Index_Type'Pos (Lst), Post => Range_Shifted'Result = ((for all I in Fst .. Lst => - Get (Left, I) - = Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset))) + Get (Left, I) = + Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset))) and (for all I in Index_Type'Val (Index_Type'Pos (Fst) + Offset) .. - Index_Type'Val (Index_Type'Pos (Lst) + Offset) => - Get (Left, Index_Type'Val (Index_Type'Pos (I) - Offset)) - = Get (Right, I))); + Index_Type'Val (Index_Type'Pos (Lst) + Offset) + => + Get (Left, Index_Type'Val (Index_Type'Pos (I) - Offset)) = + Get (Right, I))); pragma Annotate (GNATprove, Inline_For_Proof, Range_Shifted); ---------------------------- @@ -256,8 +259,9 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is with Global => null, Pre => Position in Index_Type'First .. Last (Container), - Post => Get (Set'Result, Position) = New_Item - and then Equal_Except (Container, Set'Result, Position); + Post => + Get (Set'Result, Position) = New_Item + and then Equal_Except (Container, Set'Result, Position); function Add (Container : Sequence; New_Item : Element_Type) return Sequence -- Returns a new sequence which contains the same elements as Container @@ -289,17 +293,17 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is Post => Length (Add'Result) = Length (Container) + 1 and then Get (Add'Result, Position) = New_Item - and then - Range_Equal (Left => Container, - Right => Add'Result, - Fst => Index_Type'First, - Lst => Index_Type'Pred (Position)) - and then - Range_Shifted (Left => Container, - Right => Add'Result, - Fst => Position, - Lst => Last (Container), - Offset => 1); + and then Range_Equal + (Left => Container, + Right => Add'Result, + Fst => Index_Type'First, + Lst => Index_Type'Pred (Position)) + and then Range_Shifted + (Left => Container, + Right => Add'Result, + Fst => Position, + Lst => Last (Container), + Offset => 1); function Remove (Container : Sequence; @@ -315,17 +319,17 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is and Position in Index_Type'First .. Last (Container), Post => Length (Remove'Result) = Length (Container) - 1 - and then - Range_Equal (Left => Container, - Right => Remove'Result, - Fst => Index_Type'First, - Lst => Index_Type'Pred (Position)) - and then - Range_Shifted (Left => Remove'Result, - Right => Container, - Fst => Position, - Lst => Last (Remove'Result), - Offset => 1); + and then Range_Equal + (Left => Container, + Right => Remove'Result, + Fst => Index_Type'First, + Lst => Index_Type'Pred (Position)) + and then Range_Shifted + (Left => Remove'Result, + Right => Container, + Fst => Position, + Lst => Last (Remove'Result), + Offset => 1); --------------------------- -- Iteration Primitives -- @@ -339,7 +343,8 @@ package Ada.Containers.Functional_Vectors with SPARK_Mode is Position : Extended_Index) return Boolean with Global => null, - Post => Iter_Has_Element'Result = + Post => + Iter_Has_Element'Result = (Position in Index_Type'First .. Last (Container)); pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element); @@ -364,19 +369,22 @@ private function Iter_First (Container : Sequence) return Extended_Index is (Index_Type'First); + function Iter_Next (Container : Sequence; Position : Extended_Index) return Extended_Index is - (if Position = Extended_Index'Last then Extended_Index'First - else Extended_Index'Succ (Position)); + (if Position = Extended_Index'Last then + Extended_Index'First + else + Extended_Index'Succ (Position)); function Iter_Has_Element (Container : Sequence; Position : Extended_Index) return Boolean is (Position in Index_Type'First .. - (Index_Type'Val - ((Index_Type'Pos (Index_Type'First) - 1) + Length (Container)))); + (Index_Type'Val + ((Index_Type'Pos (Index_Type'First) - 1) + Length (Container)))); end Ada.Containers.Functional_Vectors; diff --git a/gcc/ada/exp_attr.adb b/gcc/ada/exp_attr.adb index ec16bee..56a92d3 100644 --- a/gcc/ada/exp_attr.adb +++ b/gcc/ada/exp_attr.adb @@ -3598,6 +3598,14 @@ package body Exp_Attr is -- Image attribute is handled in separate unit Exp_Imgv 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); --------- @@ -6995,6 +7003,14 @@ package body Exp_Attr is -- Wide_Image attribute is handled in separate unit Exp_Imgv 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); --------------------- @@ -7004,6 +7020,14 @@ package body Exp_Attr is -- Wide_Wide_Image attribute is handled in separate unit Exp_Imgv 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); ---------------- diff --git a/gcc/ada/exp_disp.adb b/gcc/ada/exp_disp.adb index 96f62a0..4bdd525 100644 --- a/gcc/ada/exp_disp.adb +++ b/gcc/ada/exp_disp.adb @@ -4510,10 +4510,13 @@ package body Exp_Disp is if Building_Static_DT (Typ) then 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_Elmt : Elmt_Id; - Frnodes : List_Id; begin Freezing_Library_Level_Tagged_Type := True; @@ -4523,18 +4526,21 @@ package body Exp_Disp is Prim := Node (Prim_Elmt); Frnodes := Freeze_Entity (Prim, Typ); - declare - F : Entity_Id; - - begin - F := First_Formal (Prim); - while Present (F) loop - Check_Premature_Freezing (Prim, Typ, Etype (F)); - Next_Formal (F); + -- We disable this check for abstract subprograms, given that + -- they cannot be called directly and thus the state of their + -- untagged formals is of no concern. The RM is unclear in any + -- case concerning the need for this check, and this topic may + -- go back to the ARG. + + if not Is_Abstract_Subprogram (Prim) then + Formal := First_Formal (Prim); + while Present (Formal) loop + Check_Premature_Freezing (Prim, Typ, Etype (Formal)); + Next_Formal (Formal); end loop; Check_Premature_Freezing (Prim, Typ, Etype (Prim)); - end; + end if; if Present (Frnodes) then Append_List_To (Result, Frnodes); @@ -4543,7 +4549,7 @@ package body Exp_Disp is Next_Elmt (Prim_Elmt); end loop; - Freezing_Library_Level_Tagged_Type := Save; + Freezing_Library_Level_Tagged_Type := Saved_FLLTT; end; end if; diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 790b6f6..0184d8e 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -6310,21 +6310,28 @@ package body Sem_Attr is end; end if; - -- Fold in representation aspects for the type, which appear in - -- the same source buffer. + if Is_First_Subtype (T) then - 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 - 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 := First_Rep_Item (T); - Rep := Next_Rep_Item (Rep); - end loop; + while Present (Rep) 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; -- Start of processing for Type_Key diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index 4e54edb..8da266a 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -1463,6 +1463,25 @@ package body Sem_Ch4 is -- actuals. 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 Analyze_Call; diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb index e024c6d..24e0963 100644 --- a/gcc/ada/sem_eval.adb +++ b/gcc/ada/sem_eval.adb @@ -630,17 +630,17 @@ package body Sem_Eval is -- to discrete and non-discrete types. elsif (Nkind (Choice) = N_Subtype_Indication - or else (Is_Entity_Name (Choice) - and then Is_Type (Entity (Choice)))) + or else (Is_Entity_Name (Choice) + and then Is_Type (Entity (Choice)))) and then Has_Predicates (Etype (Choice)) and then Has_Static_Predicate (Etype (Choice)) then if Is_Discrete_Type (Etype (Choice)) then - return Choices_Match - (Expr, Static_Discrete_Predicate (Etype (Choice))); + return + Choices_Match + (Expr, Static_Discrete_Predicate (Etype (Choice))); - elsif - Real_Or_String_Static_Predicate_Matches (Expr, Etype (Choice)) + elsif Real_Or_String_Static_Predicate_Matches (Expr, Etype (Choice)) then return Match; |