[Spark2014-discuss] SPARK 2014 strings. Basic I/O

David MENTRÉ dmentre at linux-france.org
Sat Jul 5 21:30:41 CEST 2014


Hello Yannick,

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 
instantiate Bounded_String?

Please find attached the files of the project. Everything compiles 
cleanly without warning.

Best regards,
david
-------------- next part --------------
A non-text attachment was scrubbed...
Name: bounded-str-issue.tar.gz
Type: application/gzip
Size: 742 bytes
Desc: not available
URL: <http://lists.forge.open-do.org/pipermail/spark2014-discuss/attachments/20140705/1d9cd366/attachment.gz>


More information about the Spark2014-discuss mailing list