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;
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)).