On Mon, 20 Jul 2015, Florian Weimer wrote:

> Date: Mon, 20 Jul 2015 21:33:01 +0200
> From: Florian Weimer <fw@deneb.enyo.de>
>> I guess GPL SPARK is not included.
>
> It's not.

But it is not difficult to *develope* your software using gnat/GPL (with 
SPARK support) and then *compile* the final production executable using 
gnat/FSF. The compilers are essentially the same. Well, the fronend of 
gnat/FSF appears to be a bit behind the gnat/GPL frontend. When Ada 2012 
was fresh, gnat/FSF needed some time to include new Ada features already 
supported by gnat/GPL. But this issue is moot, now ... at least until the 
next revision of the Standard.

Stefan


--------  I  love  the  taste  of  Cryptanalysis  in  the morning!  --------
www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany----