SPARK_Mode does not like Indefinite_Holders?

General
1

I tried “pragma SPARK_Mode (On);” and the compiler complained about this code line:

package holder_ppos_p is new Indefinite_Holders(element_type => ppos_t);

error: instantiation error at a-coinho.ads:92
error: launch “gnatprove --explain=E0015” for more information
error: function cannot have parameter of mode “out” or “in out” in SPARK [E0015]

Any workaround?

reinert

2

The Ada containers (under Ada.Containers) are unfortunately incompatible with SPARK. For most Ada containers there are SPARK-compatible variants in SPARKlib for things like vectors, maps, etc, but there’s no equivalent to Ada.Containers.Indefinite_Holders.

A workaround for SPARK could be to just use manual heap allocation & deallocation yourself using access types, since SPARK’s ownership rules will make sure you’re using the pointers properly.

3

There are in fact holders in sparkilb (link) but the package is declared as private.