Re: Spark, pragma

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Fri, 28 May 2010 11:08:37 +0200, Alexandre K  
<alexandre.nospam@gmail.com> a écrit:
> But it exists in my manual, just after warning 420, and this is the
> last one. (for me page 91)
> Maybe as you mentionned this is due to Spark version, as I am using
> Spark PRO v 9.0 with ada 2005 option.
Ok, that is why: I have SPARK GPL 8.1.1 only.

Well, the "s" style checks stands for requirement to have a separate  
declaration for all subprograms. This is unlikely to cause a trouble with  
SPARK, even if your version was able to make special handling of these  
pragmas.

Instead, I was thinking again at your OP:

> Warning 430 - SLI generation abandoned owing to syntax or semantic
> errors or multiple units in a single source file.

It talks among other things, about a syntax error. It seems the syntax of  
this pragma is a literal, which is a letter, followed by an option On of  
Off. Here, you have "-s". Shouldn't this be "s" instead ?

May be worth to try.

-- 
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.