Building SPARK GPL with an open toolchain

Building SPARK GPL with an open toolchain

[Alexander Senier]

Hi,

SPARK GPL 2010 is out (check out http://libre.adacore.com) as binaries
and source. While the SPARK and Ada tools can be build with gcc, the
parts implemented in Prolog (namely the Simplifier and the Checker)
require a commercial license of SICStus Prolog.

I put together an experimental set of patches to build SPARK GPL 2010
using SWI Prolog. Preliminary tests indicate that the Simplifier built
with SWI actually does the right thing. The patches can be downloaded
here:

http://senier.net/spark-gpl-2010-swi_patches.tgz

Instructions how to build and test SPARK and known limitations are
contained within the README file.

Caveat: This port is in a very early stage -- use it at your own risk!
Comments, suggestions and contributions are very welcome. Please do not
use it to verify your airplane firmware (or any other critical piece of
software) ;-)

Regards
Alex

Re: Building SPARK GPL with an open toolchain

[Yannick Duchêne (Hibou57)]

Le Thu, 29 Jul 2010 00:43:28 +0200, Alexander Senier <mail@senier.net> a  
écrit:
> Caveat: This port is in a very early stage -- use it at your own risk!
> Comments, suggestions and contributions are very welcome.

Just wanted to express my interest for now (so that you do not feel  
alone). But will only test it for an unknown later date.

Have a nice time any way :)

Cheers

-- 
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
--  i.e. forget about previous premises which leads to conclusion
--  and start with new conclusion as premise.