Re: Spark, pragma

[Alexandre K <alexandre.nospam@gmail.com>]

On 28 mai, 11:26, Yannick Duchêne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> Le Fri, 28 May 2010 11:08:37 +0200, Alexandre K  
> <alexandre.nos...@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 ?
>

I don't think so. I realized that in my first message I have written
"pragma Style_Checks ("s", Off)" which is incorrect in Ada.
I would want to turn off the declaration for function used just in
body.
So yes I have to use "-s", "s" would let it on because of options used
in compilation command line that make all style, warning etc as an
error.

It clearly works in Ada, it's just the examiner that reports this
error. And if I comment the pragma, the examiner succeeds.

Thanks for your advices.

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