OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Allow for of iteration on formal vectors

Browse Source 
2019-08-21  Claire Dross  <dross@adacore.com>

gcc/ada/

	* libgnat/a-cofove.ads (Vector): Add an Iterable aspect to allow
	iteration.
	(Iter_First, Iter_Next): Primitives used for iteration.

From-SVN: r274789
This commit is contained in:
Claire Dross 2019-08-21 08:31:11 +00:00 committed by Pierre-Marie de Rodat
parent 61e33106ed
commit 0728477991
2 changed files with 54 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
gcc/ada/ChangeLog
View File

@ -1,3 +1,9 @@
2019-08-21 Claire Dross <dross@adacore.com>
* libgnat/a-cofove.ads (Vector): Add an Iterable aspect to allow
iteration.
(Iter_First, Iter_Next): Primitives used for iteration.
2019-08-21 Yannick Moy <moy@adacore.com>
* sem_ch3.adb (Analyze_Subtype_Declaration): Inherit RM_Size

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

@ -70,7 +70,11 @@ is
subtype Capacity_Range is Count_Type range 0 .. Last_Count;
type Vector (Capacity : Capacity_Range) is private with
Default_Initial_Condition => Is_Empty (Vector);
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,
@ -173,6 +177,7 @@ is
Ghost,
Global => null,
Post => M.Length (Model'Result) = Length (Container);
pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Model);
function Element
(S : M.Sequence;
@ -859,6 +864,30 @@ is
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);
@ -882,4 +911,22 @@ private
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);
end Ada.Containers.Formal_Vectors;