[Ada] Allow for of iteration on formal vectors

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

2 files changed, 54 insertions, 1 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index abe3524..1b7a09d 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -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
diff --git a/gcc/ada/libgnat/a-cofove.ads b/gcc/ada/libgnat/a-cofove.ads
index b23c661..5fb3bc9 100644
--- a/gcc/ada/libgnat/a-cofove.ads
+++ b/gcc/ada/libgnat/a-cofove.ads
@@ -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;