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 --
-----------------------
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;
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
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 --
--------------------------
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;
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;
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
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,
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
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
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
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
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
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
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
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
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
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 --
-----------------------------
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;
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;
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
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,
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
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
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
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
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
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
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
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
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
use Key_Containers;
use Element_Containers;
+ package Conversions is new Signed_Conversions (Int => Count_Type);
+ use Conversions;
+
---------
-- "=" --
---------
-- 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;
------------
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;
(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
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)
package body Ada.Containers.Functional_Sets with SPARK_Mode => Off is
use Containers;
+ package Conversions is new Signed_Conversions (Int => Count_Type);
+ use Conversions;
+
---------
-- "=" --
---------
-- 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 --
-- 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 --
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;
(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
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,
-- 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)
-- 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)