spark ada - Ada complaining that I've added a volatile object in a function call to generic type when not volatile

Question

So I've got the following declaration:

      record
         String1 : String (1 .. 64);
         String2 : String (1 .. 64);
         Timestamp : Time;
         Int1 : Long_Long_Integer;
         String3 : Unbounded_String;
      end record;

And it's used in

package My_Vectors is new Vectors (Index_Type => Positive, Element_Type => Object);

which yields the compilation error: volatile object cannot act as actual in a call (SPARK RM 7.1.3(10))

Now, Clock is volatile which is used. However I've removed the call to Clock and I still get the same result.

Also, I've tried replacing the Object type with a type of Integer and I don't have any complaints from the Ada compiler. Could someone explain this as I can't see how this is putting a volatile object into an actual anywhere please.

Just tried using the following record and I get the same result:

type My_Record is
      record
         A: Integer;
         B: Integer;
         C: String(1 .. 64);
      end record;

Answer 1

The standard Ada containers are not supported in SPARK (see SPARK RM 14.8). Use the SPARK compatible container Ada.Containers.Formal_Vectors instead (see also here and here).

Regarding the compiler error: the current implementation of Ada.Containers.Vector uses atomic operations to improve performance (see here and here). These atomic operations operate (in this case) on variables of type System.Atomic_Counters.Atomic_Unsigned (see here). This type is declared as Atomic and therefore volatile (see RM 8(3)).