[Spark2014-discuss] SPARK 2014 strings. Basic I/O
dmentre at linux-france.org
Wed Jul 9 21:51:10 CEST 2014
Sorry for the late reply, I don't have the luxury to do a daily exercise
in SPARK. ;-)
2014-07-07 09:59, Yannick Moy:
> Yes, that's as designed. The mode "Auto" is the automatic mode when
> no other mode is set, but you cannot set it manually. To get what you
> want, you should remove the SPARK_Mode=>On from your configuration
> pragma file, and set it on the units that are in SPARK only.
This is the approach I have taken. Sometimes, it is better to put one's
principles aside and use tools as designed by their creator. ;-)
I still have warnings but you warned me about some of them in a previous
email. I'll look at them in more detail.
> An alternative is to define your own wrapper package on
> Bounded_String, and define wrapper subprograms for those subprograms
> you use. Then, mark the body (not the spec) of this wrapper package
> as SPARK_Mode=>Off. This time, the instantiation is inside the body
> marked SPARK_Mode=>Off, but the type and subprogram declarations that
> you call from SPARK code are in the SPARK spec.
> Or use your own SPARK unit for bounded strings. This is ultimately
> what we'll propose: a library of basic data structures and algorithms
> in SPARK.
Yes, the SPARK library of basic data structures is the way to go on the
More information about the Spark2014-discuss