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

Yannick Moy moy at adacore.com
Mon Jul 7 09:59:00 CEST 2014


-- David MENTRÉ (2014-07-06)
> 
> 
> Well, this is really what I'm trying to do. But probably I'm reaching the limits of my Ada knowledge. :-(

In fact, that's not related to Ada, but to how GNATprove handles SPARK_Mode.

> Please find attached my latest attempt. In short:
> 
> ==> src/bounded_string_instance.ads <==
> pragma SPARK_Mode (Off);

This is the source of the problem. As soon as a package decl is SPARK_Mode=>Off, you cannot any entity declared inside it in SPARK code.

> Above code compiles cleanly but I get following SPARK error:

Yes, that's expected: you are trying to use entities declared with SPARK_Mode=>Off in SPARK code.

> As I understand it, the package instantiating the generic and used by SPARK code need to be marked in SPARK_Mode "Auto". But I found no way to set SPARK_Mode to "Auto", I can only set it to "On" or "Off".

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.

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.
--
Yannick Moy, Senior Software Engineer, AdaCore






More information about the Spark2014-discuss mailing list