mirror/gcc
2
0
Fork 0
mirror of git://gcc.gnu.org/git/gcc.git synced 2025-04-02 08:40:26 +08:00
Code Issues Packages Projects Releases Wiki Activity

[Ada] Replace SPARK containers implementation by Compile_Time_Error

Browse Source 
The SPARK containers are now maintained under the spark2014 repository.
This change replaces the implementation of SPARK containers by a
pragma Compile_Time_Error, pointing the users WITHing the libraries
to their new location.

gcc/ada/

	* Makefile.rtl: Remove SPARK containers filenames.
	* impunit.adb: Remove SPARK containers packages names.
	* libgnat/a-cfdlli.adb, libgnat/a-cfdlli.ads: Remove content and
	add pragma Compile_Time_Error with suitable message.
	* libgnat/a-cfhama.adb, libgnat/a-cfhama.ads: Likewise.
	* libgnat/a-cfhase.adb, libgnat/a-cfhase.ads: Likewise.
	* libgnat/a-cfidll.adb, libgnat/a-cfidll.ads: Likewise.
	* libgnat/a-cfinse.adb, libgnat/a-cfinse.ads: Likewise.
	* libgnat/a-cfinve.adb, libgnat/a-cfinve.ads: Likewise.
	* libgnat/a-cforma.adb, libgnat/a-cforma.ads: Likewise.
	* libgnat/a-cforse.adb, libgnat/a-cforse.ads: Likewise.
	* libgnat/a-cofove.adb, libgnat/a-cofove.ads: Likewise.
	* libgnat/a-cofuma.adb, libgnat/a-cofuma.ads: Likewise.
	* libgnat/a-cofuse.adb, libgnat/a-cofuse.ads: Likewise.
	* libgnat/a-cofuve.adb, libgnat/a-cofuve.ads: Likewise.
	* libgnat/a-cofuba.adb, libgnat/a-cofuba.ads: Remove package.

gcc/testsuite/

	* gnat.dg/aspect2.adb: Removed.
	* gnat.dg/aspect2.ads: Removed.
	* gnat.dg/config_pragma1.adb: Removed.
	* gnat.dg/config_pragma1_pkg.ads: Removed.
	* gnat.dg/equal8.adb: Removed.
	* gnat.dg/equal8.ads: Removed.
	* gnat.dg/equal8_pkg.ads: Removed.
	* gnat.dg/formal_containers.adb: Removed.
	* gnat.dg/iter1.adb: Removed.
	* gnat.dg/iter1.ads: Removed.
This commit is contained in:
Joffrey Huguet 2022-08-30 18:00:35 +02:00 committed by Marc Poulhiès
parent cf8af60f6a
commit 4a7312f7ce
38 changed files with 60 additions and 26171 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
gcc/ada/Makefile.rtl
View File

@ -110,14 +110,6 @@ GNATRTL_NONTASKING_OBJS= \
a-cbprqu$(objext) \
a-cbsyqu$(objext) \
a-cdlili$(objext) \
a-cfdlli$(objext) \
a-cfhama$(objext) \
a-cfhase$(objext) \
a-cfidll$(objext) \
a-cfinve$(objext) \
a-cfinse$(objext) \
a-cforma$(objext) \
a-cforse$(objext) \
a-cgaaso$(objext) \
a-cgarso$(objext) \
a-cgcaso$(objext) \
@ -144,14 +136,7 @@ GNATRTL_NONTASKING_OBJS= \
a-clrefi$(objext) \
a-coboho$(objext) \
a-cobove$(objext) \
a-cofove$(objext) \
a-cofuba$(objext) \
a-cofuma$(objext) \
a-cofuse$(objext) \
a-cofuve$(objext) \
a-cogeso$(objext) \
a-cohama$(objext) \
a-cohase$(objext) \
a-cohata$(objext) \
a-coinho$(objext) \
a-coinve$(objext) \

12
gcc/ada/impunit.adb
View File

@ -605,19 +605,7 @@ package body Impunit is
-- GNAT Defined Additions to Ada 2012 --
----------------------------------------
("a-cfidll", F), -- Ada.Containers.Formal_Indefinite_Doubly_Linked_Lists
("a-cfinse", F), -- Ada.Containers.Functional_Infinite_Sequences
("a-cfinve", F), -- Ada.Containers.Formal_Indefinite_Vectors
("a-coboho", F), -- Ada.Containers.Bounded_Holders
("a-cofove", F), -- Ada.Containers.Formal_Vectors
("a-cofuma", F), -- Ada.Containers.Functional_Maps
("a-cofuse", F), -- Ada.Containers.Functional_Sets
("a-cofuve", F), -- Ada.Containers.Functional_Vectors
("a-cfdlli", F), -- Ada.Containers.Formal_Doubly_Linked_Lists
("a-cforse", F), -- Ada.Containers.Formal_Ordered_Sets
("a-cforma", F), -- Ada.Containers.Formal_Ordered_Maps
("a-cfhase", F), -- Ada.Containers.Formal_Hashed_Sets
("a-cfhama", F), -- Ada.Containers.Formal_Hashed_Maps
("a-cvgpso", F) -- Ada.Containers.Vectors.Generic_Parallel_Sorting from
); -- GNATCOLL.OMP

1905
gcc/ada/libgnat/a-cfdlli.adb
View File

File diff suppressed because it is too large Load Diff

1641
gcc/ada/libgnat/a-cfdlli.ads
View File

File diff suppressed because it is too large Load Diff

976
gcc/ada/libgnat/a-cfhama.adb
View File

@ -1,976 +0,0 @@
------------------------------------------------------------------------------
-- --
-- GNAT LIBRARY COMPONENTS --
-- --
-- A D A . C O N T A I N E R S . F O R M A L _ H A S H E D _ M A P S --
-- --
-- B o d y --
-- --
-- Copyright (C) 2010-2022, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
with Ada.Containers.Hash_Tables.Generic_Formal_Operations;
pragma Elaborate_All (Ada.Containers.Hash_Tables.Generic_Formal_Operations);
with Ada.Containers.Hash_Tables.Generic_Formal_Keys;
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
SPARK_Mode => Off
is
-----------------------
-- Local Subprograms --
-----------------------
-- All local subprograms require comments ???
function Equivalent_Keys
(Key : Key_Type;
Node : Node_Type) return Boolean;
pragma Inline (Equivalent_Keys);
procedure Free
(HT : in out Map;
X : Count_Type);
generic
with procedure Set_Element (Node : in out Node_Type);
procedure Generic_Allocate
(HT : in out HT_Types.Hash_Table_Type;
Node : out Count_Type);
function Hash_Node (Node : Node_Type) return Hash_Type;
pragma Inline (Hash_Node);
function Next (Node : Node_Type) return Count_Type;
pragma Inline (Next);
procedure Set_Next (Node : in out Node_Type; Next : Count_Type);
pragma Inline (Set_Next);
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 --
--------------------------
package HT_Ops is
new Hash_Tables.Generic_Formal_Operations
(HT_Types => HT_Types,
Hash_Node => Hash_Node,
Next => Next,
Set_Next => Set_Next);
package Key_Ops is
new Hash_Tables.Generic_Formal_Keys
(HT_Types => HT_Types,
Next => Next,
Set_Next => Set_Next,
Key_Type => Key_Type,
Hash => Hash,
Equivalent_Keys => Equivalent_Keys);
---------
-- "=" --
---------
function "=" (Left, Right : Map) return Boolean is
begin
if Length (Left) /= Length (Right) then
return False;
end if;
if Length (Left) = 0 then
return True;
end if;
declare
Node : Count_Type;
ENode : Count_Type;
begin
Node := First (Left).Node;
while Node /= 0 loop
ENode :=
Find
(Container => Right,
Key => Left.Content.Nodes (Node).Key).Node;
if ENode = 0 or else
Right.Content.Nodes (ENode).Element /=
Left.Content.Nodes (Node).Element
then
return False;
end if;
Node := HT_Ops.Next (Left.Content, Node);
end loop;
return True;
end;
end "=";
------------
-- Assign --
------------
procedure Assign (Target : in out Map; Source : Map) is
procedure Insert_Element (Source_Node : Count_Type);
pragma Inline (Insert_Element);
procedure Insert_Elements is
new HT_Ops.Generic_Iteration (Insert_Element);
--------------------
-- Insert_Element --
--------------------
procedure Insert_Element (Source_Node : Count_Type) is
N : Node_Type renames Source.Content.Nodes (Source_Node);
begin
Insert (Target, N.Key, N.Element);
end Insert_Element;
-- Start of processing for Assign
begin
if Target.Capacity < Length (Source) then
raise Constraint_Error with -- correct exception ???
"Source length exceeds Target capacity";
end if;
Clear (Target);
Insert_Elements (Source.Content);
end Assign;
--------------
-- Capacity --
--------------
function Capacity (Container : Map) return Count_Type is
begin
return Container.Content.Nodes'Length;
end Capacity;
-----------
-- Clear --
-----------
procedure Clear (Container : in out Map) is
begin
HT_Ops.Clear (Container.Content);
end Clear;
------------------------
-- Constant_Reference --
------------------------
function Constant_Reference
(Container : aliased Map;
Position : Cursor) return not null access constant Element_Type
is
begin
if not Has_Element (Container, Position) then
raise Constraint_Error with "Position cursor has no element";
end if;
pragma Assert
(Vet (Container, Position),
"bad cursor in function Constant_Reference");
return Container.Content.Nodes (Position.Node).Element'Access;
end Constant_Reference;
function Constant_Reference
(Container : aliased Map;
Key : Key_Type) return not null access constant Element_Type
is
Node : constant Count_Type := Find (Container, Key).Node;
begin
if Node = 0 then
raise Constraint_Error with
"no element available because key not in map";
end if;
return Container.Content.Nodes (Node).Element'Access;
end Constant_Reference;
--------------
-- Contains --
--------------
function Contains (Container : Map; Key : Key_Type) return Boolean is
begin
return Find (Container, Key) /= No_Element;
end Contains;
----------
-- Copy --
----------
function Copy
(Source : Map;
Capacity : Count_Type := 0) return Map
is
C : constant Count_Type :=
Count_Type'Max (Capacity, Source.Capacity);
Cu : Cursor;
H : Hash_Type;
N : Count_Type;
Target : Map (C, Source.Modulus);
begin
if 0 < Capacity and then Capacity < Source.Capacity then
raise Capacity_Error;
end if;
Target.Content.Length := Source.Content.Length;
Target.Content.Free := Source.Content.Free;
H := 1;
while H <= Source.Modulus loop
Target.Content.Buckets (H) := Source.Content.Buckets (H);
H := H + 1;
end loop;
N := 1;
while N <= Source.Capacity loop
Target.Content.Nodes (N) := Source.Content.Nodes (N);
N := N + 1;
end loop;
while N <= C loop
Cu := (Node => N);
Free (Target, Cu.Node);
N := N + 1;
end loop;
return Target;
end Copy;
---------------------
-- Default_Modulus --
---------------------
function Default_Modulus (Capacity : Count_Type) return Hash_Type is
begin
return To_Prime (Capacity);
end Default_Modulus;
------------
-- Delete --
------------
procedure Delete (Container : in out Map; Key : Key_Type) is
X : Count_Type;
begin
Key_Ops.Delete_Key_Sans_Free (Container.Content, Key, X);
if X = 0 then
raise Constraint_Error with "attempt to delete key not in map";
end if;
Free (Container, X);
end Delete;
procedure Delete (Container : in out Map; Position : in out Cursor) is
begin
if not Has_Element (Container, Position) then
raise Constraint_Error with
"Position cursor of Delete has no element";
end if;
pragma Assert (Vet (Container, Position), "bad cursor in Delete");
HT_Ops.Delete_Node_Sans_Free (Container.Content, Position.Node);
Free (Container, Position.Node);
Position := No_Element;
end Delete;
-------------
-- Element --
-------------
function Element (Container : Map; Key : Key_Type) return Element_Type is
Node : constant Count_Type := Find (Container, Key).Node;
begin
if Node = 0 then
raise Constraint_Error with
"no element available because key not in map";
end if;
return Container.Content.Nodes (Node).Element;
end Element;
function Element (Container : Map; Position : Cursor) return Element_Type is
begin
if not Has_Element (Container, Position) then
raise Constraint_Error with "Position cursor equals No_Element";
end if;
pragma Assert
(Vet (Container, Position), "bad cursor in function Element");
return Container.Content.Nodes (Position.Node).Element;
end Element;
---------------------
-- Equivalent_Keys --
---------------------
function Equivalent_Keys
(Key : Key_Type;
Node : Node_Type) return Boolean
is
begin
return Equivalent_Keys (Key, Node.Key);
end Equivalent_Keys;
-------------
-- Exclude --
-------------
procedure Exclude (Container : in out Map; Key : Key_Type) is
X : Count_Type;
begin
Key_Ops.Delete_Key_Sans_Free (Container.Content, Key, X);
Free (Container, X);
end Exclude;
----------
-- Find --
----------
function Find (Container : Map; Key : Key_Type) return Cursor is
Node : constant Count_Type := Key_Ops.Find (Container.Content, Key);
begin
if Node = 0 then
return No_Element;
end if;
return (Node => Node);
end Find;
-----------
-- First --
-----------
function First (Container : Map) return Cursor is
Node : constant Count_Type := HT_Ops.First (Container.Content);
begin
if Node = 0 then
return No_Element;
end if;
return (Node => Node);
end First;
------------------
-- Formal_Model --
------------------
package body Formal_Model is
----------
-- Find --
----------
function Find
(Container : K.Sequence;
Key : Key_Type) return Count_Type
is
begin
for I in 1 .. K.Length (Container) loop
if Equivalent_Keys (Key, K.Get (Container, I)) then
return I;
end if;
end loop;
return 0;
end Find;
---------------------
-- K_Keys_Included --
---------------------
function K_Keys_Included
(Left : K.Sequence;
Right : K.Sequence) return Boolean
is
begin
for I in 1 .. K.Length (Left) loop
if not K.Contains (Right, 1, K.Length (Right), K.Get (Left, I))
then
return False;
end if;
end loop;
return True;
end K_Keys_Included;
----------
-- Keys --
----------
function Keys (Container : Map) return K.Sequence is
Position : Count_Type := HT_Ops.First (Container.Content);
R : K.Sequence;
begin
-- Can't use First, Next or Element here, since they depend on models
-- for their postconditions.
while Position /= 0 loop
R := K.Add (R, Container.Content.Nodes (Position).Key);
Position := HT_Ops.Next (Container.Content, Position);
end loop;
return R;
end Keys;
----------------------------
-- Lift_Abstraction_Level --
----------------------------
procedure Lift_Abstraction_Level (Container : Map) is null;
-----------------------
-- Mapping_Preserved --
-----------------------
function Mapping_Preserved
(K_Left : K.Sequence;
K_Right : K.Sequence;
P_Left : P.Map;
P_Right : P.Map) return Boolean
is
begin
for C of P_Left loop
if not P.Has_Key (P_Right, C)
or else P.Get (P_Left, C) > K.Length (K_Left)
or else P.Get (P_Right, C) > K.Length (K_Right)
or else K.Get (K_Left, P.Get (P_Left, C)) /=
K.Get (K_Right, P.Get (P_Right, C))
then
return False;
end if;
end loop;
return True;
end Mapping_Preserved;
-----------
-- Model --
-----------
function Model (Container : Map) return M.Map is
Position : Count_Type := HT_Ops.First (Container.Content);
R : M.Map;
begin
-- Can't use First, Next or Element here, since they depend on models
-- for their postconditions.
while Position /= 0 loop
R :=
M.Add
(Container => R,
New_Key => Container.Content.Nodes (Position).Key,
New_Item => Container.Content.Nodes (Position).Element);
Position := HT_Ops.Next (Container.Content, Position);
end loop;
return R;
end Model;
---------------
-- Positions --
---------------
function Positions (Container : Map) return P.Map is
I : Count_Type := 1;
Position : Count_Type := HT_Ops.First (Container.Content);
R : P.Map;
begin
-- 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) = Big (I));
Position := HT_Ops.Next (Container.Content, Position);
I := I + 1;
end loop;
return R;
end Positions;
end Formal_Model;
----------
-- Free --
----------
procedure Free (HT : in out Map; X : Count_Type) is
begin
if X /= 0 then
pragma Assert (X <= HT.Capacity);
HT.Content.Nodes (X).Has_Element := False;
HT_Ops.Free (HT.Content, X);
end if;
end Free;
----------------------
-- Generic_Allocate --
----------------------
procedure Generic_Allocate
(HT : in out HT_Types.Hash_Table_Type;
Node : out Count_Type)
is
procedure Allocate is
new HT_Ops.Generic_Allocate (Set_Element);
begin
Allocate (HT, Node);
HT.Nodes (Node).Has_Element := True;
end Generic_Allocate;
-----------------
-- Has_Element --
-----------------
function Has_Element (Container : Map; Position : Cursor) return Boolean is
begin
if Position.Node = 0
or else not Container.Content.Nodes (Position.Node).Has_Element
then
return False;
else
return True;
end if;
end Has_Element;
---------------
-- Hash_Node --
---------------
function Hash_Node (Node : Node_Type) return Hash_Type is
begin
return Hash (Node.Key);
end Hash_Node;
-------------
-- Include --
-------------
procedure Include
(Container : in out Map;
Key : Key_Type;
New_Item : Element_Type)
is
Position : Cursor;
Inserted : Boolean;
begin
Insert (Container, Key, New_Item, Position, Inserted);
if not Inserted then
declare
P : constant Count_Type := Position.Node;
N : Node_Type renames Container.Content.Nodes (P);
begin
N.Key := Key;
N.Element := New_Item;
end;
end if;
end Include;
------------
-- Insert --
------------
procedure Insert
(Container : in out Map;
Key : Key_Type;
New_Item : Element_Type;
Position : out Cursor;
Inserted : out Boolean)
is
procedure Assign_Key (Node : in out Node_Type);
pragma Inline (Assign_Key);
procedure New_Node
(HT : in out HT_Types.Hash_Table_Type;
Node : out Count_Type);
pragma Inline (New_Node);
procedure Local_Insert is
new Key_Ops.Generic_Conditional_Insert (New_Node);
procedure Allocate is
new Generic_Allocate (Assign_Key);
-----------------
-- Assign_Key --
-----------------
procedure Assign_Key (Node : in out Node_Type) is
begin
Node.Key := Key;
Node.Element := New_Item;
end Assign_Key;
--------------
-- New_Node --
--------------
procedure New_Node
(HT : in out HT_Types.Hash_Table_Type;
Node : out Count_Type)
is
begin
Allocate (HT, Node);
end New_Node;
-- Start of processing for Insert
begin
Local_Insert (Container.Content, Key, Position.Node, Inserted);
end Insert;
procedure Insert
(Container : in out Map;
Key : Key_Type;
New_Item : Element_Type)
is
Unused_Position : Cursor;
Inserted : Boolean;
begin
Insert (Container, Key, New_Item, Unused_Position, Inserted);
if not Inserted then
raise Constraint_Error with "attempt to insert key already in map";
end if;
end Insert;
--------------
-- Is_Empty --
--------------
function Is_Empty (Container : Map) return Boolean is
begin
return Length (Container) = 0;
end Is_Empty;
---------
-- Key --
---------
function Key (Container : Map; Position : Cursor) return Key_Type is
begin
if not Has_Element (Container, Position) then
raise Constraint_Error with
"Position cursor of function Key has no element";
end if;
pragma Assert (Vet (Container, Position), "bad cursor in function Key");
return Container.Content.Nodes (Position.Node).Key;
end Key;
------------
-- Length --
------------
function Length (Container : Map) return Count_Type is
begin
return Container.Content.Length;
end Length;
----------
-- Move --
----------
procedure Move
(Target : in out Map;
Source : in out Map)
is
NN : HT_Types.Nodes_Type renames Source.Content.Nodes;
X : Count_Type;
Y : Count_Type;
begin
if Target.Capacity < Length (Source) then
raise Constraint_Error with -- ???
"Source length exceeds Target capacity";
end if;
Clear (Target);
if Source.Content.Length = 0 then
return;
end if;
X := HT_Ops.First (Source.Content);
while X /= 0 loop
Insert (Target, NN (X).Key, NN (X).Element); -- optimize???
Y := HT_Ops.Next (Source.Content, X);
HT_Ops.Delete_Node_Sans_Free (Source.Content, X);
Free (Source, X);
X := Y;
end loop;
end Move;
----------
-- Next --
----------
function Next (Node : Node_Type) return Count_Type is
begin
return Node.Next;
end Next;
function Next (Container : Map; Position : Cursor) return Cursor is
begin
if Position.Node = 0 then
return No_Element;
end if;
if not Has_Element (Container, Position) then
raise Constraint_Error with "Position has no element";
end if;
pragma Assert (Vet (Container, Position), "bad cursor in function Next");
declare
Node : constant Count_Type :=
HT_Ops.Next (Container.Content, Position.Node);
begin
if Node = 0 then
return No_Element;
end if;
return (Node => Node);
end;
end Next;
procedure Next (Container : Map; Position : in out Cursor) is
begin
Position := Next (Container, Position);
end Next;
---------------
-- Reference --
---------------
function Reference
(Container : not null access Map;
Position : Cursor) return not null access Element_Type
is
begin
if not Has_Element (Container.all, Position) then
raise Constraint_Error with "Position cursor has no element";
end if;
pragma Assert
(Vet (Container.all, Position), "bad cursor in function Reference");
return Container.Content.Nodes (Position.Node).Element'Access;
end Reference;
function Reference
(Container : not null access Map;
Key : Key_Type) return not null access Element_Type
is
Node : constant Count_Type := Find (Container.all, Key).Node;
begin
if Node = 0 then
raise Constraint_Error with
"no element available because key not in map";
end if;
return Container.Content.Nodes (Node).Element'Access;
end Reference;
-------------
-- Replace --
-------------
procedure Replace
(Container : in out Map;
Key : Key_Type;
New_Item : Element_Type)
is
Node : constant Count_Type := Key_Ops.Find (Container.Content, Key);
begin
if Node = 0 then
raise Constraint_Error with "attempt to replace key not in map";
end if;
declare
N : Node_Type renames Container.Content.Nodes (Node);
begin
N.Key := Key;
N.Element := New_Item;
end;
end Replace;
---------------------
-- Replace_Element --
---------------------
procedure Replace_Element
(Container : in out Map;
Position : Cursor;
New_Item : Element_Type)
is
begin
if not Has_Element (Container, Position) then
raise Constraint_Error with
"Position cursor of Replace_Element has no element";
end if;
pragma Assert
(Vet (Container, Position), "bad cursor in Replace_Element");
Container.Content.Nodes (Position.Node).Element := New_Item;
end Replace_Element;
----------------------
-- Reserve_Capacity --
----------------------
procedure Reserve_Capacity
(Container : in out Map;
Capacity : Count_Type)
is
begin
if Capacity > Container.Capacity then
raise Capacity_Error with "requested capacity is too large";
end if;
end Reserve_Capacity;
--------------
-- Set_Next --
--------------
procedure Set_Next (Node : in out Node_Type; Next : Count_Type) is
begin
Node.Next := Next;
end Set_Next;
---------
-- Vet --
---------
function Vet (Container : Map; Position : Cursor) return Boolean is
begin
if not Container_Checks'Enabled then
return True;
end if;
if Position.Node = 0 then
return True;
end if;
declare
X : Count_Type;
begin
if Container.Content.Length = 0 then
return False;
end if;
if Container.Capacity = 0 then
return False;
end if;
if Container.Content.Buckets'Length = 0 then
return False;
end if;
if Position.Node > Container.Capacity then
return False;
end if;
if Container.Content.Nodes (Position.Node).Next = Position.Node then
return False;
end if;
X :=
Container.Content.Buckets
(Key_Ops.Index
(Container.Content,
Container.Content.Nodes (Position.Node).Key));
for J in 1 .. Container.Content.Length loop
if X = Position.Node then
return True;
end if;
if X = 0 then
return False;
end if;
if X = Container.Content.Nodes (X).Next then
-- Prevent unnecessary looping
return False;
end if;
X := Container.Content.Nodes (X).Next;
end loop;
return False;
end;
end Vet;
end Ada.Containers.Formal_Hashed_Maps;

883
gcc/ada/libgnat/a-cfhama.ads
View File

@ -29,885 +29,12 @@
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
-- This spec is derived from package Ada.Containers.Bounded_Hashed_Maps in the
-- Ada 2012 RM. The modifications are meant to facilitate formal proofs by
-- making it easier to express properties, and by making the specification of
-- this unit compatible with SPARK 2014. Note that the API of this unit may be
-- subject to incompatible changes as SPARK 2014 evolves.
-- The modifications are:
-- A parameter for the container is added to every function reading the
-- contents of a container: Key, Element, Next, Query_Element, Has_Element,
-- Iterate, Equivalent_Keys. This change is motivated by the need to have
-- cursors which are valid on different containers (typically a container C
-- and its previous version C'Old) for expressing properties, which is not
-- possible if cursors encapsulate an access to the underlying container.
-- Iteration over maps is done using the Iterable aspect, which is SPARK
-- compatible. "For of" iteration ranges over keys instead of elements.
with Ada.Containers.Functional_Vectors;
with Ada.Containers.Functional_Maps;
private with Ada.Containers.Hash_Tables;
generic
type Key_Type is private;
type Element_Type is private;
package Ada.Containers.Formal_Hashed_Maps with SPARK_Mode is
with function Hash (Key : Key_Type) return Hash_Type;
with function Equivalent_Keys
(Left : Key_Type;
Right : Key_Type) return Boolean is "=";
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Formal_Hashed_Maps with
SPARK_Mode,
Annotate => (GNATprove, Always_Return)
is
-- Contracts in this unit are meant for analysis only, not for run-time
-- checking.
pragma Assertion_Policy (Pre => Ignore);
pragma Assertion_Policy (Post => Ignore);
pragma Assertion_Policy (Contract_Cases => Ignore);
pragma Annotate (CodePeer, Skip_Analysis);
type Map (Capacity : Count_Type; Modulus : Hash_Type) is private with
Iterable => (First => First,
Next => Next,
Has_Element => Has_Element,
Element => Key),
Default_Initial_Condition => Is_Empty (Map);
pragma Preelaborable_Initialization (Map);
Empty_Map : constant Map;
type Cursor is record
Node : Count_Type;
end record;
No_Element : constant Cursor := (Node => 0);
function Length (Container : Map) return Count_Type with
Global => null,
Post => Length'Result <= Container.Capacity;
pragma Unevaluated_Use_Of_Old (Allow);
package Formal_Model with Ghost is
subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
package M is new Ada.Containers.Functional_Maps
(Element_Type => Element_Type,
Key_Type => Key_Type,
Equivalent_Keys => Equivalent_Keys);
function "="
(Left : M.Map;
Right : M.Map) return Boolean renames M."=";
function "<="
(Left : M.Map;
Right : M.Map) return Boolean renames M."<=";
package K is new Ada.Containers.Functional_Vectors
(Element_Type => Key_Type,
Index_Type => Positive_Count_Type);
function "="
(Left : K.Sequence;
Right : K.Sequence) return Boolean renames K."=";
function "<"
(Left : K.Sequence;
Right : K.Sequence) return Boolean renames K."<";
function "<="
(Left : K.Sequence;
Right : K.Sequence) return Boolean renames K."<=";
function Find (Container : K.Sequence; Key : Key_Type) return Count_Type
-- Search for Key in Container
with
Global => null,
Post =>
(if Find'Result > 0 then
Find'Result <= K.Length (Container)
and Equivalent_Keys (Key, K.Get (Container, Find'Result)));
function K_Keys_Included
(Left : K.Sequence;
Right : K.Sequence) return Boolean
-- Return True if Right contains all the keys of Left
with
Global => null,
Post =>
K_Keys_Included'Result =
(for all I in 1 .. K.Length (Left) =>
Find (Right, K.Get (Left, I)) > 0
and then K.Get (Right, Find (Right, K.Get (Left, I))) =
K.Get (Left, I));
package P is new Ada.Containers.Functional_Maps
(Key_Type => Cursor,
Element_Type => Positive_Count_Type,
Equivalent_Keys => "=",
Enable_Handling_Of_Equivalence => False);
function "="
(Left : P.Map;
Right : P.Map) return Boolean renames P."=";
function "<="
(Left : P.Map;
Right : P.Map) return Boolean renames P."<=";
function Mapping_Preserved
(K_Left : K.Sequence;
K_Right : K.Sequence;
P_Left : P.Map;
P_Right : P.Map) return Boolean
with
Global => null,
Post =>
(if Mapping_Preserved'Result then
-- Right contains all the cursors of Left
P.Keys_Included (P_Left, P_Right)
-- Right contains all the keys of Left
and K_Keys_Included (K_Left, K_Right)
-- Mappings from cursors to elements induced by K_Left, P_Left
-- and K_Right, P_Right are the same.
and (for all C of P_Left =>
K.Get (K_Left, P.Get (P_Left, C)) =
K.Get (K_Right, P.Get (P_Right, C))));
function Model (Container : Map) return M.Map with
-- The high-level model of a map is a map from keys to elements. Neither
-- cursors nor order of elements are represented in this model. Keys are
-- modeled up to equivalence.
Ghost,
Global => null;
function Keys (Container : Map) return K.Sequence with
-- The Keys sequence represents the underlying list structure of maps
-- that is used for iteration. It stores the actual values of keys in
-- the map. It does not model cursors nor elements.
Ghost,
Global => null,
Post =>
K.Length (Keys'Result) = Length (Container)
-- It only contains keys contained in Model
and (for all Key of Keys'Result =>
M.Has_Key (Model (Container), Key))
-- It contains all the keys contained in Model
and (for all Key of Model (Container) =>
(Find (Keys'Result, Key) > 0
and then Equivalent_Keys
(K.Get (Keys'Result, Find (Keys'Result, Key)),
Key)))
-- It has no duplicate
and (for all I in 1 .. Length (Container) =>
Find (Keys'Result, K.Get (Keys'Result, I)) = I)
and (for all I in 1 .. Length (Container) =>
(for all J in 1 .. Length (Container) =>
(if Equivalent_Keys
(K.Get (Keys'Result, I), K.Get (Keys'Result, J))
then
I = J)));
pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys);
function Positions (Container : Map) return P.Map with
-- The Positions map is used to model cursors. It only contains valid
-- cursors and maps them to their position in the container.
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 =>
(if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
then I = J)));
procedure Lift_Abstraction_Level (Container : Map) with
-- Lift_Abstraction_Level is a ghost procedure that does nothing but
-- assume that we can access the same elements by iterating over
-- positions or cursors.
-- This information is not generally useful except when switching from
-- a low-level, cursor-aware view of a container, to a high-level,
-- position-based view.
Ghost,
Global => null,
Post =>
(for all Key of Keys (Container) =>
(for some I of Positions (Container) =>
K.Get (Keys (Container), P.Get (Positions (Container), I)) =
Key));
function Contains
(C : M.Map;
K : Key_Type) return Boolean renames M.Has_Key;
-- To improve readability of contracts, we rename the function used to
-- search for a key in the model to Contains.
function Element
(C : M.Map;
K : Key_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;
function "=" (Left, Right : Map) return Boolean with
Global => null,
Post => "="'Result = (Model (Left) = Model (Right));
function Capacity (Container : Map) return Count_Type with
Global => null,
Post => Capacity'Result = Container.Capacity;
procedure Reserve_Capacity
(Container : in out Map;
Capacity : Count_Type)
with
Global => null,
Pre => Capacity <= Container.Capacity,
Post =>
Model (Container) = Model (Container)'Old
and Length (Container)'Old = Length (Container)
-- Actual keys are preserved
and K_Keys_Included (Keys (Container), Keys (Container)'Old)
and K_Keys_Included (Keys (Container)'Old, Keys (Container));
function Is_Empty (Container : Map) return Boolean with
Global => null,
Post => Is_Empty'Result = (Length (Container) = 0);
procedure Clear (Container : in out Map) with
Global => null,
Post => Length (Container) = 0 and M.Is_Empty (Model (Container));
procedure Assign (Target : in out Map; Source : Map) with
Global => null,
Pre => Target.Capacity >= Length (Source),
Post =>
Model (Target) = Model (Source)
and Length (Source) = Length (Target)
-- Actual keys are preserved
and K_Keys_Included (Keys (Target), Keys (Source))
and K_Keys_Included (Keys (Source), Keys (Target));
function Copy
(Source : Map;
Capacity : Count_Type := 0) return Map
with
Global => null,
Pre => Capacity = 0 or else Capacity >= Source.Capacity,
Post =>
Model (Copy'Result) = Model (Source)
and Keys (Copy'Result) = Keys (Source)
and Positions (Copy'Result) = Positions (Source)
and (if Capacity = 0 then
Copy'Result.Capacity = Source.Capacity
else
Copy'Result.Capacity = Capacity);
-- Copy returns a container stricty equal to Source. It must have the same
-- cursors associated with each element. Therefore:
-- - capacity=0 means use Source.Capacity as capacity of target
-- - the modulus cannot be changed.
function Key (Container : Map; Position : Cursor) return Key_Type with
Global => null,
Pre => Has_Element (Container, Position),
Post =>
Key'Result =
K.Get (Keys (Container), P.Get (Positions (Container), Position));
pragma Annotate (GNATprove, Inline_For_Proof, Key);
function Element
(Container : Map;
Position : Cursor) return Element_Type
with
Global => null,
Pre => Has_Element (Container, Position),
Post =>
Element'Result = Element (Model (Container), Key (Container, Position));
pragma Annotate (GNATprove, Inline_For_Proof, Element);
procedure Replace_Element
(Container : in out Map;
Position : Cursor;
New_Item : Element_Type)
with
Global => null,
Pre => Has_Element (Container, Position),
Post =>
-- Order of keys and cursors is preserved
Keys (Container) = Keys (Container)'Old
and Positions (Container) = Positions (Container)'Old
-- New_Item is now associated with the key at position Position in
-- Container.
and Element (Container, Position) = New_Item
-- Elements associated with other keys are preserved
and M.Same_Keys (Model (Container), Model (Container)'Old)
and M.Elements_Equal_Except
(Model (Container),
Model (Container)'Old,
Key (Container, Position));
function At_End
(E : not null access constant Map) return not null access constant Map
is (E)
with Ghost,
Annotate => (GNATprove, At_End_Borrow);
function At_End
(E : access constant Element_Type) return access constant Element_Type
is (E)
with Ghost,
Annotate => (GNATprove, At_End_Borrow);
function Constant_Reference
(Container : aliased Map;
Position : Cursor) return not null access constant Element_Type
with
Global => null,
Pre => Has_Element (Container, Position),
Post =>
Constant_Reference'Result.all =
Element (Model (Container), Key (Container, Position));
function Reference
(Container : not null access Map;
Position : Cursor) return not null access Element_Type
with
Global => null,
Pre => Has_Element (Container.all, Position),
Post =>
-- Order of keys and cursors is preserved
Keys (At_End (Container).all) = Keys (Container.all)
and Positions (At_End (Container).all) = Positions (Container.all)
-- The value designated by the result of Reference is now associated
-- with the key at position Position in Container.
and Element (At_End (Container).all, Position) =
At_End (Reference'Result).all
-- Elements associated with other keys are preserved
and M.Same_Keys
(Model (At_End (Container).all),
Model (Container.all))
and M.Elements_Equal_Except
(Model (At_End (Container).all),
Model (Container.all),
Key (At_End (Container).all, Position));
function Constant_Reference
(Container : aliased Map;
Key : Key_Type) return not null access constant Element_Type
with
Global => null,
Pre => Contains (Container, Key),
Post =>
Constant_Reference'Result.all = Element (Model (Container), Key);
function Reference
(Container : not null access Map;
Key : Key_Type) return not null access Element_Type
with
Global => null,
Pre => Contains (Container.all, Key),
Post =>
-- Order of keys and cursors is preserved
Keys (At_End (Container).all) = Keys (Container.all)
and Positions (At_End (Container).all) = Positions (Container.all)
-- The value designated by the result of Reference is now associated
-- with Key in Container.
and Element (Model (At_End (Container).all), Key) =
At_End (Reference'Result).all
-- Elements associated with other keys are preserved
and M.Same_Keys
(Model (At_End (Container).all),
Model (Container.all))
and M.Elements_Equal_Except
(Model (At_End (Container).all),
Model (Container.all),
Key);
procedure Move (Target : in out Map; Source : in out Map) with
Global => null,
Pre => Target.Capacity >= Length (Source),
Post =>
Model (Target) = Model (Source)'Old
and Length (Source)'Old = Length (Target)
and Length (Source) = 0
-- Actual keys are preserved
and K_Keys_Included (Keys (Target), Keys (Source)'Old)
and K_Keys_Included (Keys (Source)'Old, Keys (Target));
procedure Insert
(Container : in out Map;
Key : Key_Type;
New_Item : Element_Type;
Position : out Cursor;
Inserted : out Boolean)
with
Global => null,
Pre =>
Length (Container) < Container.Capacity or Contains (Container, Key),
Post =>
Contains (Container, Key)
and Has_Element (Container, Position)
and Equivalent_Keys
(Formal_Hashed_Maps.Key (Container, Position), Key),
Contract_Cases =>
-- If Key is already in Container, it is not modified and Inserted is
-- set to False.
(Contains (Container, Key) =>
not Inserted
and Model (Container) = Model (Container)'Old
and Keys (Container) = Keys (Container)'Old
and Positions (Container) = Positions (Container)'Old,
-- Otherwise, Key is inserted in Container and Inserted is set to True
others =>
Inserted
and Length (Container) = Length (Container)'Old + 1
-- Key now maps to New_Item
and Formal_Hashed_Maps.Key (Container, Position) = Key
and Element (Model (Container), Key) = New_Item
-- Other keys are preserved
and Model (Container)'Old <= Model (Container)
and M.Keys_Included_Except
(Model (Container),
Model (Container)'Old,
Key)
-- Mapping from cursors to keys is preserved
and Mapping_Preserved
(K_Left => Keys (Container)'Old,
K_Right => Keys (Container),
P_Left => Positions (Container)'Old,
P_Right => Positions (Container))
and P.Keys_Included_Except
(Positions (Container),
Positions (Container)'Old,
Position));
procedure Insert
(Container : in out Map;
Key : Key_Type;
New_Item : Element_Type)
with
Global => null,
Pre =>
Length (Container) < Container.Capacity
and then (not Contains (Container, Key)),
Post =>
Length (Container) = Length (Container)'Old + 1
and Contains (Container, Key)
-- Key now maps to New_Item
and Formal_Hashed_Maps.Key (Container, Find (Container, Key)) = Key
and Element (Model (Container), Key) = New_Item
-- Other keys are preserved
and Model (Container)'Old <= Model (Container)
and M.Keys_Included_Except
(Model (Container),
Model (Container)'Old,
Key)
-- Mapping from cursors to keys is preserved
and Mapping_Preserved
(K_Left => Keys (Container)'Old,
K_Right => Keys (Container),
P_Left => Positions (Container)'Old,
P_Right => Positions (Container))
and P.Keys_Included_Except
(Positions (Container),
Positions (Container)'Old,
Find (Container, Key));
procedure Include
(Container : in out Map;
Key : Key_Type;
New_Item : Element_Type)
with
Global => null,
Pre =>
Length (Container) < Container.Capacity or Contains (Container, Key),
Post =>
Contains (Container, Key) and Element (Container, Key) = New_Item,
Contract_Cases =>
-- If Key is already in Container, Key is mapped to New_Item
(Contains (Container, Key) =>
-- Cursors are preserved
Positions (Container) = Positions (Container)'Old
-- The key equivalent to Key in Container is replaced by Key
and K.Get
(Keys (Container),
P.Get (Positions (Container), Find (Container, Key))) = Key
and K.Equal_Except
(Keys (Container)'Old,
Keys (Container),
P.Get (Positions (Container), Find (Container, Key)))
-- Elements associated with other keys are preserved
and M.Same_Keys (Model (Container), Model (Container)'Old)
and M.Elements_Equal_Except
(Model (Container),
Model (Container)'Old,
Key),
-- Otherwise, Key is inserted in Container
others =>
Length (Container) = Length (Container)'Old + 1
-- Other keys are preserved
and Model (Container)'Old <= Model (Container)
and M.Keys_Included_Except
(Model (Container),
Model (Container)'Old,
Key)
-- Key is inserted in Container
and K.Get
(Keys (Container),
P.Get (Positions (Container), Find (Container, Key))) = Key
-- Mapping from cursors to keys is preserved
and Mapping_Preserved
(K_Left => Keys (Container)'Old,
K_Right => Keys (Container),
P_Left => Positions (Container)'Old,
P_Right => Positions (Container))
and P.Keys_Included_Except
(Positions (Container),
Positions (Container)'Old,
Find (Container, Key)));
procedure Replace
(Container : in out Map;
Key : Key_Type;
New_Item : Element_Type)
with
Global => null,
Pre => Contains (Container, Key),
Post =>
-- Cursors are preserved
Positions (Container) = Positions (Container)'Old
-- The key equivalent to Key in Container is replaced by Key
and K.Get
(Keys (Container),
P.Get (Positions (Container), Find (Container, Key))) = Key
and K.Equal_Except
(Keys (Container)'Old,
Keys (Container),
P.Get (Positions (Container), Find (Container, Key)))
-- New_Item is now associated with the Key in Container
and Element (Model (Container), Key) = New_Item
-- Elements associated with other keys are preserved
and M.Same_Keys (Model (Container), Model (Container)'Old)
and M.Elements_Equal_Except
(Model (Container),
Model (Container)'Old,
Key);
procedure Exclude (Container : in out Map; Key : Key_Type) with
Global => null,
Post => not Contains (Container, Key),
Contract_Cases =>
-- If Key is not in Container, nothing is changed
(not Contains (Container, Key) =>
Model (Container) = Model (Container)'Old
and Keys (Container) = Keys (Container)'Old
and Positions (Container) = Positions (Container)'Old,
-- Otherwise, Key is removed from Container
others =>
Length (Container) = Length (Container)'Old - 1
-- Other keys are preserved
and Model (Container) <= Model (Container)'Old
and M.Keys_Included_Except
(Model (Container)'Old,
Model (Container),
Key)
-- Mapping from cursors to keys is preserved
and Mapping_Preserved
(K_Left => Keys (Container),
K_Right => Keys (Container)'Old,
P_Left => Positions (Container),
P_Right => Positions (Container)'Old)
and P.Keys_Included_Except
(Positions (Container)'Old,
Positions (Container),
Find (Container, Key)'Old));
procedure Delete (Container : in out Map; Key : Key_Type) with
Global => null,
Pre => Contains (Container, Key),
Post =>
Length (Container) = Length (Container)'Old - 1
-- Key is no longer in Container
and not Contains (Container, Key)
-- Other keys are preserved
and Model (Container) <= Model (Container)'Old
and M.Keys_Included_Except
(Model (Container)'Old,
Model (Container),
Key)
-- Mapping from cursors to keys is preserved
and Mapping_Preserved
(K_Left => Keys (Container),
K_Right => Keys (Container)'Old,
P_Left => Positions (Container),
P_Right => Positions (Container)'Old)
and P.Keys_Included_Except
(Positions (Container)'Old,
Positions (Container),
Find (Container, Key)'Old);
procedure Delete (Container : in out Map; Position : in out Cursor) with
Global => null,
Depends => (Container =>+ Position, Position => null),
Pre => Has_Element (Container, Position),
Post =>
Position = No_Element
and Length (Container) = Length (Container)'Old - 1
-- The key at position Position is no longer in Container
and not Contains (Container, Key (Container, Position)'Old)
and not P.Has_Key (Positions (Container), Position'Old)
-- Other keys are preserved
and Model (Container) <= Model (Container)'Old
and M.Keys_Included_Except
(Model (Container)'Old,
Model (Container),
Key (Container, Position)'Old)
-- Mapping from cursors to keys is preserved
and Mapping_Preserved
(K_Left => Keys (Container),
K_Right => Keys (Container)'Old,
P_Left => Positions (Container),
P_Right => Positions (Container)'Old)
and P.Keys_Included_Except
(Positions (Container)'Old,
Positions (Container),
Position'Old);
function First (Container : Map) 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);
function Next (Container : Map; Position : Cursor) return Cursor with
Global => null,
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);
procedure Next (Container : Map; Position : in out Cursor) with
Global => null,
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);
function Find (Container : Map; Key : Key_Type) return Cursor with
Global => null,
Contract_Cases =>
-- If Key is not contained in Container, Find returns No_Element
(not Contains (Model (Container), Key) =>
Find'Result = No_Element,
-- Otherwise, Find returns a valid cursor in Container
others =>
P.Has_Key (Positions (Container), Find'Result)
and P.Get (Positions (Container), Find'Result) =
Find (Keys (Container), Key)
-- The key designated by the result of Find is Key
and Equivalent_Keys
(Formal_Hashed_Maps.Key (Container, Find'Result), Key));
function Contains (Container : Map; Key : Key_Type) return Boolean with
Global => null,
Post => Contains'Result = Contains (Model (Container), Key);
pragma Annotate (GNATprove, Inline_For_Proof, Contains);
function Element (Container : Map; Key : Key_Type) return Element_Type with
Global => null,
Pre => Contains (Container, Key),
Post => Element'Result = Element (Model (Container), Key);
pragma Annotate (GNATprove, Inline_For_Proof, Element);
function Has_Element (Container : Map; Position : Cursor) return Boolean
with
Global => null,
Post =>
Has_Element'Result = P.Has_Key (Positions (Container), Position);
pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
function Default_Modulus (Capacity : Count_Type) return Hash_Type with
Global => null;
private
pragma SPARK_Mode (Off);
pragma Inline (Length);
pragma Inline (Is_Empty);
pragma Inline (Clear);
pragma Inline (Key);
pragma Inline (Element);
pragma Inline (Contains);
pragma Inline (Capacity);
pragma Inline (Has_Element);
pragma Inline (Equivalent_Keys);
pragma Inline (Next);
type Node_Type is record
Key : Key_Type;
Element : aliased Element_Type;
Next : Count_Type;
Has_Element : Boolean := False;
end record;
package HT_Types is new
Ada.Containers.Hash_Tables.Generic_Formal_Hash_Table_Types (Node_Type);
type Map (Capacity : Count_Type; Modulus : Hash_Type) is record
Content : HT_Types.Hash_Table_Type (Capacity, Modulus);
end record;
Empty_Map : constant Map := (Capacity => 0, Modulus => 0, others => <>);
pragma Compile_Time_Error
(True,
"This package has been moved to the SPARK library shipped with any"
& " SPARK release starting with version 23.");
end Ada.Containers.Formal_Hashed_Maps;

1559
gcc/ada/libgnat/a-cfhase.adb
View File

File diff suppressed because it is too large Load Diff

1473
gcc/ada/libgnat/a-cfhase.ads
View File

File diff suppressed because it is too large Load Diff

2054
gcc/ada/libgnat/a-cfidll.adb
View File

File diff suppressed because it is too large Load Diff

1640
gcc/ada/libgnat/a-cfidll.ads
View File

File diff suppressed because it is too large Load Diff

304
gcc/ada/libgnat/a-cfinse.adb
View File

@ -1,304 +0,0 @@
------------------------------------------------------------------------------
-- --
-- GNAT LIBRARY COMPONENTS --
-- --
-- ADA.CONTAINERS.FUNCTIONAL_INFINITE_SEQUENCE --
-- --
-- B o d y --
-- --
-- Copyright (C) 2022-2022, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- apply solely to the contents of the part following the private keyword. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
pragma Ada_2012;
package body Ada.Containers.Functional_Infinite_Sequences
with SPARK_Mode => Off
is
use Containers;
-----------------------
-- Local Subprograms --
-----------------------
package Big_From_Count is new Signed_Conversions
(Int => Count_Type);
function Big (C : Count_Type) return Big_Integer renames
Big_From_Count.To_Big_Integer;
-- Store Count_Type'Last as a Big Natural because it is often used
Count_Type_Big_Last : constant Big_Natural := Big (Count_Type'Last);
function To_Count (C : Big_Natural) return Count_Type;
-- Convert Big_Natural to Count_Type
---------
-- "<" --
---------
function "<" (Left : Sequence; Right : Sequence) return Boolean is
(Length (Left) < Length (Right)
and then (for all N in Left =>
Get (Left, N) = Get (Right, N)));
----------
-- "<=" --
----------
function "<=" (Left : Sequence; Right : Sequence) return Boolean is
(Length (Left) <= Length (Right)
and then (for all N in Left =>
Get (Left, N) = Get (Right, N)));
---------
-- "=" --
---------
function "=" (Left : Sequence; Right : Sequence) return Boolean is
(Left.Content = Right.Content);
---------
-- Add --
---------
function Add (Container : Sequence; New_Item : Element_Type) return Sequence
is
(Add (Container, Last (Container) + 1, New_Item));
function Add
(Container : Sequence;
Position : Big_Positive;
New_Item : Element_Type) return Sequence is
(Content => Add (Container.Content, To_Count (Position), New_Item));
--------------------
-- Constant_Range --
--------------------
function Constant_Range
(Container : Sequence;
Fst : Big_Positive;
Lst : Big_Natural;
Item : Element_Type) return Boolean
is
Count_Fst : constant Count_Type := To_Count (Fst);
Count_Lst : constant Count_Type := To_Count (Lst);
begin
for J in Count_Fst .. Count_Lst loop
if Get (Container.Content, J) /= Item then
return False;
end if;
end loop;
return True;
end Constant_Range;
--------------
-- Contains --
--------------
function Contains
(Container : Sequence;
Fst : Big_Positive;
Lst : Big_Natural;
Item : Element_Type) return Boolean
is
Count_Fst : constant Count_Type := To_Count (Fst);
Count_Lst : constant Count_Type := To_Count (Lst);
begin
for J in Count_Fst .. Count_Lst loop
if Get (Container.Content, J) = Item then
return True;
end if;
end loop;
return False;
end Contains;
--------------------
-- Empty_Sequence --
--------------------
function Empty_Sequence return Sequence is
(Content => <>);
------------------
-- Equal_Except --
------------------
function Equal_Except
(Left : Sequence;
Right : Sequence;
Position : Big_Positive) return Boolean
is
Count_Pos : constant Count_Type := To_Count (Position);
Count_Lst : constant Count_Type := To_Count (Last (Left));
begin
if Length (Left) /= Length (Right) then
return False;
end if;
for J in 1 .. Count_Lst loop
if J /= Count_Pos
and then Get (Left.Content, J) /= Get (Right.Content, J)
then
return False;
end if;
end loop;
return True;
end Equal_Except;
function Equal_Except
(Left : Sequence;
Right : Sequence;
X : Big_Positive;
Y : Big_Positive) return Boolean
is
Count_X : constant Count_Type := To_Count (X);
Count_Y : constant Count_Type := To_Count (Y);
Count_Lst : constant Count_Type := To_Count (Last (Left));
begin
if Length (Left) /= Length (Right) then
return False;
end if;
for J in 1 .. Count_Lst loop
if J /= Count_X
and then J /= Count_Y
and then Get (Left.Content, J) /= Get (Right.Content, J)
then
return False;
end if;
end loop;
return True;
end Equal_Except;
---------
-- Get --
---------
function Get
(Container : Sequence;
Position : Big_Integer) return Element_Type is
(Get (Container.Content, To_Count (Position)));
----------
-- Last --
----------
function Last (Container : Sequence) return Big_Natural is
(Length (Container));
------------
-- Length --
------------
function Length (Container : Sequence) return Big_Natural is
(Big (Length (Container.Content)));
-----------------
-- Range_Equal --
-----------------
function Range_Equal
(Left : Sequence;
Right : Sequence;
Fst : Big_Positive;
Lst : Big_Natural) return Boolean
is
Count_Fst : constant Count_Type := To_Count (Fst);
Count_Lst : constant Count_Type := To_Count (Lst);
begin
for J in Count_Fst .. Count_Lst loop
if Get (Left.Content, J) /= Get (Right.Content, J) then
return False;
end if;
end loop;
return True;
end Range_Equal;
-------------------
-- Range_Shifted --
-------------------
function Range_Shifted
(Left : Sequence;
Right : Sequence;
Fst : Big_Positive;
Lst : Big_Natural;
Offset : Big_Integer) return Boolean
is
Count_Fst : constant Count_Type := To_Count (Fst);
Count_Lst : constant Count_Type := To_Count (Lst);
begin
for J in Count_Fst .. Count_Lst loop
if Get (Left.Content, J) /= Get (Right, Big (J) + Offset) then
return False;
end if;
end loop;
return True;
end Range_Shifted;
------------
-- Remove --
------------
function Remove
(Container : Sequence;
Position : Big_Positive) return Sequence is
(Content => Remove (Container.Content, To_Count (Position)));
---------
-- Set --
---------
function Set
(Container : Sequence;
Position : Big_Positive;
New_Item : Element_Type) return Sequence is
(Content => Set (Container.Content, To_Count (Position), New_Item));
--------------
-- To_Count --
--------------
function To_Count (C : Big_Natural) return Count_Type is
begin
if C > Count_Type_Big_Last then
raise Program_Error with "Big_Integer too large for Count_Type";
end if;
return Big_From_Count.From_Big_Integer (C);
end To_Count;
end Ada.Containers.Functional_Infinite_Sequences;

350
gcc/ada/libgnat/a-cfinse.ads
View File

@ -29,352 +29,12 @@
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
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;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Functional_Infinite_Sequences with SPARK_Mode is
package Ada.Containers.Functional_Infinite_Sequences with
SPARK_Mode,
Annotate => (GNATprove, Always_Return)
is
pragma Compile_Time_Error
(True,
"This package has been moved to the SPARK library shipped with any"
& " SPARK release starting with version 23.");
type Sequence is private
with Default_Initial_Condition => Length (Sequence) = 0,
Iterable => (First => Iter_First,
Has_Element => Iter_Has_Element,
Next => Iter_Next,
Element => Get);
-- Sequences are empty when default initialized.
-- Quantification over sequences can be done using the regular
-- quantification over its range or directly on its elements with "for of".
-----------------------
-- Basic operations --
-----------------------
-- Sequences are axiomatized using Length and Get, providing respectively
-- the length of a sequence and an accessor to its Nth element:
function Length (Container : Sequence) return Big_Natural with
-- Length of a sequence
Global => null;
function Get
(Container : Sequence;
Position : Big_Integer) return Element_Type
-- Access the Element at position Position in Container
with
Global => null,
Pre => Iter_Has_Element (Container, Position);
function Last (Container : Sequence) return Big_Natural with
-- Last index of a sequence
Global => null,
Post =>
Last'Result = Length (Container);
pragma Annotate (GNATprove, Inline_For_Proof, Last);
function First return Big_Positive is (1) with
-- First index of a sequence
Global => null;
------------------------
-- Property Functions --
------------------------
function "=" (Left : Sequence; Right : Sequence) return Boolean with
-- Extensional equality over sequences
Global => null,
Post =>
"="'Result =
(Length (Left) = Length (Right)
and then (for all N in Left => Get (Left, N) = Get (Right, N)));
pragma Annotate (GNATprove, Inline_For_Proof, "=");
function "<" (Left : Sequence; Right : Sequence) return Boolean with
-- Left is a strict subsequence of Right
Global => null,
Post =>
"<"'Result =
(Length (Left) < Length (Right)
and then (for all N in Left => Get (Left, N) = Get (Right, N)));
pragma Annotate (GNATprove, Inline_For_Proof, "<");
function "<=" (Left : Sequence; Right : Sequence) return Boolean with
-- Left is a subsequence of Right
Global => null,
Post =>
"<="'Result =
(Length (Left) <= Length (Right)
and then (for all N in Left => Get (Left, N) = Get (Right, N)));
pragma Annotate (GNATprove, Inline_For_Proof, "<=");
function Contains
(Container : Sequence;
Fst : Big_Positive;
Lst : Big_Natural;
Item : Element_Type) return Boolean
-- Returns True if Item occurs in the range from Fst to Lst of Container
with
Global => null,
Pre => Lst <= Last (Container),
Post =>
Contains'Result =
(for some J in Container =>
Fst <= J and J <= Lst and Get (Container, J) = Item);
pragma Annotate (GNATprove, Inline_For_Proof, Contains);
function Constant_Range
(Container : Sequence;
Fst : Big_Positive;
Lst : Big_Natural;
Item : Element_Type) return Boolean
-- Returns True if every element of the range from Fst to Lst of Container
-- is equal to Item.
with
Global => null,
Pre => Lst <= Last (Container),
Post =>
Constant_Range'Result =
(for all J in Container =>
(if Fst <= J and J <= Lst then Get (Container, J) = Item));
pragma Annotate (GNATprove, Inline_For_Proof, Constant_Range);
function Equal_Except
(Left : Sequence;
Right : Sequence;
Position : Big_Positive) return Boolean
-- Returns True is Left and Right are the same except at position Position
with
Global => null,
Pre => Position <= Last (Left),
Post =>
Equal_Except'Result =
(Length (Left) = Length (Right)
and then (for all J in Left =>
(if J /= Position then
Get (Left, J) = Get (Right, J))));
pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
function Equal_Except
(Left : Sequence;
Right : Sequence;
X : Big_Positive;
Y : Big_Positive) return Boolean
-- Returns True is Left and Right are the same except at positions X and Y
with
Global => null,
Pre => X <= Last (Left) and Y <= Last (Left),
Post =>
Equal_Except'Result =
(Length (Left) = Length (Right)
and then (for all J in Left =>
(if J /= X and J /= Y then
Get (Left, J) = Get (Right, J))));
pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
function Range_Equal
(Left : Sequence;
Right : Sequence;
Fst : Big_Positive;
Lst : Big_Natural) return Boolean
-- Returns True if the ranges from Fst to Lst contain the same elements in
-- Left and Right.
with
Global => null,
Pre => Lst <= Last (Left) and Lst <= Last (Right),
Post =>
Range_Equal'Result =
(for all J in Left =>
(if Fst <= J and J <= Lst then Get (Left, J) = Get (Right, J)));
pragma Annotate (GNATprove, Inline_For_Proof, Range_Equal);
function Range_Shifted
(Left : Sequence;
Right : Sequence;
Fst : Big_Positive;
Lst : Big_Natural;
Offset : Big_Integer) return Boolean
-- Returns True if the range from Fst to Lst in Left contains the same
-- elements as the range from Fst + Offset to Lst + Offset in Right.
with
Global => null,
Pre =>
Lst <= Last (Left)
and then
(if Fst <= Lst then
Offset + Fst >= 1 and Offset + Lst <= Length (Right)),
Post =>
Range_Shifted'Result =
((for all J in Left =>
(if Fst <= J and J <= Lst then
Get (Left, J) = Get (Right, J + Offset)))
and
(for all J in Right =>
(if Fst + Offset <= J and J <= Lst + Offset then
Get (Left, J - Offset) = Get (Right, J))));
pragma Annotate (GNATprove, Inline_For_Proof, Range_Shifted);
----------------------------
-- Construction Functions --
----------------------------
-- For better efficiency of both proofs and execution, avoid using
-- construction functions in annotations and rather use property functions.
function Set
(Container : Sequence;
Position : Big_Positive;
New_Item : Element_Type) return Sequence
-- Returns a new sequence which contains the same elements as Container
-- except for the one at position Position which is replaced by New_Item.
with
Global => null,
Pre => Position <= Last (Container),
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
-- plus New_Item at the end.
with
Global => null,
Post =>
Length (Add'Result) = Length (Container) + 1
and then Get (Add'Result, Last (Add'Result)) = New_Item
and then Container <= Add'Result;
function Add
(Container : Sequence;
Position : Big_Positive;
New_Item : Element_Type) return Sequence
with
-- Returns a new sequence which contains the same elements as Container
-- except that New_Item has been inserted at position Position.
Global => null,
Pre => Position <= Last (Container) + 1,
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 => 1,
Lst => Position - 1)
and then Range_Shifted
(Left => Container,
Right => Add'Result,
Fst => Position,
Lst => Last (Container),
Offset => 1);
function Remove
(Container : Sequence;
Position : Big_Positive) return Sequence
-- Returns a new sequence which contains the same elements as Container
-- except that the element at position Position has been removed.
with
Global => null,
Pre => Position <= Last (Container),
Post =>
Length (Remove'Result) = Length (Container) - 1
and then Range_Equal
(Left => Container,
Right => Remove'Result,
Fst => 1,
Lst => Position - 1)
and then Range_Shifted
(Left => Remove'Result,
Right => Container,
Fst => Position,
Lst => Last (Remove'Result),
Offset => 1);
function Copy_Element (Item : Element_Type) return Element_Type is (Item);
-- Elements of containers are copied by numerous primitives in this
-- package. This function causes GNATprove to verify that such a copy is
-- valid (in particular, it does not break the ownership policy of SPARK,
-- i.e. it does not contain pointers that could be used to alias mutable
-- data).
function Empty_Sequence return Sequence with
-- Return an empty Sequence
Global => null,
Post => Length (Empty_Sequence'Result) = 0;
---------------------------
-- Iteration Primitives --
---------------------------
function Iter_First (Container : Sequence) return Big_Integer with
Global => null,
Post => Iter_First'Result = 1;
function Iter_Has_Element
(Container : Sequence;
Position : Big_Integer) return Boolean
with
Global => null,
Post => Iter_Has_Element'Result =
In_Range (Position, 1, Length (Container));
pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element);
function Iter_Next
(Container : Sequence;
Position : Big_Integer) return Big_Integer
with
Global => null,
Pre => Iter_Has_Element (Container, Position),
Post => Iter_Next'Result = Position + 1;
private
pragma SPARK_Mode (Off);
subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
package Containers is new Ada.Containers.Functional_Base
(Index_Type => Positive_Count_Type,
Element_Type => Element_Type);
type Sequence is record
Content : Containers.Container;
end record;
function Iter_First (Container : Sequence) return Big_Integer is (1);
function Iter_Next
(Container : Sequence;
Position : Big_Integer) return Big_Integer
is
(Position + 1);
function Iter_Has_Element
(Container : Sequence;
Position : Big_Integer) return Boolean
is
(In_Range (Position, 1, Length (Container)));
end Ada.Containers.Functional_Infinite_Sequences;

1452
gcc/ada/libgnat/a-cfinve.adb
View File

File diff suppressed because it is too large Load Diff

957
gcc/ada/libgnat/a-cfinve.ads
View File

@ -29,959 +29,12 @@
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
-- Similar to Ada.Containers.Formal_Vectors. The main difference is that
-- Element_Type may be indefinite (but not an unconstrained array).
with Ada.Containers.Bounded_Holders;
with Ada.Containers.Functional_Vectors;
generic
type Index_Type is range <>;
type Element_Type (<>) is private;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
Max_Size_In_Storage_Elements : Natural;
-- Maximum size of Vector elements in bytes. This has the same meaning as
-- in Ada.Containers.Bounded_Holders, with the same restrictions. Note that
-- setting this too small can lead to erroneous execution; see comments in
-- Ada.Containers.Bounded_Holders. If Element_Type is class-wide, it is the
-- responsibility of clients to calculate the maximum size of all types in
-- the class.
package Ada.Containers.Formal_Indefinite_Vectors with SPARK_Mode is
Bounded : Boolean := True;
-- If True, the containers are bounded; the initial capacity is the maximum
-- size, and heap allocation will be avoided. If False, the containers can
-- grow via heap allocation.
package Ada.Containers.Formal_Indefinite_Vectors with
SPARK_Mode,
Annotate => (GNATprove, Always_Return)
is
-- Contracts in this unit are meant for analysis only, not for run-time
-- checking.
pragma Assertion_Policy (Pre => Ignore);
pragma Assertion_Policy (Post => Ignore);
pragma Assertion_Policy (Contract_Cases => Ignore);
pragma Annotate (CodePeer, Skip_Analysis);
subtype Extended_Index is Index_Type'Base
range Index_Type'First - 1 ..
Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
No_Index : constant Extended_Index := Extended_Index'First;
Last_Count : constant Count_Type :=
(if Index_Type'Last < Index_Type'First then
0
elsif Index_Type'Last < -1
or else Index_Type'Pos (Index_Type'First) >
Index_Type'Pos (Index_Type'Last) - Count_Type'Last
then
Index_Type'Pos (Index_Type'Last) -
Index_Type'Pos (Index_Type'First) + 1
else
Count_Type'Last);
-- Maximal capacity of any vector. It is the minimum of the size of the
-- index range and the last possible Count_Type.
subtype Capacity_Range is Count_Type range 0 .. Last_Count;
type Vector (Capacity : Capacity_Range) is limited private with
Default_Initial_Condition => Is_Empty (Vector);
-- In the bounded case, Capacity is the capacity of the container, which
-- never changes. In the unbounded case, Capacity is the initial capacity
-- of the container, and operations such as Reserve_Capacity and Append can
-- increase the capacity. The capacity never shrinks, except in the case of
-- Clear.
--
-- Note that all objects of type Vector are constrained, including in the
-- unbounded case; you can't assign from one object to another if the
-- Capacity is different.
function Length (Container : Vector) return Capacity_Range with
Global => null,
Post => Length'Result <= Capacity (Container);
pragma Unevaluated_Use_Of_Old (Allow);
package Formal_Model with Ghost is
package M is new Ada.Containers.Functional_Vectors
(Index_Type => Index_Type,
Element_Type => Element_Type);
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_In_Union
(Container : M.Sequence;
Left : M.Sequence;
Right : M.Sequence) return Boolean
-- The elements of Container are contained in either Left or Right
with
Global => null,
Post =>
M_Elements_In_Union'Result =
(for all I in Index_Type'First .. M.Last (Container) =>
(for some J in Index_Type'First .. M.Last (Left) =>
Element (Container, I) = Element (Left, J))
or (for some J in Index_Type'First .. M.Last (Right) =>
Element (Container, I) = Element (Right, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union);
function M_Elements_Included
(Left : M.Sequence;
L_Fst : Index_Type := Index_Type'First;
L_Lst : Extended_Index;
Right : M.Sequence;
R_Fst : Index_Type := Index_Type'First;
R_Lst : Extended_Index) return Boolean
-- The elements of the slice from L_Fst to L_Lst in Left are contained
-- in the slide from R_Fst to R_Lst in Right.
with
Global => null,
Pre => L_Lst <= M.Last (Left) and R_Lst <= M.Last (Right),
Post =>
M_Elements_Included'Result =
(for all I in L_Fst .. L_Lst =>
(for some J in R_Fst .. R_Lst =>
Element (Left, I) = Element (Right, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Included);
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 Index_Type'First .. M.Last (Left) =>
Element (Left, I) =
Element (Right, M.Last (Left) - I + 1))
and (for all I in Index_Type'First .. M.Last (Right) =>
Element (Right, I) =
Element (Left, M.Last (Left) - I + 1)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed);
function M_Elements_Swapped
(Left : M.Sequence;
Right : M.Sequence;
X : Index_Type;
Y : Index_Type) return Boolean
-- Elements stored at X and Y are reversed in Left and Right
with
Global => null,
Pre => X <= M.Last (Left) and Y <= M.Last (Left),
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));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped);
function Model (Container : Vector) return M.Sequence with
-- The high-level model of a vector is a sequence of elements. The
-- sequence really is similar to the vector itself. However, it is not
-- limited which allows usage of 'Old and 'Loop_Entry attributes.
Ghost,
Global => null,
Post => M.Length (Model'Result) = Length (Container);
function Element
(S : M.Sequence;
I : Index_Type) return Element_Type renames M.Get;
-- To improve readability of contracts, we rename the function used to
-- access an element in the model to Element.
end Formal_Model;
use Formal_Model;
function Empty_Vector return Vector with
Global => null,
Post => Length (Empty_Vector'Result) = 0;
function "=" (Left, Right : Vector) return Boolean with
Global => null,
Post => "="'Result = (Model (Left) = Model (Right));
function To_Vector
(New_Item : Element_Type;
Length : Capacity_Range) return Vector
with
Global => null,
Post =>
Formal_Indefinite_Vectors.Length (To_Vector'Result) = Length
and M.Constant_Range
(Container => Model (To_Vector'Result),
Fst => Index_Type'First,
Lst => Last_Index (To_Vector'Result),
Item => New_Item);
function Capacity (Container : Vector) return Capacity_Range with
Global => null,
Post =>
Capacity'Result =
(if Bounded then
Container.Capacity
else
Capacity_Range'Last);
pragma Annotate (GNATprove, Inline_For_Proof, Capacity);
procedure Reserve_Capacity
(Container : in out Vector;
Capacity : Capacity_Range)
with
Global => null,
Pre => (if Bounded then Capacity <= Container.Capacity),
Post => Model (Container) = Model (Container)'Old;
function Is_Empty (Container : Vector) return Boolean with
Global => null,
Post => Is_Empty'Result = (Length (Container) = 0);
procedure Clear (Container : in out Vector) with
Global => null,
Post => Length (Container) = 0;
-- Note that this reclaims storage in the unbounded case. You need to call
-- this before a container goes out of scope in order to avoid storage
-- leaks. In addition, "X := ..." can leak unless you Clear(X) first.
procedure Assign (Target : in out Vector; Source : Vector) with
Global => null,
Pre => (if Bounded then Length (Source) <= Target.Capacity),
Post => Model (Target) = Model (Source);
function Copy
(Source : Vector;
Capacity : Capacity_Range := 0) return Vector
with
Global => null,
Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)),
Post =>
Model (Copy'Result) = Model (Source)
and (if Capacity = 0 then
Copy'Result.Capacity = Length (Source)
else
Copy'Result.Capacity = Capacity);
procedure Move (Target : in out Vector; Source : in out Vector)
with
Global => null,
Pre => (if Bounded then Length (Source) <= Capacity (Target)),
Post => Model (Target) = Model (Source)'Old and Length (Source) = 0;
function Element
(Container : Vector;
Index : Extended_Index) return Element_Type
with
Global => null,
Pre => Index in First_Index (Container) .. Last_Index (Container),
Post => Element'Result = Element (Model (Container), Index);
pragma Annotate (GNATprove, Inline_For_Proof, Element);
procedure Replace_Element
(Container : in out Vector;
Index : Index_Type;
New_Item : Element_Type)
with
Global => null,
Pre => Index in First_Index (Container) .. Last_Index (Container),
Post =>
Length (Container) = Length (Container)'Old
-- Container now has New_Item at index Index
and Element (Model (Container), Index) = New_Item
-- All other elements are preserved
and M.Equal_Except
(Left => Model (Container)'Old,
Right => Model (Container),
Position => Index);
function At_End (E : access constant Vector) return access constant Vector
is (E)
with Ghost,
Annotate => (GNATprove, At_End_Borrow);
function At_End
(E : access constant Element_Type) return access constant Element_Type
is (E)
with Ghost,
Annotate => (GNATprove, At_End_Borrow);
function Constant_Reference
(Container : aliased Vector;
Index : Index_Type) return not null access constant Element_Type
with
Global => null,
Pre => Index in First_Index (Container) .. Last_Index (Container),
Post =>
Constant_Reference'Result.all = Element (Model (Container), Index);
function Reference
(Container : not null access Vector;
Index : Index_Type) return not null access Element_Type
with
Global => null,
Pre =>
Index in First_Index (Container.all) .. Last_Index (Container.all),
Post =>
Length (Container.all) = Length (At_End (Container).all)
-- Container will have Result.all at index Index
and At_End (Reference'Result).all =
Element (Model (At_End (Container).all), Index)
-- All other elements are preserved
and M.Equal_Except
(Left => Model (Container.all),
Right => Model (At_End (Container).all),
Position => Index);
procedure Insert
(Container : in out Vector;
Before : Extended_Index;
New_Item : Vector)
with
Global => null,
Pre =>
Length (Container) <= Capacity (Container) - Length (New_Item)
and (Before in Index_Type'First .. Last_Index (Container)
or (Before /= No_Index
and then Before - 1 = Last_Index (Container))),
Post =>
Length (Container) = Length (Container)'Old + Length (New_Item)
-- Elements located before Before in Container are preserved
and M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Before - 1)
-- Elements of New_Item are inserted at position Before
and (if Length (New_Item) > 0 then
M.Range_Shifted
(Left => Model (New_Item),
Right => Model (Container),
Fst => Index_Type'First,
Lst => Last_Index (New_Item),
Offset => Count_Type (Before - Index_Type'First)))
-- Elements located after Before in Container are shifted
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Before,
Lst => Last_Index (Container)'Old,
Offset => Length (New_Item));
procedure Insert
(Container : in out Vector;
Before : Extended_Index;
New_Item : Element_Type)
with
Global => null,
Pre =>
Length (Container) < Capacity (Container)
and then (Before in Index_Type'First .. Last_Index (Container) + 1),
Post =>
Length (Container) = Length (Container)'Old + 1
-- Elements located before Before in Container are preserved
and M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Before - 1)
-- Container now has New_Item at index Before
and Element (Model (Container), Before) = New_Item
-- Elements located after Before in Container are shifted by 1
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Before,
Lst => Last_Index (Container)'Old,
Offset => 1);
procedure Insert
(Container : in out Vector;
Before : Extended_Index;
New_Item : Element_Type;
Count : Count_Type)
with
Global => null,
Pre =>
Length (Container) <= Capacity (Container) - Count
and (Before in Index_Type'First .. Last_Index (Container)
or (Before /= No_Index
and then Before - 1 = Last_Index (Container))),
Post =>
Length (Container) = Length (Container)'Old + Count
-- Elements located before Before in Container are preserved
and M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Before - 1)
-- New_Item is inserted Count times at position Before
and (if Count > 0 then
M.Constant_Range
(Container => Model (Container),
Fst => Before,
Lst => Before + Index_Type'Base (Count - 1),
Item => New_Item))
-- Elements located after Before in Container are shifted
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Before,
Lst => Last_Index (Container)'Old,
Offset => Count);
procedure Prepend (Container : in out Vector; New_Item : Vector) with
Global => null,
Pre => Length (Container) <= Capacity (Container) - Length (New_Item),
Post =>
Length (Container) = Length (Container)'Old + Length (New_Item)
-- Elements of New_Item are inserted at the beginning of Container
and M.Range_Equal
(Left => Model (New_Item),
Right => Model (Container),
Fst => Index_Type'First,
Lst => Last_Index (New_Item))
-- Elements of Container are shifted
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Last_Index (Container)'Old,
Offset => Length (New_Item));
procedure Prepend (Container : in out Vector; New_Item : Element_Type) with
Global => null,
Pre => Length (Container) < Capacity (Container),
Post =>
Length (Container) = Length (Container)'Old + 1
-- Container now has New_Item at Index_Type'First
and Element (Model (Container), Index_Type'First) = New_Item
-- Elements of Container are shifted by 1
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Last_Index (Container)'Old,
Offset => 1);
procedure Prepend
(Container : in out Vector;
New_Item : Element_Type;
Count : Count_Type)
with
Global => null,
Pre => Length (Container) <= Capacity (Container) - Count,
Post =>
Length (Container) = Length (Container)'Old + Count
-- New_Item is inserted Count times at the beginning of Container
and M.Constant_Range
(Container => Model (Container),
Fst => Index_Type'First,
Lst => Index_Type'First + Index_Type'Base (Count - 1),
Item => New_Item)
-- Elements of Container are shifted
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Last_Index (Container)'Old,
Offset => Count);
procedure Append (Container : in out Vector; New_Item : Vector) with
Global => null,
Pre =>
Length (Container) <= Capacity (Container) - Length (New_Item),
Post =>
Length (Container) = Length (Container)'Old + Length (New_Item)
-- The elements of Container are preserved
and Model (Container)'Old <= Model (Container)
-- Elements of New_Item are inserted at the end of Container
and (if Length (New_Item) > 0 then
M.Range_Shifted
(Left => Model (New_Item),
Right => Model (Container),
Fst => Index_Type'First,
Lst => Last_Index (New_Item),
Offset =>
Count_Type
(Last_Index (Container)'Old - Index_Type'First + 1)));
procedure Append (Container : in out Vector; New_Item : Element_Type) with
Global => null,
Pre => Length (Container) < Capacity (Container),
Post =>
Length (Container) = Length (Container)'Old + 1
-- Elements of Container are preserved
and Model (Container)'Old < Model (Container)
-- Container now has New_Item at the end of Container
and Element
(Model (Container), Last_Index (Container)'Old + 1) = New_Item;
procedure Append
(Container : in out Vector;
New_Item : Element_Type;
Count : Count_Type)
with
Global => null,
Pre => Length (Container) <= Capacity (Container) - Count,
Post =>
Length (Container) = Length (Container)'Old + Count
-- Elements of Container are preserved
and Model (Container)'Old <= Model (Container)
-- New_Item is inserted Count times at the end of Container
and (if Count > 0 then
M.Constant_Range
(Container => Model (Container),
Fst => Last_Index (Container)'Old + 1,
Lst =>
Last_Index (Container)'Old + Index_Type'Base (Count),
Item => New_Item));
procedure Delete (Container : in out Vector; Index : Extended_Index) with
Global => null,
Pre => Index in First_Index (Container) .. Last_Index (Container),
Post =>
Length (Container) = Length (Container)'Old - 1
-- Elements located before Index in Container are preserved
and M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Index - 1)
-- Elements located after Index in Container are shifted by 1
and M.Range_Shifted
(Left => Model (Container),
Right => Model (Container)'Old,
Fst => Index,
Lst => Last_Index (Container),
Offset => 1);
procedure Delete
(Container : in out Vector;
Index : Extended_Index;
Count : Count_Type)
with
Global => null,
Pre =>
Index in First_Index (Container) .. Last_Index (Container),
Post =>
Length (Container) in
Length (Container)'Old - Count .. Length (Container)'Old
-- The elements of Container located before Index are preserved.
and M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Index - 1),
Contract_Cases =>
-- All the elements after Position have been erased
(Length (Container) - Count <= Count_Type (Index - Index_Type'First) =>
Length (Container) = Count_Type (Index - Index_Type'First),
others =>
Length (Container) = Length (Container)'Old - Count
-- Other elements are shifted by Count
and M.Range_Shifted
(Left => Model (Container),
Right => Model (Container)'Old,
Fst => Index,
Lst => Last_Index (Container),
Offset => Count));
procedure Delete_First (Container : in out Vector) with
Global => null,
Pre => Length (Container) > 0,
Post =>
Length (Container) = Length (Container)'Old - 1
-- Elements of Container are shifted by 1
and M.Range_Shifted
(Left => Model (Container),
Right => Model (Container)'Old,
Fst => Index_Type'First,
Lst => Last_Index (Container),
Offset => 1);
procedure Delete_First (Container : in out Vector; 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) = Length (Container)'Old - Count
-- Elements of Container are shifted by Count
and M.Range_Shifted
(Left => Model (Container),
Right => Model (Container)'Old,
Fst => Index_Type'First,
Lst => Last_Index (Container),
Offset => Count));
procedure Delete_Last (Container : in out Vector) with
Global => null,
Pre => Length (Container) > 0,
Post =>
Length (Container) = Length (Container)'Old - 1
-- Elements of Container are preserved
and Model (Container) < Model (Container)'Old;
procedure Delete_Last (Container : in out Vector; Count : Count_Type) with
Global => null,
Contract_Cases =>
-- All the elements after Position have been erased
(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);
procedure Reverse_Elements (Container : in out Vector) with
Global => null,
Post => M_Elements_Reversed (Model (Container)'Old, Model (Container));
procedure Swap
(Container : in out Vector;
I : Index_Type;
J : Index_Type)
with
Global => null,
Pre =>
I in First_Index (Container) .. Last_Index (Container)
and then J in First_Index (Container) .. Last_Index (Container),
Post =>
M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J);
function First_Index (Container : Vector) return Index_Type with
Global => null,
Post => First_Index'Result = Index_Type'First;
pragma Annotate (GNATprove, Inline_For_Proof, First_Index);
function First_Element (Container : Vector) return Element_Type with
Global => null,
Pre => not Is_Empty (Container),
Post =>
First_Element'Result = Element (Model (Container), Index_Type'First);
pragma Annotate (GNATprove, Inline_For_Proof, First_Element);
function Last_Index (Container : Vector) return Extended_Index with
Global => null,
Post => Last_Index'Result = M.Last (Model (Container));
pragma Annotate (GNATprove, Inline_For_Proof, Last_Index);
function Last_Element (Container : Vector) return Element_Type with
Global => null,
Pre => not Is_Empty (Container),
Post =>
Last_Element'Result =
Element (Model (Container), Last_Index (Container));
pragma Annotate (GNATprove, Inline_For_Proof, Last_Element);
function Find_Index
(Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'First) return Extended_Index
with
Global => null,
Contract_Cases =>
-- If Item is not contained in Container after Index, Find_Index
-- returns No_Index.
(Index > Last_Index (Container)
or else not M.Contains
(Container => Model (Container),
Fst => Index,
Lst => Last_Index (Container),
Item => Item)
=>
Find_Index'Result = No_Index,
-- Otherwise, Find_Index returns a valid index greater than Index
others =>
Find_Index'Result in Index .. Last_Index (Container)
-- The element at this index in Container is Item
and Element (Model (Container), Find_Index'Result) = Item
-- It is the first occurrence of Item after Index in Container
and not M.Contains
(Container => Model (Container),
Fst => Index,
Lst => Find_Index'Result - 1,
Item => Item));
function Reverse_Find_Index
(Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'Last) return Extended_Index
with
Global => null,
Contract_Cases =>
-- If Item is not contained in Container before Index,
-- Reverse_Find_Index returns No_Index.
(not M.Contains
(Container => Model (Container),
Fst => Index_Type'First,
Lst => (if Index <= Last_Index (Container) then Index
else Last_Index (Container)),
Item => Item)
=>
Reverse_Find_Index'Result = No_Index,
-- Otherwise, Reverse_Find_Index returns a valid index smaller than
-- Index
others =>
Reverse_Find_Index'Result in Index_Type'First .. Index
and Reverse_Find_Index'Result <= Last_Index (Container)
-- The element at this index in Container is Item
and Element (Model (Container), Reverse_Find_Index'Result) = Item
-- It is the last occurrence of Item before Index in Container
and not M.Contains
(Container => Model (Container),
Fst => Reverse_Find_Index'Result + 1,
Lst =>
(if Index <= Last_Index (Container) then
Index
else
Last_Index (Container)),
Item => Item));
function Contains
(Container : Vector;
Item : Element_Type) return Boolean
with
Global => null,
Post =>
Contains'Result =
M.Contains
(Container => Model (Container),
Fst => Index_Type'First,
Lst => Last_Index (Container),
Item => Item);
function Has_Element
(Container : Vector;
Position : Extended_Index) return Boolean
with
Global => null,
Post =>
Has_Element'Result =
(Position in Index_Type'First .. Last_Index (Container));
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
package Formal_Model with Ghost is
function M_Elements_Sorted (Container : M.Sequence) return Boolean
with
Global => null,
Post =>
M_Elements_Sorted'Result =
(for all I in Index_Type'First .. M.Last (Container) =>
(for all J in I .. M.Last (Container) =>
Element (Container, I) = Element (Container, J)
or Element (Container, I) < Element (Container, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
end Formal_Model;
use Formal_Model;
function Is_Sorted (Container : Vector) return Boolean with
Global => null,
Post => Is_Sorted'Result = M_Elements_Sorted (Model (Container));
procedure Sort (Container : in out Vector) with
Global => null,
Post =>
Length (Container) = Length (Container)'Old
and M_Elements_Sorted (Model (Container))
and M_Elements_Included
(Left => Model (Container)'Old,
L_Lst => Last_Index (Container),
Right => Model (Container),
R_Lst => Last_Index (Container))
and M_Elements_Included
(Left => Model (Container),
L_Lst => Last_Index (Container),
Right => Model (Container)'Old,
R_Lst => Last_Index (Container));
procedure Merge (Target : in out Vector; Source : in out Vector) with
-- Target and Source should not be aliased
Global => null,
Pre => Length (Source) <= Capacity (Target) - 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)))
and M_Elements_Included
(Left => Model (Target)'Old,
L_Lst => Last_Index (Target)'Old,
Right => Model (Target),
R_Lst => Last_Index (Target))
and M_Elements_Included
(Left => Model (Source)'Old,
L_Lst => Last_Index (Source)'Old,
Right => Model (Target),
R_Lst => Last_Index (Target))
and M_Elements_In_Union
(Model (Target),
Model (Source)'Old,
Model (Target)'Old);
end Generic_Sorting;
private
pragma SPARK_Mode (Off);
pragma Inline (First_Index);
pragma Inline (Last_Index);
pragma Inline (Element);
pragma Inline (First_Element);
pragma Inline (Last_Element);
pragma Inline (Replace_Element);
pragma Inline (Contains);
-- The implementation method is to instantiate Bounded_Holders to get a
-- definite type for Element_Type.
package Holders is new Bounded_Holders
(Element_Type, Max_Size_In_Storage_Elements, "=");
use Holders;
subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last;
type Elements_Array is array (Array_Index range <>) of aliased Holder;
function "=" (L, R : Elements_Array) return Boolean is abstract;
type Elements_Array_Ptr is access all Elements_Array;
type Vector (Capacity : Capacity_Range) is limited record
-- In the bounded case, the elements are stored in Elements. In the
-- unbounded case, the elements are initially stored in Elements, until
-- we run out of room, then we switch to Elements_Ptr.
Last : Extended_Index := No_Index;
Elements_Ptr : Elements_Array_Ptr := null;
Elements : aliased Elements_Array (1 .. Capacity);
end record;
-- The primary reason Vector is limited is that in the unbounded case, once
-- Elements_Ptr is in use, assignment statements won't work. "X := Y;" will
-- cause X and Y to share state; that is, X.Elements_Ptr = Y.Elements_Ptr,
-- so for example "Append (X, ...);" will modify BOTH X and Y. That would
-- allow SPARK to "prove" things that are false. We could fix that by
-- making Vector a controlled type, and override Adjust to make a deep
-- copy, but finalization is not allowed in SPARK.
--
-- Note that (unfortunately) this means that 'Old and 'Loop_Entry are not
-- allowed on Vectors.
function Empty_Vector return Vector is
((Capacity => 0, others => <>));
pragma Compile_Time_Error
(True,
"This package has been moved to the SPARK library shipped with any"
& " SPARK release starting with version 23.");
end Ada.Containers.Formal_Indefinite_Vectors;

1239
gcc/ada/libgnat/a-cforma.adb
View File

File diff suppressed because it is too large Load Diff

1122
gcc/ada/libgnat/a-cforma.ads
View File

File diff suppressed because it is too large Load Diff

1939
gcc/ada/libgnat/a-cforse.adb
View File

File diff suppressed because it is too large Load Diff

1784
gcc/ada/libgnat/a-cforse.ads
View File

File diff suppressed because it is too large Load Diff

1311
gcc/ada/libgnat/a-cofove.adb
View File

File diff suppressed because it is too large Load Diff

952
gcc/ada/libgnat/a-cofove.ads
View File

@ -29,954 +29,12 @@
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
-- This spec is derived from package Ada.Containers.Bounded_Vectors in the Ada
-- 2012 RM. The modifications are meant to facilitate formal proofs by making
-- it easier to express properties, and by making the specification of this
-- unit compatible with SPARK 2014. Note that the API of this unit may be
-- subject to incompatible changes as SPARK 2014 evolves.
with Ada.Containers.Functional_Vectors;
generic
type Index_Type is range <>;
type Element_Type is private;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Formal_Vectors with SPARK_Mode is
package Ada.Containers.Formal_Vectors with
SPARK_Mode
is
pragma Annotate (GNATprove, Always_Return, Formal_Vectors);
-- Contracts in this unit are meant for analysis only, not for run-time
-- checking.
pragma Assertion_Policy (Pre => Ignore);
pragma Assertion_Policy (Post => Ignore);
pragma Assertion_Policy (Contract_Cases => Ignore);
pragma Annotate (CodePeer, Skip_Analysis);
subtype Extended_Index is Index_Type'Base
range Index_Type'First - 1 ..
Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
No_Index : constant Extended_Index := Extended_Index'First;
Last_Count : constant Count_Type :=
(if Index_Type'Last < Index_Type'First then
0
elsif Index_Type'Last < -1
or else Index_Type'Pos (Index_Type'First) >
Index_Type'Pos (Index_Type'Last) - Count_Type'Last
then
Index_Type'Pos (Index_Type'Last) -
Index_Type'Pos (Index_Type'First) + 1
else
Count_Type'Last);
-- Maximal capacity of any vector. It is the minimum of the size of the
-- index range and the last possible Count_Type.
subtype Capacity_Range is Count_Type range 0 .. Last_Count;
type Vector (Capacity : Capacity_Range) is private with
Default_Initial_Condition => Is_Empty (Vector),
Iterable => (First => Iter_First,
Has_Element => Iter_Has_Element,
Next => Iter_Next,
Element => Element);
function Length (Container : Vector) return Capacity_Range with
Global => null,
Post => Length'Result <= Capacity (Container);
pragma Unevaluated_Use_Of_Old (Allow);
package Formal_Model with Ghost is
package M is new Ada.Containers.Functional_Vectors
(Index_Type => Index_Type,
Element_Type => Element_Type);
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_In_Union
(Container : M.Sequence;
Left : M.Sequence;
Right : M.Sequence) return Boolean
-- The elements of Container are contained in either Left or Right
with
Global => null,
Post =>
M_Elements_In_Union'Result =
(for all I in Index_Type'First .. M.Last (Container) =>
(for some J in Index_Type'First .. M.Last (Left) =>
Element (Container, I) = Element (Left, J))
or (for some J in Index_Type'First .. M.Last (Right) =>
Element (Container, I) = Element (Right, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union);
function M_Elements_Included
(Left : M.Sequence;
L_Fst : Index_Type := Index_Type'First;
L_Lst : Extended_Index;
Right : M.Sequence;
R_Fst : Index_Type := Index_Type'First;
R_Lst : Extended_Index) return Boolean
-- The elements of the slice from L_Fst to L_Lst in Left are contained
-- in the slide from R_Fst to R_Lst in Right.
with
Global => null,
Pre => L_Lst <= M.Last (Left) and R_Lst <= M.Last (Right),
Post =>
M_Elements_Included'Result =
(for all I in L_Fst .. L_Lst =>
(for some J in R_Fst .. R_Lst =>
Element (Left, I) = Element (Right, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Included);
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 Index_Type'First .. M.Last (Left) =>
Element (Left, I) =
Element (Right, M.Last (Left) - I + 1))
and (for all I in Index_Type'First .. M.Last (Right) =>
Element (Right, I) =
Element (Left, M.Last (Left) - I + 1)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed);
function M_Elements_Swapped
(Left : M.Sequence;
Right : M.Sequence;
X : Index_Type;
Y : Index_Type) return Boolean
-- Elements stored at X and Y are reversed in Left and Right
with
Global => null,
Pre => X <= M.Last (Left) and Y <= M.Last (Left),
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));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped);
function Model (Container : Vector) return M.Sequence with
-- The high-level model of a vector is a sequence of elements. The
-- sequence really is similar to the vector itself. However, it is not
-- limited which allows usage of 'Old and 'Loop_Entry attributes.
Ghost,
Global => null,
Post => M.Length (Model'Result) = Length (Container);
pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Model);
function Element
(S : M.Sequence;
I : Index_Type) return Element_Type renames M.Get;
-- To improve readability of contracts, we rename the function used to
-- access an element in the model to Element.
end Formal_Model;
use Formal_Model;
function Empty_Vector return Vector with
Global => null,
Post => Length (Empty_Vector'Result) = 0;
function "=" (Left, Right : Vector) return Boolean with
Global => null,
Post => "="'Result = (Model (Left) = Model (Right));
function To_Vector
(New_Item : Element_Type;
Length : Capacity_Range) return Vector
with
Global => null,
Post =>
Formal_Vectors.Length (To_Vector'Result) = Length
and M.Constant_Range
(Container => Model (To_Vector'Result),
Fst => Index_Type'First,
Lst => Last_Index (To_Vector'Result),
Item => New_Item);
function Capacity (Container : Vector) return Capacity_Range with
Global => null,
Post =>
Capacity'Result = Container.Capacity;
pragma Annotate (GNATprove, Inline_For_Proof, Capacity);
procedure Reserve_Capacity
(Container : in out Vector;
Capacity : Capacity_Range)
with
Global => null,
Pre => Capacity <= Container.Capacity,
Post => Model (Container) = Model (Container)'Old;
function Is_Empty (Container : Vector) return Boolean with
Global => null,
Post => Is_Empty'Result = (Length (Container) = 0);
procedure Clear (Container : in out Vector) with
Global => null,
Post => Length (Container) = 0;
procedure Assign (Target : in out Vector; Source : Vector) with
Global => null,
Pre => Length (Source) <= Target.Capacity,
Post => Model (Target) = Model (Source);
function Copy
(Source : Vector;
Capacity : Capacity_Range := 0) return Vector
with
Global => null,
Pre => (Capacity = 0 or Length (Source) <= Capacity),
Post =>
Model (Copy'Result) = Model (Source)
and (if Capacity = 0 then
Copy'Result.Capacity = Length (Source)
else
Copy'Result.Capacity = Capacity);
procedure Move (Target : in out Vector; Source : in out Vector)
with
Global => null,
Pre => Length (Source) <= Capacity (Target),
Post => Model (Target) = Model (Source)'Old and Length (Source) = 0;
function Element
(Container : Vector;
Index : Extended_Index) return Element_Type
with
Global => null,
Pre => Index in First_Index (Container) .. Last_Index (Container),
Post => Element'Result = Element (Model (Container), Index);
pragma Annotate (GNATprove, Inline_For_Proof, Element);
procedure Replace_Element
(Container : in out Vector;
Index : Index_Type;
New_Item : Element_Type)
with
Global => null,
Pre => Index in First_Index (Container) .. Last_Index (Container),
Post =>
Length (Container) = Length (Container)'Old
-- Container now has New_Item at index Index
and Element (Model (Container), Index) = New_Item
-- All other elements are preserved
and M.Equal_Except
(Left => Model (Container)'Old,
Right => Model (Container),
Position => Index);
function At_End (E : access constant Vector) return access constant Vector
is (E)
with Ghost,
Annotate => (GNATprove, At_End_Borrow);
function At_End
(E : access constant Element_Type) return access constant Element_Type
is (E)
with Ghost,
Annotate => (GNATprove, At_End_Borrow);
function Constant_Reference
(Container : aliased Vector;
Index : Index_Type) return not null access constant Element_Type
with
Global => null,
Pre => Index in First_Index (Container) .. Last_Index (Container),
Post =>
Constant_Reference'Result.all = Element (Model (Container), Index);
function Reference
(Container : not null access Vector;
Index : Index_Type) return not null access Element_Type
with
Global => null,
Pre =>
Index in First_Index (Container.all) .. Last_Index (Container.all),
Post =>
Length (Container.all) = Length (At_End (Container).all)
-- Container will have Result.all at index Index
and At_End (Reference'Result).all =
Element (Model (At_End (Container).all), Index)
-- All other elements are preserved
and M.Equal_Except
(Left => Model (Container.all),
Right => Model (At_End (Container).all),
Position => Index);
procedure Insert
(Container : in out Vector;
Before : Extended_Index;
New_Item : Vector)
with
Global => null,
Pre =>
Length (Container) <= Capacity (Container) - Length (New_Item)
and (Before in Index_Type'First .. Last_Index (Container)
or (Before /= No_Index
and then Before - 1 = Last_Index (Container))),
Post =>
Length (Container) = Length (Container)'Old + Length (New_Item)
-- Elements located before Before in Container are preserved
and M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Before - 1)
-- Elements of New_Item are inserted at position Before
and (if Length (New_Item) > 0 then
M.Range_Shifted
(Left => Model (New_Item),
Right => Model (Container),
Fst => Index_Type'First,
Lst => Last_Index (New_Item),
Offset => Count_Type (Before - Index_Type'First)))
-- Elements located after Before in Container are shifted
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Before,
Lst => Last_Index (Container)'Old,
Offset => Length (New_Item));
procedure Insert
(Container : in out Vector;
Before : Extended_Index;
New_Item : Element_Type)
with
Global => null,
Pre =>
Length (Container) < Capacity (Container)
and then (Before in Index_Type'First .. Last_Index (Container) + 1),
Post =>
Length (Container) = Length (Container)'Old + 1
-- Elements located before Before in Container are preserved
and M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Before - 1)
-- Container now has New_Item at index Before
and Element (Model (Container), Before) = New_Item
-- Elements located after Before in Container are shifted by 1
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Before,
Lst => Last_Index (Container)'Old,
Offset => 1);
procedure Insert
(Container : in out Vector;
Before : Extended_Index;
New_Item : Element_Type;
Count : Count_Type)
with
Global => null,
Pre =>
Length (Container) <= Capacity (Container) - Count
and (Before in Index_Type'First .. Last_Index (Container)
or (Before /= No_Index
and then Before - 1 = Last_Index (Container))),
Post =>
Length (Container) = Length (Container)'Old + Count
-- Elements located before Before in Container are preserved
and M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Before - 1)
-- New_Item is inserted Count times at position Before
and (if Count > 0 then
M.Constant_Range
(Container => Model (Container),
Fst => Before,
Lst => Before + Index_Type'Base (Count - 1),
Item => New_Item))
-- Elements located after Before in Container are shifted
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Before,
Lst => Last_Index (Container)'Old,
Offset => Count);
procedure Prepend (Container : in out Vector; New_Item : Vector) with
Global => null,
Pre => Length (Container) <= Capacity (Container) - Length (New_Item),
Post =>
Length (Container) = Length (Container)'Old + Length (New_Item)
-- Elements of New_Item are inserted at the beginning of Container
and M.Range_Equal
(Left => Model (New_Item),
Right => Model (Container),
Fst => Index_Type'First,
Lst => Last_Index (New_Item))
-- Elements of Container are shifted
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Last_Index (Container)'Old,
Offset => Length (New_Item));
procedure Prepend (Container : in out Vector; New_Item : Element_Type) with
Global => null,
Pre => Length (Container) < Capacity (Container),
Post =>
Length (Container) = Length (Container)'Old + 1
-- Container now has New_Item at Index_Type'First
and Element (Model (Container), Index_Type'First) = New_Item
-- Elements of Container are shifted by 1
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Last_Index (Container)'Old,
Offset => 1);
procedure Prepend
(Container : in out Vector;
New_Item : Element_Type;
Count : Count_Type)
with
Global => null,
Pre => Length (Container) <= Capacity (Container) - Count,
Post =>
Length (Container) = Length (Container)'Old + Count
-- New_Item is inserted Count times at the beginning of Container
and M.Constant_Range
(Container => Model (Container),
Fst => Index_Type'First,
Lst => Index_Type'First + Index_Type'Base (Count - 1),
Item => New_Item)
-- Elements of Container are shifted
and M.Range_Shifted
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Last_Index (Container)'Old,
Offset => Count);
procedure Append (Container : in out Vector; New_Item : Vector) with
Global => null,
Pre =>
Length (Container) <= Capacity (Container) - Length (New_Item),
Post =>
Length (Container) = Length (Container)'Old + Length (New_Item)
-- The elements of Container are preserved
and Model (Container)'Old <= Model (Container)
-- Elements of New_Item are inserted at the end of Container
and (if Length (New_Item) > 0 then
M.Range_Shifted
(Left => Model (New_Item),
Right => Model (Container),
Fst => Index_Type'First,
Lst => Last_Index (New_Item),
Offset =>
Count_Type
(Last_Index (Container)'Old - Index_Type'First + 1)));
procedure Append (Container : in out Vector; New_Item : Element_Type) with
Global => null,
Pre => Length (Container) < Capacity (Container),
Post =>
Length (Container) = Length (Container)'Old + 1
-- Elements of Container are preserved
and Model (Container)'Old < Model (Container)
-- Container now has New_Item at the end of Container
and Element
(Model (Container), Last_Index (Container)'Old + 1) = New_Item;
procedure Append
(Container : in out Vector;
New_Item : Element_Type;
Count : Count_Type)
with
Global => null,
Pre => Length (Container) <= Capacity (Container) - Count,
Post =>
Length (Container) = Length (Container)'Old + Count
-- Elements of Container are preserved
and Model (Container)'Old <= Model (Container)
-- New_Item is inserted Count times at the end of Container
and (if Count > 0 then
M.Constant_Range
(Container => Model (Container),
Fst => Last_Index (Container)'Old + 1,
Lst =>
Last_Index (Container)'Old + Index_Type'Base (Count),
Item => New_Item));
procedure Delete (Container : in out Vector; Index : Extended_Index) with
Global => null,
Pre => Index in First_Index (Container) .. Last_Index (Container),
Post =>
Length (Container) = Length (Container)'Old - 1
-- Elements located before Index in Container are preserved
and M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Index - 1)
-- Elements located after Index in Container are shifted by 1
and M.Range_Shifted
(Left => Model (Container),
Right => Model (Container)'Old,
Fst => Index,
Lst => Last_Index (Container),
Offset => 1);
procedure Delete
(Container : in out Vector;
Index : Extended_Index;
Count : Count_Type)
with
Global => null,
Pre =>
Index in First_Index (Container) .. Last_Index (Container),
Post =>
Length (Container) in
Length (Container)'Old - Count .. Length (Container)'Old
-- The elements of Container located before Index are preserved.
and M.Range_Equal
(Left => Model (Container)'Old,
Right => Model (Container),
Fst => Index_Type'First,
Lst => Index - 1),
Contract_Cases =>
-- All the elements after Position have been erased
(Length (Container) - Count <= Count_Type (Index - Index_Type'First) =>
Length (Container) = Count_Type (Index - Index_Type'First),
others =>
Length (Container) = Length (Container)'Old - Count
-- Other elements are shifted by Count
and M.Range_Shifted
(Left => Model (Container),
Right => Model (Container)'Old,
Fst => Index,
Lst => Last_Index (Container),
Offset => Count));
procedure Delete_First (Container : in out Vector) with
Global => null,
Pre => Length (Container) > 0,
Post =>
Length (Container) = Length (Container)'Old - 1
-- Elements of Container are shifted by 1
and M.Range_Shifted
(Left => Model (Container),
Right => Model (Container)'Old,
Fst => Index_Type'First,
Lst => Last_Index (Container),
Offset => 1);
procedure Delete_First (Container : in out Vector; 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) = Length (Container)'Old - Count
-- Elements of Container are shifted by Count
and M.Range_Shifted
(Left => Model (Container),
Right => Model (Container)'Old,
Fst => Index_Type'First,
Lst => Last_Index (Container),
Offset => Count));
procedure Delete_Last (Container : in out Vector) with
Global => null,
Pre => Length (Container) > 0,
Post =>
Length (Container) = Length (Container)'Old - 1
-- Elements of Container are preserved
and Model (Container) < Model (Container)'Old;
procedure Delete_Last (Container : in out Vector; Count : Count_Type) with
Global => null,
Contract_Cases =>
-- All the elements after Position have been erased
(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);
procedure Reverse_Elements (Container : in out Vector) with
Global => null,
Post => M_Elements_Reversed (Model (Container)'Old, Model (Container));
procedure Swap
(Container : in out Vector;
I : Index_Type;
J : Index_Type)
with
Global => null,
Pre =>
I in First_Index (Container) .. Last_Index (Container)
and then J in First_Index (Container) .. Last_Index (Container),
Post =>
M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J);
function First_Index (Container : Vector) return Index_Type with
Global => null,
Post => First_Index'Result = Index_Type'First;
pragma Annotate (GNATprove, Inline_For_Proof, First_Index);
function First_Element (Container : Vector) return Element_Type with
Global => null,
Pre => not Is_Empty (Container),
Post =>
First_Element'Result = Element (Model (Container), Index_Type'First);
pragma Annotate (GNATprove, Inline_For_Proof, First_Element);
function Last_Index (Container : Vector) return Extended_Index with
Global => null,
Post => Last_Index'Result = M.Last (Model (Container));
pragma Annotate (GNATprove, Inline_For_Proof, Last_Index);
function Last_Element (Container : Vector) return Element_Type with
Global => null,
Pre => not Is_Empty (Container),
Post =>
Last_Element'Result =
Element (Model (Container), Last_Index (Container));
pragma Annotate (GNATprove, Inline_For_Proof, Last_Element);
function Find_Index
(Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'First) return Extended_Index
with
Global => null,
Contract_Cases =>
-- If Item is not contained in Container after Index, Find_Index
-- returns No_Index.
(Index > Last_Index (Container)
or else not M.Contains
(Container => Model (Container),
Fst => Index,
Lst => Last_Index (Container),
Item => Item)
=>
Find_Index'Result = No_Index,
-- Otherwise, Find_Index returns a valid index greater than Index
others =>
Find_Index'Result in Index .. Last_Index (Container)
-- The element at this index in Container is Item
and Element (Model (Container), Find_Index'Result) = Item
-- It is the first occurrence of Item after Index in Container
and not M.Contains
(Container => Model (Container),
Fst => Index,
Lst => Find_Index'Result - 1,
Item => Item));
function Reverse_Find_Index
(Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'Last) return Extended_Index
with
Global => null,
Contract_Cases =>
-- If Item is not contained in Container before Index,
-- Reverse_Find_Index returns No_Index.
(not M.Contains
(Container => Model (Container),
Fst => Index_Type'First,
Lst => (if Index <= Last_Index (Container) then Index
else Last_Index (Container)),
Item => Item)
=>
Reverse_Find_Index'Result = No_Index,
-- Otherwise, Reverse_Find_Index returns a valid index smaller than
-- Index
others =>
Reverse_Find_Index'Result in Index_Type'First .. Index
and Reverse_Find_Index'Result <= Last_Index (Container)
-- The element at this index in Container is Item
and Element (Model (Container), Reverse_Find_Index'Result) = Item
-- It is the last occurrence of Item before Index in Container
and not M.Contains
(Container => Model (Container),
Fst => Reverse_Find_Index'Result + 1,
Lst =>
(if Index <= Last_Index (Container) then
Index
else
Last_Index (Container)),
Item => Item));
function Contains
(Container : Vector;
Item : Element_Type) return Boolean
with
Global => null,
Post =>
Contains'Result =
M.Contains
(Container => Model (Container),
Fst => Index_Type'First,
Lst => Last_Index (Container),
Item => Item);
function Has_Element
(Container : Vector;
Position : Extended_Index) return Boolean
with
Global => null,
Post =>
Has_Element'Result =
(Position in Index_Type'First .. Last_Index (Container));
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
package Formal_Model with Ghost is
function M_Elements_Sorted (Container : M.Sequence) return Boolean
with
Global => null,
Post =>
M_Elements_Sorted'Result =
(for all I in Index_Type'First .. M.Last (Container) =>
(for all J in I .. M.Last (Container) =>
Element (Container, I) = Element (Container, J)
or Element (Container, I) < Element (Container, J)));
pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted);
end Formal_Model;
use Formal_Model;
function Is_Sorted (Container : Vector) return Boolean with
Global => null,
Post => Is_Sorted'Result = M_Elements_Sorted (Model (Container));
procedure Sort (Container : in out Vector) with
Global => null,
Post =>
Length (Container) = Length (Container)'Old
and M_Elements_Sorted (Model (Container))
and M_Elements_Included
(Left => Model (Container)'Old,
L_Lst => Last_Index (Container),
Right => Model (Container),
R_Lst => Last_Index (Container))
and M_Elements_Included
(Left => Model (Container),
L_Lst => Last_Index (Container),
Right => Model (Container)'Old,
R_Lst => Last_Index (Container));
procedure Merge (Target : in out Vector; Source : in out Vector) with
-- Target and Source should not be aliased
Global => null,
Pre => Length (Source) <= Capacity (Target) - 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)))
and M_Elements_Included
(Left => Model (Target)'Old,
L_Lst => Last_Index (Target)'Old,
Right => Model (Target),
R_Lst => Last_Index (Target))
and M_Elements_Included
(Left => Model (Source)'Old,
L_Lst => Last_Index (Source)'Old,
Right => Model (Target),
R_Lst => Last_Index (Target))
and M_Elements_In_Union
(Model (Target),
Model (Source)'Old,
Model (Target)'Old);
end Generic_Sorting;
---------------------------
-- Iteration Primitives --
---------------------------
function Iter_First (Container : Vector) return Extended_Index with
Global => null;
function Iter_Has_Element
(Container : Vector;
Position : Extended_Index) return Boolean
with
Global => null,
Post =>
Iter_Has_Element'Result =
(Position in Index_Type'First .. Last_Index (Container));
pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element);
function Iter_Next
(Container : Vector;
Position : Extended_Index) return Extended_Index
with
Global => null,
Pre => Iter_Has_Element (Container, Position);
private
pragma SPARK_Mode (Off);
pragma Inline (First_Index);
pragma Inline (Last_Index);
pragma Inline (Element);
pragma Inline (First_Element);
pragma Inline (Last_Element);
pragma Inline (Replace_Element);
pragma Inline (Contains);
subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last;
type Elements_Array is array (Array_Index range <>) of aliased Element_Type;
function "=" (L, R : Elements_Array) return Boolean is abstract;
type Vector (Capacity : Capacity_Range) is record
Last : Extended_Index := No_Index;
Elements : Elements_Array (1 .. Capacity);
end record;
function Empty_Vector return Vector is
((Capacity => 0, others => <>));
function Iter_First (Container : Vector) return Extended_Index is
(Index_Type'First);
function Iter_Next
(Container : Vector;
Position : Extended_Index) return Extended_Index
is
(if Position = Extended_Index'Last then
Extended_Index'First
else
Extended_Index'Succ (Position));
function Iter_Has_Element
(Container : Vector;
Position : Extended_Index) return Boolean
is
(Position in Index_Type'First .. Container.Last);
pragma Compile_Time_Error
(True,
"This package has been moved to the SPARK library shipped with any"
& " SPARK release starting with version 23.");
end Ada.Containers.Formal_Vectors;

432
gcc/ada/libgnat/a-cofuba.adb
View File

@ -1,432 +0,0 @@
------------------------------------------------------------------------------
-- --
-- GNAT LIBRARY COMPONENTS --
-- --
-- ADA.CONTAINERS.FUNCTIONAL_BASE --
-- --
-- B o d y --
-- --
-- Copyright (C) 2016-2022, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- apply solely to the contents of the part following the private keyword. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
pragma Ada_2012;
with Ada.Unchecked_Deallocation;
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)));
-- Conversion functions between Index_Type and Count_Type
function Find (C : Container; E : access Element_Type) return Count_Type;
-- Search a container C for an element equal to E.all, returning the
-- position in the underlying array.
procedure Resize (Base : Array_Base_Access);
-- Resize the underlying array if needed so that it can contain one more
-- element.
function Elements (C : Container) return Element_Array_Access is
(C.Controlled_Base.Base.Elements)
with
Global => null,
Pre =>
C.Controlled_Base.Base /= null
and then C.Controlled_Base.Base.Elements /= null;
function Get
(C_E : Element_Array_Access;
I : Count_Type)
return Element_Access
is
(C_E (I).Ref.E_Access)
with
Global => null,
Pre => C_E /= null and then C_E (I).Ref /= null;
---------
-- "=" --
---------
function "=" (C1 : Container; C2 : Container) return Boolean is
begin
if C1.Length /= C2.Length then
return False;
end if;
for I in 1 .. C1.Length loop
if Get (Elements (C1), I).all /= Get (Elements (C2), I).all then
return False;
end if;
end loop;
return True;
end "=";
----------
-- "<=" --
----------
function "<=" (C1 : Container; C2 : Container) return Boolean is
begin
for I in 1 .. C1.Length loop
if Find (C2, Get (Elements (C1), I)) = 0 then
return False;
end if;
end loop;
return True;
end "<=";
---------
-- Add --
---------
function Add
(C : Container;
I : Index_Type;
E : Element_Type) return Container
is
C_B : Array_Base_Access renames C.Controlled_Base.Base;
begin
if To_Count (I) = C.Length + 1 and then C.Length = C_B.Max_Length then
Resize (C_B);
C_B.Max_Length := C_B.Max_Length + 1;
C_B.Elements (C_B.Max_Length) := Element_Init (E);
return Container'(Length => C_B.Max_Length,
Controlled_Base => C.Controlled_Base);
else
declare
A : constant Array_Base_Controlled_Access :=
Content_Init (C.Length);
P : Count_Type := 0;
begin
A.Base.Max_Length := C.Length + 1;
for J in 1 .. C.Length + 1 loop
if J /= To_Count (I) then
P := P + 1;
A.Base.Elements (J) := C_B.Elements (P);
else
A.Base.Elements (J) := Element_Init (E);
end if;
end loop;
return Container'(Length => A.Base.Max_Length,
Controlled_Base => A);
end;
end if;
end Add;
------------
-- Adjust --
------------
procedure Adjust (Controlled_Base : in out Array_Base_Controlled_Access) is
C_B : Array_Base_Access renames Controlled_Base.Base;
begin
if C_B /= null then
C_B.Reference_Count := C_B.Reference_Count + 1;
end if;
end Adjust;
procedure Adjust (Ctrl_E : in out Controlled_Element_Access) is
begin
if Ctrl_E.Ref /= null then
Ctrl_E.Ref.Reference_Count := Ctrl_E.Ref.Reference_Count + 1;
end if;
end Adjust;
------------------
-- Content_Init --
------------------
function Content_Init
(L : Count_Type := 0) return Array_Base_Controlled_Access
is
Max_Init : constant Count_Type := 100;
Size : constant Count_Type :=
(if L < Count_Type'Last - Max_Init then L + Max_Init
else Count_Type'Last);
-- The Access in the array will be initialized to null
Elements : constant Element_Array_Access :=
new Element_Array'(1 .. Size => <>);
B : constant Array_Base_Access :=
new Array_Base'(Reference_Count => 1,
Max_Length => 0,
Elements => Elements);
begin
return (Ada.Finalization.Controlled with Base => B);
end Content_Init;
------------------
-- Element_Init --
------------------
function Element_Init (E : Element_Type) return Controlled_Element_Access
is
Refcounted_E : constant Refcounted_Element_Access :=
new Refcounted_Element'(Reference_Count => 1,
E_Access => new Element_Type'(E));
begin
return (Ada.Finalization.Controlled with Ref => Refcounted_E);
end Element_Init;
--------------
-- Finalize --
--------------
procedure Finalize (Controlled_Base : in out Array_Base_Controlled_Access)
is
procedure Unchecked_Free_Base is new Ada.Unchecked_Deallocation
(Object => Array_Base,
Name => Array_Base_Access);
procedure Unchecked_Free_Array is new Ada.Unchecked_Deallocation
(Object => Element_Array,
Name => Element_Array_Access);
C_B : Array_Base_Access renames Controlled_Base.Base;
begin
if C_B /= null then
C_B.Reference_Count := C_B.Reference_Count - 1;
if C_B.Reference_Count = 0 then
Unchecked_Free_Array (Controlled_Base.Base.Elements);
Unchecked_Free_Base (Controlled_Base.Base);
end if;
C_B := null;
end if;
end Finalize;
procedure Finalize (Ctrl_E : in out Controlled_Element_Access) is
procedure Unchecked_Free_Ref is new Ada.Unchecked_Deallocation
(Object => Refcounted_Element,
Name => Refcounted_Element_Access);
procedure Unchecked_Free_Element is new Ada.Unchecked_Deallocation
(Object => Element_Type,
Name => Element_Access);
begin
if Ctrl_E.Ref /= null then
Ctrl_E.Ref.Reference_Count := Ctrl_E.Ref.Reference_Count - 1;
if Ctrl_E.Ref.Reference_Count = 0 then
Unchecked_Free_Element (Ctrl_E.Ref.E_Access);
Unchecked_Free_Ref (Ctrl_E.Ref);
end if;
Ctrl_E.Ref := null;
end if;
end Finalize;
----------
-- Find --
----------
function Find (C : Container; E : access Element_Type) return Count_Type is
begin
for I in 1 .. C.Length loop
if Get (Elements (C), I).all = E.all then
return I;
end if;
end loop;
return 0;
end Find;
function Find (C : Container; E : Element_Type) return Extended_Index is
(To_Index (Find (C, E'Unrestricted_Access)));
---------
-- Get --
---------
function Get (C : Container; I : Index_Type) return Element_Type is
(Get (Elements (C), To_Count (I)).all);
------------------
-- Intersection --
------------------
function Intersection (C1 : Container; C2 : Container) return Container is
L : constant Count_Type := Num_Overlaps (C1, C2);
A : constant Array_Base_Controlled_Access := Content_Init (L);
P : Count_Type := 0;
begin
A.Base.Max_Length := L;
for I in 1 .. C1.Length loop
if Find (C2, Get (Elements (C1), I)) > 0 then
P := P + 1;
A.Base.Elements (P) := Elements (C1) (I);
end if;
end loop;
return Container'(Length => P, Controlled_Base => A);
end Intersection;
------------
-- Length --
------------
function Length (C : Container) return Count_Type is (C.Length);
---------------------
-- Num_Overlaps --
---------------------
function Num_Overlaps (C1 : Container; C2 : Container) return Count_Type is
P : Count_Type := 0;
begin
for I in 1 .. C1.Length loop
if Find (C2, Get (Elements (C1), I)) > 0 then
P := P + 1;
end if;
end loop;
return P;
end Num_Overlaps;
------------
-- Remove --
------------
function Remove (C : Container; I : Index_Type) return Container is
begin
if To_Count (I) = C.Length then
return Container'(Length => C.Length - 1,
Controlled_Base => C.Controlled_Base);
else
declare
A : constant Array_Base_Controlled_Access
:= Content_Init (C.Length - 1);
P : Count_Type := 0;
begin
A.Base.Max_Length := C.Length - 1;
for J in 1 .. C.Length loop
if J /= To_Count (I) then
P := P + 1;
A.Base.Elements (P) := Elements (C) (J);
end if;
end loop;
return Container'(Length => C.Length - 1, Controlled_Base => A);
end;
end if;
end Remove;
------------
-- Resize --
------------
procedure Resize (Base : Array_Base_Access) is
begin
if Base.Max_Length < Base.Elements'Length then
return;
end if;
pragma Assert (Base.Max_Length = Base.Elements'Length);
if Base.Max_Length = Count_Type'Last then
raise Constraint_Error;
end if;
declare
procedure Finalize is new Ada.Unchecked_Deallocation
(Object => Element_Array,
Name => Element_Array_Access_Base);
New_Length : constant Positive_Count_Type :=
(if Base.Max_Length > Count_Type'Last / 2 then Count_Type'Last
else 2 * Base.Max_Length);
Elements : constant Element_Array_Access :=
new Element_Array (1 .. New_Length);
Old_Elmts : Element_Array_Access_Base := Base.Elements;
begin
Elements (1 .. Base.Max_Length) := Base.Elements.all;
Base.Elements := Elements;
Finalize (Old_Elmts);
end;
end Resize;
---------
-- Set --
---------
function Set
(C : Container;
I : Index_Type;
E : Element_Type) return Container
is
Result : constant Container :=
Container'(Length => C.Length,
Controlled_Base => Content_Init (C.Length));
R_Base : Array_Base_Access renames Result.Controlled_Base.Base;
begin
R_Base.Max_Length := C.Length;
R_Base.Elements (1 .. C.Length) := Elements (C) (1 .. C.Length);
R_Base.Elements (To_Count (I)) := Element_Init (E);
return Result;
end Set;
-----------
-- Union --
-----------
function Union (C1 : Container; C2 : Container) return Container is
N : constant Count_Type := Num_Overlaps (C1, C2);
begin
-- if C2 is completely included in C1 then return C1
if N = Length (C2) then
return C1;
end if;
-- else loop through C2 to find the remaining elements
declare
L : constant Count_Type := Length (C1) - N + Length (C2);
A : constant Array_Base_Controlled_Access := Content_Init (L);
P : Count_Type := Length (C1);
begin
A.Base.Max_Length := L;
A.Base.Elements (1 .. C1.Length) := Elements (C1) (1 .. C1.Length);
for I in 1 .. C2.Length loop
if Find (C1, Get (Elements (C2), I)) = 0 then
P := P + 1;
A.Base.Elements (P) := Elements (C2) (I);
end if;
end loop;
return Container'(Length => L, Controlled_Base => A);
end;
end Union;
end Ada.Containers.Functional_Base;

198
gcc/ada/libgnat/a-cofuba.ads
View File

@ -1,198 +0,0 @@
------------------------------------------------------------------------------
-- --
-- GNAT LIBRARY COMPONENTS --
-- --
-- ADA.CONTAINERS.FUNCTIONAL_BASE --
-- --
-- S p e c --
-- --
-- Copyright (C) 2016-2022, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- apply solely to the contents of the part following the private keyword. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
-- Functional containers are neither controlled nor limited. This is safe, as
-- no primitives are provided to modify them.
-- Memory allocated inside functional containers is never reclaimed.
pragma Ada_2012;
-- To allow reference counting on the base container
private with Ada.Finalization;
private generic
type Index_Type is (<>);
-- To avoid Constraint_Error being raised at run time, Index_Type'Base
-- should have at least one more element at the low end than Index_Type.
type Element_Type (<>) is private;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Functional_Base with SPARK_Mode => Off is
subtype Extended_Index is Index_Type'Base range
Index_Type'Pred (Index_Type'First) .. Index_Type'Last;
type Container is private;
function "=" (C1 : Container; C2 : Container) return Boolean;
-- Return True if C1 and C2 contain the same elements at the same position
function Length (C : Container) return Count_Type;
-- Number of elements stored in C
function Get (C : Container; I : Index_Type) return Element_Type;
-- Access to the element at index I in C
function Set
(C : Container;
I : Index_Type;
E : Element_Type) return Container;
-- Return a new container which is equal to C except for the element at
-- index I, which is set to E.
function Add
(C : Container;
I : Index_Type;
E : Element_Type) return Container;
-- Return a new container that is C with E inserted at index I
function Remove (C : Container; I : Index_Type) return Container;
-- Return a new container that is C without the element at index I
function Find (C : Container; E : Element_Type) return Extended_Index;
-- Return the first index for which the element stored in C is I. If there
-- are no such indexes, return Extended_Index'First.
--------------------
-- Set Operations --
--------------------
function "<=" (C1 : Container; C2 : Container) return Boolean;
-- Return True if every element of C1 is in C2
function Num_Overlaps (C1 : Container; C2 : Container) return Count_Type;
-- Return the number of elements that are in both C1 and C2
function Union (C1 : Container; C2 : Container) return Container;
-- Return a container which is C1 plus all the elements of C2 that are not
-- in C1.
function Intersection (C1 : Container; C2 : Container) return Container;
-- Return a container which is C1 minus all the elements that are also in
-- C2.
private
-- Theoretically, each operation on a functional container implies the
-- creation of a new container i.e. the copy of the array itself and all
-- the elements in it. In the implementation, most of these copies are
-- avoided by sharing between the containers.
--
-- A container stores its last used index. So, when adding an
-- element at the end of the container, the exact same array can be reused.
-- As a functionnal container cannot be modifed once created, there is no
-- risk of unwanted modifications.
--
-- _1_2_3_
-- S : end => [1, 2, 3]
-- |
-- |1|2|3|4|.|.|
-- |
-- Add (S, 4, 4) : end => [1, 2, 3, 4]
--
-- The elements are also shared between containers as much as possible. For
-- example, when something is added in the middle, the array is changed but
-- the elementes are reused.
--
-- _1_2_3_4_
-- S : |1|2|3|4| => [1, 2, 3, 4]
-- | \ \ \
-- Add (S, 2, 5) : |1|5|2|3|4| => [1, 5, 2, 3, 4]
--
-- To make this sharing possible, both the elements and the arrays are
-- stored inside dynamically allocated access types which shall be
-- deallocated when they are no longer used. The memory is managed using
-- reference counting both at the array and at the element level.
subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
type Reference_Count_Type is new Natural;
type Element_Access is access all Element_Type;
type Refcounted_Element is record
Reference_Count : Reference_Count_Type;
E_Access : Element_Access;
end record;
type Refcounted_Element_Access is access Refcounted_Element;
type Controlled_Element_Access is new Ada.Finalization.Controlled
with record
Ref : Refcounted_Element_Access := null;
end record;
function Element_Init (E : Element_Type) return Controlled_Element_Access;
-- Use to initialize a refcounted element
type Element_Array is
array (Positive_Count_Type range <>) of Controlled_Element_Access;
type Element_Array_Access_Base is access Element_Array;
subtype Element_Array_Access is Element_Array_Access_Base;
type Array_Base is record
Reference_Count : Reference_Count_Type;
Max_Length : Count_Type;
Elements : Element_Array_Access;
end record;
type Array_Base_Access is access Array_Base;
type Array_Base_Controlled_Access is new Ada.Finalization.Controlled
with record
Base : Array_Base_Access;
end record;
overriding procedure Adjust
(Controlled_Base : in out Array_Base_Controlled_Access);
overriding procedure Finalize
(Controlled_Base : in out Array_Base_Controlled_Access);
overriding procedure Adjust
(Ctrl_E : in out Controlled_Element_Access);
overriding procedure Finalize
(Ctrl_E : in out Controlled_Element_Access);
function Content_Init (L : Count_Type := 0)
return Array_Base_Controlled_Access;
-- Used to initialize the content of an array base with length L
type Container is record
Length : Count_Type := 0;
Controlled_Base : Array_Base_Controlled_Access := Content_Init;
end record;
end Ada.Containers.Functional_Base;

306
gcc/ada/libgnat/a-cofuma.adb
View File

@ -1,306 +0,0 @@
------------------------------------------------------------------------------
-- --
-- GNAT LIBRARY COMPONENTS --
-- --
-- ADA.CONTAINERS.FUNCTIONAL_MAPS --
-- --
-- B o d y --
-- --
-- Copyright (C) 2016-2022, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- apply solely to the contents of the part following the private keyword. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
pragma Ada_2012;
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;
---------
-- "=" --
---------
function "=" (Left : Map; Right : Map) return Boolean is
(Left.Keys <= Right.Keys and Right <= Left);
----------
-- "<=" --
----------
function "<=" (Left : Map; Right : Map) return Boolean is
I2 : Count_Type;
begin
for I1 in 1 .. Length (Left.Keys) loop
I2 := Find (Right.Keys, Get (Left.Keys, I1));
if I2 = 0
or else Get (Right.Elements, I2) /= Get (Left.Elements, I1)
then
return False;
end if;
end loop;
return True;
end "<=";
---------
-- Add --
---------
function Add
(Container : Map;
New_Key : Key_Type;
New_Item : Element_Type) return Map
is
begin
return
(Keys =>
Add (Container.Keys, Length (Container.Keys) + 1, New_Key),
Elements =>
Add
(Container.Elements, Length (Container.Elements) + 1, New_Item));
end Add;
---------------------------
-- Elements_Equal_Except --
---------------------------
function Elements_Equal_Except
(Left : Map;
Right : Map;
New_Key : Key_Type) return Boolean
is
begin
for J in 1 .. Length (Left.Keys) loop
declare
K : constant Key_Type := Get (Left.Keys, J);
begin
if not Equivalent_Keys (K, New_Key)
and then
(Find (Right.Keys, K) = 0
or else Get (Right.Elements, Find (Right.Keys, K)) /=
Get (Left.Elements, J))
then
return False;
end if;
end;
end loop;
return True;
end Elements_Equal_Except;
function Elements_Equal_Except
(Left : Map;
Right : Map;
X : Key_Type;
Y : Key_Type) return Boolean
is
begin
for J in 1 .. Length (Left.Keys) loop
declare
K : constant Key_Type := Get (Left.Keys, J);
begin
if not Equivalent_Keys (K, X)
and then not Equivalent_Keys (K, Y)
and then
(Find (Right.Keys, K) = 0
or else Get (Right.Elements, Find (Right.Keys, K)) /=
Get (Left.Elements, J))
then
return False;
end if;
end;
end loop;
return True;
end Elements_Equal_Except;
---------------
-- Empty_Map --
---------------
function Empty_Map return Map is
((others => <>));
---------
-- Get --
---------
function Get (Container : Map; Key : Key_Type) return Element_Type is
begin
return Get (Container.Elements, Find (Container.Keys, Key));
end Get;
-------------
-- Has_Key --
-------------
function Has_Key (Container : Map; Key : Key_Type) return Boolean is
begin
return Find (Container.Keys, Key) > 0;
end Has_Key;
-----------------
-- Has_Witness --
-----------------
function Has_Witness
(Container : Map;
Witness : Count_Type) return Boolean
is
(Witness in 1 .. Length (Container.Keys));
--------------
-- Is_Empty --
--------------
function Is_Empty (Container : Map) return Boolean is
begin
return Length (Container.Keys) = 0;
end Is_Empty;
-------------------
-- Keys_Included --
-------------------
function Keys_Included (Left : Map; Right : Map) return Boolean is
begin
for J in 1 .. Length (Left.Keys) loop
declare
K : constant Key_Type := Get (Left.Keys, J);
begin
if Find (Right.Keys, K) = 0 then
return False;
end if;
end;
end loop;
return True;
end Keys_Included;
--------------------------
-- Keys_Included_Except --
--------------------------
function Keys_Included_Except
(Left : Map;
Right : Map;
New_Key : Key_Type) return Boolean
is
begin
for J in 1 .. Length (Left.Keys) loop
declare
K : constant Key_Type := Get (Left.Keys, J);
begin
if not Equivalent_Keys (K, New_Key)
and then Find (Right.Keys, K) = 0
then
return False;
end if;
end;
end loop;
return True;
end Keys_Included_Except;
function Keys_Included_Except
(Left : Map;
Right : Map;
X : Key_Type;
Y : Key_Type) return Boolean
is
begin
for J in 1 .. Length (Left.Keys) loop
declare
K : constant Key_Type := Get (Left.Keys, J);
begin
if not Equivalent_Keys (K, X)
and then not Equivalent_Keys (K, Y)
and then Find (Right.Keys, K) = 0
then
return False;
end if;
end;
end loop;
return True;
end Keys_Included_Except;
------------
-- Length --
------------
function Length (Container : Map) return Big_Natural is
begin
return To_Big_Integer (Length (Container.Elements));
end Length;
------------
-- Remove --
------------
function Remove (Container : Map; Key : Key_Type) return Map is
J : constant Extended_Index := Find (Container.Keys, Key);
begin
return
(Keys => Remove (Container.Keys, J),
Elements => Remove (Container.Elements, J));
end Remove;
---------------
-- Same_Keys --
---------------
function Same_Keys (Left : Map; Right : Map) return Boolean is
(Keys_Included (Left, Right)
and Keys_Included (Left => Right, Right => Left));
---------
-- Set --
---------
function Set
(Container : Map;
Key : Key_Type;
New_Item : Element_Type) return Map
is
(Keys => Container.Keys,
Elements =>
Set (Container.Elements, Find (Container.Keys, Key), New_Item));
-----------
-- W_Get --
-----------
function W_Get
(Container : Map;
Witness : Count_Type) return Element_Type
is
(Get (Container.Elements, Witness));
-------------
-- Witness --
-------------
function Witness (Container : Map; Key : Key_Type) return Count_Type is
(Find (Container.Keys, Key));
end Ada.Containers.Functional_Maps;

366
gcc/ada/libgnat/a-cofuma.ads
View File

@ -29,368 +29,12 @@
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
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;
package Ada.Containers.Functional_Maps with SPARK_Mode is
with function Equivalent_Keys
(Left : Key_Type;
Right : Key_Type) return Boolean is "=";
with function "=" (Left, Right : Element_Type) return Boolean is <>;
Enable_Handling_Of_Equivalence : Boolean := True;
-- This constant should only be set to False when no particular handling
-- of equivalence over keys is needed, that is, Equivalent_Keys defines a
-- key uniquely.
package Ada.Containers.Functional_Maps with
SPARK_Mode,
Annotate => (GNATprove, Always_Return)
is
type Map is private with
Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0,
Iterable => (First => Iter_First,
Next => Iter_Next,
Has_Element => Iter_Has_Element,
Element => Iter_Element);
-- Maps are empty when default initialized.
-- "For in" quantification over maps should not be used.
-- "For of" quantification over maps iterates over keys.
-- Note that, for proof, "for of" quantification is understood modulo
-- equivalence (the range of quantification comprises all the keys that are
-- equivalent to any key of the map).
-----------------------
-- Basic operations --
-----------------------
-- Maps are axiomatized using Has_Key and Get, encoding respectively the
-- presence of a key in a map and an accessor to elements associated with
-- its keys. The length of a map is also added to protect Add against
-- overflows but it is not actually modeled.
function Has_Key (Container : Map; Key : Key_Type) return Boolean with
-- Return True if Key is present in Container
Global => null,
Post =>
(if Enable_Handling_Of_Equivalence then
-- Has_Key returns the same result on all equivalent keys
(if (for some K of Container => Equivalent_Keys (K, Key)) then
Has_Key'Result));
function Get (Container : Map; Key : Key_Type) return Element_Type with
-- Return the element associated with Key in Container
Global => null,
Pre => Has_Key (Container, Key),
Post =>
(if Enable_Handling_Of_Equivalence then
-- Get returns the same result on all equivalent keys
Get'Result = W_Get (Container, Witness (Container, Key))
and (for all K of Container =>
(Equivalent_Keys (K, Key) =
(Witness (Container, Key) = Witness (Container, K)))));
function Length (Container : Map) return Big_Natural with
Global => null;
-- Return the number of mappings in Container
------------------------
-- Property Functions --
------------------------
function "<=" (Left : Map; Right : Map) return Boolean with
-- Map inclusion
Global => null,
Post =>
"<="'Result =
(for all Key of Left =>
Has_Key (Right, Key) and then Get (Right, Key) = Get (Left, Key));
function "=" (Left : Map; Right : Map) return Boolean with
-- Extensional equality over maps
Global => null,
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)));
pragma Warnings (Off, "unused variable ""Key""");
function Is_Empty (Container : Map) return Boolean with
-- A map is empty if it contains no key
Global => null,
Post => Is_Empty'Result = (for all Key of Container => False);
pragma Warnings (On, "unused variable ""Key""");
function Keys_Included (Left : Map; Right : Map) return Boolean
-- Returns True if every Key of Left is in Right
with
Global => null,
Post =>
Keys_Included'Result = (for all Key of Left => Has_Key (Right, Key));
function Same_Keys (Left : Map; Right : Map) return Boolean
-- Returns True if Left and Right have the same keys
with
Global => null,
Post =>
Same_Keys'Result =
(Keys_Included (Left, Right)
and Keys_Included (Left => Right, Right => Left));
pragma Annotate (GNATprove, Inline_For_Proof, Same_Keys);
function Keys_Included_Except
(Left : Map;
Right : Map;
New_Key : Key_Type) return Boolean
-- Returns True if Left contains only keys of Right and possibly New_Key
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)));
function Keys_Included_Except
(Left : Map;
Right : Map;
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)));
function Elements_Equal_Except
(Left : Map;
Right : Map;
New_Key : Key_Type) return Boolean
-- Returns True if all the keys of Left are mapped to the same elements in
-- Left and Right except New_Key.
with
Global => null,
Post =>
Elements_Equal_Except'Result =
(for all Key of Left =>
(if not Equivalent_Keys (Key, New_Key) then
Has_Key (Right, Key)
and then Get (Left, Key) = Get (Right, Key)));
function Elements_Equal_Except
(Left : Map;
Right : Map;
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.
with
Global => null,
Post =>
Elements_Equal_Except'Result =
(for all Key of Left =>
(if not Equivalent_Keys (Key, X)
and not Equivalent_Keys (Key, Y)
then
Has_Key (Right, Key)
and then Get (Left, Key) = Get (Right, Key)));
----------------------------
-- Construction Functions --
----------------------------
-- For better efficiency of both proofs and execution, avoid using
-- construction functions in annotations and rather use property functions.
function Add
(Container : Map;
New_Key : Key_Type;
New_Item : Element_Type) return Map
-- Returns Container augmented with the mapping Key -> New_Item
with
Global => null,
Pre => not Has_Key (Container, New_Key),
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);
function Empty_Map return Map with
-- Return an empty Map
Global => null,
Post =>
Length (Empty_Map'Result) = 0
and Is_Empty (Empty_Map'Result);
function Remove
(Container : Map;
Key : Key_Type) return Map
-- Returns Container without any mapping for Key
with
Global => null,
Pre => Has_Key (Container, Key),
Post =>
Length (Container) = Length (Remove'Result) + 1
and not Has_Key (Remove'Result, Key)
and Remove'Result <= Container
and Keys_Included_Except (Container, Remove'Result, Key);
function Set
(Container : Map;
Key : Key_Type;
New_Item : Element_Type) return Map
-- Returns Container, where the element associated with Key has been
-- replaced by New_Item.
with
Global => null,
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);
------------------------------
-- Handling of Equivalence --
------------------------------
-- These functions are used to specify that Get returns the same value on
-- equivalent keys. They should not be used directly in user code.
function Has_Witness (Container : Map; Witness : Count_Type) return Boolean
with
Ghost,
Global => null;
-- Returns True if there is a key with witness Witness in Container
function Witness (Container : Map; Key : Key_Type) return Count_Type with
-- Returns the witness of Key in Container
Ghost,
Global => null,
Pre => Has_Key (Container, Key),
Post => Has_Witness (Container, Witness'Result);
function W_Get (Container : Map; Witness : Count_Type) return Element_Type
with
-- Returns the element associated with a witness in Container
Ghost,
Global => null,
Pre => Has_Witness (Container, Witness);
function Copy_Key (Key : Key_Type) return Key_Type is (Key);
function Copy_Element (Item : Element_Type) return Element_Type is (Item);
-- Elements and Keys of maps are copied by numerous primitives in this
-- package. This function causes GNATprove to verify that such a copy is
-- valid (in particular, it does not break the ownership policy of SPARK,
-- i.e. it does not contain pointers that could be used to alias mutable
-- data).
---------------------------
-- Iteration Primitives --
---------------------------
type Private_Key is private;
function Iter_First (Container : Map) return Private_Key with
Global => null;
function Iter_Has_Element
(Container : Map;
Key : Private_Key) return Boolean
with
Global => null;
function Iter_Next (Container : Map; Key : Private_Key) return Private_Key
with
Global => null,
Pre => Iter_Has_Element (Container, Key);
function Iter_Element (Container : Map; Key : Private_Key) return Key_Type
with
Global => null,
Pre => Iter_Has_Element (Container, Key);
pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Has_Key);
private
pragma SPARK_Mode (Off);
function "="
(Left : Key_Type;
Right : Key_Type) return Boolean renames Equivalent_Keys;
subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
package Element_Containers is new Ada.Containers.Functional_Base
(Element_Type => Element_Type,
Index_Type => Positive_Count_Type);
package Key_Containers is new Ada.Containers.Functional_Base
(Element_Type => Key_Type,
Index_Type => Positive_Count_Type);
type Map is record
Keys : Key_Containers.Container;
Elements : Element_Containers.Container;
end record;
type Private_Key is new Count_Type;
function Iter_First (Container : Map) return Private_Key is (1);
function Iter_Has_Element
(Container : Map;
Key : Private_Key) return Boolean
is
(Count_Type (Key) in 1 .. Key_Containers.Length (Container.Keys));
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
is
(Key_Containers.Get (Container.Keys, Count_Type (Key)));
pragma Compile_Time_Error
(True,
"This package has been moved to the SPARK library shipped with any"
& " SPARK release starting with version 23.");
end Ada.Containers.Functional_Maps;

184
gcc/ada/libgnat/a-cofuse.adb
View File

@ -1,184 +0,0 @@
------------------------------------------------------------------------------
-- --
-- GNAT LIBRARY COMPONENTS --
-- --
-- ADA.CONTAINERS.FUNCTIONAL_SETS --
-- --
-- B o d y --
-- --
-- Copyright (C) 2016-2022, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- apply solely to the contents of the part following the private keyword. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
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;
---------
-- "=" --
---------
function "=" (Left : Set; Right : Set) return Boolean is
(Left.Content <= Right.Content and Right.Content <= Left.Content);
----------
-- "<=" --
----------
function "<=" (Left : Set; Right : Set) return Boolean is
(Left.Content <= Right.Content);
---------
-- Add --
---------
function Add (Container : Set; Item : Element_Type) return Set is
(Content =>
Add (Container.Content, Length (Container.Content) + 1, Item));
--------------
-- Contains --
--------------
function Contains (Container : Set; Item : Element_Type) return Boolean is
(Find (Container.Content, Item) > 0);
---------------
-- Empty_Set --
---------------
function Empty_Set return Set is
((others => <>));
---------------------
-- Included_Except --
---------------------
function Included_Except
(Left : Set;
Right : Set;
Item : Element_Type) return Boolean
is
(for all E of Left =>
Equivalent_Elements (E, Item) or Contains (Right, E));
-----------------------
-- Included_In_Union --
-----------------------
function Included_In_Union
(Container : Set;
Left : Set;
Right : Set) return Boolean
is
(for all Item of Container =>
Contains (Left, Item) or Contains (Right, Item));
---------------------------
-- Includes_Intersection --
---------------------------
function Includes_Intersection
(Container : Set;
Left : Set;
Right : Set) return Boolean
is
(for all Item of Left =>
(if Contains (Right, Item) then Contains (Container, Item)));
------------------
-- Intersection --
------------------
function Intersection (Left : Set; Right : Set) return Set is
(Content => Intersection (Left.Content, Right.Content));
--------------
-- Is_Empty --
--------------
function Is_Empty (Container : Set) return Boolean is
(Length (Container.Content) = 0);
------------------
-- Is_Singleton --
------------------
function Is_Singleton
(Container : Set;
New_Item : Element_Type) return Boolean
is
(Length (Container.Content) = 1
and New_Item = Get (Container.Content, 1));
------------
-- Length --
------------
function Length (Container : Set) return Big_Natural is
(To_Big_Integer (Length (Container.Content)));
-----------------
-- Not_In_Both --
-----------------
function Not_In_Both
(Container : Set;
Left : Set;
Right : Set) return Boolean
is
(for all Item of Container =>
not Contains (Right, Item) or not Contains (Left, Item));
----------------
-- No_Overlap --
----------------
function No_Overlap (Left : Set; Right : Set) return Boolean is
(Num_Overlaps (Left.Content, Right.Content) = 0);
------------------
-- Num_Overlaps --
------------------
function Num_Overlaps (Left : Set; Right : Set) return Big_Natural is
(To_Big_Integer (Num_Overlaps (Left.Content, Right.Content)));
------------
-- Remove --
------------
function Remove (Container : Set; Item : Element_Type) return Set is
(Content => Remove (Container.Content, Find (Container.Content, Item)));
-----------
-- Union --
-----------
function Union (Left : Set; Right : Set) return Set is
(Content => Union (Left.Content, Right.Content));
end Ada.Containers.Functional_Sets;

306
gcc/ada/libgnat/a-cofuse.ads
View File

@ -29,308 +29,12 @@
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
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;
package Ada.Containers.Functional_Sets with SPARK_Mode is
with function Equivalent_Elements
(Left : Element_Type;
Right : Element_Type) return Boolean is "=";
Enable_Handling_Of_Equivalence : Boolean := True;
-- This constant should only be set to False when no particular handling
-- of equivalence over elements is needed, that is, Equivalent_Elements
-- defines an element uniquely.
package Ada.Containers.Functional_Sets with
SPARK_Mode,
Annotate => (GNATprove, Always_Return)
is
type Set is private with
Default_Initial_Condition => Is_Empty (Set),
Iterable => (First => Iter_First,
Next => Iter_Next,
Has_Element => Iter_Has_Element,
Element => Iter_Element);
-- Sets are empty when default initialized.
-- "For in" quantification over sets should not be used.
-- "For of" quantification over sets iterates over elements.
-- Note that, for proof, "for of" quantification is understood modulo
-- equivalence (the range of quantification comprises all the elements that
-- are equivalent to any element of the set).
-----------------------
-- Basic operations --
-----------------------
-- Sets are axiomatized using Contains, which encodes whether an element is
-- contained in a set. The length of a set is also added to protect Add
-- against overflows but it is not actually modeled.
function Contains (Container : Set; Item : Element_Type) return Boolean with
-- Return True if Item is contained in Container
Global => null,
Post =>
(if Enable_Handling_Of_Equivalence then
-- Contains returns the same result on all equivalent elements
(if (for some E of Container => Equivalent_Elements (E, Item)) then
Contains'Result));
function Length (Container : Set) return Big_Natural with
Global => null;
-- Return the number of elements in Container
------------------------
-- Property Functions --
------------------------
function "<=" (Left : Set; Right : Set) return Boolean with
-- Set inclusion
Global => null,
Post => "<="'Result = (for all Item of Left => Contains (Right, Item));
function "=" (Left : Set; Right : Set) return Boolean with
-- Extensional equality over sets
Global => null,
Post => "="'Result = (Left <= Right and Right <= Left);
pragma Warnings (Off, "unused variable ""Item""");
function Is_Empty (Container : Set) return Boolean with
-- A set is empty if it contains no element
Global => null,
Post =>
Is_Empty'Result = (for all Item of Container => False)
and Is_Empty'Result = (Length (Container) = 0);
pragma Warnings (On, "unused variable ""Item""");
function Included_Except
(Left : Set;
Right : Set;
Item : Element_Type) return Boolean
-- Return True if Left contains only elements of Right except possibly
-- Item.
with
Global => null,
Post =>
Included_Except'Result =
(for all E of Left =>
Contains (Right, E) or Equivalent_Elements (E, Item));
function Includes_Intersection
(Container : Set;
Left : Set;
Right : Set) return Boolean
with
-- Return True if every element of the intersection of Left and Right is
-- in Container.
Global => null,
Post =>
Includes_Intersection'Result =
(for all Item of Left =>
(if Contains (Right, Item) then Contains (Container, Item)));
function Included_In_Union
(Container : Set;
Left : Set;
Right : Set) return Boolean
with
-- Return True if every element of Container is the union of Left and Right
Global => null,
Post =>
Included_In_Union'Result =
(for all Item of Container =>
Contains (Left, Item) or Contains (Right, Item));
function Is_Singleton
(Container : Set;
New_Item : Element_Type) return Boolean
with
-- Return True Container only contains New_Item
Global => null,
Post =>
Is_Singleton'Result =
(for all Item of Container => Equivalent_Elements (Item, New_Item));
function Not_In_Both
(Container : Set;
Left : Set;
Right : Set) return Boolean
-- Return True if there are no elements in Container that are in Left and
-- Right.
with
Global => null,
Post =>
Not_In_Both'Result =
(for all Item of Container =>
not Contains (Left, Item) or not Contains (Right, Item));
function No_Overlap (Left : Set; Right : Set) return Boolean with
-- Return True if there are no equivalent elements in Left and Right
Global => null,
Post =>
No_Overlap'Result =
(for all Item of Left => not Contains (Right, Item));
function Num_Overlaps (Left : Set; Right : Set) return Big_Natural with
-- Number of elements that are both in Left and Right
Global => null,
Post =>
Num_Overlaps'Result = Length (Intersection (Left, Right))
and (if Left <= Right then Num_Overlaps'Result = Length (Left)
else Num_Overlaps'Result < Length (Left))
and (if Right <= Left then Num_Overlaps'Result = Length (Right)
else Num_Overlaps'Result < Length (Right))
and (Num_Overlaps'Result = 0) = No_Overlap (Left, Right);
----------------------------
-- Construction Functions --
----------------------------
-- For better efficiency of both proofs and execution, avoid using
-- construction functions in annotations and rather use property functions.
function Add (Container : Set; Item : Element_Type) return Set with
-- Return a new set containing all the elements of Container plus E
Global => null,
Pre => not Contains (Container, Item),
Post =>
Length (Add'Result) = Length (Container) + 1
and Contains (Add'Result, Item)
and Container <= Add'Result
and Included_Except (Add'Result, Container, Item);
function Empty_Set return Set with
-- Return a new empty set
Global => null,
Post => Is_Empty (Empty_Set'Result);
function Remove (Container : Set; Item : Element_Type) return Set with
-- Return a new set containing all the elements of Container except E
Global => null,
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);
function Intersection (Left : Set; Right : Set) return Set with
-- Returns the intersection of Left and Right
Global => null,
Post =>
Intersection'Result <= Left
and Intersection'Result <= Right
and Includes_Intersection (Intersection'Result, Left, Right);
function Union (Left : Set; Right : Set) return Set with
-- Returns the union of Left and Right
Global => null,
Post =>
Length (Union'Result) =
Length (Left) - Num_Overlaps (Left, Right) + Length (Right)
and Left <= Union'Result
and Right <= Union'Result
and Included_In_Union (Union'Result, Left, Right);
function Copy_Element (Item : Element_Type) return Element_Type is (Item);
-- Elements of containers are copied by numerous primitives in this
-- package. This function causes GNATprove to verify that such a copy is
-- valid (in particular, it does not break the ownership policy of SPARK,
-- i.e. it does not contain pointers that could be used to alias mutable
-- data).
---------------------------
-- Iteration Primitives --
---------------------------
type Private_Key is private;
function Iter_First (Container : Set) return Private_Key with
Global => null;
function Iter_Has_Element
(Container : Set;
Key : Private_Key) return Boolean
with
Global => null;
function Iter_Next
(Container : Set;
Key : Private_Key) return Private_Key
with
Global => null,
Pre => Iter_Has_Element (Container, Key);
function Iter_Element
(Container : Set;
Key : Private_Key) return Element_Type
with
Global => null,
Pre => Iter_Has_Element (Container, Key);
pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Contains);
private
pragma SPARK_Mode (Off);
subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
function "="
(Left : Element_Type;
Right : Element_Type) return Boolean renames Equivalent_Elements;
package Containers is new Ada.Containers.Functional_Base
(Element_Type => Element_Type,
Index_Type => Positive_Count_Type);
type Set is record
Content : Containers.Container;
end record;
type Private_Key is new Count_Type;
function Iter_First (Container : Set) return Private_Key is (1);
function Iter_Has_Element
(Container : Set;
Key : Private_Key) return Boolean
is
(Count_Type (Key) in 1 .. Containers.Length (Container.Content));
function Iter_Next
(Container : Set;
Key : Private_Key) return Private_Key
is
(if Key = Private_Key'Last then 0 else Key + 1);
function Iter_Element
(Container : Set;
Key : Private_Key) return Element_Type
is
(Containers.Get (Container.Content, Count_Type (Key)));
pragma Compile_Time_Error
(True,
"This package has been moved to the SPARK library shipped with any"
& " SPARK release starting with version 23.");
end Ada.Containers.Functional_Sets;

262
gcc/ada/libgnat/a-cofuve.adb
View File

@ -1,262 +0,0 @@
------------------------------------------------------------------------------
-- --
-- GNAT LIBRARY COMPONENTS --
-- --
-- ADA.CONTAINERS.FUNCTIONAL_VECTORS --
-- --
-- B o d y --
-- --
-- Copyright (C) 2016-2022, Free Software Foundation, Inc. --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- apply solely to the contents of the part following the private keyword. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
pragma Ada_2012;
package body Ada.Containers.Functional_Vectors with SPARK_Mode => Off is
use Containers;
---------
-- "<" --
---------
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)));
----------
-- "<=" --
----------
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)));
---------
-- "=" --
---------
function "=" (Left : Sequence; Right : Sequence) return Boolean is
(Left.Content = Right.Content);
---------
-- Add --
---------
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));
function Add
(Container : Sequence;
Position : Index_Type;
New_Item : Element_Type) return Sequence
is
(Content => Add (Container.Content, Position, New_Item));
--------------------
-- Constant_Range --
--------------------
function Constant_Range
(Container : Sequence;
Fst : Index_Type;
Lst : Extended_Index;
Item : Element_Type) return Boolean is
begin
for I in Fst .. Lst loop
if Get (Container.Content, I) /= Item then
return False;
end if;
end loop;
return True;
end Constant_Range;
--------------
-- Contains --
--------------
function Contains
(Container : Sequence;
Fst : Index_Type;
Lst : Extended_Index;
Item : Element_Type) return Boolean
is
begin
for I in Fst .. Lst loop
if Get (Container.Content, I) = Item then
return True;
end if;
end loop;
return False;
end Contains;
--------------------
-- Empty_Sequence --
--------------------
function Empty_Sequence return Sequence is
((others => <>));
------------------
-- Equal_Except --
------------------
function Equal_Except
(Left : Sequence;
Right : Sequence;
Position : Index_Type) return Boolean
is
begin
if Length (Left.Content) /= Length (Right.Content) then
return False;
end if;
for I in Index_Type'First .. Last (Left) loop
if I /= Position
and then Get (Left.Content, I) /= Get (Right.Content, I)
then
return False;
end if;
end loop;
return True;
end Equal_Except;
function Equal_Except
(Left : Sequence;
Right : Sequence;
X : Index_Type;
Y : Index_Type) return Boolean
is
begin
if Length (Left.Content) /= Length (Right.Content) then
return False;
end if;
for I in Index_Type'First .. Last (Left) loop
if I /= X and then I /= Y
and then Get (Left.Content, I) /= Get (Right.Content, I)
then
return False;
end if;
end loop;
return True;
end Equal_Except;
---------
-- Get --
---------
function Get (Container : Sequence;
Position : Extended_Index) return Element_Type
is
(Get (Container.Content, Position));
----------
-- Last --
----------
function Last (Container : Sequence) return Extended_Index is
(Index_Type'Val
((Index_Type'Pos (Index_Type'First) - 1) + Length (Container)));
------------
-- Length --
------------
function Length (Container : Sequence) return Count_Type is
(Length (Container.Content));
-----------------
-- Range_Equal --
-----------------
function Range_Equal
(Left : Sequence;
Right : Sequence;
Fst : Index_Type;
Lst : Extended_Index) return Boolean
is
begin
for I in Fst .. Lst loop
if Get (Left, I) /= Get (Right, I) then
return False;
end if;
end loop;
return True;
end Range_Equal;
-------------------
-- Range_Shifted --
-------------------
function Range_Shifted
(Left : Sequence;
Right : Sequence;
Fst : Index_Type;
Lst : Extended_Index;
Offset : Count_Type'Base) return Boolean
is
begin
for I in Fst .. Lst loop
if Get (Left, I) /=
Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset))
then
return False;
end if;
end loop;
return True;
end Range_Shifted;
------------
-- Remove --
------------
function Remove
(Container : Sequence;
Position : Index_Type) return Sequence
is
(Content => Remove (Container.Content, Position));
---------
-- Set --
---------
function Set
(Container : Sequence;
Position : Index_Type;
New_Item : Element_Type) return Sequence
is
(Content => Set (Container.Content, Position, New_Item));
end Ada.Containers.Functional_Vectors;

381
gcc/ada/libgnat/a-cofuve.ads
View File

@ -29,383 +29,12 @@
-- <http://www.gnu.org/licenses/>. --
------------------------------------------------------------------------------
pragma Ada_2012;
private with Ada.Containers.Functional_Base;
generic
type Index_Type is (<>);
-- To avoid Constraint_Error being raised at run time, Index_Type'Base
-- should have at least one more element at the low end than Index_Type.
package Ada.Containers.Functional_Vectors with SPARK_Mode is
type Element_Type (<>) is private;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Functional_Vectors with
SPARK_Mode,
Annotate => (GNATprove, Always_Return)
is
subtype Extended_Index is Index_Type'Base range
Index_Type'Pred (Index_Type'First) .. Index_Type'Last;
-- Index_Type with one more element at the low end of the range.
-- This type is never used but it forces GNATprove to check that there is
-- room for one more element at the low end of Index_Type.
type Sequence is private
with Default_Initial_Condition => Length (Sequence) = 0,
Iterable => (First => Iter_First,
Has_Element => Iter_Has_Element,
Next => Iter_Next,
Element => Get);
-- Sequences are empty when default initialized.
-- Quantification over sequences can be done using the regular
-- quantification over its range or directly on its elements with "for of".
-----------------------
-- Basic operations --
-----------------------
-- Sequences are axiomatized using Length and Get, providing respectively
-- the length of a sequence and an accessor to its Nth element:
function Length (Container : Sequence) return Count_Type with
-- Length of a sequence
Global => null,
Post =>
(Index_Type'Pos (Index_Type'First) - 1) + Length'Result <=
Index_Type'Pos (Index_Type'Last);
function Get
(Container : Sequence;
Position : Extended_Index) return Element_Type
-- Access the Element at position Position in Container
with
Global => null,
Pre => Position in Index_Type'First .. Last (Container);
function Last (Container : Sequence) return Extended_Index with
-- Last index of a sequence
Global => null,
Post =>
Last'Result =
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) with
Global => null;
-- First index of a sequence
------------------------
-- Property Functions --
------------------------
function "=" (Left : Sequence; Right : Sequence) return Boolean with
-- Extensional equality over sequences
Global => null,
Post =>
"="'Result =
(Length (Left) = Length (Right)
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
-- Left is a strict subsequence of Right
Global => null,
Post =>
"<"'Result =
(Length (Left) < Length (Right)
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
-- Left is a subsequence of Right
Global => null,
Post =>
"<="'Result =
(Length (Left) <= Length (Right)
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
-- Returns True if Item occurs in the range from Fst to Lst of Container
with
Global => null,
Pre => Lst <= Last (Container),
Post =>
Contains'Result =
(for some I in Fst .. Lst => Get (Container, I) = Item);
pragma Annotate (GNATprove, Inline_For_Proof, Contains);
function Constant_Range
(Container : Sequence;
Fst : Index_Type;
Lst : Extended_Index;
Item : Element_Type) return Boolean
-- Returns True if every element of the range from Fst to Lst of Container
-- is equal to Item.
with
Global => null,
Pre => Lst <= Last (Container),
Post =>
Constant_Range'Result =
(for all I in Fst .. Lst => Get (Container, I) = Item);
pragma Annotate (GNATprove, Inline_For_Proof, Constant_Range);
function Equal_Except
(Left : Sequence;
Right : Sequence;
Position : Index_Type) return Boolean
-- Returns True is Left and Right are the same except at position Position
with
Global => null,
Pre => Position <= Last (Left),
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))));
pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
function Equal_Except
(Left : Sequence;
Right : Sequence;
X : Index_Type;
Y : Index_Type) return Boolean
-- Returns True is Left and Right are the same except at positions X and Y
with
Global => null,
Pre => X <= Last (Left) and Y <= Last (Left),
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))));
pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
function Range_Equal
(Left : Sequence;
Right : Sequence;
Fst : Index_Type;
Lst : Extended_Index) return Boolean
-- Returns True if the ranges from Fst to Lst contain the same elements in
-- Left and Right.
with
Global => null,
Pre => Lst <= Last (Left) and Lst <= Last (Right),
Post =>
Range_Equal'Result =
(for all I in Fst .. Lst => Get (Left, I) = Get (Right, I));
pragma Annotate (GNATprove, Inline_For_Proof, Range_Equal);
function Range_Shifted
(Left : Sequence;
Right : Sequence;
Fst : Index_Type;
Lst : Extended_Index;
Offset : Count_Type'Base) return Boolean
-- Returns True if the range from Fst to Lst in Left contains the same
-- elements as the range from Fst + Offset to Lst + Offset in Right.
with
Global => null,
Pre =>
Lst <= Last (Left)
and then
(if Offset < 0 then
Index_Type'Pos (Index_Type'Base'First) - Offset <=
Index_Type'Pos (Index_Type'First))
and then
(if Fst <= Lst then
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)))
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)));
pragma Annotate (GNATprove, Inline_For_Proof, Range_Shifted);
----------------------------
-- Construction Functions --
----------------------------
-- For better efficiency of both proofs and execution, avoid using
-- construction functions in annotations and rather use property functions.
function Set
(Container : Sequence;
Position : Index_Type;
New_Item : Element_Type) return Sequence
-- Returns a new sequence which contains the same elements as Container
-- except for the one at position Position which is replaced by New_Item.
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);
function Add (Container : Sequence; New_Item : Element_Type) return Sequence
-- Returns a new sequence which contains the same elements as Container
-- plus New_Item at the end.
with
Global => null,
Pre =>
Length (Container) < Count_Type'Last
and then Last (Container) < Index_Type'Last,
Post =>
Length (Add'Result) = Length (Container) + 1
and then Get (Add'Result, Last (Add'Result)) = New_Item
and then Container <= Add'Result;
function Add
(Container : Sequence;
Position : Index_Type;
New_Item : Element_Type) return Sequence
with
-- Returns a new sequence which contains the same elements as Container
-- except that New_Item has been inserted at position Position.
Global => null,
Pre =>
Length (Container) < Count_Type'Last
and then Last (Container) < Index_Type'Last
and then Position <= Extended_Index'Succ (Last (Container)),
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);
function Remove
(Container : Sequence;
Position : Index_Type) return Sequence
-- Returns a new sequence which contains the same elements as Container
-- except that the element at position Position has been removed.
with
Global => null,
Pre => 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);
function Copy_Element (Item : Element_Type) return Element_Type is (Item);
-- Elements of containers are copied by numerous primitives in this
-- package. This function causes GNATprove to verify that such a copy is
-- valid (in particular, it does not break the ownership policy of SPARK,
-- i.e. it does not contain pointers that could be used to alias mutable
-- data).
function Empty_Sequence return Sequence with
-- Return an empty Sequence
Global => null,
Post => Length (Empty_Sequence'Result) = 0;
---------------------------
-- Iteration Primitives --
---------------------------
function Iter_First (Container : Sequence) return Extended_Index with
Global => null;
function Iter_Has_Element
(Container : Sequence;
Position : Extended_Index) return Boolean
with
Global => null,
Post =>
Iter_Has_Element'Result =
(Position in Index_Type'First .. Last (Container));
pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element);
function Iter_Next
(Container : Sequence;
Position : Extended_Index) return Extended_Index
with
Global => null,
Pre => Iter_Has_Element (Container, Position);
private
pragma SPARK_Mode (Off);
package Containers is new Ada.Containers.Functional_Base
(Index_Type => Index_Type,
Element_Type => Element_Type);
type Sequence is record
Content : Containers.Container;
end record;
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));
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))));
pragma Compile_Time_Error
(True,
"This package has been moved to the SPARK library shipped with any"
& " SPARK release starting with version 23.");
end Ada.Containers.Functional_Vectors;

5
gcc/testsuite/gnat.dg/aspect2.adb
View File

@ -1,5 +0,0 @@
-- { dg-do compile }
package body Aspect2 is
procedure Foo is null;
end Aspect2;

30
gcc/testsuite/gnat.dg/aspect2.ads
View File

@ -1,30 +0,0 @@
with Ada.Containers.Functional_Vectors;
with Ada.Containers; use Ada.Containers;
generic
type Element_Type (<>) is private;
type Element_Model (<>) is private;
with function Model (X : Element_Type) return Element_Model is <>;
with function Copy (X : Element_Type) return Element_Type is <>;
package Aspect2 with SPARK_Mode is
pragma Unevaluated_Use_Of_Old (Allow);
type Vector is private;
function Length (V : Vector) return Natural;
procedure Foo;
private
type Element_Access is access Element_Type;
type Element_Array is array (Positive range <>) of Element_Access with
Dynamic_Predicate => Element_Array'First = 1;
type Element_Array_Access is access Element_Array;
type Vector is record
Top : Natural := 0;
Content : Element_Array_Access;
end record;
function Length (V : Vector) return Natural is
(V.Top);
end Aspect2;

21
gcc/testsuite/gnat.dg/config_pragma1.adb
View File

@ -1,21 +0,0 @@
-- { dg-do run }
-- { dg-options "-gnata" }
with Ada.Strings.Fixed; use Ada.Strings.Fixed;
with Config_Pragma1_Pkg; use Config_Pragma1_Pkg;
procedure Config_Pragma1 is
Target : String10;
begin
for I in Positive10 loop
Move
(Source => Positive10'Image(I),
Target => Target);
FHM.Include
(Container => FHMM,
Key => Target,
New_Item => I);
end loop;
end Config_Pragma1;

21
gcc/testsuite/gnat.dg/config_pragma1_pkg.ads
View File

@ -1,21 +0,0 @@
pragma Assertion_Policy (Ignore);
with Ada.Containers; use Ada.Containers;
with Ada.Containers.Formal_Hashed_Maps;
with Ada.Strings; use Ada.Strings;
with Ada.Strings.Hash;
package Config_Pragma1_Pkg is
subtype Positive10 is Positive range 1 .. 1000;
subtype String10 is String (Positive10);
package FHM is new Formal_Hashed_Maps
(Key_Type => String10,
Element_Type => Positive10,
Hash => Hash,
Equivalent_Keys => "=");
FHMM : FHM.Map
(Capacity => 1_000_000,
Modulus => FHM.Default_Modulus (Count_Type (1_000_000)));
end Config_Pragma1_Pkg;

6
gcc/testsuite/gnat.dg/equal8.adb
View File

@ -1,6 +0,0 @@
-- { dg-do compile }
-- { dg-options "-gnata" }
package body Equal8 is
procedure Foo is null;
end Equal8;

36
gcc/testsuite/gnat.dg/equal8.ads
View File

@ -1,36 +0,0 @@
with Ada.Containers.Formal_Hashed_Sets;
with Ada.Strings.Hash;
-- with Dynamic_Strings; use Dynamic_Strings;
-- with Bounded_Dynamic_Strings;
with Equal8_Pkg;
package Equal8 is
package Dynamic_Strings is
-- pragma SPARK_Mode (On);
package Bounded_Dynamic_Strings is new Equal8_Pkg
(Component => Character,
List_Index => Positive,
List => String,
Default_Value => ' ');
type Dynamic_String is new Bounded_Dynamic_Strings.Sequence;
end Dynamic_Strings;
use Dynamic_Strings;
subtype Subscription_Address is Dynamic_String (Capacity => 255);
function Hashed_Subscription_Address (Element : Subscription_Address)
return Ada.Containers.Hash_Type is
(Ada.Strings.Hash (Value (Element)));
package Subscription_Addresses is new Ada.Containers.Formal_Hashed_Sets
(Element_Type => Subscription_Address,
Hash => Hashed_Subscription_Address,
Equivalent_Elements => "=");
procedure Foo;
end Equal8;

58
gcc/testsuite/gnat.dg/equal8_pkg.ads
View File

@ -1,58 +0,0 @@
generic
type Component is private;
type List_Index is range <>;
type List is array (List_Index range <>) of Component;
Default_Value : Component;
-- with function "=" (Left, Right : List) return Boolean is <>;
package Equal8_Pkg is
pragma Pure;
Maximum_Length : constant List_Index := List_Index'Last;
subtype Natural_Index is List_Index'Base range 0 .. Maximum_Length;
type Sequence (Capacity : Natural_Index) is private;
-- from zero to Capacity.
function Value (This : Sequence) return List;
-- Returns the content of this sequence. The value returned is the
-- "logical" value in that only that slice which is currently assigned
-- is returned, as opposed to the entire physical representation.
overriding
function "=" (Left, Right : Sequence) return Boolean with
Inline;
function "=" (Left : Sequence; Right : List) return Boolean with
Inline;
private
type Sequence (Capacity : Natural_Index) is record
Current_Length : Natural_Index := 0;
Content : List (1 .. Capacity) := (others => Default_Value);
end record;
-----------
-- Value --
-----------
function Value (This : Sequence) return List is
(This.Content (1 .. This.Current_Length));
---------
-- "=" --
---------
overriding
function "=" (Left, Right : Sequence) return Boolean is
(Value (Left) = Value (Right));
---------
-- "=" --
---------
function "=" (Left : Sequence; Right : List) return Boolean is
(Value (Left) = Right);
end Equal8_Pkg;

23
gcc/testsuite/gnat.dg/formal_containers.adb
View File

@ -1,23 +0,0 @@
-- { dg-do compile }
with Ada.Containers.Formal_Hashed_Sets;
procedure Formal_Containers is
type T is new Integer;
function Eq (X : T; Y : T) return Boolean;
function Hash (X : T) return Ada.Containers.Hash_Type is (0);
package TSet is new Ada.Containers.Formal_Hashed_Sets
(Element_Type => T,
Hash => Hash,
Equivalent_Elements => Eq);
S : Tset.Set := TSet.Empty_Set;
function Eq (X : T; Y : T) return Boolean is
begin
return TSet.Contains (S, X) or TSet.Contains (S, Y);
end Eq;
begin null; end Formal_Containers;

20
gcc/testsuite/gnat.dg/iter1.adb
View File

@ -1,20 +0,0 @@
-- { dg-do compile }
with Ada.Text_IO;
package body Iter1 is
type Table is array (Integer range <>) of Float;
My_Table : Table := (1.0, 2.0, 3.0);
procedure Dummy (L : My_Lists.List) is
begin
for Item : Boolean of L loop -- { dg-error "subtype indication does not match element type" }
Ada.Text_IO.Put_Line (Integer'Image (Item));
end loop;
for Item : Boolean of My_Table loop -- { dg-error "subtype indication does not match component type" }
null;
end loop;
end;
end Iter1;

8
gcc/testsuite/gnat.dg/iter1.ads
View File

@ -1,8 +0,0 @@
with Ada.Containers.Formal_Doubly_Linked_Lists;
package Iter1 is
package My_Lists is new Ada.Containers.Formal_Doubly_Linked_Lists
(Element_Type => Integer);
procedure Dummy (L : My_Lists.List);
end Iter1;