[Spark2014-discuss] SPARK 2014 strings. Basic I/O
dmentre at linux-france.org
Sat Jul 5 21:30:41 CEST 2014
2014-07-02 21:57, Yannick Moy:
> Instead, you should instantiate the package Generic_Bounded_Length
> defined inside Ada.Strings.Bounded in a separate unit not marked
> SPARK_Mode=>On (so it defaults to SPARK_Mode=>Auto, which means that
> you can use entities from it whose declaration is compatible with
> SPARK). I have attached an example of such a use.
Your example works but this approach fails on my own program. The main
difference is that I want to use SPARK 2014 by default using a global
pragma (as discussed previously on this list). However, it seems that as
soon as Bounded_String package is seen in the SPARK module (in my case
words.ads), it is rejected:
words.ads:5:09: "Bounded_String" is not allowed in SPARK
I tried various ways, playing with pragma SPARK_Mode Off and On as well
as SPARK_Mode aspect, without success so far.
The obvious work around would be to disable SPARK_Mode by default and
activate it on each package as you do. I would prefer to avoid that, for
methodological reason on this project.
Is there another workaround to keep SPARK_Mode by default but still
Please find attached the files of the project. Everything compiles
cleanly without warning.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 742 bytes
Desc: not available
More information about the Spark2014-discuss