1with Ada.Containers.Functional_Vectors;
2with Ada.Containers; use Ada.Containers;
3
4generic
5   type Element_Type (<>) is private;
6   type Element_Model (<>) is private;
7   with function Model (X : Element_Type) return Element_Model is <>;
8   with function Copy (X : Element_Type) return Element_Type is <>;
9package Aspect2 with SPARK_Mode is
10   pragma Unevaluated_Use_Of_Old (Allow);
11
12   type Vector is private;
13
14   function Length (V : Vector) return Natural;
15
16   procedure Foo;
17
18private
19   type Element_Access is access Element_Type;
20   type Element_Array is array (Positive range <>) of Element_Access with
21     Dynamic_Predicate => Element_Array'First = 1;
22   type Element_Array_Access is access Element_Array;
23   type Vector is record
24      Top     : Natural := 0;
25      Content : Element_Array_Access;
26   end record;
27
28   function Length (V : Vector) return Natural is
29     (V.Top);
30end Aspect2;
31