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

David MENTRÉ dmentre at linux-france.org
Sun Jul 6 21:47:59 CEST 2014

Hello Jérôme,

2014-07-06 11:23, Hugues Jérôme:
> Review discussion "Mixing SPARK and non-SPARK code in a generic”, the trick is to instantiate the generic in a non_SPARK unit

Well, this is really what I'm trying to do. But probably I'm reaching 
the limits of my Ada knowledge. :-(

Please find attached my latest attempt. In short:

==> src/bounded_string_instance.ads <==
pragma SPARK_Mode (Off);

with Ada.Strings.Bounded; use Ada.Strings.Bounded;

package Bounded_String_Instance is new Generic_Bounded_Length (20);

==> src/types.ads <==
pragma SPARK_Mode(Off);

with Bounded_String_Instance; use Bounded_String_Instance;

package Types is
    type String_Array is array (Positive range <>) of Bounded_String;
    function To_Bounded_String(Source : String) return Bounded_String;
end Types;

==> src/types.adb <==
pragma SPARK_Mode(Off);

package body Types is
    function To_Bounded_String(Source : String) return Bounded_String is
       return Bounded_String_Instance.To_Bounded_String(Source);
end Types;

==> src/words.ads <==
with Types; use Types;

package Words
    Adjective : constant String_Array :=
      (1 => To_Bounded_String("Black"),
       2 => To_Bounded_String("Blue"));
end Words;

Above code compiles cleanly but I get following SPARK error:
> words.ads:5:25: "String_Array" is not allowed in SPARK
> words.ads:5:25: violation of pragma SPARK_Mode at /home/david/dice-passphrase/global_pragma.adc:1
> words.ads:6:06: "Bounded_String" is not allowed in SPARK
> words.ads:6:06: violation of pragma SPARK_Mode at /home/david/dice-passphrase/global_pragma.adc:1
> words.ads:6:06: subtype of "String_Array" is not allowed in SPARK
> words.ads:6:06: violation of pragma SPARK_Mode at /home/david/dice-passphrase/global_pragma.adc:1

Quoting Yannick in the "Mixing SPARK and non-SPARK code in a generic” 
> If you don't mark this wrapper package as SPARK_Mode=>On or SPARK_Mode=>Off, then it is analyzed in mode "Auto", which means that SPARK-compatible declarations can be used by client code. So you can call functions and use types from this package inside you 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".

> types.ads:1:19: argument for pragma "Spark_Mode" must be "On" or "Off"

Best regards,

-------------- next part --------------
A non-text attachment was scrubbed...
Name: bounded-str-issue.tar.gz
Type: application/gzip
Size: 939 bytes
Desc: not available
URL: <http://lists.forge.open-do.org/pipermail/spark2014-discuss/attachments/20140706/034eee10/attachment.gz>

More information about the Spark2014-discuss mailing list