diff --git a/gcc/ada/libgnat/a-cfdlli.adb b/gcc/ada/libgnat/a-cfdlli.adb --- a/gcc/ada/libgnat/a-cfdlli.adb +++ b/gcc/ada/libgnat/a-cfdlli.adb @@ -29,9 +29,17 @@ with Ada.Containers.Stable_Sorting; use Ada.Containers.Stable_Sorting; with System; use type System.Address; +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; + package body Ada.Containers.Formal_Doubly_Linked_Lists with SPARK_Mode => Off is + -- Convert Count_Type to Big_Interger + + package Conversions is new Signed_Conversions (Int => Count_Type); + use Conversions; + ----------------------- -- Local Subprograms -- ----------------------- @@ -809,7 +817,7 @@ is while Position /= 0 loop R := P.Add (R, (Node => Position), I); - pragma Assert (P.Length (R) = I); + pragma Assert (P.Length (R) = To_Big_Integer (I)); Position := Container.Nodes (Position).Next; I := I + 1; end loop; diff --git a/gcc/ada/libgnat/a-cfhama.adb b/gcc/ada/libgnat/a-cfhama.adb --- a/gcc/ada/libgnat/a-cfhama.adb +++ b/gcc/ada/libgnat/a-cfhama.adb @@ -33,6 +33,9 @@ pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Formal_Keys); with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers; +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; + with System; use type System.Address; package body Ada.Containers.Formal_Hashed_Maps with @@ -71,6 +74,13 @@ is function Vet (Container : Map; Position : Cursor) return Boolean with Inline; + -- Convert Count_Type to Big_Interger + + package Conversions is new Signed_Conversions (Int => Count_Type); + + function Big (J : Count_Type) return Big_Integer renames + Conversions.To_Big_Integer; + -------------------------- -- Local Instantiations -- -------------------------- @@ -526,7 +536,7 @@ is while Position /= 0 loop R := P.Add (R, (Node => Position), I); - pragma Assert (P.Length (R) = I); + pragma Assert (P.Length (R) = Big (I)); Position := HT_Ops.Next (Container.Content, Position); I := I + 1; end loop; diff --git a/gcc/ada/libgnat/a-cfhase.adb b/gcc/ada/libgnat/a-cfhase.adb --- a/gcc/ada/libgnat/a-cfhase.adb +++ b/gcc/ada/libgnat/a-cfhase.adb @@ -753,7 +753,7 @@ is while Position /= 0 loop R := P.Add (R, (Node => Position), I); - pragma Assert (P.Length (R) = I); + pragma Assert (P.Length (R) = Big (I)); Position := HT_Ops.Next (Container.Content, Position); I := I + 1; end loop; diff --git a/gcc/ada/libgnat/a-cfhase.ads b/gcc/ada/libgnat/a-cfhase.ads --- a/gcc/ada/libgnat/a-cfhase.ads +++ b/gcc/ada/libgnat/a-cfhase.ads @@ -48,6 +48,8 @@ with Ada.Containers.Functional_Maps; with Ada.Containers.Functional_Sets; with Ada.Containers.Functional_Vectors; +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; private with Ada.Containers.Hash_Tables; generic @@ -70,6 +72,13 @@ is pragma Assertion_Policy (Contract_Cases => Ignore); pragma Annotate (CodePeer, Skip_Analysis); + -- Convert Count_Type to Big_Interger. + + package Conversions is new Signed_Conversions (Int => Count_Type); + + function Big (J : Count_Type) return Big_Integer renames + Conversions.To_Big_Integer; + type Set (Capacity : Count_Type; Modulus : Hash_Type) is private with Iterable => (First => First, Next => Next, @@ -261,7 +270,7 @@ is Ghost, Global => null, - Post => M.Length (Model'Result) = Length (Container); + Post => M.Length (Model'Result) = Big (Length (Container)); function Elements (Container : Set) return E.Sequence with -- The Elements sequence represents the underlying list structure of @@ -859,9 +868,9 @@ is Length (Source) - Length (Target and Source) <= Target.Capacity - Length (Target), Post => - Length (Target) = Length (Target)'Old + Big (Length (Target)) = Big (Length (Target)'Old) - M.Num_Overlaps (Model (Target)'Old, Model (Source)) - + Length (Source) + + Big (Length (Source)) -- Elements already in Target are still in Target @@ -907,9 +916,9 @@ is Global => null, Pre => Length (Left) <= Count_Type'Last - Length (Right), Post => - Length (Union'Result) = Length (Left) + Big (Length (Union'Result)) = Big (Length (Left)) - M.Num_Overlaps (Model (Left), Model (Right)) - + Length (Right) + + Big (Length (Right)) -- Elements of Left and Right are in the result of Union @@ -946,7 +955,7 @@ is procedure Intersection (Target : in out Set; Source : Set) with Global => null, Post => - Length (Target) = + Big (Length (Target)) = M.Num_Overlaps (Model (Target)'Old, Model (Source)) -- Elements of Target were already in Target @@ -982,7 +991,7 @@ is function Intersection (Left, Right : Set) return Set with Global => null, Post => - Length (Intersection'Result) = + Big (Length (Intersection'Result)) = M.Num_Overlaps (Model (Left), Model (Right)) -- Elements in the result of Intersection are in Left and Right @@ -1012,7 +1021,7 @@ is procedure Difference (Target : in out Set; Source : Set) with Global => null, Post => - Length (Target) = Length (Target)'Old - + Big (Length (Target)) = Big (Length (Target)'Old) - M.Num_Overlaps (Model (Target)'Old, Model (Source)) -- Elements of Target were already in Target @@ -1048,7 +1057,7 @@ is function Difference (Left, Right : Set) return Set with Global => null, Post => - Length (Difference'Result) = Length (Left) - + Big (Length (Difference'Result)) = Big (Length (Left)) - M.Num_Overlaps (Model (Left), Model (Right)) -- Elements of the result of Difference are in Left @@ -1085,9 +1094,9 @@ is Length (Source) - Length (Target and Source) <= Target.Capacity - Length (Target) + Length (Target and Source), Post => - Length (Target) = Length (Target)'Old - + Big (Length (Target)) = Big (Length (Target)'Old) - 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) + - Length (Source) + Big (Length (Source)) -- Elements of the difference were not both in Source and in Target @@ -1125,9 +1134,9 @@ is Global => null, Pre => Length (Left) <= Count_Type'Last - Length (Right), Post => - Length (Symmetric_Difference'Result) = Length (Left) - + Big (Length (Symmetric_Difference'Result)) = Big (Length (Left)) - 2 * M.Num_Overlaps (Model (Left), Model (Right)) + - Length (Right) + Big (Length (Right)) -- Elements of the difference were not both in Left and Right diff --git a/gcc/ada/libgnat/a-cforma.adb b/gcc/ada/libgnat/a-cforma.adb --- a/gcc/ada/libgnat/a-cforma.adb +++ b/gcc/ada/libgnat/a-cforma.adb @@ -32,12 +32,22 @@ pragma Elaborate_All with Ada.Containers.Red_Black_Trees.Generic_Bounded_Keys; pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Bounded_Keys); +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; + with System; use type System.Address; package body Ada.Containers.Formal_Ordered_Maps with SPARK_Mode => Off is + -- Convert Count_Type to Big_Interger + + package Conversions is new Signed_Conversions (Int => Count_Type); + + function Big (J : Count_Type) return Big_Integer renames + Conversions.To_Big_Integer; + ----------------------------- -- Node Access Subprograms -- ----------------------------- @@ -745,7 +755,7 @@ is while Position /= 0 loop R := P.Add (R, (Node => Position), I); - pragma Assert (P.Length (R) = I); + pragma Assert (P.Length (R) = Big (I)); Position := Tree_Operations.Next (Container.Content, Position); I := I + 1; end loop; diff --git a/gcc/ada/libgnat/a-cforse.adb b/gcc/ada/libgnat/a-cforse.adb --- a/gcc/ada/libgnat/a-cforse.adb +++ b/gcc/ada/libgnat/a-cforse.adb @@ -943,7 +943,7 @@ is while Position /= 0 loop R := P.Add (R, (Node => Position), I); - pragma Assert (P.Length (R) = I); + pragma Assert (P.Length (R) = Big (I)); Position := Tree_Operations.Next (Container.Content, Position); I := I + 1; end loop; diff --git a/gcc/ada/libgnat/a-cforse.ads b/gcc/ada/libgnat/a-cforse.ads --- a/gcc/ada/libgnat/a-cforse.ads +++ b/gcc/ada/libgnat/a-cforse.ads @@ -49,6 +49,8 @@ with Ada.Containers.Functional_Maps; with Ada.Containers.Functional_Sets; with Ada.Containers.Functional_Vectors; +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; private with Ada.Containers.Red_Black_Trees; generic @@ -67,6 +69,13 @@ is pragma Assertion_Policy (Contract_Cases => Ignore); pragma Annotate (CodePeer, Skip_Analysis); + -- Convert Count_Type to Big_Interger + + package Conversions is new Signed_Conversions (Int => Count_Type); + + function Big (J : Count_Type) return Big_Integer renames + Conversions.To_Big_Integer; + function Equivalent_Elements (Left, Right : Element_Type) return Boolean with Global => null, @@ -341,7 +350,7 @@ is Ghost, Global => null, - Post => M.Length (Model'Result) = Length (Container); + Post => M.Length (Model'Result) = Big (Length (Container)); function Elements (Container : Set) return E.Sequence with -- The Elements sequence represents the underlying list structure of @@ -990,9 +999,9 @@ is Length (Source) - Length (Target and Source) <= Target.Capacity - Length (Target), Post => - Length (Target) = Length (Target)'Old + Big (Length (Target)) = Big (Length (Target)'Old) - M.Num_Overlaps (Model (Target)'Old, Model (Source)) - + Length (Source) + + Big (Length (Source)) -- Elements already in Target are still in Target @@ -1038,9 +1047,9 @@ is Global => null, Pre => Length (Left) <= Count_Type'Last - Length (Right), Post => - Length (Union'Result) = Length (Left) + Big (Length (Union'Result)) = Big (Length (Left)) - M.Num_Overlaps (Model (Left), Model (Right)) - + Length (Right) + + Big (Length (Right)) -- Elements of Left and Right are in the result of Union @@ -1076,7 +1085,7 @@ is procedure Intersection (Target : in out Set; Source : Set) with Global => null, Post => - Length (Target) = + Big (Length (Target)) = M.Num_Overlaps (Model (Target)'Old, Model (Source)) -- Elements of Target were already in Target @@ -1111,7 +1120,7 @@ is function Intersection (Left, Right : Set) return Set with Global => null, Post => - Length (Intersection'Result) = + Big (Length (Intersection'Result)) = M.Num_Overlaps (Model (Left), Model (Right)) -- Elements in the result of Intersection are in Left and Right @@ -1139,7 +1148,7 @@ is procedure Difference (Target : in out Set; Source : Set) with Global => null, Post => - Length (Target) = Length (Target)'Old - + Big (Length (Target)) = Big (Length (Target)'Old) - M.Num_Overlaps (Model (Target)'Old, Model (Source)) -- Elements of Target were already in Target @@ -1174,7 +1183,7 @@ is function Difference (Left, Right : Set) return Set with Global => null, Post => - Length (Difference'Result) = Length (Left) - + Big (Length (Difference'Result)) = Big (Length (Left)) - M.Num_Overlaps (Model (Left), Model (Right)) -- Elements of the result of Difference are in Left @@ -1209,9 +1218,9 @@ is Length (Source) - Length (Target and Source) <= Target.Capacity - Length (Target) + Length (Target and Source), Post => - Length (Target) = Length (Target)'Old - + Big (Length (Target)) = Big (Length (Target)'Old) - 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) + - Length (Source) + Big (Length (Source)) -- Elements of the difference were not both in Source and in Target @@ -1248,9 +1257,9 @@ is Global => null, Pre => Length (Left) <= Count_Type'Last - Length (Right), Post => - Length (Symmetric_Difference'Result) = Length (Left) - + Big (Length (Symmetric_Difference'Result)) = Big (Length (Left)) - 2 * M.Num_Overlaps (Model (Left), Model (Right)) + - Length (Right) + Big (Length (Right)) -- Elements of the difference were not both in Left and Right diff --git a/gcc/ada/libgnat/a-cofuma.adb b/gcc/ada/libgnat/a-cofuma.adb --- a/gcc/ada/libgnat/a-cofuma.adb +++ b/gcc/ada/libgnat/a-cofuma.adb @@ -34,6 +34,9 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is use Key_Containers; use Element_Containers; + package Conversions is new Signed_Conversions (Int => Count_Type); + use Conversions; + --------- -- "=" -- --------- @@ -245,9 +248,9 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is -- Length -- ------------ - function Length (Container : Map) return Count_Type is + function Length (Container : Map) return Big_Natural is begin - return Length (Container.Elements); + return To_Big_Integer (Length (Container.Elements)); end Length; ------------ diff --git a/gcc/ada/libgnat/a-cofuma.ads b/gcc/ada/libgnat/a-cofuma.ads --- a/gcc/ada/libgnat/a-cofuma.ads +++ b/gcc/ada/libgnat/a-cofuma.ads @@ -32,6 +32,9 @@ pragma Ada_2012; private with Ada.Containers.Functional_Base; +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; + generic type Key_Type (<>) is private; type Element_Type (<>) is private; @@ -97,7 +100,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is (Equivalent_Keys (K, Key) = (Witness (Container, Key) = Witness (Container, K))))); - function Length (Container : Map) return Count_Type with + function Length (Container : Map) return Big_Natural with Global => null; -- Return the number of mappings in Container @@ -233,9 +236,7 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is with Global => null, - Pre => - not Has_Key (Container, New_Key) - and Length (Container) < Count_Type'Last, + Pre => not Has_Key (Container, New_Key), Post => Length (Container) + 1 = Length (Add'Result) and Has_Key (Add'Result, New_Key) diff --git a/gcc/ada/libgnat/a-cofuse.adb b/gcc/ada/libgnat/a-cofuse.adb --- a/gcc/ada/libgnat/a-cofuse.adb +++ b/gcc/ada/libgnat/a-cofuse.adb @@ -34,6 +34,9 @@ pragma Ada_2012; package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is use Containers; + package Conversions is new Signed_Conversions (Int => Count_Type); + use Conversions; + --------- -- "=" -- --------- @@ -135,8 +138,8 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is -- Length -- ------------ - function Length (Container : Set) return Count_Type is - (Length (Container.Content)); + function Length (Container : Set) return Big_Natural is + (To_Big_Integer (Length (Container.Content))); ----------------- -- Not_In_Both -- @@ -161,8 +164,8 @@ package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is -- Num_Overlaps -- ------------------ - function Num_Overlaps (Left : Set; Right : Set) return Count_Type is - (Num_Overlaps (Left.Content, Right.Content)); + function Num_Overlaps (Left : Set; Right : Set) return Big_Natural is + (To_Big_Integer (Num_Overlaps (Left.Content, Right.Content))); ------------ -- Remove -- diff --git a/gcc/ada/libgnat/a-cofuse.ads b/gcc/ada/libgnat/a-cofuse.ads --- a/gcc/ada/libgnat/a-cofuse.ads +++ b/gcc/ada/libgnat/a-cofuse.ads @@ -32,6 +32,9 @@ pragma Ada_2012; private with Ada.Containers.Functional_Base; +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; + generic type Element_Type (<>) is private; @@ -79,7 +82,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is (if (for some E of Container => Equivalent_Elements (E, Item)) then Contains'Result)); - function Length (Container : Set) return Count_Type with + function Length (Container : Set) return Big_Natural with Global => null; -- Return the number of elements in Container @@ -183,7 +186,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is No_Overlap'Result = (for all Item of Left => not Contains (Right, Item)); - function Num_Overlaps (Left : Set; Right : Set) return Count_Type with + function Num_Overlaps (Left : Set; Right : Set) return Big_Natural with -- Number of elements that are both in Left and Right Global => null, @@ -206,9 +209,7 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is -- Return a new set containing all the elements of Container plus E Global => null, - Pre => - not Contains (Container, Item) - and Length (Container) < Count_Type'Last, + Pre => not Contains (Container, Item), Post => Length (Add'Result) = Length (Container) + 1 and Contains (Add'Result, Item) @@ -245,9 +246,6 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is -- Returns the union of Left and Right Global => null, - Pre => - Length (Left) - Num_Overlaps (Left, Right) <= - Count_Type'Last - Length (Right), Post => Length (Union'Result) = Length (Left) - Num_Overlaps (Left, Right) + Length (Right)